1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: NRootIR.v,v 1.5 2004/04/23 10:01:05 lcf Exp $ *)
21 (*#* printing NRoot %\ensuremath{\sqrt[n]{\cdot}}% *)
23 (*#* printing sqrt %\ensuremath{\sqrt{\cdot}}% *)
25 include "reals/OddPolyRootIR.ma".
27 (*#* * Roots of Real Numbers *)
33 (*#* ** Existence of roots
35 %\begin{convention}% Let [n] be a natural number and [c] a nonnegative real.
36 [p] is the auxiliary polynomial [_X_[^]n[-] (_C_ c)].
41 cic:/CoRN/reals/NRootIR/NRoot/n.var
45 cic:/CoRN/reals/NRootIR/NRoot/n_pos.var
49 cic:/CoRN/reals/NRootIR/NRoot/c.var
53 cic:/CoRN/reals/NRootIR/NRoot/c_nonneg.var
58 inline procedural "cic:/CoRN/reals/NRootIR/NRoot/p.con" "NRoot__" as definition.
62 inline procedural "cic:/CoRN/reals/NRootIR/CnrootIR.con" as lemma.
68 (*#* We define the root of order [n] for any nonnegative real number and
69 prove its main properties:
70 - $\left(\sqrt[n]x\right)^n=x$#(sqrt(n) x)^n =x#;
71 - $0\leq\sqrt[n]x$#0≤sqrt(n)x#;
72 - if [Zero [<] x] then $0<\sqrt[n]x$#0<sqrt(n)x#;
73 - $\sqrt[n]{x^n}=x$#sqrt(n) x^n =x#;
74 - the nth root is monotonous;
75 - in particular, if [x [<] One] then $\sqrt[n]x<1$#sqrt(n) x<1#.
77 [(nroot ??)] will be written as [NRoot].
84 inline procedural "cic:/CoRN/reals/NRootIR/nroot.con" as lemma.
86 inline procedural "cic:/CoRN/reals/NRootIR/NRoot.con" as definition.
88 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_power.con" as lemma.
91 Hint Resolve NRoot_power: algebra.
94 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_nonneg.con" as lemma.
96 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_pos.con" as lemma.
98 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_power'.con" as lemma.
100 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_pres_less.con" as lemma.
102 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_less_one.con" as lemma.
104 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_cancel.con" as lemma.
106 (*#* %\begin{convention}% Let [x,y] be nonnegative real numbers.
107 %\end{convention}% *)
110 cic:/CoRN/reals/NRootIR/Nth_Root/x.var
114 cic:/CoRN/reals/NRootIR/Nth_Root/y.var
118 cic:/CoRN/reals/NRootIR/Nth_Root/Hx.var
122 cic:/CoRN/reals/NRootIR/Nth_Root/Hy.var
125 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_wd.con" as lemma.
127 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_unique.con" as lemma.
134 Implicit Arguments NRoot [x n].
138 Hint Resolve NRoot_power NRoot_power': algebra.
141 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_resp_leEq.con" as lemma.
143 (*#**********************************)
149 (*#**********************************)
151 (*#* ** Square root *)
153 inline procedural "cic:/CoRN/reals/NRootIR/sqrt.con" as definition.
155 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_sqr.con" as lemma.
158 Hint Resolve sqrt_sqr: algebra.
161 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_nonneg.con" as lemma.
163 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_wd.con" as lemma.
166 Hint Resolve sqrt_wd: algebra_c.
169 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_to_nonneg.con" as lemma.
171 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_to_nonpos.con" as lemma.
173 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_mult.con" as lemma.
176 Hint Resolve sqrt_mult: algebra.
179 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_mult_wd.con" as lemma.
181 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_less.con" as lemma.
183 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_less'.con" as lemma.
185 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_resp_leEq.con" as lemma.
187 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_resp_less.con" as lemma.
194 Hint Resolve sqrt_wd: algebra_c.
198 Hint Resolve sqrt_sqr sqrt_mult: algebra.
202 Section Absolute_Props
205 (*#* ** More on absolute value
207 With the help of square roots, we can prove some more properties of absolute
211 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_sqrt_sqr.con" as lemma.
214 Hint Resolve AbsIR_sqrt_sqr: algebra.
217 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_resp_mult.con" as lemma.
219 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_mult_pos.con" as lemma.
221 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_mult_pos'.con" as lemma.
223 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_nexp.con" as lemma.
225 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_nexp_op.con" as lemma.
227 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_less_square.con" as lemma.
229 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_leEq_square.con" as lemma.
231 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_division.con" as lemma.
233 (*#* Some special cases. *)
235 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_recip.con" as lemma.
237 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_div_two.con" as lemma.
239 (*#* Cauchy-Schwartz for IR and variants on that subject. *)
241 inline procedural "cic:/CoRN/reals/NRootIR/triangle_IR.con" as lemma.
243 inline procedural "cic:/CoRN/reals/NRootIR/triangle_SumIR.con" as lemma.
245 inline procedural "cic:/CoRN/reals/NRootIR/triangle_IR_minus.con" as lemma.
247 inline procedural "cic:/CoRN/reals/NRootIR/weird_triangleIR.con" as lemma.
249 inline procedural "cic:/CoRN/reals/NRootIR/triangle_IR_minus'.con" as lemma.
251 inline procedural "cic:/CoRN/reals/NRootIR/triangle_SumxIR.con" as lemma.
253 inline procedural "cic:/CoRN/reals/NRootIR/triangle_Sum2IR.con" as lemma.
255 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_str_bnd_AbsIR.con" as lemma.
257 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_bnd_AbsIR.con" as lemma.
267 (*#* **Cauchy sequences
269 With these results, we can also prove that the sequence of reciprocals of a
270 Cauchy sequence that is never zero and whose Limit is not zero is also a
274 inline procedural "cic:/CoRN/reals/NRootIR/Cauchy_Lim_recip.con" as lemma.
276 inline procedural "cic:/CoRN/reals/NRootIR/Cauchy_recip.con" as lemma.
278 inline procedural "cic:/CoRN/reals/NRootIR/Lim_recip.con" as lemma.