12196
|
1 |
(* Title : NthRoot.thy
|
|
2 |
Author : Jacques D. Fleuriot
|
|
3 |
Copyright : 1998 University of Cambridge
|
|
4 |
Description : Existence of nth root. Adapted from
|
|
5 |
http://www.math.unl.edu/~webnotes
|
|
6 |
*)
|
|
7 |
|
14324
|
8 |
header{*Existence of Nth Root*}
|
|
9 |
|
|
10 |
theory NthRoot = SEQ + HSeries:
|
|
11 |
|
|
12 |
text{*Various lemmas needed for this result. We follow the proof
|
|
13 |
given by John Lindsay Orr (jorr@math.unl.edu) in his Analysis
|
|
14 |
Webnotes available on the www at http://www.math.unl.edu/~webnotes
|
|
15 |
Lemmas about sequences of reals are used to reach the result.*}
|
|
16 |
|
|
17 |
lemma lemma_nth_realpow_non_empty:
|
|
18 |
"[| (0::real) < a; 0 < n |] ==> \<exists>s. s : {x. x ^ n <= a & 0 < x}"
|
|
19 |
apply (case_tac "1 <= a")
|
|
20 |
apply (rule_tac x = "1" in exI)
|
|
21 |
apply (drule_tac [2] not_real_leE)
|
|
22 |
apply (drule_tac [2] less_not_refl2 [THEN not0_implies_Suc])
|
|
23 |
apply (auto intro!: realpow_Suc_le_self simp add: real_zero_less_one)
|
|
24 |
done
|
|
25 |
|
|
26 |
lemma lemma_nth_realpow_isUb_ex:
|
|
27 |
"[| (0::real) < a; 0 < n |]
|
|
28 |
==> \<exists>u. isUb (UNIV::real set) {x. x ^ n <= a & 0 < x} u"
|
|
29 |
apply (case_tac "1 <= a")
|
|
30 |
apply (rule_tac x = "a" in exI)
|
|
31 |
apply (drule_tac [2] not_real_leE)
|
|
32 |
apply (rule_tac [2] x = "1" in exI)
|
|
33 |
apply (rule_tac [!] setleI [THEN isUbI])
|
|
34 |
apply safe
|
|
35 |
apply (simp_all (no_asm))
|
|
36 |
apply (rule_tac [!] ccontr)
|
|
37 |
apply (drule_tac [!] not_real_leE)
|
|
38 |
apply (drule realpow_ge_self2 , assumption)
|
|
39 |
apply (drule_tac n = "n" in realpow_less)
|
|
40 |
apply (assumption+)
|
|
41 |
apply (drule real_le_trans , assumption)
|
|
42 |
apply (drule_tac y = "y ^ n" in order_less_le_trans)
|
|
43 |
apply (assumption , erule real_less_irrefl)
|
|
44 |
apply (drule_tac n = "n" in real_zero_less_one [THEN realpow_less])
|
|
45 |
apply auto
|
|
46 |
done
|
|
47 |
|
|
48 |
lemma nth_realpow_isLub_ex:
|
|
49 |
"[| (0::real) < a; 0 < n |]
|
|
50 |
==> \<exists>u. isLub (UNIV::real set) {x. x ^ n <= a & 0 < x} u"
|
|
51 |
apply (blast intro: lemma_nth_realpow_isUb_ex lemma_nth_realpow_non_empty reals_complete)
|
|
52 |
done
|
|
53 |
|
|
54 |
subsection{*First Half -- Lemmas First*}
|
|
55 |
|
|
56 |
lemma lemma_nth_realpow_seq:
|
|
57 |
"isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u
|
|
58 |
==> u + inverse(real (Suc k)) ~: {x. x ^ n <= a & 0 < x}"
|
|
59 |
apply (safe , drule isLubD2 , blast)
|
|
60 |
apply (simp add: real_le_def)
|
|
61 |
done
|
|
62 |
|
|
63 |
lemma lemma_nth_realpow_isLub_gt_zero:
|
|
64 |
"[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u;
|
|
65 |
0 < a; 0 < n |] ==> 0 < u"
|
|
66 |
apply (drule lemma_nth_realpow_non_empty , auto)
|
|
67 |
apply (drule_tac y = "s" in isLub_isUb [THEN isUbD])
|
|
68 |
apply (auto intro: order_less_le_trans)
|
|
69 |
done
|
|
70 |
|
|
71 |
lemma lemma_nth_realpow_isLub_ge:
|
|
72 |
"[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u;
|
|
73 |
0 < a; 0 < n |] ==> ALL k. a <= (u + inverse(real (Suc k))) ^ n"
|
|
74 |
apply (safe)
|
|
75 |
apply (frule lemma_nth_realpow_seq , safe)
|
|
76 |
apply (auto elim: real_less_asym simp add: real_le_def)
|
|
77 |
apply (simp add: real_le_def [symmetric])
|
|
78 |
apply (rule order_less_trans [of _ 0])
|
14325
|
79 |
apply (auto intro: lemma_nth_realpow_isLub_gt_zero)
|
14324
|
80 |
done
|
|
81 |
|
|
82 |
text{*First result we want*}
|
|
83 |
lemma realpow_nth_ge:
|
|
84 |
"[| (0::real) < a; 0 < n;
|
|
85 |
isLub (UNIV::real set)
|
|
86 |
{x. x ^ n <= a & 0 < x} u |] ==> a <= u ^ n"
|
|
87 |
apply (frule lemma_nth_realpow_isLub_ge , safe)
|
|
88 |
apply (rule LIMSEQ_inverse_real_of_nat_add [THEN LIMSEQ_pow, THEN LIMSEQ_le_const])
|
|
89 |
apply (auto simp add: real_of_nat_def real_of_posnat_Suc)
|
|
90 |
done
|
|
91 |
|
|
92 |
subsection{*Second Half*}
|
|
93 |
|
|
94 |
lemma less_isLub_not_isUb:
|
|
95 |
"[| isLub (UNIV::real set) S u; x < u |]
|
|
96 |
==> ~ isUb (UNIV::real set) S x"
|
|
97 |
apply (safe)
|
|
98 |
apply (drule isLub_le_isUb)
|
|
99 |
apply assumption
|
|
100 |
apply (drule order_less_le_trans)
|
|
101 |
apply (auto simp add: real_less_not_refl)
|
|
102 |
done
|
|
103 |
|
|
104 |
lemma not_isUb_less_ex:
|
|
105 |
"~ isUb (UNIV::real set) S u ==> \<exists>x \<in> S. u < x"
|
|
106 |
apply (rule ccontr , erule swap)
|
|
107 |
apply (rule setleI [THEN isUbI])
|
|
108 |
apply (auto simp add: real_le_def)
|
|
109 |
done
|
|
110 |
|
14325
|
111 |
lemma real_mult_less_self: "0 < r ==> r * (1 + -inverse(real (Suc n))) < r"
|
|
112 |
apply (simp (no_asm) add: real_add_mult_distrib2)
|
|
113 |
apply (rule_tac C = "-r" in real_less_add_left_cancel)
|
|
114 |
apply (auto intro: real_mult_order simp add: real_add_assoc [symmetric] real_minus_zero_less_iff2)
|
|
115 |
done
|
|
116 |
|
|
117 |
lemma real_mult_add_one_minus_ge_zero:
|
|
118 |
"0 < r ==> 0 <= r*(1 + -inverse(real (Suc n)))"
|
|
119 |
apply (simp add: zero_le_mult_iff real_of_nat_inverse_le_iff)
|
|
120 |
apply (simp add: RealOrd.real_of_nat_Suc)
|
|
121 |
done
|
|
122 |
|
14324
|
123 |
lemma lemma_nth_realpow_isLub_le:
|
|
124 |
"[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u;
|
14325
|
125 |
0 < a; 0 < n |] ==> ALL k. (u*(1 + -inverse(real (Suc k)))) ^ n <= a"
|
14324
|
126 |
apply (safe)
|
|
127 |
apply (frule less_isLub_not_isUb [THEN not_isUb_less_ex])
|
|
128 |
apply (rule_tac n = "k" in real_mult_less_self)
|
|
129 |
apply (blast intro: lemma_nth_realpow_isLub_gt_zero)
|
|
130 |
apply (safe)
|
|
131 |
apply (drule_tac n = "k" in lemma_nth_realpow_isLub_gt_zero [THEN real_mult_add_one_minus_ge_zero])
|
|
132 |
apply (drule_tac [3] conjI [THEN realpow_le2])
|
|
133 |
apply (rule_tac [3] order_less_imp_le)
|
|
134 |
apply (auto intro: order_trans)
|
|
135 |
done
|
|
136 |
|
|
137 |
text{*Second result we want*}
|
|
138 |
lemma realpow_nth_le:
|
|
139 |
"[| (0::real) < a; 0 < n;
|
|
140 |
isLub (UNIV::real set)
|
|
141 |
{x. x ^ n <= a & 0 < x} u |] ==> u ^ n <= a"
|
|
142 |
apply (frule lemma_nth_realpow_isLub_le , safe)
|
|
143 |
apply (rule LIMSEQ_inverse_real_of_nat_add_minus_mult [THEN LIMSEQ_pow, THEN LIMSEQ_le_const2])
|
|
144 |
apply (auto simp add: real_of_nat_def real_of_posnat_Suc)
|
|
145 |
done
|
|
146 |
|
|
147 |
(*----------- The theorem at last! -----------*)
|
|
148 |
lemma realpow_nth: "[| (0::real) < a; 0 < n |] ==> \<exists>r. r ^ n = a"
|
|
149 |
apply (frule nth_realpow_isLub_ex , auto)
|
|
150 |
apply (auto intro: realpow_nth_le realpow_nth_ge real_le_anti_sym)
|
|
151 |
done
|
|
152 |
|
|
153 |
(* positive only *)
|
|
154 |
lemma realpow_pos_nth: "[| (0::real) < a; 0 < n |] ==> \<exists>r. 0 < r & r ^ n = a"
|
|
155 |
apply (frule nth_realpow_isLub_ex , auto)
|
|
156 |
apply (auto intro: realpow_nth_le realpow_nth_ge real_le_anti_sym lemma_nth_realpow_isLub_gt_zero)
|
|
157 |
done
|
|
158 |
|
|
159 |
lemma realpow_pos_nth2: "(0::real) < a ==> \<exists>r. 0 < r & r ^ Suc n = a"
|
|
160 |
apply (blast intro: realpow_pos_nth)
|
|
161 |
done
|
|
162 |
|
|
163 |
(* uniqueness of nth positive root *)
|
|
164 |
lemma realpow_pos_nth_unique:
|
|
165 |
"[| (0::real) < a; 0 < n |] ==> EX! r. 0 < r & r ^ n = a"
|
|
166 |
apply (auto intro!: realpow_pos_nth)
|
|
167 |
apply (cut_tac x = "r" and y = "y" in linorder_less_linear)
|
|
168 |
apply auto
|
|
169 |
apply (drule_tac x = "r" in realpow_less)
|
|
170 |
apply (drule_tac [4] x = "y" in realpow_less)
|
|
171 |
apply (auto simp add: real_less_not_refl)
|
|
172 |
done
|
|
173 |
|
|
174 |
ML
|
|
175 |
{*
|
|
176 |
val nth_realpow_isLub_ex = thm"nth_realpow_isLub_ex";
|
|
177 |
val realpow_nth_ge = thm"realpow_nth_ge";
|
|
178 |
val less_isLub_not_isUb = thm"less_isLub_not_isUb";
|
|
179 |
val not_isUb_less_ex = thm"not_isUb_less_ex";
|
|
180 |
val realpow_nth_le = thm"realpow_nth_le";
|
|
181 |
val realpow_nth = thm"realpow_nth";
|
|
182 |
val realpow_pos_nth = thm"realpow_pos_nth";
|
|
183 |
val realpow_pos_nth2 = thm"realpow_pos_nth2";
|
|
184 |
val realpow_pos_nth_unique = thm"realpow_pos_nth_unique";
|
|
185 |
*}
|
|
186 |
|
|
187 |
end
|