equal
deleted
inserted
replaced
7 section\<open>Power Series, Transcendental Functions etc.\<close> |
7 section\<open>Power Series, Transcendental Functions etc.\<close> |
8 |
8 |
9 theory Transcendental |
9 theory Transcendental |
10 imports Binomial Series Deriv NthRoot |
10 imports Binomial Series Deriv NthRoot |
11 begin |
11 begin |
|
12 |
|
13 text \<open>A fact theorem on reals.\<close> |
|
14 |
|
15 lemma square_fact_le_2_fact: |
|
16 shows "fact n * fact n \<le> (fact (2 * n) :: real)" |
|
17 proof (induct n) |
|
18 case 0 then show ?case by simp |
|
19 next |
|
20 case (Suc n) |
|
21 have "(fact (Suc n)) * (fact (Suc n)) = of_nat (Suc n) * of_nat (Suc n) * (fact n * fact n :: real)" |
|
22 by (simp add: field_simps) |
|
23 also have "\<dots> \<le> of_nat (Suc n) * of_nat (Suc n) * fact (2 * n)" |
|
24 by (rule mult_left_mono [OF Suc]) simp |
|
25 also have "\<dots> \<le> of_nat (Suc (Suc (2 * n))) * of_nat (Suc (2 * n)) * fact (2 * n)" |
|
26 by (rule mult_right_mono)+ (auto simp: field_simps) |
|
27 also have "\<dots> = fact (2 * Suc n)" by (simp add: field_simps) |
|
28 finally show ?case . |
|
29 qed |
|
30 |
12 |
31 |
13 lemma of_int_leD: |
32 lemma of_int_leD: |
14 fixes x :: "'a :: linordered_idom" |
33 fixes x :: "'a :: linordered_idom" |
15 shows "\<bar>of_int n\<bar> \<le> x \<Longrightarrow> n=0 \<or> x\<ge>1" |
34 shows "\<bar>of_int n\<bar> \<le> x \<Longrightarrow> n=0 \<or> x\<ge>1" |
16 by (metis (no_types) le_less_trans not_less of_int_abs of_int_less_1_iff zabs_less_one_iff) |
35 by (metis (no_types) le_less_trans not_less of_int_abs of_int_less_1_iff zabs_less_one_iff) |