equal
deleted
inserted
replaced
6 |
6 |
7 header{*Existence of Nth Root*} |
7 header{*Existence of Nth Root*} |
8 |
8 |
9 theory NthRoot = SEQ + HSeries: |
9 theory NthRoot = SEQ + HSeries: |
10 |
10 |
11 text{*Various lemmas needed for this result. We follow the proof |
11 text {* |
12 given by John Lindsay Orr (jorr@math.unl.edu) in his Analysis |
12 Various lemmas needed for this result. We follow the proof given by |
13 Webnotes available on the www at http://www.math.unl.edu/~webnotes |
13 John Lindsay Orr (\texttt{jorr@math.unl.edu}) in his Analysis |
14 Lemmas about sequences of reals are used to reach the result.*} |
14 Webnotes available at \url{http://www.math.unl.edu/~webnotes}. |
|
15 |
|
16 Lemmas about sequences of reals are used to reach the result. |
|
17 *} |
15 |
18 |
16 lemma lemma_nth_realpow_non_empty: |
19 lemma lemma_nth_realpow_non_empty: |
17 "[| (0::real) < a; 0 < n |] ==> \<exists>s. s : {x. x ^ n <= a & 0 < x}" |
20 "[| (0::real) < a; 0 < n |] ==> \<exists>s. s : {x. x ^ n <= a & 0 < x}" |
18 apply (case_tac "1 <= a") |
21 apply (case_tac "1 <= a") |
19 apply (rule_tac x = 1 in exI) |
22 apply (rule_tac x = 1 in exI) |