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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/reals/NRootIR".
21 (* $Id: NRootIR.v,v 1.5 2004/04/23 10:01:05 lcf Exp $ *)
23 (*#* printing NRoot %\ensuremath{\sqrt[n]{\cdot}}% *)
25 (*#* printing sqrt %\ensuremath{\sqrt{\cdot}}% *)
27 include "reals/OddPolyRootIR.ma".
29 (*#* * Roots of Real Numbers *)
35 (*#* ** Existence of roots
37 %\begin{convention}% Let [n] be a natural number and [c] a nonnegative real.
38 [p] is the auxiliary polynomial [_X_[^]n[-] (_C_ c)].
42 alias id "n" = "cic:/CoRN/reals/NRootIR/NRoot/n.var".
44 alias id "n_pos" = "cic:/CoRN/reals/NRootIR/NRoot/n_pos.var".
46 alias id "c" = "cic:/CoRN/reals/NRootIR/NRoot/c.var".
48 alias id "c_nonneg" = "cic:/CoRN/reals/NRootIR/NRoot/c_nonneg.var".
52 inline "cic:/CoRN/reals/NRootIR/NRoot/p.con" "NRoot__".
56 inline "cic:/CoRN/reals/NRootIR/CnrootIR.con".
62 (*#* We define the root of order [n] for any nonnegative real number and
63 prove its main properties:
64 - $\left(\sqrt[n]x\right)^n=x$#(sqrt(n) x)^n =x#;
65 - $0\leq\sqrt[n]x$#0≤sqrt(n)x#;
66 - if [Zero [<] x] then $0<\sqrt[n]x$#0<sqrt(n)x#;
67 - $\sqrt[n]{x^n}=x$#sqrt(n) x^n =x#;
68 - the nth root is monotonous;
69 - in particular, if [x [<] One] then $\sqrt[n]x<1$#sqrt(n) x<1#.
71 [(nroot ??)] will be written as [NRoot].
78 inline "cic:/CoRN/reals/NRootIR/nroot.con".
80 inline "cic:/CoRN/reals/NRootIR/NRoot.con".
82 inline "cic:/CoRN/reals/NRootIR/NRoot_power.con".
85 Hint Resolve NRoot_power: algebra.
88 inline "cic:/CoRN/reals/NRootIR/NRoot_nonneg.con".
90 inline "cic:/CoRN/reals/NRootIR/NRoot_pos.con".
92 inline "cic:/CoRN/reals/NRootIR/NRoot_power'.con".
94 inline "cic:/CoRN/reals/NRootIR/NRoot_pres_less.con".
96 inline "cic:/CoRN/reals/NRootIR/NRoot_less_one.con".
98 inline "cic:/CoRN/reals/NRootIR/NRoot_cancel.con".
100 (*#* %\begin{convention}% Let [x,y] be nonnegative real numbers.
101 %\end{convention}% *)
103 alias id "x" = "cic:/CoRN/reals/NRootIR/Nth_Root/x.var".
105 alias id "y" = "cic:/CoRN/reals/NRootIR/Nth_Root/y.var".
107 alias id "Hx" = "cic:/CoRN/reals/NRootIR/Nth_Root/Hx.var".
109 alias id "Hy" = "cic:/CoRN/reals/NRootIR/Nth_Root/Hy.var".
111 inline "cic:/CoRN/reals/NRootIR/NRoot_wd.con".
113 inline "cic:/CoRN/reals/NRootIR/NRoot_unique.con".
120 Implicit Arguments NRoot [x n].
124 Hint Resolve NRoot_power NRoot_power': algebra.
127 inline "cic:/CoRN/reals/NRootIR/NRoot_resp_leEq.con".
129 (*#**********************************)
135 (*#**********************************)
137 (*#* ** Square root *)
139 inline "cic:/CoRN/reals/NRootIR/sqrt.con".
141 inline "cic:/CoRN/reals/NRootIR/sqrt_sqr.con".
144 Hint Resolve sqrt_sqr: algebra.
147 inline "cic:/CoRN/reals/NRootIR/sqrt_nonneg.con".
149 inline "cic:/CoRN/reals/NRootIR/sqrt_wd.con".
152 Hint Resolve sqrt_wd: algebra_c.
155 inline "cic:/CoRN/reals/NRootIR/sqrt_to_nonneg.con".
157 inline "cic:/CoRN/reals/NRootIR/sqrt_to_nonpos.con".
159 inline "cic:/CoRN/reals/NRootIR/sqrt_mult.con".
162 Hint Resolve sqrt_mult: algebra.
165 inline "cic:/CoRN/reals/NRootIR/sqrt_mult_wd.con".
167 inline "cic:/CoRN/reals/NRootIR/sqrt_less.con".
169 inline "cic:/CoRN/reals/NRootIR/sqrt_less'.con".
171 inline "cic:/CoRN/reals/NRootIR/sqrt_resp_leEq.con".
173 inline "cic:/CoRN/reals/NRootIR/sqrt_resp_less.con".
180 Hint Resolve sqrt_wd: algebra_c.
184 Hint Resolve sqrt_sqr sqrt_mult: algebra.
188 Section Absolute_Props
191 (*#* ** More on absolute value
193 With the help of square roots, we can prove some more properties of absolute
197 inline "cic:/CoRN/reals/NRootIR/AbsIR_sqrt_sqr.con".
200 Hint Resolve AbsIR_sqrt_sqr: algebra.
203 inline "cic:/CoRN/reals/NRootIR/AbsIR_resp_mult.con".
205 inline "cic:/CoRN/reals/NRootIR/AbsIR_mult_pos.con".
207 inline "cic:/CoRN/reals/NRootIR/AbsIR_mult_pos'.con".
209 inline "cic:/CoRN/reals/NRootIR/AbsIR_nexp.con".
211 inline "cic:/CoRN/reals/NRootIR/AbsIR_nexp_op.con".
213 inline "cic:/CoRN/reals/NRootIR/AbsIR_less_square.con".
215 inline "cic:/CoRN/reals/NRootIR/AbsIR_leEq_square.con".
217 inline "cic:/CoRN/reals/NRootIR/AbsIR_division.con".
219 (*#* Some special cases. *)
221 inline "cic:/CoRN/reals/NRootIR/AbsIR_recip.con".
223 inline "cic:/CoRN/reals/NRootIR/AbsIR_div_two.con".
225 (*#* Cauchy-Schwartz for IR and variants on that subject. *)
227 inline "cic:/CoRN/reals/NRootIR/triangle_IR.con".
229 inline "cic:/CoRN/reals/NRootIR/triangle_SumIR.con".
231 inline "cic:/CoRN/reals/NRootIR/triangle_IR_minus.con".
233 inline "cic:/CoRN/reals/NRootIR/weird_triangleIR.con".
235 inline "cic:/CoRN/reals/NRootIR/triangle_IR_minus'.con".
237 inline "cic:/CoRN/reals/NRootIR/triangle_SumxIR.con".
239 inline "cic:/CoRN/reals/NRootIR/triangle_Sum2IR.con".
241 inline "cic:/CoRN/reals/NRootIR/AbsIR_str_bnd_AbsIR.con".
243 inline "cic:/CoRN/reals/NRootIR/AbsIR_bnd_AbsIR.con".
253 (*#* **Cauchy sequences
255 With these results, we can also prove that the sequence of reciprocals of a
256 Cauchy sequence that is never zero and whose Limit is not zero is also a
260 inline "cic:/CoRN/reals/NRootIR/Cauchy_Lim_recip.con".
262 inline "cic:/CoRN/reals/NRootIR/Cauchy_recip.con".
264 inline "cic:/CoRN/reals/NRootIR/Lim_recip.con".