equal
deleted
inserted
replaced
371 then obtain n where "inverse (real (Suc n)) < inverse x" |
371 then obtain n where "inverse (real (Suc n)) < inverse x" |
372 using reals_Archimedean by blast |
372 using reals_Archimedean by blast |
373 hence "inverse (real (Suc n)) * x < inverse x * x" |
373 hence "inverse (real (Suc n)) * x < inverse x * x" |
374 using x_greater_zero by (rule mult_strict_right_mono) |
374 using x_greater_zero by (rule mult_strict_right_mono) |
375 hence "inverse (real (Suc n)) * x < 1" |
375 hence "inverse (real (Suc n)) * x < 1" |
376 using x_greater_zero by (simp add: real_mult_inverse_left mult_commute) |
376 using x_greater_zero by simp |
377 hence "real (Suc n) * (inverse (real (Suc n)) * x) < real (Suc n) * 1" |
377 hence "real (Suc n) * (inverse (real (Suc n)) * x) < real (Suc n) * 1" |
378 by (rule mult_strict_left_mono) simp |
378 by (rule mult_strict_left_mono) simp |
379 hence "x < real (Suc n)" |
379 hence "x < real (Suc n)" |
380 by (simp add: mult_commute ring_eq_simps real_mult_inverse_left) |
380 by (simp add: ring_eq_simps) |
381 thus "\<exists>(n::nat). x < real n" .. |
381 thus "\<exists>(n::nat). x < real n" .. |
382 qed |
382 qed |
383 |
383 |
384 lemma reals_Archimedean3: |
384 lemma reals_Archimedean3: |
385 assumes x_greater_zero: "0 < x" |
385 assumes x_greater_zero: "0 < x" |
390 obtain n where "y * inverse x < real (n::nat)" |
390 obtain n where "y * inverse x < real (n::nat)" |
391 using reals_Archimedean2 .. |
391 using reals_Archimedean2 .. |
392 hence "y * inverse x * x < real n * x" |
392 hence "y * inverse x * x < real n * x" |
393 using x_greater_zero by (simp add: mult_strict_right_mono) |
393 using x_greater_zero by (simp add: mult_strict_right_mono) |
394 hence "x * inverse x * y < x * real n" |
394 hence "x * inverse x * y < x * real n" |
395 by (simp add: mult_commute ring_eq_simps) |
395 by (simp add: ring_eq_simps) |
396 hence "y < real (n::nat) * x" |
396 hence "y < real (n::nat) * x" |
397 using x_not_zero by (simp add: real_mult_inverse_left ring_eq_simps) |
397 using x_not_zero by (simp add: ring_eq_simps) |
398 thus "\<exists>(n::nat). y < real n * x" .. |
398 thus "\<exists>(n::nat). y < real n * x" .. |
399 qed |
399 qed |
400 |
400 |
401 lemma reals_Archimedean6: |
401 lemma reals_Archimedean6: |
402 "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)" |
402 "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)" |