(* Title : NthRoot.thy Author : Jacques D. Fleuriot Copyright : 1998 University of Cambridge Conversion to Isar and new proofs by Lawrence C Paulson, 2004 *) header{*Existence of Nth Root*} theory NthRoot imports SEQ HSeries begin text {* Various lemmas needed for this result. We follow the proof given by John Lindsay Orr (\texttt{jorr@math.unl.edu}) in his Analysis Webnotes available at \url{http://www.math.unl.edu/~webnotes}. Lemmas about sequences of reals are used to reach the result. *} lemma lemma_nth_realpow_non_empty: "[| (0::real) < a; 0 < n |] ==> ∃s. s : {x. x ^ n <= a & 0 < x}" apply (case_tac "1 <= a") apply (rule_tac x = 1 in exI) apply (drule_tac [2] linorder_not_le [THEN iffD1]) apply (drule_tac [2] less_not_refl2 [THEN not0_implies_Suc], simp) apply (force intro!: realpow_Suc_le_self simp del: realpow_Suc) done text{*Used only just below*} lemma realpow_ge_self2: "[| (1::real) ≤ r; 0 < n |] ==> r ≤ r ^ n" by (insert power_increasing [of 1 n r], simp) lemma lemma_nth_realpow_isUb_ex: "[| (0::real) < a; 0 < n |] ==> ∃u. isUb (UNIV::real set) {x. x ^ n <= a & 0 < x} u" apply (case_tac "1 <= a") apply (rule_tac x = a in exI) apply (drule_tac [2] linorder_not_le [THEN iffD1]) apply (rule_tac [2] x = 1 in exI) apply (rule_tac [!] setleI [THEN isUbI], safe) apply (simp_all (no_asm)) apply (rule_tac [!] ccontr) apply (drule_tac [!] linorder_not_le [THEN iffD1]) apply (drule realpow_ge_self2, assumption) apply (drule_tac n = n in realpow_less) apply (assumption+) apply (drule real_le_trans, assumption) apply (drule_tac y = "y ^ n" in order_less_le_trans, assumption, simp) apply (drule_tac n = n in zero_less_one [THEN realpow_less], auto) done lemma nth_realpow_isLub_ex: "[| (0::real) < a; 0 < n |] ==> ∃u. isLub (UNIV::real set) {x. x ^ n <= a & 0 < x} u" by (blast intro: lemma_nth_realpow_isUb_ex lemma_nth_realpow_non_empty reals_complete) subsection{*First Half -- Lemmas First*} lemma lemma_nth_realpow_seq: "isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u ==> u + inverse(real (Suc k)) ~: {x. x ^ n <= a & 0 < x}" apply (safe, drule isLubD2, blast) apply (simp add: linorder_not_less [symmetric]) done lemma lemma_nth_realpow_isLub_gt_zero: "[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u; 0 < a; 0 < n |] ==> 0 < u" apply (drule lemma_nth_realpow_non_empty, auto) apply (drule_tac y = s in isLub_isUb [THEN isUbD]) apply (auto intro: order_less_le_trans) done lemma lemma_nth_realpow_isLub_ge: "[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u; 0 < a; 0 < n |] ==> ALL k. a <= (u + inverse(real (Suc k))) ^ n" apply safe apply (frule lemma_nth_realpow_seq, safe) apply (auto elim: order_less_asym simp add: linorder_not_less [symmetric] iff: real_0_less_add_iff) --{*legacy iff rule!*} apply (simp add: linorder_not_less) apply (rule order_less_trans [of _ 0]) apply (auto intro: lemma_nth_realpow_isLub_gt_zero) done text{*First result we want*} lemma realpow_nth_ge: "[| (0::real) < a; 0 < n; isLub (UNIV::real set) {x. x ^ n <= a & 0 < x} u |] ==> a <= u ^ n" apply (frule lemma_nth_realpow_isLub_ge, safe) apply (rule LIMSEQ_inverse_real_of_nat_add [THEN LIMSEQ_pow, THEN LIMSEQ_le_const]) apply (auto simp add: real_of_nat_def) done subsection{*Second Half*} lemma less_isLub_not_isUb: "[| isLub (UNIV::real set) S u; x < u |] ==> ~ isUb (UNIV::real set) S x" apply safe apply (drule isLub_le_isUb, assumption) apply (drule order_less_le_trans, auto) done lemma not_isUb_less_ex: "~ isUb (UNIV::real set) S u ==> ∃x ∈ S. u < x" apply (rule ccontr, erule swap) apply (rule setleI [THEN isUbI]) apply (auto simp add: linorder_not_less [symmetric]) done lemma real_mult_less_self: "0 < r ==> r * (1 + -inverse(real (Suc n))) < r" apply (simp (no_asm) add: right_distrib) apply (rule add_less_cancel_left [of "-r", THEN iffD1]) apply (auto intro: mult_pos_pos simp add: add_assoc [symmetric] neg_less_0_iff_less) done lemma real_mult_add_one_minus_ge_zero: "0 < r ==> 0 <= r*(1 + -inverse(real (Suc n)))" by (simp add: zero_le_mult_iff real_of_nat_inverse_le_iff real_0_le_add_iff) lemma lemma_nth_realpow_isLub_le: "[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u; 0 < a; 0 < n |] ==> ALL k. (u*(1 + -inverse(real (Suc k)))) ^ n <= a" apply safe apply (frule less_isLub_not_isUb [THEN not_isUb_less_ex]) apply (rule_tac n = k in real_mult_less_self) apply (blast intro: lemma_nth_realpow_isLub_gt_zero, safe) apply (drule_tac n = k in lemma_nth_realpow_isLub_gt_zero [THEN real_mult_add_one_minus_ge_zero], assumption+) apply (blast intro: order_trans order_less_imp_le power_mono) done text{*Second result we want*} lemma realpow_nth_le: "[| (0::real) < a; 0 < n; isLub (UNIV::real set) {x. x ^ n <= a & 0 < x} u |] ==> u ^ n <= a" apply (frule lemma_nth_realpow_isLub_le, safe) apply (rule LIMSEQ_inverse_real_of_nat_add_minus_mult [THEN LIMSEQ_pow, THEN LIMSEQ_le_const2]) apply (auto simp add: real_of_nat_def) done text{*The theorem at last!*} lemma realpow_nth: "[| (0::real) < a; 0 < n |] ==> ∃r. r ^ n = a" apply (frule nth_realpow_isLub_ex, auto) apply (auto intro: realpow_nth_le realpow_nth_ge order_antisym) done (* positive only *) lemma realpow_pos_nth: "[| (0::real) < a; 0 < n |] ==> ∃r. 0 < r & r ^ n = a" apply (frule nth_realpow_isLub_ex, auto) apply (auto intro: realpow_nth_le realpow_nth_ge order_antisym lemma_nth_realpow_isLub_gt_zero) done lemma realpow_pos_nth2: "(0::real) < a ==> ∃r. 0 < r & r ^ Suc n = a" by (blast intro: realpow_pos_nth) (* uniqueness of nth positive root *) lemma realpow_pos_nth_unique: "[| (0::real) < a; 0 < n |] ==> EX! r. 0 < r & r ^ n = a" apply (auto intro!: realpow_pos_nth) apply (cut_tac x = r and y = y in linorder_less_linear, auto) apply (drule_tac x = r in realpow_less) apply (drule_tac [4] x = y in realpow_less, auto) done ML {* val nth_realpow_isLub_ex = thm"nth_realpow_isLub_ex"; val realpow_nth_ge = thm"realpow_nth_ge"; val less_isLub_not_isUb = thm"less_isLub_not_isUb"; val not_isUb_less_ex = thm"not_isUb_less_ex"; val realpow_nth_le = thm"realpow_nth_le"; val realpow_nth = thm"realpow_nth"; val realpow_pos_nth = thm"realpow_pos_nth"; val realpow_pos_nth2 = thm"realpow_pos_nth2"; val realpow_pos_nth_unique = thm"realpow_pos_nth_unique"; *} end
lemma lemma_nth_realpow_non_empty:
[| 0 < a; 0 < n |] ==> ∃s. s ∈ {x. x ^ n ≤ a ∧ 0 < x}
lemma realpow_ge_self2:
[| 1 ≤ r; 0 < n |] ==> r ≤ r ^ n
lemma lemma_nth_realpow_isUb_ex:
[| 0 < a; 0 < n |] ==> ∃u. isUb UNIV {x. x ^ n ≤ a ∧ 0 < x} u
lemma nth_realpow_isLub_ex:
[| 0 < a; 0 < n |] ==> ∃u. isLub UNIV {x. x ^ n ≤ a ∧ 0 < x} u
lemma lemma_nth_realpow_seq:
isLub UNIV {x. x ^ n ≤ a ∧ 0 < x} u ==> u + inverse (real (Suc k)) ∉ {x. x ^ n ≤ a ∧ 0 < x}
lemma lemma_nth_realpow_isLub_gt_zero:
[| isLub UNIV {x. x ^ n ≤ a ∧ 0 < x} u; 0 < a; 0 < n |] ==> 0 < u
lemma lemma_nth_realpow_isLub_ge:
[| isLub UNIV {x. x ^ n ≤ a ∧ 0 < x} u; 0 < a; 0 < n |] ==> ∀k. a ≤ (u + inverse (real (Suc k))) ^ n
lemma realpow_nth_ge:
[| 0 < a; 0 < n; isLub UNIV {x. x ^ n ≤ a ∧ 0 < x} u |] ==> a ≤ u ^ n
lemma less_isLub_not_isUb:
[| isLub UNIV S u; x < u |] ==> ¬ isUb UNIV S x
lemma not_isUb_less_ex:
¬ isUb UNIV S u ==> ∃x∈S. u < x
lemma real_mult_less_self:
0 < r ==> r * (1 + - inverse (real (Suc n))) < r
lemma real_mult_add_one_minus_ge_zero:
0 < r ==> 0 ≤ r * (1 + - inverse (real (Suc n)))
lemma lemma_nth_realpow_isLub_le:
[| isLub UNIV {x. x ^ n ≤ a ∧ 0 < x} u; 0 < a; 0 < n |] ==> ∀k. (u * (1 + - inverse (real (Suc k)))) ^ n ≤ a
lemma realpow_nth_le:
[| 0 < a; 0 < n; isLub UNIV {x. x ^ n ≤ a ∧ 0 < x} u |] ==> u ^ n ≤ a
lemma realpow_nth:
[| 0 < a; 0 < n |] ==> ∃r. r ^ n = a
lemma realpow_pos_nth:
[| 0 < a; 0 < n |] ==> ∃r>0. r ^ n = a
lemma realpow_pos_nth2:
0 < a ==> ∃r>0. r ^ Suc n = a
lemma realpow_pos_nth_unique:
[| 0 < a; 0 < n |] ==> ∃!r. 0 < r ∧ r ^ n = a