:: PREPOWER semantic presentation
begin
registration
let i be Integer;
cluster|.i.| -> natural ;
coherence
abs i is natural ;
end;
theorem Th1: :: PREPOWER:1
for a being real number
for s1 being Real_Sequence st s1 is convergent & ( for n being Element of NAT holds s1 . n >= a ) holds
lim s1 >= a
proof
let a be real number ; ::_thesis: for s1 being Real_Sequence st s1 is convergent & ( for n being Element of NAT holds s1 . n >= a ) holds
lim s1 >= a
let s1 be Real_Sequence; ::_thesis: ( s1 is convergent & ( for n being Element of NAT holds s1 . n >= a ) implies lim s1 >= a )
assume that
A1: s1 is convergent and
A2: for n being Element of NAT holds s1 . n >= a ; ::_thesis: lim s1 >= a
a in REAL by XREAL_0:def_1;
then reconsider s = NAT --> a as Real_Sequence by FUNCOP_1:45;
A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_>=_s_._n
let n be Element of NAT ; ::_thesis: s1 . n >= s . n
s1 . n >= a by A2;
hence s1 . n >= s . n by FUNCOP_1:7; ::_thesis: verum
end;
lim s = s . 0 by SEQ_4:26
.= a by FUNCOP_1:7 ;
hence lim s1 >= a by A1, A3, SEQ_2:18; ::_thesis: verum
end;
theorem Th2: :: PREPOWER:2
for a being real number
for s1 being Real_Sequence st s1 is convergent & ( for n being Element of NAT holds s1 . n <= a ) holds
lim s1 <= a
proof
let a be real number ; ::_thesis: for s1 being Real_Sequence st s1 is convergent & ( for n being Element of NAT holds s1 . n <= a ) holds
lim s1 <= a
let s1 be Real_Sequence; ::_thesis: ( s1 is convergent & ( for n being Element of NAT holds s1 . n <= a ) implies lim s1 <= a )
assume that
A1: s1 is convergent and
A2: for n being Element of NAT holds s1 . n <= a ; ::_thesis: lim s1 <= a
a in REAL by XREAL_0:def_1;
then reconsider s = NAT --> a as Real_Sequence by FUNCOP_1:45;
A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<=_s_._n
let n be Element of NAT ; ::_thesis: s1 . n <= s . n
s1 . n <= a by A2;
hence s1 . n <= s . n by FUNCOP_1:7; ::_thesis: verum
end;
lim s = s . 0 by SEQ_4:26
.= a by FUNCOP_1:7 ;
hence lim s1 <= a by A1, A3, SEQ_2:18; ::_thesis: verum
end;
definition
let a be real number ;
funca GeoSeq -> Real_Sequence means :Def1: :: PREPOWER:def 1
for m being Element of NAT holds it . m = a |^ m;
existence
ex b1 being Real_Sequence st
for m being Element of NAT holds b1 . m = a |^ m
proof
reconsider a = a as Real by XREAL_0:def_1;
deffunc H1( Element of NAT ) -> Element of REAL = a |^ $1;
ex f being Real_Sequence st
for m being Element of NAT holds f . m = H1(m) from FUNCT_2:sch_4();
hence ex b1 being Real_Sequence st
for m being Element of NAT holds b1 . m = a |^ m ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Real_Sequence st ( for m being Element of NAT holds b1 . m = a |^ m ) & ( for m being Element of NAT holds b2 . m = a |^ m ) holds
b1 = b2
proof
let s1, s2 be Real_Sequence; ::_thesis: ( ( for m being Element of NAT holds s1 . m = a |^ m ) & ( for m being Element of NAT holds s2 . m = a |^ m ) implies s1 = s2 )
assume that
A1: for n being Element of NAT holds s1 . n = a |^ n and
A2: for n being Element of NAT holds s2 . n = a |^ n ; ::_thesis: s1 = s2
for n being Element of NAT holds s1 . n = s2 . n
proof
let n be Element of NAT ; ::_thesis: s1 . n = s2 . n
thus s1 . n = a |^ n by A1
.= s2 . n by A2 ; ::_thesis: verum
end;
hence s1 = s2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines GeoSeq PREPOWER:def_1_:_
for a being real number
for b2 being Real_Sequence holds
( b2 = a GeoSeq iff for m being Element of NAT holds b2 . m = a |^ m );
theorem Th3: :: PREPOWER:3
for a being real number
for s1 being Real_Sequence holds
( s1 = a GeoSeq iff ( s1 . 0 = 1 & ( for m being Element of NAT holds s1 . (m + 1) = (s1 . m) * a ) ) )
proof
let a be real number ; ::_thesis: for s1 being Real_Sequence holds
( s1 = a GeoSeq iff ( s1 . 0 = 1 & ( for m being Element of NAT holds s1 . (m + 1) = (s1 . m) * a ) ) )
let s1 be Real_Sequence; ::_thesis: ( s1 = a GeoSeq iff ( s1 . 0 = 1 & ( for m being Element of NAT holds s1 . (m + 1) = (s1 . m) * a ) ) )
defpred S1[ Element of NAT ] means s1 . $1 = (a GeoSeq) . $1;
hereby ::_thesis: ( s1 . 0 = 1 & ( for m being Element of NAT holds s1 . (m + 1) = (s1 . m) * a ) implies s1 = a GeoSeq )
assume A1: s1 = a GeoSeq ; ::_thesis: ( s1 . 0 = 1 & ( for m being Element of NAT holds s1 . (m + 1) = (s1 . m) * a ) )
hence s1 . 0 = a |^ 0 by Def1
.= 1 by NEWTON:4 ;
::_thesis: for m being Element of NAT holds s1 . (m + 1) = (s1 . m) * a
let m be Element of NAT ; ::_thesis: s1 . (m + 1) = (s1 . m) * a
thus s1 . (m + 1) = a |^ (m + 1) by A1, Def1
.= (a |^ m) * a by NEWTON:6
.= (s1 . m) * a by A1, Def1 ; ::_thesis: verum
end;
assume that
A2: s1 . 0 = 1 and
A3: for m being Element of NAT holds s1 . (m + 1) = (s1 . m) * a ; ::_thesis: s1 = a GeoSeq
A4: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A5: s1 . m = (a GeoSeq) . m ; ::_thesis: S1[m + 1]
thus s1 . (m + 1) = (s1 . m) * a by A3
.= (a |^ m) * a by A5, Def1
.= a |^ (m + 1) by NEWTON:6
.= (a GeoSeq) . (m + 1) by Def1 ; ::_thesis: verum
end;
s1 . 0 = a |^ 0 by A2, NEWTON:4
.= (a GeoSeq) . 0 by Def1 ;
then A6: S1[ 0 ] ;
for m being Element of NAT holds S1[m] from NAT_1:sch_1(A6, A4);
hence s1 = a GeoSeq by FUNCT_2:63; ::_thesis: verum
end;
theorem :: PREPOWER:4
for a being real number st a <> 0 holds
for m being Element of NAT holds (a GeoSeq) . m <> 0
proof
let a be real number ; ::_thesis: ( a <> 0 implies for m being Element of NAT holds (a GeoSeq) . m <> 0 )
assume A1: a <> 0 ; ::_thesis: for m being Element of NAT holds (a GeoSeq) . m <> 0
defpred S1[ Element of NAT ] means (a GeoSeq) . $1 <> 0 ;
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: (a GeoSeq) . n <> 0 ; ::_thesis: S1[n + 1]
(a GeoSeq) . (n + 1) = ((a GeoSeq) . n) * a by Th3;
hence S1[n + 1] by A1, A3, XCMPLX_1:6; ::_thesis: verum
end;
A4: S1[ 0 ] by Th3;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); ::_thesis: verum
end;
theorem Th5: :: PREPOWER:5
for a being real number
for n being Nat st 0 <> a holds
0 <> a |^ n
proof
let a be real number ; ::_thesis: for n being Nat st 0 <> a holds
0 <> a |^ n
let n be Nat; ::_thesis: ( 0 <> a implies 0 <> a |^ n )
defpred S1[ Nat] means a |^ $1 <> 0 ;
assume A1: 0 <> a ; ::_thesis: 0 <> a |^ n
A2: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume a |^ m <> 0 ; ::_thesis: S1[m + 1]
then (a |^ m) * a <> 0 by A1, XCMPLX_1:6;
hence S1[m + 1] by NEWTON:6; ::_thesis: verum
end;
A3: S1[ 0 ] by NEWTON:4;
for m being Nat holds S1[m] from NAT_1:sch_2(A3, A2);
hence 0 <> a |^ n ; ::_thesis: verum
end;
theorem Th6: :: PREPOWER:6
for a being real number
for n being Nat st 0 < a holds
0 < a |^ n
proof
let a be real number ; ::_thesis: for n being Nat st 0 < a holds
0 < a |^ n
let n be Nat; ::_thesis: ( 0 < a implies 0 < a |^ n )
defpred S1[ Nat] means 0 < a |^ $1;
assume A1: 0 < a ; ::_thesis: 0 < a |^ n
A2: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume a |^ m > 0 ; ::_thesis: S1[m + 1]
then (a |^ m) * a > 0 * a by A1, XREAL_1:68;
hence S1[m + 1] by NEWTON:6; ::_thesis: verum
end;
A3: S1[ 0 ] by NEWTON:4;
for m being Nat holds S1[m] from NAT_1:sch_2(A3, A2);
hence 0 < a |^ n ; ::_thesis: verum
end;
theorem Th7: :: PREPOWER:7
for a being real number
for n being Nat holds (1 / a) |^ n = 1 / (a |^ n)
proof
let a be real number ; ::_thesis: for n being Nat holds (1 / a) |^ n = 1 / (a |^ n)
let n be Nat; ::_thesis: (1 / a) |^ n = 1 / (a |^ n)
defpred S1[ Nat] means (1 / a) |^ $1 = 1 / (a |^ $1);
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume (1 / a) |^ m = 1 / (a |^ m) ; ::_thesis: S1[m + 1]
hence (1 / a) |^ (m + 1) = (1 / (a |^ m)) * (1 / a) by NEWTON:6
.= (1 * 1) / ((a |^ m) * a) by XCMPLX_1:76
.= 1 / (a |^ (m + 1)) by NEWTON:6 ;
::_thesis: verum
end;
(1 / a) |^ 0 = ((1 / a) GeoSeq) . 0 by Def1
.= 1 / 1 by Th3
.= 1 / ((a GeoSeq) . 0) by Th3
.= 1 / (a |^ 0) by Def1 ;
then A2: S1[ 0 ] ;
for m being Nat holds S1[m] from NAT_1:sch_2(A2, A1);
hence (1 / a) |^ n = 1 / (a |^ n) ; ::_thesis: verum
end;
theorem :: PREPOWER:8
for b, a being real number
for n being Nat holds (b / a) |^ n = (b |^ n) / (a |^ n)
proof
let b, a be real number ; ::_thesis: for n being Nat holds (b / a) |^ n = (b |^ n) / (a |^ n)
let n be Nat; ::_thesis: (b / a) |^ n = (b |^ n) / (a |^ n)
thus (b / a) |^ n = (b * (a ")) |^ n
.= (b |^ n) * ((a ") |^ n) by NEWTON:7
.= (b |^ n) * ((1 / a) |^ n)
.= (b |^ n) * (1 / (a |^ n)) by Th7
.= ((b |^ n) * 1) / (a |^ n)
.= (b |^ n) / (a |^ n) ; ::_thesis: verum
end;
theorem Th9: :: PREPOWER:9
for a, b being real number
for n being Nat st 0 < a & a <= b holds
a |^ n <= b |^ n
proof
let a, b be real number ; ::_thesis: for n being Nat st 0 < a & a <= b holds
a |^ n <= b |^ n
let n be Nat; ::_thesis: ( 0 < a & a <= b implies a |^ n <= b |^ n )
assume that
A1: 0 < a and
A2: a <= b ; ::_thesis: a |^ n <= b |^ n
defpred S1[ Nat] means a |^ $1 <= b |^ $1;
A3: for m1 being Nat st S1[m1] holds
S1[m1 + 1]
proof
let m1 be Nat; ::_thesis: ( S1[m1] implies S1[m1 + 1] )
assume A4: a |^ m1 <= b |^ m1 ; ::_thesis: S1[m1 + 1]
a |^ m1 > 0 by A1, Th6;
then (a |^ m1) * a <= (b |^ m1) * b by A1, A2, A4, XREAL_1:66;
then a |^ (m1 + 1) <= (b |^ m1) * b by NEWTON:6;
hence S1[m1 + 1] by NEWTON:6; ::_thesis: verum
end;
A5: b |^ 0 = (b GeoSeq) . 0 by Def1
.= 1 by Th3 ;
a |^ 0 = (a GeoSeq) . 0 by Def1
.= 1 by Th3 ;
then A6: S1[ 0 ] by A5;
for m1 being Nat holds S1[m1] from NAT_1:sch_2(A6, A3);
hence a |^ n <= b |^ n ; ::_thesis: verum
end;
Lm1: for a, b being real number
for n being Nat st 0 < a & a < b & 1 <= n holds
a |^ n < b |^ n
proof
let a, b be real number ; ::_thesis: for n being Nat st 0 < a & a < b & 1 <= n holds
a |^ n < b |^ n
let n be Nat; ::_thesis: ( 0 < a & a < b & 1 <= n implies a |^ n < b |^ n )
assume that
A1: 0 < a and
A2: a < b and
A3: 1 <= n ; ::_thesis: a |^ n < b |^ n
consider m being Nat such that
A4: n = 1 + m by A3, NAT_1:10;
defpred S1[ Element of NAT ] means a |^ (1 + $1) < b |^ (1 + $1);
A5: for m1 being Element of NAT st S1[m1] holds
S1[m1 + 1]
proof
let m1 be Element of NAT ; ::_thesis: ( S1[m1] implies S1[m1 + 1] )
assume A6: a |^ (1 + m1) < b |^ (1 + m1) ; ::_thesis: S1[m1 + 1]
a |^ (1 + m1) > 0 by A1, Th6;
then (a |^ (1 + m1)) * a < (b |^ (1 + m1)) * b by A1, A2, A6, XREAL_1:97;
then a |^ ((1 + m1) + 1) < (b |^ (1 + m1)) * b by NEWTON:6;
hence S1[m1 + 1] by NEWTON:6; ::_thesis: verum
end;
A7: b |^ (1 + 0) = (b GeoSeq) . (0 + 1) by Def1
.= ((b GeoSeq) . 0) * b by Th3
.= 1 * b by Th3
.= b ;
a |^ (1 + 0) = (a GeoSeq) . (0 + 1) by Def1
.= ((a GeoSeq) . 0) * a by Th3
.= 1 * a by Th3
.= a ;
then A8: S1[ 0 ] by A2, A7;
A9: for m1 being Element of NAT holds S1[m1] from NAT_1:sch_1(A8, A5);
m in NAT by ORDINAL1:def_12;
hence a |^ n < b |^ n by A4, A9; ::_thesis: verum
end;
theorem Th10: :: PREPOWER:10
for a, b being real number
for n being Nat st 0 <= a & a < b & 1 <= n holds
a |^ n < b |^ n
proof
let a, b be real number ; ::_thesis: for n being Nat st 0 <= a & a < b & 1 <= n holds
a |^ n < b |^ n
let n be Nat; ::_thesis: ( 0 <= a & a < b & 1 <= n implies a |^ n < b |^ n )
assume that
A1: 0 <= a and
A2: a < b and
A3: 1 <= n ; ::_thesis: a |^ n < b |^ n
percases ( a > 0 or a = 0 ) by A1;
suppose a > 0 ; ::_thesis: a |^ n < b |^ n
hence a |^ n < b |^ n by A2, A3, Lm1; ::_thesis: verum
end;
supposeA4: a = 0 ; ::_thesis: a |^ n < b |^ n
reconsider k = n, k1 = 1 as Integer ;
reconsider m = k - k1 as Element of NAT by A3, INT_1:5;
a |^ n = a |^ (m + 1)
.= (a |^ m) * (a |^ 1) by NEWTON:8
.= (a |^ m) * ((a GeoSeq) . (0 + 1)) by Def1
.= (a |^ m) * (((a GeoSeq) . 0) * 0) by A4, Th3
.= 0 ;
hence a |^ n < b |^ n by A1, A2, Th6; ::_thesis: verum
end;
end;
end;
theorem Th11: :: PREPOWER:11
for a being real number
for n being Nat st a >= 1 holds
a |^ n >= 1
proof
let a be real number ; ::_thesis: for n being Nat st a >= 1 holds
a |^ n >= 1
let n be Nat; ::_thesis: ( a >= 1 implies a |^ n >= 1 )
assume a >= 1 ; ::_thesis: a |^ n >= 1
then a |^ n >= 1 |^ n by Th9;
hence a |^ n >= 1 by NEWTON:10; ::_thesis: verum
end;
theorem Th12: :: PREPOWER:12
for a being real number
for n being Nat st 1 <= a & 1 <= n holds
a <= a |^ n
proof
let a be real number ; ::_thesis: for n being Nat st 1 <= a & 1 <= n holds
a <= a |^ n
let n be Nat; ::_thesis: ( 1 <= a & 1 <= n implies a <= a |^ n )
assume that
A1: 1 <= a and
A2: 1 <= n ; ::_thesis: a <= a |^ n
consider m being Nat such that
A3: n = m + 1 by A2, NAT_1:6;
defpred S1[ Element of NAT ] means a <= a |^ ($1 + 1);
A4: for m1 being Element of NAT st S1[m1] holds
S1[m1 + 1]
proof
let m1 be Element of NAT ; ::_thesis: ( S1[m1] implies S1[m1 + 1] )
assume a <= a |^ (m1 + 1) ; ::_thesis: S1[m1 + 1]
then a * 1 <= (a |^ (m1 + 1)) * a by A1, XREAL_1:66;
hence S1[m1 + 1] by NEWTON:6; ::_thesis: verum
end;
a <= 1 * a ;
then a <= ((a GeoSeq) . 0) * a by Th3;
then a <= (a |^ 0) * a by Def1;
then A5: S1[ 0 ] by NEWTON:6;
A6: for m1 being Element of NAT holds S1[m1] from NAT_1:sch_1(A5, A4);
m in NAT by ORDINAL1:def_12;
hence a <= a |^ n by A3, A6; ::_thesis: verum
end;
theorem :: PREPOWER:13
for a being real number
for n being Nat st 1 < a & 2 <= n holds
a < a |^ n
proof
let a be real number ; ::_thesis: for n being Nat st 1 < a & 2 <= n holds
a < a |^ n
let n be Nat; ::_thesis: ( 1 < a & 2 <= n implies a < a |^ n )
assume that
A1: 1 < a and
A2: 2 <= n ; ::_thesis: a < a |^ n
consider m being Nat such that
A3: n = 2 + m by A2, NAT_1:10;
defpred S1[ Element of NAT ] means a < a |^ (2 + $1);
A4: a * a > a * 1 by A1, XREAL_1:68;
A5: for m1 being Element of NAT st S1[m1] holds
S1[m1 + 1]
proof
let m1 be Element of NAT ; ::_thesis: ( S1[m1] implies S1[m1 + 1] )
assume a < a |^ (2 + m1) ; ::_thesis: S1[m1 + 1]
then (a |^ (2 + m1)) * a > a * a by A1, XREAL_1:68;
then a |^ ((2 + m1) + 1) > a * a by NEWTON:6;
hence S1[m1 + 1] by A4, XXREAL_0:2; ::_thesis: verum
end;
a |^ (2 + 0) = (a GeoSeq) . (1 + 1) by Def1
.= ((a GeoSeq) . (0 + 1)) * a by Th3
.= (((a GeoSeq) . 0) * a) * a by Th3
.= (1 * a) * a by Th3
.= a * a ;
then A6: S1[ 0 ] by A4;
A7: for m1 being Element of NAT holds S1[m1] from NAT_1:sch_1(A6, A5);
m in NAT by ORDINAL1:def_12;
hence a < a |^ n by A3, A7; ::_thesis: verum
end;
theorem Th14: :: PREPOWER:14
for a being real number
for n being Nat st 0 < a & a <= 1 & 1 <= n holds
a |^ n <= a
proof
let a be real number ; ::_thesis: for n being Nat st 0 < a & a <= 1 & 1 <= n holds
a |^ n <= a
let n be Nat; ::_thesis: ( 0 < a & a <= 1 & 1 <= n implies a |^ n <= a )
assume that
A1: 0 < a and
A2: a <= 1 and
A3: 1 <= n ; ::_thesis: a |^ n <= a
consider m being Nat such that
A4: n = 1 + m by A3, NAT_1:10;
defpred S1[ Element of NAT ] means a |^ (1 + $1) <= a;
A5: a * a <= a * 1 by A1, A2, XREAL_1:64;
A6: for m1 being Element of NAT st S1[m1] holds
S1[m1 + 1]
proof
let m1 be Element of NAT ; ::_thesis: ( S1[m1] implies S1[m1 + 1] )
assume a |^ (1 + m1) <= a ; ::_thesis: S1[m1 + 1]
then (a |^ (1 + m1)) * a <= a * a by A1, XREAL_1:64;
then a |^ (1 + (m1 + 1)) <= a * a by NEWTON:6;
hence S1[m1 + 1] by A5, XXREAL_0:2; ::_thesis: verum
end;
a |^ (1 + 0) = (a GeoSeq) . (0 + 1) by Def1
.= ((a GeoSeq) . 0) * a by Th3
.= 1 * a by Th3
.= a ;
then A7: S1[ 0 ] ;
A8: for m1 being Element of NAT holds S1[m1] from NAT_1:sch_1(A7, A6);
m in NAT by ORDINAL1:def_12;
hence a |^ n <= a by A4, A8; ::_thesis: verum
end;
theorem :: PREPOWER:15
for a being real number
for n being Nat st 0 < a & a < 1 & 2 <= n holds
a |^ n < a
proof
let a be real number ; ::_thesis: for n being Nat st 0 < a & a < 1 & 2 <= n holds
a |^ n < a
let n be Nat; ::_thesis: ( 0 < a & a < 1 & 2 <= n implies a |^ n < a )
assume that
A1: 0 < a and
A2: a < 1 and
A3: 2 <= n ; ::_thesis: a |^ n < a
consider m being Nat such that
A4: n = 2 + m by A3, NAT_1:10;
defpred S1[ Element of NAT ] means a |^ (2 + $1) < a;
A5: a * a < a * 1 by A1, A2, XREAL_1:68;
A6: for m1 being Element of NAT st S1[m1] holds
S1[m1 + 1]
proof
let m1 be Element of NAT ; ::_thesis: ( S1[m1] implies S1[m1 + 1] )
assume a |^ (2 + m1) < a ; ::_thesis: S1[m1 + 1]
then (a |^ (2 + m1)) * a < a * a by A1, XREAL_1:68;
then a |^ ((2 + m1) + 1) < a * a by NEWTON:6;
hence S1[m1 + 1] by A5, XXREAL_0:2; ::_thesis: verum
end;
a |^ (2 + 0) = (a GeoSeq) . (1 + 1) by Def1
.= ((a GeoSeq) . (0 + 1)) * a by Th3
.= (((a GeoSeq) . 0) * a) * a by Th3
.= (1 * a) * a by Th3
.= a * a ;
then A7: S1[ 0 ] by A5;
A8: for m1 being Element of NAT holds S1[m1] from NAT_1:sch_1(A7, A6);
m in NAT by ORDINAL1:def_12;
hence a |^ n < a by A4, A8; ::_thesis: verum
end;
theorem Th16: :: PREPOWER:16
for a being real number
for n being Nat st - 1 < a holds
(1 + a) |^ n >= 1 + (n * a)
proof
let a be real number ; ::_thesis: for n being Nat st - 1 < a holds
(1 + a) |^ n >= 1 + (n * a)
let n be Nat; ::_thesis: ( - 1 < a implies (1 + a) |^ n >= 1 + (n * a) )
defpred S1[ Nat] means (1 + a) |^ $1 >= 1 + ($1 * a);
assume A1: - 1 < a ; ::_thesis: (1 + a) |^ n >= 1 + (n * a)
A2: for m being Nat st S1[m] holds
S1[m + 1]
proof
A3: (- 1) + 1 < 1 + a by A1, XREAL_1:6;
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume (1 + a) |^ m >= 1 + (m * a) ; ::_thesis: S1[m + 1]
then ((1 + a) |^ m) * (1 + a) >= (1 + (m * a)) * (1 + a) by A3, XREAL_1:64;
then A4: (1 + a) |^ (m + 1) >= ((1 + (1 * a)) + (m * a)) + ((m * a) * a) by NEWTON:6;
0 <= a * a by XREAL_1:63;
then (1 + ((m + 1) * a)) + 0 <= (1 + ((m + 1) * a)) + (m * (a * a)) by XREAL_1:7;
hence S1[m + 1] by A4, XXREAL_0:2; ::_thesis: verum
end;
(1 + a) |^ 0 = ((1 + a) GeoSeq) . 0 by Def1
.= 1 by Th3 ;
then A5: S1[ 0 ] ;
for m being Nat holds S1[m] from NAT_1:sch_2(A5, A2);
hence (1 + a) |^ n >= 1 + (n * a) ; ::_thesis: verum
end;
theorem Th17: :: PREPOWER:17
for a being real number
for n being Nat st 0 < a & a < 1 holds
(1 + a) |^ n <= 1 + ((3 |^ n) * a)
proof
let a be real number ; ::_thesis: for n being Nat st 0 < a & a < 1 holds
(1 + a) |^ n <= 1 + ((3 |^ n) * a)
let n be Nat; ::_thesis: ( 0 < a & a < 1 implies (1 + a) |^ n <= 1 + ((3 |^ n) * a) )
assume that
A1: 0 < a and
A2: a < 1 ; ::_thesis: (1 + a) |^ n <= 1 + ((3 |^ n) * a)
A3: 1 + 0 < 1 + a by A1, XREAL_1:6;
defpred S1[ Nat] means (1 + a) |^ $1 <= 1 + ((3 |^ $1) * a);
A4: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume (1 + a) |^ n <= 1 + ((3 |^ n) * a) ; ::_thesis: S1[n + 1]
then A5: ((1 + a) |^ n) * (1 + a) <= (1 + ((3 |^ n) * a)) * (1 + a) by A1, XREAL_1:64;
A6: (1 + ((3 |^ n) * a)) + (((3 |^ n) + (3 |^ n)) * a) = 1 + (((3 |^ n) * (1 + 2)) * a)
.= 1 + ((3 |^ (n + 1)) * a) by NEWTON:6 ;
A7: 1 <= 3 |^ n
proof
percases ( 0 = n or 0 <> n ) ;
supposeA8: 0 = n ; ::_thesis: 1 <= 3 |^ n
n is Element of NAT by ORDINAL1:def_12;
then 3 |^ n = (3 GeoSeq) . n by Def1
.= 1 by A8, Th3 ;
hence 1 <= 3 |^ n ; ::_thesis: verum
end;
suppose 0 <> n ; ::_thesis: 1 <= 3 |^ n
then 0 + 1 <= n by NAT_1:13;
then 1 |^ n < 3 |^ n by Lm1;
hence 1 <= 3 |^ n by NEWTON:10; ::_thesis: verum
end;
end;
end;
then 1 * a <= (3 |^ n) * a by A1, XREAL_1:64;
then A9: 1 + a <= 1 + ((3 |^ n) * a) by XREAL_1:7;
a * a < 1 * a by A1, A2, XREAL_1:68;
then (3 |^ n) * (a * a) < (3 |^ n) * a by A7, XREAL_1:68;
then A10: ((3 |^ n) * a) + ((3 |^ n) * (a * a)) < ((3 |^ n) * a) + ((3 |^ n) * a) by XREAL_1:6;
(1 + ((3 |^ n) * a)) * (1 + a) = (1 + a) + (((3 |^ n) * a) + ((3 |^ n) * (a * a))) ;
then (1 + ((3 |^ n) * a)) * (1 + a) < 1 + ((3 |^ (n + 1)) * a) by A9, A6, A10, XREAL_1:8;
then ((1 + a) |^ n) * (1 + a) <= 1 + ((3 |^ (n + 1)) * a) by A5, XXREAL_0:2;
hence S1[n + 1] by NEWTON:6; ::_thesis: verum
end;
A11: 1 + ((3 |^ 0) * a) = 1 + (((3 GeoSeq) . 0) * a) by Def1
.= 1 + (1 * a) by Th3
.= 1 + a ;
(1 + a) |^ 0 = ((1 + a) GeoSeq) . 0 by Def1
.= 1 by Th3 ;
then A12: S1[ 0 ] by A11, A3;
for n being Nat holds S1[n] from NAT_1:sch_2(A12, A4);
hence (1 + a) |^ n <= 1 + ((3 |^ n) * a) ; ::_thesis: verum
end;
theorem Th18: :: PREPOWER:18
for m being Element of NAT
for s1, s2 being Real_Sequence st s1 is convergent & ( for n being Element of NAT holds s2 . n = (s1 . n) |^ m ) holds
( s2 is convergent & lim s2 = (lim s1) |^ m )
proof
let m be Element of NAT ; ::_thesis: for s1, s2 being Real_Sequence st s1 is convergent & ( for n being Element of NAT holds s2 . n = (s1 . n) |^ m ) holds
( s2 is convergent & lim s2 = (lim s1) |^ m )
let s1, s2 be Real_Sequence; ::_thesis: ( s1 is convergent & ( for n being Element of NAT holds s2 . n = (s1 . n) |^ m ) implies ( s2 is convergent & lim s2 = (lim s1) |^ m ) )
assume that
A1: s1 is convergent and
A2: for n being Element of NAT holds s2 . n = (s1 . n) |^ m ; ::_thesis: ( s2 is convergent & lim s2 = (lim s1) |^ m )
defpred S1[ Element of NAT ] means for s being Real_Sequence st ( for n being Element of NAT holds s . n = (s1 . n) |^ $1 ) holds
( s is convergent & lim s = (lim s1) |^ $1 );
A3: S1[ 0 ]
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (s1 . n) |^ 0 ) implies ( s is convergent & lim s = (lim s1) |^ 0 ) )
assume A4: for n being Element of NAT holds s . n = (s1 . n) |^ 0 ; ::_thesis: ( s is convergent & lim s = (lim s1) |^ 0 )
A5: now__::_thesis:_for_n_being_Nat_holds_s_._n_=_1
let n be Nat; ::_thesis: s . n = 1
n in NAT by ORDINAL1:def_12;
hence s . n = (s1 . n) |^ 0 by A4
.= ((s1 . n) GeoSeq) . 0 by Def1
.= 1 by Th3 ;
::_thesis: verum
end;
then A6: s is constant by VALUED_0:def_18;
hence s is convergent ; ::_thesis: lim s = (lim s1) |^ 0
thus lim s = s . 0 by A6, SEQ_4:26
.= 1 by A5
.= ((lim s1) GeoSeq) . 0 by Th3
.= (lim s1) |^ 0 by Def1 ; ::_thesis: verum
end;
A7: for m1 being Element of NAT st S1[m1] holds
S1[m1 + 1]
proof
let m1 be Element of NAT ; ::_thesis: ( S1[m1] implies S1[m1 + 1] )
assume A8: for s being Real_Sequence st ( for n being Element of NAT holds s . n = (s1 . n) |^ m1 ) holds
( s is convergent & lim s = (lim s1) |^ m1 ) ; ::_thesis: S1[m1 + 1]
deffunc H1( Element of NAT ) -> Element of REAL = (s1 . $1) |^ m1;
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (s1 . n) |^ (m1 + 1) ) implies ( s is convergent & lim s = (lim s1) |^ (m1 + 1) ) )
consider s3 being Real_Sequence such that
A9: for n being Element of NAT holds s3 . n = H1(n) from SEQ_1:sch_1();
assume A10: for n being Element of NAT holds s . n = (s1 . n) |^ (m1 + 1) ; ::_thesis: ( s is convergent & lim s = (lim s1) |^ (m1 + 1) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_s_._n_=_(s3_._n)_*_(s1_._n)
let n be Element of NAT ; ::_thesis: s . n = (s3 . n) * (s1 . n)
thus s . n = (s1 . n) |^ (m1 + 1) by A10
.= ((s1 . n) |^ m1) * (s1 . n) by NEWTON:6
.= (s3 . n) * (s1 . n) by A9 ; ::_thesis: verum
end;
then A11: s = s3 (#) s1 by SEQ_1:8;
A12: s3 is convergent by A8, A9;
hence s is convergent by A1, A11, SEQ_2:14; ::_thesis: lim s = (lim s1) |^ (m1 + 1)
lim s3 = (lim s1) |^ m1 by A8, A9;
hence lim s = ((lim s1) |^ m1) * (lim s1) by A1, A12, A11, SEQ_2:15
.= (lim s1) |^ (m1 + 1) by NEWTON:6 ;
::_thesis: verum
end;
for m1 being Element of NAT holds S1[m1] from NAT_1:sch_1(A3, A7);
hence ( s2 is convergent & lim s2 = (lim s1) |^ m ) by A2; ::_thesis: verum
end;
definition
let n be Nat;
let a be real number ;
assume A1: 1 <= n ;
funcn -Root a -> real number means :Def2: :: PREPOWER:def 2
( it |^ n = a & it > 0 ) if a > 0
it = 0 if a = 0
;
consistency
for b1 being real number st a > 0 & a = 0 holds
( ( b1 |^ n = a & b1 > 0 ) iff b1 = 0 ) ;
existence
( ( a > 0 implies ex b1 being real number st
( b1 |^ n = a & b1 > 0 ) ) & ( a = 0 implies ex b1 being real number st b1 = 0 ) )
proof
now__::_thesis:_(_a_>_0_implies_ex_d_being_Element_of_REAL_st_
(_a_=_d_|^_n_&_d_>_0_)_)
set X = { b where b is Real : ( 0 < b & b |^ n <= a ) } ;
for x being set st x in { b where b is Real : ( 0 < b & b |^ n <= a ) } holds
x in REAL
proof
let x be set ; ::_thesis: ( x in { b where b is Real : ( 0 < b & b |^ n <= a ) } implies x in REAL )
assume x in { b where b is Real : ( 0 < b & b |^ n <= a ) } ; ::_thesis: x in REAL
then ex b being Real st
( x = b & 0 < b & b |^ n <= a ) ;
hence x in REAL ; ::_thesis: verum
end;
then reconsider X = { b where b is Real : ( 0 < b & b |^ n <= a ) } as Subset of REAL by TARSKI:def_3;
reconsider a1 = a as Real by XREAL_0:def_1;
A2: ( 1 <= a implies ex c being real number st c in X )
proof
assume A3: 1 <= a ; ::_thesis: ex c being real number st c in X
consider c being real number such that
A4: c = 1 ;
take c ; ::_thesis: c in X
c |^ n <= a by A3, A4, NEWTON:10;
hence c in X by A4; ::_thesis: verum
end;
A5: ( a < 1 implies ex c being real number st c is UpperBound of X )
proof
consider c being real number such that
A6: c = 1 ;
assume A7: a < 1 ; ::_thesis: ex c being real number st c is UpperBound of X
take c ; ::_thesis: c is UpperBound of X
let b be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not b in X or b <= c )
assume b in X ; ::_thesis: b <= c
then consider d being Real such that
A8: ( d = b & 0 < d & d |^ n <= a ) ;
assume not b <= c ; ::_thesis: contradiction
then 1 |^ n < d |^ n by A1, A6, Lm1, A8;
then 1 < d |^ n by NEWTON:10;
hence contradiction by A7, A8, XXREAL_0:2; ::_thesis: verum
end;
assume A9: a > 0 ; ::_thesis: ex d being Element of REAL st
( a = d |^ n & d > 0 )
( 1 <= a implies ex c being real number st c is UpperBound of X )
proof
assume A10: 1 <= a ; ::_thesis: ex c being real number st c is UpperBound of X
take a ; ::_thesis: a is UpperBound of X
let b be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not b in X or b <= a )
assume b in X ; ::_thesis: b <= a
then consider d being Real such that
A11: ( b = d & 0 < d & d |^ n <= a ) ;
assume a < b ; ::_thesis: contradiction
then a |^ n < d |^ n by A1, A9, Lm1, A11;
then a |^ n < a by A11, XXREAL_0:2;
hence contradiction by A1, A10, Th12; ::_thesis: verum
end;
then A12: X is bounded_above by A5, XXREAL_2:def_10;
take d = upper_bound X; ::_thesis: ( a = d |^ n & d > 0 )
A13: ( a < 1 implies ex c being real number st c in X )
proof
assume A14: a < 1 ; ::_thesis: ex c being real number st c in X
reconsider a = a as Real by XREAL_0:def_1;
take a ; ::_thesis: a in X
a |^ n <= a by A1, A9, A14, Th14;
hence a in X by A9; ::_thesis: verum
end;
A15: 0 < d
proof
consider c being real number such that
A16: c in X by A2, A13;
ex e being Real st
( e = c & 0 < e & e |^ n <= a ) by A16;
hence 0 < d by A12, A16, SEQ_4:def_1; ::_thesis: verum
end;
A17: not a < d |^ n
proof
set b = (d * (1 - (a / (d |^ n)))) / (n + 1);
assume A18: a < d |^ n ; ::_thesis: contradiction
then A19: (1 / (n + 1)) * (d |^ n) > (1 / (n + 1)) * a by XREAL_1:68;
a * ((d |^ n) ") > 0 * a by A9, A18, XREAL_1:68;
then - (- (a / (d |^ n))) > 0 ;
then - (a / (d |^ n)) < 0 ;
then 1 + (- (a / (d |^ n))) < 1 + 0 by XREAL_1:6;
then A20: (1 - (a / (d |^ n))) * ((n + 1) ") < 1 * ((n + 1) ") by XREAL_1:68;
1 < n + 1 by A1, NAT_1:13;
then (n + 1) " < 1 by XREAL_1:212;
then (1 - (a / (d |^ n))) / (n + 1) < 1 by A20, XXREAL_0:2;
then A21: d * ((1 - (a / (d |^ n))) / (n + 1)) < d * 1 by A15, XREAL_1:68;
then ((d * (1 - (a / (d |^ n)))) / (n + 1)) / d < d / d by A15, XREAL_1:74;
then ((d * (1 - (a / (d |^ n)))) / (n + 1)) / d < 1 by A15, XCMPLX_1:60;
then - 1 < - (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d) by XREAL_1:24;
then A22: (1 + (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d))) |^ n >= 1 + (n * (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d))) by Th16;
a / (d |^ n) < (d |^ n) / (d |^ n) by A9, A18, XREAL_1:74;
then 0 + (a / (d |^ n)) < 1 by A9, A18, XCMPLX_1:60;
then 0 < 1 - (a / (d |^ n)) by XREAL_1:20;
then d * 0 < d * (1 - (a / (d |^ n))) by A15, XREAL_1:68;
then 0 / (n + 1) < (d * (1 - (a / (d |^ n)))) / (n + 1) by XREAL_1:74;
then consider c being real number such that
A23: c in X and
A24: d - ((d * (1 - (a / (d |^ n)))) / (n + 1)) < c by A2, A13, A12, SEQ_4:def_1;
0 < d - ((d * (1 - (a / (d |^ n)))) / (n + 1)) by A21, XREAL_1:50;
then A25: (d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) |^ n < c |^ n by A1, A24, Lm1;
(1 + (n * (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d)))) * (d |^ n) = (1 - (n * (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d))) * (d |^ n)
.= (1 - (n * ((d * ((1 - (a / (d |^ n))) / (n + 1))) / d))) * (d |^ n)
.= (1 - (n * ((((1 - (a / (d |^ n))) / (n + 1)) / d) * d))) * (d |^ n)
.= (1 - (n * ((1 - (a / (d |^ n))) / (n + 1)))) * (d |^ n) by A15, XCMPLX_1:87
.= (1 - (((1 - (a / (d |^ n))) * n) / (n + 1))) * (d |^ n)
.= (1 - ((1 - (a / (d |^ n))) * (n / (n + 1)))) * (d |^ n)
.= ((1 - (n / (n + 1))) + ((a / (d |^ n)) * (n / (n + 1)))) * (d |^ n)
.= ((((n + 1) / (n + 1)) - (n / (n + 1))) + ((a / (d |^ n)) * (n / (n + 1)))) * (d |^ n) by XCMPLX_1:60
.= ((((n + 1) - n) / (n + 1)) + ((a / (d |^ n)) * (n / (n + 1)))) * (d |^ n)
.= ((1 / (n + 1)) + (((n / (n + 1)) * a) / (d |^ n))) * (d |^ n)
.= ((1 / (n + 1)) * (d |^ n)) + ((((n / (n + 1)) * a) / (d |^ n)) * (d |^ n))
.= ((1 / (n + 1)) * (d |^ n)) + ((n / (n + 1)) * a) by A9, A18, XCMPLX_1:87 ;
then A26: (1 + (n * (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d)))) * (d |^ n) > ((1 / (n + 1)) * a) + ((n / (n + 1)) * a) by A19, XREAL_1:6;
(d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) |^ n = ((d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) * 1) |^ n
.= ((d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) * ((d ") * d)) |^ n by A15, XCMPLX_0:def_7
.= (((d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) * (d ")) * d) |^ n
.= (((d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) / d) * d) |^ n
.= (((d / d) - (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d)) * d) |^ n
.= ((1 - (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d)) * d) |^ n by A15, XCMPLX_1:60
.= ((1 + (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d))) |^ n) * (d |^ n) by NEWTON:7 ;
then (d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) |^ n >= (1 + (n * (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d)))) * (d |^ n) by A9, A18, A22, XREAL_1:64;
then (d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) |^ n > ((n + 1) / (n + 1)) * a by A26, XXREAL_0:2;
then A27: (d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) |^ n > 1 * a by XCMPLX_1:60;
ex e being Real st
( e = c & 0 < e & e |^ n <= a ) by A23;
hence contradiction by A25, A27, XXREAL_0:2; ::_thesis: verum
end;
not d |^ n < a
proof
set b = min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)));
set c = (1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) * d;
A28: ((1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) * d) |^ n = ((1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) |^ n) * (d |^ n) by NEWTON:7;
A29: 0 < 3 |^ n by Th6;
(3 |^ n) * (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) <= (((a / (d |^ n)) - 1) / (3 |^ n)) * (3 |^ n) by XREAL_1:64, XXREAL_0:17;
then (3 |^ n) * (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) <= (a / (d |^ n)) - 1 by A29, XCMPLX_1:87;
then A30: 1 + ((3 |^ n) * (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) <= a / (d |^ n) by XREAL_1:19;
A31: d |^ n > 0 by A15, Th6;
A32: d |^ n <> 0 by A15, Th6;
assume d |^ n < a ; ::_thesis: contradiction
then (d |^ n) / (d |^ n) < a / (d |^ n) by A31, XREAL_1:74;
then 1 < a / (d |^ n) by A32, XCMPLX_1:60;
then 1 - 1 < (a / (d |^ n)) - 1 by XREAL_1:9;
then ((a / (d |^ n)) - 1) / (3 |^ n) > 0 / (3 |^ n) by A29, XREAL_1:74;
then A33: min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))) > 0 by XXREAL_0:15;
then 1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) > 1 + 0 by XREAL_1:6;
then A34: (1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) * d > 1 * d by A15, XREAL_1:68;
min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))) <= 1 / 2 by XXREAL_0:17;
then min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))) < 1 by XXREAL_0:2;
then (1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) |^ n <= 1 + ((3 |^ n) * (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) by A33, Th17;
then (1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) |^ n <= a / (d |^ n) by A30, XXREAL_0:2;
then ((1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) * d) |^ n <= (a / (d |^ n)) * (d |^ n) by A31, A28, XREAL_1:64;
then A35: ((1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) * d) |^ n <= a by A32, XCMPLX_1:87;
(1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) * d > 0 * d by A15, A33, XREAL_1:68;
then (1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) * d in X by A35;
hence contradiction by A12, A34, SEQ_4:def_1; ::_thesis: verum
end;
hence ( a = d |^ n & d > 0 ) by A15, A17, XXREAL_0:1; ::_thesis: verum
end;
hence ( ( a > 0 implies ex b1 being real number st
( b1 |^ n = a & b1 > 0 ) ) & ( a = 0 implies ex b1 being real number st b1 = 0 ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being real number holds
( ( a > 0 & b1 |^ n = a & b1 > 0 & b2 |^ n = a & b2 > 0 implies b1 = b2 ) & ( a = 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof
now__::_thesis:_for_b,_c_being_real_number_st_b_|^_n_=_a_&_b_>_0_&_c_|^_n_=_a_&_c_>_0_holds_
not_b_<>_c
let b, c be real number ; ::_thesis: ( b |^ n = a & b > 0 & c |^ n = a & c > 0 implies not b <> c )
assume that
A36: b |^ n = a and
A37: b > 0 and
A38: c |^ n = a and
A39: c > 0 and
A40: b <> c ; ::_thesis: contradiction
percases ( b > c or c > b ) by A40, XXREAL_0:1;
suppose b > c ; ::_thesis: contradiction
hence contradiction by A1, A36, A38, A39, Lm1; ::_thesis: verum
end;
suppose c > b ; ::_thesis: contradiction
hence contradiction by A1, A36, A37, A38, Lm1; ::_thesis: verum
end;
end;
end;
hence for b1, b2 being real number holds
( ( a > 0 & b1 |^ n = a & b1 > 0 & b2 |^ n = a & b2 > 0 implies b1 = b2 ) & ( a = 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines -Root PREPOWER:def_2_:_
for n being Nat
for a being real number st 1 <= n holds
for b3 being real number holds
( ( a > 0 implies ( b3 = n -Root a iff ( b3 |^ n = a & b3 > 0 ) ) ) & ( a = 0 implies ( b3 = n -Root a iff b3 = 0 ) ) );
definition
let n be Element of NAT ;
let a be Real;
:: original: -Root
redefine funcn -Root a -> Real;
coherence
n -Root a is Real by XREAL_0:def_1;
end;
Lm2: for a being real number
for n being Nat st a > 0 & n >= 1 holds
( (n -Root a) |^ n = a & n -Root (a |^ n) = a )
proof
let a be real number ; ::_thesis: for n being Nat st a > 0 & n >= 1 holds
( (n -Root a) |^ n = a & n -Root (a |^ n) = a )
let n be Nat; ::_thesis: ( a > 0 & n >= 1 implies ( (n -Root a) |^ n = a & n -Root (a |^ n) = a ) )
assume that
A1: a > 0 and
A2: n >= 1 ; ::_thesis: ( (n -Root a) |^ n = a & n -Root (a |^ n) = a )
thus (n -Root a) |^ n = a by A1, A2, Def2; ::_thesis: n -Root (a |^ n) = a
assume A3: n -Root (a |^ n) <> a ; ::_thesis: contradiction
percases ( n -Root (a |^ n) > a or n -Root (a |^ n) < a ) by A3, XXREAL_0:1;
supposeA4: n -Root (a |^ n) > a ; ::_thesis: contradiction
a |^ n > 0 by A1, Th6;
hence contradiction by A1, A2, A4, Def2; ::_thesis: verum
end;
supposeA5: n -Root (a |^ n) < a ; ::_thesis: contradiction
a |^ n > 0 by A1, Th6;
hence contradiction by A1, A2, A5, Def2; ::_thesis: verum
end;
end;
end;
theorem Th19: :: PREPOWER:19
for a being real number
for n being Nat st a >= 0 & n >= 1 holds
( (n -Root a) |^ n = a & n -Root (a |^ n) = a )
proof
let a be real number ; ::_thesis: for n being Nat st a >= 0 & n >= 1 holds
( (n -Root a) |^ n = a & n -Root (a |^ n) = a )
let n be Nat; ::_thesis: ( a >= 0 & n >= 1 implies ( (n -Root a) |^ n = a & n -Root (a |^ n) = a ) )
assume that
A1: a >= 0 and
A2: n >= 1 ; ::_thesis: ( (n -Root a) |^ n = a & n -Root (a |^ n) = a )
percases ( a > 0 or a = 0 ) by A1;
suppose a > 0 ; ::_thesis: ( (n -Root a) |^ n = a & n -Root (a |^ n) = a )
hence ( (n -Root a) |^ n = a & n -Root (a |^ n) = a ) by A2, Lm2; ::_thesis: verum
end;
supposeA3: a = 0 ; ::_thesis: ( (n -Root a) |^ n = a & n -Root (a |^ n) = a )
reconsider k = n, k1 = 1 as Integer ;
reconsider m = k - k1 as Element of NAT by A2, INT_1:5;
A4: 0 |^ n = 0 |^ (m + 1)
.= (0 |^ m) * (0 |^ 1) by NEWTON:8
.= (0 |^ m) * ((0 GeoSeq) . (0 + 1)) by Def1
.= (0 |^ m) * (((0 GeoSeq) . 0) * 0) by Th3
.= 0 ;
hence (n -Root a) |^ n = a by A2, A3, Def2; ::_thesis: n -Root (a |^ n) = a
thus n -Root (a |^ n) = a by A2, A3, A4, Def2; ::_thesis: verum
end;
end;
end;
theorem Th20: :: PREPOWER:20
for n being Element of NAT st n >= 1 holds
n -Root 1 = 1
proof
let n be Element of NAT ; ::_thesis: ( n >= 1 implies n -Root 1 = 1 )
A1: 1 |^ n = 1 by NEWTON:10;
assume n >= 1 ; ::_thesis: n -Root 1 = 1
hence n -Root 1 = 1 by A1, Def2; ::_thesis: verum
end;
theorem Th21: :: PREPOWER:21
for a being real number st a >= 0 holds
1 -Root a = a
proof
let a be real number ; ::_thesis: ( a >= 0 implies 1 -Root a = a )
assume A1: a >= 0 ; ::_thesis: 1 -Root a = a
a |^ 1 = (a GeoSeq) . (0 + 1) by Def1
.= ((a GeoSeq) . 0) * a by Th3
.= 1 * a by Th3
.= a ;
hence 1 -Root a = a by A1, Th19; ::_thesis: verum
end;
theorem Th22: :: PREPOWER:22
for a, b being real number
for n being Element of NAT st a >= 0 & b >= 0 & n >= 1 holds
n -Root (a * b) = (n -Root a) * (n -Root b)
proof
let a, b be real number ; ::_thesis: for n being Element of NAT st a >= 0 & b >= 0 & n >= 1 holds
n -Root (a * b) = (n -Root a) * (n -Root b)
let n be Element of NAT ; ::_thesis: ( a >= 0 & b >= 0 & n >= 1 implies n -Root (a * b) = (n -Root a) * (n -Root b) )
assume that
A1: a >= 0 and
A2: b >= 0 and
A3: n >= 1 and
A4: n -Root (a * b) <> (n -Root a) * (n -Root b) ; ::_thesis: contradiction
A5: ((n -Root a) * (n -Root b)) |^ n = ((n -Root a) |^ n) * ((n -Root b) |^ n) by NEWTON:7
.= a * ((n -Root b) |^ n) by A1, A3, Th19
.= a * b by A2, A3, Th19 ;
percases ( ( a > 0 & b > 0 ) or ( a = 0 & b > 0 ) or ( a > 0 & b = 0 ) or ( a = 0 & b = 0 ) ) by A1, A2;
supposeA6: ( a > 0 & b > 0 ) ; ::_thesis: contradiction
then A7: n -Root b > 0 by A3, Def2;
A8: n -Root a > 0 by A3, A6, Def2;
a * b > 0 by A6, XREAL_1:129;
then A9: n -Root (a * b) > 0 by A3, Def2;
percases ( n -Root (a * b) < (n -Root a) * (n -Root b) or n -Root (a * b) > (n -Root a) * (n -Root b) ) by A4, XXREAL_0:1;
suppose n -Root (a * b) < (n -Root a) * (n -Root b) ; ::_thesis: contradiction
hence contradiction by A3, A5, A9, Th19; ::_thesis: verum
end;
suppose n -Root (a * b) > (n -Root a) * (n -Root b) ; ::_thesis: contradiction
hence contradiction by A3, A5, A8, A7, Th19; ::_thesis: verum
end;
end;
end;
supposeA10: ( a = 0 & b > 0 ) ; ::_thesis: contradiction
then n -Root (a * b) = 0 by A3, Def2;
hence contradiction by A4, A10; ::_thesis: verum
end;
supposeA11: ( a > 0 & b = 0 ) ; ::_thesis: contradiction
then n -Root (a * b) = 0 by A3, Def2;
hence contradiction by A4, A11; ::_thesis: verum
end;
supposeA12: ( a = 0 & b = 0 ) ; ::_thesis: contradiction
then n -Root (a * b) = 0 by A3, Def2;
hence contradiction by A4, A12; ::_thesis: verum
end;
end;
end;
theorem Th23: :: PREPOWER:23
for a being real number
for n being Element of NAT st a > 0 & n >= 1 holds
n -Root (1 / a) = 1 / (n -Root a)
proof
let a be real number ; ::_thesis: for n being Element of NAT st a > 0 & n >= 1 holds
n -Root (1 / a) = 1 / (n -Root a)
let n be Element of NAT ; ::_thesis: ( a > 0 & n >= 1 implies n -Root (1 / a) = 1 / (n -Root a) )
assume that
A1: a > 0 and
A2: n >= 1 and
A3: n -Root (1 / a) <> 1 / (n -Root a) ; ::_thesis: contradiction
A4: n -Root a > 0 by A1, A2, Def2;
A5: (1 / (n -Root a)) |^ n = 1 / ((n -Root a) |^ n) by Th7
.= 1 / a by A1, A2, Lm2 ;
A6: n -Root (1 / a) > 0 by A1, A2, Def2;
percases ( n -Root (1 / a) > 1 / (n -Root a) or n -Root (1 / a) < 1 / (n -Root a) ) by A3, XXREAL_0:1;
suppose n -Root (1 / a) > 1 / (n -Root a) ; ::_thesis: contradiction
hence contradiction by A2, A4, A5, Lm2; ::_thesis: verum
end;
suppose n -Root (1 / a) < 1 / (n -Root a) ; ::_thesis: contradiction
hence contradiction by A2, A5, A6, Lm2; ::_thesis: verum
end;
end;
end;
theorem :: PREPOWER:24
for a, b being real number
for n being Element of NAT st a >= 0 & b > 0 & n >= 1 holds
n -Root (a / b) = (n -Root a) / (n -Root b)
proof
let a, b be real number ; ::_thesis: for n being Element of NAT st a >= 0 & b > 0 & n >= 1 holds
n -Root (a / b) = (n -Root a) / (n -Root b)
let n be Element of NAT ; ::_thesis: ( a >= 0 & b > 0 & n >= 1 implies n -Root (a / b) = (n -Root a) / (n -Root b) )
assume that
A1: a >= 0 and
A2: b > 0 and
A3: n >= 1 ; ::_thesis: n -Root (a / b) = (n -Root a) / (n -Root b)
thus n -Root (a / b) = n -Root (a * (b "))
.= (n -Root a) * (n -Root (b ")) by A1, A2, A3, Th22
.= (n -Root a) * (n -Root (1 / b))
.= (n -Root a) * (1 / (n -Root b)) by A2, A3, Th23
.= ((n -Root a) * 1) / (n -Root b)
.= (n -Root a) / (n -Root b) ; ::_thesis: verum
end;
theorem Th25: :: PREPOWER:25
for a being real number
for n, m being Element of NAT st a >= 0 & n >= 1 & m >= 1 holds
n -Root (m -Root a) = (n * m) -Root a
proof
let a be real number ; ::_thesis: for n, m being Element of NAT st a >= 0 & n >= 1 & m >= 1 holds
n -Root (m -Root a) = (n * m) -Root a
let n, m be Element of NAT ; ::_thesis: ( a >= 0 & n >= 1 & m >= 1 implies n -Root (m -Root a) = (n * m) -Root a )
assume that
A1: a >= 0 and
A2: n >= 1 and
A3: m >= 1 and
A4: n -Root (m -Root a) <> (n * m) -Root a ; ::_thesis: contradiction
percases ( a > 0 or a = 0 ) by A1;
supposeA5: a > 0 ; ::_thesis: contradiction
then A6: m -Root a > 0 by A3, Def2;
then A7: n -Root (m -Root a) > 0 by A2, Def2;
A8: (n -Root (m -Root a)) |^ (n * m) = ((n -Root (m -Root a)) |^ n) |^ m by NEWTON:9
.= (m -Root a) |^ m by A2, A6, Lm2
.= a by A1, A3, Th19 ;
A9: n * m >= 1 by A2, A3, XREAL_1:159;
then A10: (n * m) -Root a > 0 by A5, Def2;
percases ( n -Root (m -Root a) < (n * m) -Root a or (n * m) -Root a < n -Root (m -Root a) ) by A4, XXREAL_0:1;
suppose n -Root (m -Root a) < (n * m) -Root a ; ::_thesis: contradiction
hence contradiction by A5, A8, A9, A7, Def2; ::_thesis: verum
end;
suppose (n * m) -Root a < n -Root (m -Root a) ; ::_thesis: contradiction
hence contradiction by A5, A8, A9, A10, Def2; ::_thesis: verum
end;
end;
end;
supposeA11: a = 0 ; ::_thesis: contradiction
n * m >= 1 by A2, A3, XREAL_1:159;
then A12: (n * m) -Root a = 0 by A11, Def2;
m -Root a = 0 by A3, A11, Def2;
hence contradiction by A2, A4, A12, Def2; ::_thesis: verum
end;
end;
end;
theorem Th26: :: PREPOWER:26
for a being real number
for n, m being Element of NAT st a >= 0 & n >= 1 & m >= 1 holds
(n -Root a) * (m -Root a) = (n * m) -Root (a |^ (n + m))
proof
let a be real number ; ::_thesis: for n, m being Element of NAT st a >= 0 & n >= 1 & m >= 1 holds
(n -Root a) * (m -Root a) = (n * m) -Root (a |^ (n + m))
let n, m be Element of NAT ; ::_thesis: ( a >= 0 & n >= 1 & m >= 1 implies (n -Root a) * (m -Root a) = (n * m) -Root (a |^ (n + m)) )
assume that
A1: a >= 0 and
A2: n >= 1 and
A3: m >= 1 and
A4: (n -Root a) * (m -Root a) <> (n * m) -Root (a |^ (n + m)) ; ::_thesis: contradiction
A5: ((n -Root a) * (m -Root a)) |^ (n * m) = ((n -Root a) |^ (n * m)) * ((m -Root a) |^ (n * m)) by NEWTON:7
.= (((n -Root a) |^ n) |^ m) * ((m -Root a) |^ (n * m)) by NEWTON:9
.= (a |^ m) * ((m -Root a) |^ (m * n)) by A1, A2, Th19
.= (a |^ m) * (((m -Root a) |^ m) |^ n) by NEWTON:9
.= (a |^ m) * (a |^ n) by A1, A3, Th19
.= a |^ (n + m) by NEWTON:8 ;
A6: n * m >= 1 by A2, A3, XREAL_1:159;
percases ( a > 0 or a = 0 ) by A1;
supposeA7: a > 0 ; ::_thesis: contradiction
then A8: m -Root a > 0 by A3, Def2;
n -Root a > 0 by A2, A7, Def2;
then A9: (n -Root a) * (m -Root a) > 0 by A8, XREAL_1:129;
A10: a |^ (n + m) > 0 by A7, Th6;
then A11: (n * m) -Root (a |^ (n + m)) > 0 by A6, Def2;
percases ( (n -Root a) * (m -Root a) < (n * m) -Root (a |^ (n + m)) or (n -Root a) * (m -Root a) > (n * m) -Root (a |^ (n + m)) ) by A4, XXREAL_0:1;
suppose (n -Root a) * (m -Root a) < (n * m) -Root (a |^ (n + m)) ; ::_thesis: contradiction
hence contradiction by A5, A6, A10, A9, Def2; ::_thesis: verum
end;
suppose (n -Root a) * (m -Root a) > (n * m) -Root (a |^ (n + m)) ; ::_thesis: contradiction
hence contradiction by A5, A6, A10, A11, Def2; ::_thesis: verum
end;
end;
end;
supposeA12: a = 0 ; ::_thesis: contradiction
reconsider k = n, k1 = 1 as Integer ;
reconsider m1 = k - k1 as Element of NAT by A2, INT_1:5;
A13: a |^ (n + m) = a |^ ((m1 + m) + 1)
.= (a |^ (m1 + m)) * a by NEWTON:6
.= 0 by A12 ;
n -Root a = 0 by A2, A12, Def2;
hence contradiction by A4, A6, A13, Def2; ::_thesis: verum
end;
end;
end;
theorem Th27: :: PREPOWER:27
for a, b being real number
for n being Element of NAT st 0 <= a & a <= b & n >= 1 holds
n -Root a <= n -Root b
proof
let a, b be real number ; ::_thesis: for n being Element of NAT st 0 <= a & a <= b & n >= 1 holds
n -Root a <= n -Root b
let n be Element of NAT ; ::_thesis: ( 0 <= a & a <= b & n >= 1 implies n -Root a <= n -Root b )
assume that
A1: a >= 0 and
A2: a <= b and
A3: n >= 1 and
A4: n -Root a > n -Root b ; ::_thesis: contradiction
A5: now__::_thesis:_n_-Root_b_>=_0
percases ( b > 0 or b = 0 ) by A1, A2;
suppose b > 0 ; ::_thesis: n -Root b >= 0
hence n -Root b >= 0 by A3, Def2; ::_thesis: verum
end;
suppose b = 0 ; ::_thesis: n -Root b >= 0
hence n -Root b >= 0 by A3, Def2; ::_thesis: verum
end;
end;
end;
(n -Root a) |^ n = a by A1, A3, Th19;
then (n -Root a) |^ n <= (n -Root b) |^ n by A1, A2, A3, Th19;
hence contradiction by A3, A4, A5, Th10; ::_thesis: verum
end;
theorem Th28: :: PREPOWER:28
for a, b being real number
for n being Element of NAT st a >= 0 & a < b & n >= 1 holds
n -Root a < n -Root b
proof
let a, b be real number ; ::_thesis: for n being Element of NAT st a >= 0 & a < b & n >= 1 holds
n -Root a < n -Root b
let n be Element of NAT ; ::_thesis: ( a >= 0 & a < b & n >= 1 implies n -Root a < n -Root b )
assume that
A1: a >= 0 and
A2: a < b and
A3: n >= 1 and
A4: n -Root a >= n -Root b ; ::_thesis: contradiction
(n -Root a) |^ n = a by A1, A3, Th19;
then A5: (n -Root a) |^ n < (n -Root b) |^ n by A1, A2, A3, Lm2;
n -Root b > 0 by A1, A2, A3, Def2;
hence contradiction by A4, A5, Th9; ::_thesis: verum
end;
theorem Th29: :: PREPOWER:29
for a being real number
for n being Element of NAT st a >= 1 & n >= 1 holds
( n -Root a >= 1 & a >= n -Root a )
proof
let a be real number ; ::_thesis: for n being Element of NAT st a >= 1 & n >= 1 holds
( n -Root a >= 1 & a >= n -Root a )
let n be Element of NAT ; ::_thesis: ( a >= 1 & n >= 1 implies ( n -Root a >= 1 & a >= n -Root a ) )
assume that
A1: a >= 1 and
A2: n >= 1 ; ::_thesis: ( n -Root a >= 1 & a >= n -Root a )
n -Root a >= n -Root 1 by A1, A2, Th27;
hence n -Root a >= 1 by A2, Th20; ::_thesis: a >= n -Root a
n -Root a <= n -Root (a |^ n) by A1, A2, Th12, Th27;
hence a >= n -Root a by A1, A2, Lm2; ::_thesis: verum
end;
theorem Th30: :: PREPOWER:30
for a being real number
for n being Element of NAT st 0 <= a & a < 1 & n >= 1 holds
( a <= n -Root a & n -Root a < 1 )
proof
let a be real number ; ::_thesis: for n being Element of NAT st 0 <= a & a < 1 & n >= 1 holds
( a <= n -Root a & n -Root a < 1 )
let n be Element of NAT ; ::_thesis: ( 0 <= a & a < 1 & n >= 1 implies ( a <= n -Root a & n -Root a < 1 ) )
assume that
A1: 0 <= a and
A2: a < 1 and
A3: n >= 1 ; ::_thesis: ( a <= n -Root a & n -Root a < 1 )
A4: now__::_thesis:_a_|^_n_>=_0
percases ( a > 0 or a = 0 ) by A1;
suppose a > 0 ; ::_thesis: a |^ n >= 0
hence a |^ n >= 0 by Th6; ::_thesis: verum
end;
suppose a = 0 ; ::_thesis: a |^ n >= 0
hence a |^ n >= 0 ; ::_thesis: verum
end;
end;
end;
now__::_thesis:_a_|^_n_<=_a
percases ( a > 0 or a = 0 ) by A1;
suppose a > 0 ; ::_thesis: a |^ n <= a
hence a |^ n <= a by A2, A3, Th14; ::_thesis: verum
end;
suppose a = 0 ; ::_thesis: a |^ n <= a
hence a |^ n <= a by A3, NEWTON:11; ::_thesis: verum
end;
end;
end;
then n -Root (a |^ n) <= n -Root a by A3, A4, Th27;
hence a <= n -Root a by A1, A3, Th19; ::_thesis: n -Root a < 1
n -Root a < n -Root 1 by A1, A2, A3, Th28;
hence n -Root a < 1 by A3, Th20; ::_thesis: verum
end;
theorem Th31: :: PREPOWER:31
for a being real number
for n being Element of NAT st a > 0 & n >= 1 holds
(n -Root a) - 1 <= (a - 1) / n
proof
let a be real number ; ::_thesis: for n being Element of NAT st a > 0 & n >= 1 holds
(n -Root a) - 1 <= (a - 1) / n
let n be Element of NAT ; ::_thesis: ( a > 0 & n >= 1 implies (n -Root a) - 1 <= (a - 1) / n )
assume that
A1: a > 0 and
A2: n >= 1 ; ::_thesis: (n -Root a) - 1 <= (a - 1) / n
n -Root a > 0 by A1, A2, Def2;
then (n -Root a) - 1 > 0 - 1 by XREAL_1:9;
then (1 + ((n -Root a) - 1)) |^ n >= 1 + (n * ((n -Root a) - 1)) by Th16;
then a >= 1 + (n * ((n -Root a) - 1)) by A1, A2, Lm2;
then a - 1 >= n * ((n -Root a) - 1) by XREAL_1:19;
then (a - 1) / n >= (n * ((n -Root a) - 1)) / n by XREAL_1:72;
hence (n -Root a) - 1 <= (a - 1) / n by A2, XCMPLX_1:89; ::_thesis: verum
end;
theorem :: PREPOWER:32
for a being real number st a >= 0 holds
2 -Root a = sqrt a
proof
let a be real number ; ::_thesis: ( a >= 0 implies 2 -Root a = sqrt a )
assume that
A1: a >= 0 and
A2: 2 -Root a <> sqrt a ; ::_thesis: contradiction
A3: sqrt a >= 0 by A1, SQUARE_1:def_2;
(sqrt a) |^ 2 = (sqrt a) ^2 by NEWTON:81
.= a by A1, SQUARE_1:def_2 ;
hence contradiction by A2, A3, Th19; ::_thesis: verum
end;
Lm3: for s being Real_Sequence
for a being real number st a >= 1 & ( for n being Element of NAT st n >= 1 holds
s . n = n -Root a ) holds
( s is convergent & lim s = 1 )
proof
reconsider s2 = NAT --> 1 as Real_Sequence by FUNCOP_1:45;
let s be Real_Sequence; ::_thesis: for a being real number st a >= 1 & ( for n being Element of NAT st n >= 1 holds
s . n = n -Root a ) holds
( s is convergent & lim s = 1 )
let a be real number ; ::_thesis: ( a >= 1 & ( for n being Element of NAT st n >= 1 holds
s . n = n -Root a ) implies ( s is convergent & lim s = 1 ) )
assume A1: a >= 1 ; ::_thesis: ( ex n being Element of NAT st
( n >= 1 & not s . n = n -Root a ) or ( s is convergent & lim s = 1 ) )
deffunc H1( Element of NAT ) -> Element of REAL = (a - 1) / ($1 + 1);
consider s1 being Real_Sequence such that
A2: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
set s3 = s2 + s1;
A3: s1 is convergent by A2, SEQ_4:31;
then A4: s2 + s1 is convergent by SEQ_2:5;
assume A5: for n being Element of NAT st n >= 1 holds
s . n = n -Root a ; ::_thesis: ( s is convergent & lim s = 1 )
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_s2_._n_<=_(s_^\_1)_._n_&_(s_^\_1)_._n_<=_(s2_+_s1)_._n_)
let n be Element of NAT ; ::_thesis: ( s2 . n <= (s ^\ 1) . n & (s ^\ 1) . n <= (s2 + s1) . n )
A7: n + 1 >= 0 + 1 by XREAL_1:6;
set b = ((s ^\ 1) . n) - 1;
A8: (s ^\ 1) . n = s . (n + 1) by NAT_1:def_3
.= (n + 1) -Root a by A5, A7 ;
then A9: (s ^\ 1) . n >= 1 by A1, A7, Th29;
then ((s ^\ 1) . n) - 1 >= 0 by XREAL_1:48;
then A10: - 1 < ((s ^\ 1) . n) - 1 by XXREAL_0:2;
a = (1 + (((s ^\ 1) . n) - 1)) |^ (n + 1) by A1, A7, A8, Lm2;
then a >= 1 + ((n + 1) * (((s ^\ 1) . n) - 1)) by A10, Th16;
then a - 1 >= (1 + ((n + 1) * (((s ^\ 1) . n) - 1))) - 1 by XREAL_1:9;
then (a - 1) * ((n + 1) ") >= ((n + 1) ") * ((n + 1) * (((s ^\ 1) . n) - 1)) by XREAL_1:64;
then (a - 1) * ((n + 1) ") >= (((n + 1) ") * (n + 1)) * (((s ^\ 1) . n) - 1) ;
then (a - 1) * ((n + 1) ") >= 1 * (((s ^\ 1) . n) - 1) by XCMPLX_0:def_7;
then ((a - 1) / (n + 1)) + 1 >= (((s ^\ 1) . n) - 1) + 1 by XREAL_1:6;
then (s2 . n) + ((a - 1) / (n + 1)) >= (s ^\ 1) . n by FUNCOP_1:7;
then (s2 . n) + (s1 . n) >= (s ^\ 1) . n by A2;
hence ( s2 . n <= (s ^\ 1) . n & (s ^\ 1) . n <= (s2 + s1) . n ) by A9, FUNCOP_1:7, SEQ_1:7; ::_thesis: verum
end;
lim s1 = 0 by A2, SEQ_4:31;
then A11: lim (s2 + s1) = (s2 . 0) + 0 by A3, SEQ_4:42
.= 1 by FUNCOP_1:7 ;
A12: lim s2 = s2 . 0 by SEQ_4:26
.= 1 by FUNCOP_1:7 ;
then A13: s ^\ 1 is convergent by A4, A11, A6, SEQ_2:19;
hence s is convergent by SEQ_4:21; ::_thesis: lim s = 1
lim (s ^\ 1) = 1 by A4, A11, A12, A6, SEQ_2:20;
hence lim s = 1 by A13, SEQ_4:22; ::_thesis: verum
end;
theorem :: PREPOWER:33
for a being real number
for s being Real_Sequence st a > 0 & ( for n being Element of NAT st n >= 1 holds
s . n = n -Root a ) holds
( s is convergent & lim s = 1 )
proof
let a be real number ; ::_thesis: for s being Real_Sequence st a > 0 & ( for n being Element of NAT st n >= 1 holds
s . n = n -Root a ) holds
( s is convergent & lim s = 1 )
let s be Real_Sequence; ::_thesis: ( a > 0 & ( for n being Element of NAT st n >= 1 holds
s . n = n -Root a ) implies ( s is convergent & lim s = 1 ) )
assume A1: a > 0 ; ::_thesis: ( ex n being Element of NAT st
( n >= 1 & not s . n = n -Root a ) or ( s is convergent & lim s = 1 ) )
assume A2: for n being Element of NAT st n >= 1 holds
s . n = n -Root a ; ::_thesis: ( s is convergent & lim s = 1 )
percases ( a >= 1 or a < 1 ) ;
suppose a >= 1 ; ::_thesis: ( s is convergent & lim s = 1 )
hence ( s is convergent & lim s = 1 ) by A2, Lm3; ::_thesis: verum
end;
supposeA3: a < 1 ; ::_thesis: ( s is convergent & lim s = 1 )
then a / a < 1 / a by A1, XREAL_1:74;
then A4: 1 <= 1 / a by A1, XCMPLX_1:60;
deffunc H1( Element of NAT ) -> Real = $1 -Root (1 / a);
consider s1 being Real_Sequence such that
A5: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
A6: for n being Element of NAT st n >= 1 holds
s1 . n = n -Root (1 / a) by A5;
then A7: lim s1 = 1 by A4, Lm3;
A8: s1 is convergent by A4, A6, Lm3;
A9: now__::_thesis:_for_b_being_real_number_st_b_>_0_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((s_._m)_-_1)_<_b
let b be real number ; ::_thesis: ( b > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - 1) < b )
assume b > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - 1) < b
then consider m1 being Element of NAT such that
A10: for m being Element of NAT st m1 <= m holds
abs ((s1 . m) - 1) < b by A8, A7, SEQ_2:def_7;
take n = m1 + 1; ::_thesis: for m being Element of NAT st n <= m holds
abs ((s . m) - 1) < b
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((s . m) - 1) < b )
assume A11: n <= m ; ::_thesis: abs ((s . m) - 1) < b
A12: n >= 0 + 1 by XREAL_1:6;
then A13: 1 <= m by A11, XXREAL_0:2;
then A14: m -Root a < 1 by A1, A3, Th30;
A15: m -Root a <> 0 by A1, A13, Def2;
then A16: abs ((1 / (m -Root a)) - 1) = abs ((1 / (m -Root a)) - ((m -Root a) / (m -Root a))) by XCMPLX_1:60
.= abs ((1 - (m -Root a)) / (m -Root a))
.= abs ((1 - (m -Root a)) * ((m -Root a) "))
.= (abs (1 - (m -Root a))) * (abs ((m -Root a) ")) by COMPLEX1:65 ;
0 < m -Root a by A1, A3, A13, Th30;
then (m -Root a) * ((m -Root a) ") < 1 * ((m -Root a) ") by A14, XREAL_1:68;
then 1 < (m -Root a) " by A15, XCMPLX_0:def_7;
then A17: 1 < abs ((m -Root a) ") by ABSVALUE:def_1;
0 <> 1 - (m -Root a) by A1, A3, A13, Th30;
then abs (1 - (m -Root a)) > 0 by COMPLEX1:47;
then A18: 1 * (abs (1 - (m -Root a))) < (abs (1 - (m -Root a))) * (abs ((m -Root a) ")) by A17, XREAL_1:68;
m1 <= n by XREAL_1:29;
then m1 <= m by A11, XXREAL_0:2;
then abs ((s1 . m) - 1) < b by A10;
then abs ((m -Root (1 / a)) - 1) < b by A5;
then abs ((1 / (m -Root a)) - 1) < b by A1, A13, Th23;
then abs (- ((m -Root a) - 1)) < b by A16, A18, XXREAL_0:2;
then abs ((m -Root a) - 1) < b by COMPLEX1:52;
hence abs ((s . m) - 1) < b by A2, A12, A11, XXREAL_0:2; ::_thesis: verum
end;
hence s is convergent by SEQ_2:def_6; ::_thesis: lim s = 1
hence lim s = 1 by A9, SEQ_2:def_7; ::_thesis: verum
end;
end;
end;
definition
let a be real number ;
let k be Integer;
funca #Z k -> set equals :Def3: :: PREPOWER:def 3
a |^ (abs k) if k >= 0
(a |^ (abs k)) " if k < 0
;
consistency
for b1 being set st k >= 0 & k < 0 holds
( b1 = a |^ (abs k) iff b1 = (a |^ (abs k)) " ) ;
coherence
( ( k >= 0 implies a |^ (abs k) is set ) & ( k < 0 implies (a |^ (abs k)) " is set ) ) ;
end;
:: deftheorem Def3 defines #Z PREPOWER:def_3_:_
for a being real number
for k being Integer holds
( ( k >= 0 implies a #Z k = a |^ (abs k) ) & ( k < 0 implies a #Z k = (a |^ (abs k)) " ) );
registration
let a be real number ;
let k be Integer;
clustera #Z k -> real ;
coherence
a #Z k is real
proof
( a #Z k = a |^ (abs k) or a #Z k = (a |^ (abs k)) " ) by Def3;
hence a #Z k is real ; ::_thesis: verum
end;
end;
definition
let a be Real;
let k be Integer;
:: original: #Z
redefine funca #Z k -> Real;
coherence
a #Z k is Real by XREAL_0:def_1;
end;
theorem Th34: :: PREPOWER:34
for a being real number holds a #Z 0 = 1
proof
let a be real number ; ::_thesis: a #Z 0 = 1
thus a #Z 0 = a |^ (abs 0) by Def3
.= a |^ 0 by ABSVALUE:2
.= (a GeoSeq) . 0 by Def1
.= 1 by Th3 ; ::_thesis: verum
end;
theorem Th35: :: PREPOWER:35
for a being real number holds a #Z 1 = a
proof
let a be real number ; ::_thesis: a #Z 1 = a
thus a #Z 1 = a |^ (abs 1) by Def3
.= a |^ (0 + 1) by ABSVALUE:def_1
.= (a GeoSeq) . (0 + 1) by Def1
.= ((a GeoSeq) . 0) * a by Th3
.= 1 * a by Th3
.= a ; ::_thesis: verum
end;
theorem Th36: :: PREPOWER:36
for a being real number
for n being Nat holds a #Z n = a |^ n
proof
let a be real number ; ::_thesis: for n being Nat holds a #Z n = a |^ n
let n be Nat; ::_thesis: a #Z n = a |^ n
thus a #Z n = a |^ (abs n) by Def3
.= a |^ n by ABSVALUE:def_1 ; ::_thesis: verum
end;
Lm4: 1 " = 1
;
theorem Th37: :: PREPOWER:37
for k being Integer holds 1 #Z k = 1
proof
let k be Integer; ::_thesis: 1 #Z k = 1
percases ( k >= 0 or k < 0 ) ;
suppose k >= 0 ; ::_thesis: 1 #Z k = 1
hence 1 #Z k = 1 |^ (abs k) by Def3
.= 1 by NEWTON:10 ;
::_thesis: verum
end;
suppose k < 0 ; ::_thesis: 1 #Z k = 1
then 1 #Z k = (1 |^ (abs k)) " by Def3;
hence 1 #Z k = 1 by Lm4, NEWTON:10; ::_thesis: verum
end;
end;
end;
theorem :: PREPOWER:38
for a being real number
for k being Integer st a <> 0 holds
a #Z k <> 0
proof
let a be real number ; ::_thesis: for k being Integer st a <> 0 holds
a #Z k <> 0
let k be Integer; ::_thesis: ( a <> 0 implies a #Z k <> 0 )
assume A1: a <> 0 ; ::_thesis: a #Z k <> 0
percases ( k >= 0 or k < 0 ) ;
suppose k >= 0 ; ::_thesis: a #Z k <> 0
then a #Z k = a |^ (abs k) by Def3;
hence a #Z k <> 0 by A1, Th5; ::_thesis: verum
end;
suppose k < 0 ; ::_thesis: a #Z k <> 0
then a #Z k = (a |^ (abs k)) " by Def3;
hence a #Z k <> 0 by A1, Th5, XCMPLX_1:202; ::_thesis: verum
end;
end;
end;
theorem Th39: :: PREPOWER:39
for a being real number
for k being Integer st a > 0 holds
a #Z k > 0
proof
let a be real number ; ::_thesis: for k being Integer st a > 0 holds
a #Z k > 0
let k be Integer; ::_thesis: ( a > 0 implies a #Z k > 0 )
assume A1: a > 0 ; ::_thesis: a #Z k > 0
percases ( k >= 0 or k < 0 ) ;
suppose k >= 0 ; ::_thesis: a #Z k > 0
then a #Z k = a |^ (abs k) by Def3;
hence a #Z k > 0 by A1, Th6; ::_thesis: verum
end;
supposeA2: k < 0 ; ::_thesis: a #Z k > 0
A3: a |^ (abs k) > 0 by A1, Th6;
a #Z k = (a |^ (abs k)) " by A2, Def3;
hence a #Z k > 0 by A3; ::_thesis: verum
end;
end;
end;
theorem Th40: :: PREPOWER:40
for a, b being real number
for k being Integer holds (a * b) #Z k = (a #Z k) * (b #Z k)
proof
let a, b be real number ; ::_thesis: for k being Integer holds (a * b) #Z k = (a #Z k) * (b #Z k)
let k be Integer; ::_thesis: (a * b) #Z k = (a #Z k) * (b #Z k)
percases ( k >= 0 or k < 0 ) ;
supposeA1: k >= 0 ; ::_thesis: (a * b) #Z k = (a #Z k) * (b #Z k)
hence (a * b) #Z k = (a * b) |^ (abs k) by Def3
.= (a |^ (abs k)) * (b |^ (abs k)) by NEWTON:7
.= (a #Z k) * (b |^ (abs k)) by A1, Def3
.= (a #Z k) * (b #Z k) by A1, Def3 ;
::_thesis: verum
end;
supposeA2: k < 0 ; ::_thesis: (a * b) #Z k = (a #Z k) * (b #Z k)
hence (a * b) #Z k = ((a * b) |^ (abs k)) " by Def3
.= ((a |^ (abs k)) * (b |^ (abs k))) " by NEWTON:7
.= ((a |^ (abs k)) ") * ((b |^ (abs k)) ") by XCMPLX_1:204
.= (a #Z k) * ((b |^ (abs k)) ") by A2, Def3
.= (a #Z k) * (b #Z k) by A2, Def3 ;
::_thesis: verum
end;
end;
end;
theorem Th41: :: PREPOWER:41
for a being real number
for k being Integer holds a #Z (- k) = 1 / (a #Z k)
proof
let a be real number ; ::_thesis: for k being Integer holds a #Z (- k) = 1 / (a #Z k)
let k be Integer; ::_thesis: a #Z (- k) = 1 / (a #Z k)
percases ( k > 0 or k = 0 or k < 0 ) ;
supposeA1: k > 0 ; ::_thesis: a #Z (- k) = 1 / (a #Z k)
then - k < - 0 by XREAL_1:24;
hence a #Z (- k) = (a |^ (abs (- k))) " by Def3
.= (a |^ (abs k)) " by COMPLEX1:52
.= 1 / (a |^ (abs k))
.= 1 / (a #Z k) by A1, Def3 ;
::_thesis: verum
end;
supposeA2: k = 0 ; ::_thesis: a #Z (- k) = 1 / (a #Z k)
hence a #Z (- k) = 1 / 1 by Th34
.= 1 / ((a GeoSeq) . 0) by Th3
.= 1 / (a |^ 0) by Def1
.= 1 / (a #Z k) by A2, Th36 ;
::_thesis: verum
end;
supposeA3: k < 0 ; ::_thesis: a #Z (- k) = 1 / (a #Z k)
then a #Z k = (a |^ (abs k)) " by Def3
.= 1 / (a |^ (abs k))
.= 1 / (a |^ (abs (- k))) by COMPLEX1:52
.= 1 / (a #Z (- k)) by A3, Def3 ;
hence a #Z (- k) = 1 / (a #Z k) ; ::_thesis: verum
end;
end;
end;
theorem Th42: :: PREPOWER:42
for a being real number
for k being Integer holds (1 / a) #Z k = 1 / (a #Z k)
proof
let a be real number ; ::_thesis: for k being Integer holds (1 / a) #Z k = 1 / (a #Z k)
let k be Integer; ::_thesis: (1 / a) #Z k = 1 / (a #Z k)
percases ( k >= 0 or k < 0 ) ;
supposeA1: k >= 0 ; ::_thesis: (1 / a) #Z k = 1 / (a #Z k)
hence (1 / a) #Z k = (1 / a) |^ (abs k) by Def3
.= 1 / (a |^ (abs k)) by Th7
.= 1 / (a #Z k) by A1, Def3 ;
::_thesis: verum
end;
supposeA2: k < 0 ; ::_thesis: (1 / a) #Z k = 1 / (a #Z k)
hence (1 / a) #Z k = ((1 / a) |^ (abs k)) " by Def3
.= (1 / (a |^ (abs k))) " by Th7
.= ((a |^ (abs k)) ") "
.= (a #Z k) " by A2, Def3
.= 1 / (a #Z k) ;
::_thesis: verum
end;
end;
end;
theorem Th43: :: PREPOWER:43
for a being real number
for m, n being Nat st a <> 0 holds
a #Z (m - n) = (a |^ m) / (a |^ n)
proof
let a be real number ; ::_thesis: for m, n being Nat st a <> 0 holds
a #Z (m - n) = (a |^ m) / (a |^ n)
let m, n be Nat; ::_thesis: ( a <> 0 implies a #Z (m - n) = (a |^ m) / (a |^ n) )
assume A1: a <> 0 ; ::_thesis: a #Z (m - n) = (a |^ m) / (a |^ n)
percases ( m - n >= 0 or m - n < 0 ) ;
suppose m - n >= 0 ; ::_thesis: a #Z (m - n) = (a |^ m) / (a |^ n)
then reconsider m1 = m - n as Element of NAT by INT_1:3;
A2: (a #Z (m - n)) * (a |^ n) = (a |^ m1) * (a |^ n) by Th36
.= a |^ (m1 + n) by NEWTON:8
.= a |^ m ;
a |^ n <> 0 by A1, Th5;
hence a #Z (m - n) = (a |^ m) / (a |^ n) by A2, XCMPLX_1:89; ::_thesis: verum
end;
suppose m - n < 0 ; ::_thesis: a #Z (m - n) = (a |^ m) / (a |^ n)
then - (m - n) > 0 by XREAL_1:58;
then reconsider m1 = n - m as Element of NAT by INT_1:3;
A3: a #Z (n - m) = a #Z (- (m - n))
.= 1 / (a #Z (m - n)) by Th41 ;
(a #Z (n - m)) * (a |^ m) = (a |^ m1) * (a |^ m) by Th36
.= a |^ (m1 + m) by NEWTON:8
.= a |^ n ;
then A4: (a |^ m) / (a #Z (m - n)) = a |^ n by A3;
a |^ n <> 0 by A1, Th5;
hence a #Z (m - n) = (a |^ m) / (a |^ n) by A4, XCMPLX_1:54; ::_thesis: verum
end;
end;
end;
theorem Th44: :: PREPOWER:44
for a being real number
for k, l being Integer st a <> 0 holds
a #Z (k + l) = (a #Z k) * (a #Z l)
proof
let a be real number ; ::_thesis: for k, l being Integer st a <> 0 holds
a #Z (k + l) = (a #Z k) * (a #Z l)
let k, l be Integer; ::_thesis: ( a <> 0 implies a #Z (k + l) = (a #Z k) * (a #Z l) )
assume A1: a <> 0 ; ::_thesis: a #Z (k + l) = (a #Z k) * (a #Z l)
percases ( ( k >= 0 & l >= 0 ) or ( k >= 0 & l < 0 ) or ( k < 0 & l >= 0 ) or ( k < 0 & l < 0 ) ) ;
supposeA2: ( k >= 0 & l >= 0 ) ; ::_thesis: a #Z (k + l) = (a #Z k) * (a #Z l)
then A3: k * l >= 0 ;
thus a #Z (k + l) = a |^ (abs (k + l)) by A2, Def3
.= a |^ ((abs k) + (abs l)) by A3, ABSVALUE:11
.= (a |^ (abs k)) * (a |^ (abs l)) by NEWTON:8
.= (a #Z k) * (a |^ (abs l)) by A2, Def3
.= (a #Z k) * (a #Z l) by A2, Def3 ; ::_thesis: verum
end;
supposeA4: ( k >= 0 & l < 0 ) ; ::_thesis: a #Z (k + l) = (a #Z k) * (a #Z l)
then reconsider m = k as Element of NAT by INT_1:3;
reconsider n = - l as Element of NAT by A4, INT_1:3;
k + l = m - n ;
hence a #Z (k + l) = (a |^ m) / (a |^ n) by A1, Th43
.= (a |^ m) * ((a |^ n) ")
.= (a |^ (abs k)) * ((a |^ n) ") by ABSVALUE:def_1
.= (a |^ (abs k)) * ((a |^ (abs (- l))) ") by ABSVALUE:def_1
.= (a |^ (abs k)) * ((a |^ (abs l)) ") by COMPLEX1:52
.= (a #Z k) * ((a |^ (abs l)) ") by A4, Def3
.= (a #Z k) * (a #Z l) by A4, Def3 ;
::_thesis: verum
end;
supposeA5: ( k < 0 & l >= 0 ) ; ::_thesis: a #Z (k + l) = (a #Z k) * (a #Z l)
then reconsider m = l as Element of NAT by INT_1:3;
reconsider n = - k as Element of NAT by A5, INT_1:3;
k + l = m - n ;
hence a #Z (k + l) = (a |^ m) / (a |^ n) by A1, Th43
.= (a |^ m) * ((a |^ n) ")
.= (a |^ (abs l)) * ((a |^ n) ") by ABSVALUE:def_1
.= (a |^ (abs l)) * ((a |^ (abs (- k))) ") by ABSVALUE:def_1
.= (a |^ (abs l)) * ((a |^ (abs k)) ") by COMPLEX1:52
.= (a #Z l) * ((a |^ (abs k)) ") by A5, Def3
.= (a #Z k) * (a #Z l) by A5, Def3 ;
::_thesis: verum
end;
supposeA6: ( k < 0 & l < 0 ) ; ::_thesis: a #Z (k + l) = (a #Z k) * (a #Z l)
then A7: k * l >= 0 ;
thus a #Z (k + l) = (a |^ (abs (k + l))) " by A6, Def3
.= (a |^ ((abs k) + (abs l))) " by A7, ABSVALUE:11
.= ((a |^ (abs k)) * (a |^ (abs l))) " by NEWTON:8
.= ((a |^ (abs k)) ") * ((a |^ (abs l)) ") by XCMPLX_1:204
.= (a #Z k) * ((a |^ (abs l)) ") by A6, Def3
.= (a #Z k) * (a #Z l) by A6, Def3 ; ::_thesis: verum
end;
end;
end;
theorem Th45: :: PREPOWER:45
for a being real number
for k, l being Integer holds (a #Z k) #Z l = a #Z (k * l)
proof
let a be real number ; ::_thesis: for k, l being Integer holds (a #Z k) #Z l = a #Z (k * l)
let k, l be Integer; ::_thesis: (a #Z k) #Z l = a #Z (k * l)
percases ( k * l > 0 or k * l < 0 or k * l = 0 ) ;
supposeA1: k * l > 0 ; ::_thesis: (a #Z k) #Z l = a #Z (k * l)
percases ( ( k > 0 & l > 0 ) or ( k < 0 & l < 0 ) ) by A1, XREAL_1:134;
supposeA2: ( k > 0 & l > 0 ) ; ::_thesis: (a #Z k) #Z l = a #Z (k * l)
hence (a #Z k) #Z l = (a #Z k) |^ (abs l) by Def3
.= (a |^ (abs k)) |^ (abs l) by A2, Def3
.= a |^ ((abs k) * (abs l)) by NEWTON:9
.= a |^ (abs (k * l)) by COMPLEX1:65
.= a #Z (k * l) by A1, Def3 ;
::_thesis: verum
end;
supposeA3: ( k < 0 & l < 0 ) ; ::_thesis: (a #Z k) #Z l = a #Z (k * l)
hence (a #Z k) #Z l = ((a #Z k) |^ (abs l)) " by Def3
.= (((a |^ (abs k)) ") |^ (abs l)) " by A3, Def3
.= ((1 / (a |^ (abs k))) |^ (abs l)) "
.= (1 / ((a |^ (abs k)) |^ (abs l))) " by Th7
.= (((a |^ (abs k)) |^ (abs l)) ") "
.= a |^ ((abs k) * (abs l)) by NEWTON:9
.= a |^ (abs (k * l)) by COMPLEX1:65
.= a #Z (k * l) by A1, Def3 ;
::_thesis: verum
end;
end;
end;
supposeA4: k * l < 0 ; ::_thesis: (a #Z k) #Z l = a #Z (k * l)
percases ( ( k < 0 & l > 0 ) or ( k > 0 & l < 0 ) ) by A4, XREAL_1:133;
supposeA5: ( k < 0 & l > 0 ) ; ::_thesis: (a #Z k) #Z l = a #Z (k * l)
hence (a #Z k) #Z l = (a #Z k) |^ (abs l) by Def3
.= ((a |^ (abs k)) ") |^ (abs l) by A5, Def3
.= (1 / (a |^ (abs k))) |^ (abs l)
.= 1 / ((a |^ (abs k)) |^ (abs l)) by Th7
.= 1 / (a |^ ((abs k) * (abs l))) by NEWTON:9
.= 1 / (a |^ (abs (k * l))) by COMPLEX1:65
.= (a |^ (abs (k * l))) "
.= a #Z (k * l) by A4, Def3 ;
::_thesis: verum
end;
supposeA6: ( k > 0 & l < 0 ) ; ::_thesis: (a #Z k) #Z l = a #Z (k * l)
hence (a #Z k) #Z l = ((a #Z k) |^ (abs l)) " by Def3
.= ((a |^ (abs k)) |^ (abs l)) " by A6, Def3
.= (a |^ ((abs k) * (abs l))) " by NEWTON:9
.= (a |^ (abs (k * l))) " by COMPLEX1:65
.= a #Z (k * l) by A4, Def3 ;
::_thesis: verum
end;
end;
end;
supposeA7: k * l = 0 ; ::_thesis: (a #Z k) #Z l = a #Z (k * l)
percases ( k = 0 or l = 0 ) by A7, XCMPLX_1:6;
suppose k = 0 ; ::_thesis: (a #Z k) #Z l = a #Z (k * l)
hence (a #Z k) #Z l = 1 #Z l by Th34
.= 1 by Th37
.= a #Z (k * l) by A7, Th34 ;
::_thesis: verum
end;
suppose l = 0 ; ::_thesis: (a #Z k) #Z l = a #Z (k * l)
hence (a #Z k) #Z l = 1 by Th34
.= a #Z (k * l) by A7, Th34 ;
::_thesis: verum
end;
end;
end;
end;
end;
theorem Th46: :: PREPOWER:46
for a being real number
for n being Element of NAT
for k being Integer st a > 0 & n >= 1 holds
(n -Root a) #Z k = n -Root (a #Z k)
proof
let a be real number ; ::_thesis: for n being Element of NAT
for k being Integer st a > 0 & n >= 1 holds
(n -Root a) #Z k = n -Root (a #Z k)
let n be Element of NAT ; ::_thesis: for k being Integer st a > 0 & n >= 1 holds
(n -Root a) #Z k = n -Root (a #Z k)
let k be Integer; ::_thesis: ( a > 0 & n >= 1 implies (n -Root a) #Z k = n -Root (a #Z k) )
assume that
A1: a > 0 and
A2: n >= 1 ; ::_thesis: (n -Root a) #Z k = n -Root (a #Z k)
A3: n -Root a > 0 by A1, A2, Def2;
A4: for m being Element of NAT st m >= 1 holds
(n -Root a) |^ m = n -Root (a |^ m)
proof
let m be Element of NAT ; ::_thesis: ( m >= 1 implies (n -Root a) |^ m = n -Root (a |^ m) )
assume that
A5: m >= 1 and
A6: (n -Root a) |^ m <> n -Root (a |^ m) ; ::_thesis: contradiction
A7: a |^ m > 0 by A1, Th6;
then A8: n -Root (a |^ m) >= 0 by A2, Def2;
A9: m -Root (n -Root (a |^ m)) = (n * m) -Root (a |^ m) by A2, A5, A7, Th25
.= n -Root (m -Root (a |^ m)) by A2, A5, A7, Th25
.= n -Root a by A1, A5, Lm2 ;
A10: m -Root ((n -Root a) |^ m) = n -Root a by A3, A5, Lm2;
A11: (n -Root a) |^ m >= 0 by A3, Th6;
percases ( (n -Root a) |^ m < n -Root (a |^ m) or (n -Root a) |^ m > n -Root (a |^ m) ) by A6, XXREAL_0:1;
suppose (n -Root a) |^ m < n -Root (a |^ m) ; ::_thesis: contradiction
hence contradiction by A5, A9, A11, Lm2; ::_thesis: verum
end;
suppose (n -Root a) |^ m > n -Root (a |^ m) ; ::_thesis: contradiction
hence contradiction by A5, A9, A10, A8, Th28; ::_thesis: verum
end;
end;
end;
percases ( k > 0 or k < 0 or k = 0 ) ;
supposeA12: k > 0 ; ::_thesis: (n -Root a) #Z k = n -Root (a #Z k)
then abs k > 0 by ABSVALUE:def_1;
then A13: abs k >= 0 + 1 by NAT_1:13;
thus (n -Root a) #Z k = (n -Root a) |^ (abs k) by A12, Def3
.= n -Root (a |^ (abs k)) by A4, A13
.= n -Root (a #Z k) by A12, Def3 ; ::_thesis: verum
end;
supposeA14: k < 0 ; ::_thesis: (n -Root a) #Z k = n -Root (a #Z k)
then abs k > 0 by COMPLEX1:47;
then A15: abs k >= 0 + 1 by NAT_1:13;
A16: a |^ (abs k) > 0 by A1, Th6;
thus (n -Root a) #Z k = ((n -Root a) |^ (abs k)) " by A14, Def3
.= (n -Root (a |^ (abs k))) " by A4, A15
.= 1 / (n -Root (a |^ (abs k)))
.= n -Root (1 / (a |^ (abs k))) by A2, A16, Th23
.= n -Root ((a |^ (abs k)) ")
.= n -Root (a #Z k) by A14, Def3 ; ::_thesis: verum
end;
supposeA17: k = 0 ; ::_thesis: (n -Root a) #Z k = n -Root (a #Z k)
then n -Root (a #Z k) = n -Root 1 by Th34
.= 1 by A2, Th20 ;
hence (n -Root a) #Z k = n -Root (a #Z k) by A17, Th34; ::_thesis: verum
end;
end;
end;
definition
let a be real number ;
let p be Rational;
funca #Q p -> set equals :: PREPOWER:def 4
(denominator p) -Root (a #Z (numerator p));
coherence
(denominator p) -Root (a #Z (numerator p)) is set ;
end;
:: deftheorem defines #Q PREPOWER:def_4_:_
for a being real number
for p being Rational holds a #Q p = (denominator p) -Root (a #Z (numerator p));
registration
let a be real number ;
let p be Rational;
clustera #Q p -> real ;
coherence
a #Q p is real ;
end;
definition
let a be Real;
let p be Rational;
:: original: #Q
redefine funca #Q p -> Real;
coherence
a #Q p is Real by XREAL_0:def_1;
end;
theorem Th47: :: PREPOWER:47
for a being real number
for p being Rational st p = 0 holds
a #Q p = 1
proof
let a be real number ; ::_thesis: for p being Rational st p = 0 holds
a #Q p = 1
let p be Rational; ::_thesis: ( p = 0 implies a #Q p = 1 )
reconsider i = 0 as Integer ;
assume A1: p = 0 ; ::_thesis: a #Q p = 1
numerator p = 0 by A1, RAT_1:14;
hence a #Q p = 1 -Root (a #Z i) by A1, RAT_1:19
.= 1 -Root 1 by Th34
.= 1 by Th21 ;
::_thesis: verum
end;
theorem Th48: :: PREPOWER:48
for a being real number
for p being Rational st a > 0 & p = 1 holds
a #Q p = a
proof
let a be real number ; ::_thesis: for p being Rational st a > 0 & p = 1 holds
a #Q p = a
let p be Rational; ::_thesis: ( a > 0 & p = 1 implies a #Q p = a )
assume that
A1: a > 0 and
A2: p = 1 ; ::_thesis: a #Q p = a
A3: denominator p = 1 by A2, RAT_1:17;
numerator p = p by A2, RAT_1:17;
hence a #Q p = 1 -Root a by A2, A3, Th35
.= a by A1, Th21 ;
::_thesis: verum
end;
Lm5: for a being real number
for k being Integer st a >= 0 holds
a #Z k >= 0
proof
let a be real number ; ::_thesis: for k being Integer st a >= 0 holds
a #Z k >= 0
let k be Integer; ::_thesis: ( a >= 0 implies a #Z k >= 0 )
assume A1: a >= 0 ; ::_thesis: a #Z k >= 0
percases ( a = 0 or a > 0 ) by A1;
supposeA2: a = 0 ; ::_thesis: a #Z k >= 0
( abs k = 0 or abs k >= 1 ) by NAT_1:14;
then ( (0 |^ (abs k)) " = 0 " or (0 |^ (abs k)) " = 1 " ) by NEWTON:4, NEWTON:11;
hence a #Z k >= 0 by A2, Def3; ::_thesis: verum
end;
suppose a > 0 ; ::_thesis: a #Z k >= 0
hence a #Z k >= 0 by Th39; ::_thesis: verum
end;
end;
end;
theorem Th49: :: PREPOWER:49
for a being real number
for n being Nat st 0 <= a holds
a #Q n = a |^ n
proof
let a be real number ; ::_thesis: for n being Nat st 0 <= a holds
a #Q n = a |^ n
let n be Nat; ::_thesis: ( 0 <= a implies a #Q n = a |^ n )
A1: denominator n = 1 by RAT_1:17;
A2: numerator n = n by RAT_1:17;
assume 0 <= a ; ::_thesis: a #Q n = a |^ n
hence a #Q n = a #Z n by A1, A2, Lm5, Th21
.= a |^ n by Th36 ;
::_thesis: verum
end;
theorem Th50: :: PREPOWER:50
for a being real number
for p being Rational
for n being Nat st n >= 1 & p = n " holds
a #Q p = n -Root a
proof
let a be real number ; ::_thesis: for p being Rational
for n being Nat st n >= 1 & p = n " holds
a #Q p = n -Root a
let p be Rational; ::_thesis: for n being Nat st n >= 1 & p = n " holds
a #Q p = n -Root a
let n be Nat; ::_thesis: ( n >= 1 & p = n " implies a #Q p = n -Root a )
assume that
A1: n >= 1 and
A2: p = n " ; ::_thesis: a #Q p = n -Root a
reconsider q = n as Rational ;
A3: p = 1 / n by A2;
then denominator p = numerator q by A1, RAT_1:44;
then A4: denominator p = n by RAT_1:17;
numerator p = denominator q by A1, A3, RAT_1:44;
then numerator p = 1 by RAT_1:17;
hence a #Q p = n -Root a by A4, Th35; ::_thesis: verum
end;
theorem Th51: :: PREPOWER:51
for p being Rational holds 1 #Q p = 1
proof
let p be Rational; ::_thesis: 1 #Q p = 1
thus 1 #Q p = (denominator p) -Root 1 by Th37
.= 1 by Th20, RAT_1:11 ; ::_thesis: verum
end;
theorem Th52: :: PREPOWER:52
for a being real number
for p being Rational st a > 0 holds
a #Q p > 0
proof
let a be real number ; ::_thesis: for p being Rational st a > 0 holds
a #Q p > 0
let p be Rational; ::_thesis: ( a > 0 implies a #Q p > 0 )
assume a > 0 ; ::_thesis: a #Q p > 0
then A1: a #Z (numerator p) > 0 by Th39;
denominator p >= 1 by RAT_1:11;
hence a #Q p > 0 by A1, Def2; ::_thesis: verum
end;
theorem Th53: :: PREPOWER:53
for a being real number
for p, q being Rational st a > 0 holds
(a #Q p) * (a #Q q) = a #Q (p + q)
proof
let a be real number ; ::_thesis: for p, q being Rational st a > 0 holds
(a #Q p) * (a #Q q) = a #Q (p + q)
let p, q be Rational; ::_thesis: ( a > 0 implies (a #Q p) * (a #Q q) = a #Q (p + q) )
set dp = denominator p;
set dq = denominator q;
set np = numerator p;
set nq = numerator q;
A1: denominator p >= 1 by RAT_1:11;
reconsider ddq = denominator q as Integer ;
reconsider ddp = denominator p as Integer ;
A2: denominator (p + q) >= 1 by RAT_1:11;
A3: denominator p <> 0 by RAT_1:def_3;
A4: denominator q >= 1 by RAT_1:11;
then A5: (denominator p) * (denominator q) >= 1 by A1, XREAL_1:159;
A6: denominator q <> 0 by RAT_1:def_3;
p + q = ((numerator p) / (denominator p)) + q by RAT_1:15
.= ((numerator p) / (denominator p)) + ((numerator q) / (denominator q)) by RAT_1:15
.= (((numerator p) * (denominator q)) + ((numerator q) * (denominator p))) / ((denominator p) * (denominator q)) by A3, A6, XCMPLX_1:116 ;
then consider n being Element of NAT such that
A7: ((numerator p) * (denominator q)) + ((numerator q) * (denominator p)) = (numerator (p + q)) * n and
A8: (denominator p) * (denominator q) = (denominator (p + q)) * n by A3, A6, RAT_1:27, XCMPLX_1:6;
reconsider k = n as Integer ;
assume A9: a > 0 ; ::_thesis: (a #Q p) * (a #Q q) = a #Q (p + q)
then A10: a #Z ((numerator q) - (numerator p)) >= 0 by Th39;
n > 0 by A4, A1, A8, XREAL_1:159;
then A11: n >= 0 + 1 by NAT_1:13;
A12: a #Z (numerator p) > 0 by A9, Th39;
then A13: (a #Z (numerator p)) |^ ((denominator p) + (denominator q)) >= 0 by Th6;
A14: a #Z ((numerator q) - (numerator p)) > 0 by A9, Th39;
then A15: (a #Z ((numerator q) - (numerator p))) |^ (denominator p) >= 0 by Th6;
A16: a #Q (p + q) > 0 by A9, Th52;
A17: a #Z (numerator (p + q)) > 0 by A9, Th39;
thus (a #Q p) * (a #Q q) = ((denominator p) -Root (a #Z (numerator p))) * ((denominator q) -Root (a #Z ((numerator p) + ((numerator q) - (numerator p)))))
.= ((denominator p) -Root (a #Z (numerator p))) * ((denominator q) -Root ((a #Z (numerator p)) * (a #Z ((numerator q) - (numerator p))))) by A9, Th44
.= ((denominator p) -Root (a #Z (numerator p))) * (((denominator q) -Root (a #Z (numerator p))) * ((denominator q) -Root (a #Z ((numerator q) - (numerator p))))) by A12, A10, Th22, RAT_1:11
.= (((denominator p) -Root (a #Z (numerator p))) * ((denominator q) -Root (a #Z (numerator p)))) * ((denominator q) -Root (a #Z ((numerator q) - (numerator p))))
.= (((denominator p) * (denominator q)) -Root ((a #Z (numerator p)) |^ ((denominator p) + (denominator q)))) * ((denominator q) -Root (a #Z ((numerator q) - (numerator p)))) by A12, A4, A1, Th26
.= (((denominator p) * (denominator q)) -Root ((a #Z (numerator p)) |^ ((denominator p) + (denominator q)))) * ((denominator q) -Root ((denominator p) -Root ((a #Z ((numerator q) - (numerator p))) |^ (denominator p)))) by A14, A1, Lm2
.= (((denominator p) * (denominator q)) -Root ((a #Z (numerator p)) |^ ((denominator p) + (denominator q)))) * (((denominator p) * (denominator q)) -Root ((a #Z ((numerator q) - (numerator p))) |^ (denominator p))) by A4, A1, A15, Th25
.= ((denominator p) * (denominator q)) -Root (((a #Z (numerator p)) |^ ((denominator p) + (denominator q))) * ((a #Z ((numerator q) - (numerator p))) |^ (denominator p))) by A4, A1, A15, A13, Th22, XREAL_1:159
.= ((denominator p) * (denominator q)) -Root (((a #Z (numerator p)) #Z (ddp + ddq)) * ((a #Z ((numerator q) - (numerator p))) |^ (denominator p))) by Th36
.= ((denominator p) * (denominator q)) -Root (((a #Z (numerator p)) #Z (ddp + ddq)) * ((a #Z ((numerator q) - (numerator p))) #Z ddp)) by Th36
.= ((denominator p) * (denominator q)) -Root ((a #Z ((numerator p) * (ddp + ddq))) * ((a #Z ((numerator q) - (numerator p))) #Z ddp)) by Th45
.= ((denominator p) * (denominator q)) -Root ((a #Z ((numerator p) * (ddp + ddq))) * (a #Z (((numerator q) - (numerator p)) * ddp))) by Th45
.= ((denominator p) * (denominator q)) -Root (a #Z ((((numerator p) * ddp) + ((numerator p) * ddq)) + (((numerator q) - (numerator p)) * ddp))) by A9, Th44
.= ((denominator (p + q)) * n) -Root ((a #Z (numerator (p + q))) #Z k) by A7, A8, Th45
.= (((denominator (p + q)) * n) -Root (a #Z (numerator (p + q)))) #Z k by A5, A8, A17, Th46
.= ((n * (denominator (p + q))) -Root (a #Z (numerator (p + q)))) |^ n by Th36
.= (n -Root (a #Q (p + q))) |^ n by A11, A2, A17, Th25
.= a #Q (p + q) by A11, A16, Lm2 ; ::_thesis: verum
end;
theorem Th54: :: PREPOWER:54
for a being real number
for p being Rational st a > 0 holds
1 / (a #Q p) = a #Q (- p)
proof
let a be real number ; ::_thesis: for p being Rational st a > 0 holds
1 / (a #Q p) = a #Q (- p)
let p be Rational; ::_thesis: ( a > 0 implies 1 / (a #Q p) = a #Q (- p) )
assume a > 0 ; ::_thesis: 1 / (a #Q p) = a #Q (- p)
then A1: a #Z (numerator p) > 0 by Th39;
thus a #Q (- p) = (denominator (- p)) -Root (a #Z (- (numerator p))) by RAT_1:43
.= (denominator p) -Root (a #Z (- (numerator p))) by RAT_1:43
.= (denominator p) -Root (1 / (a #Z (numerator p))) by Th41
.= 1 / (a #Q p) by A1, Th23, RAT_1:11 ; ::_thesis: verum
end;
theorem Th55: :: PREPOWER:55
for a being real number
for p, q being Rational st a > 0 holds
(a #Q p) / (a #Q q) = a #Q (p - q)
proof
let a be real number ; ::_thesis: for p, q being Rational st a > 0 holds
(a #Q p) / (a #Q q) = a #Q (p - q)
let p, q be Rational; ::_thesis: ( a > 0 implies (a #Q p) / (a #Q q) = a #Q (p - q) )
assume A1: a > 0 ; ::_thesis: (a #Q p) / (a #Q q) = a #Q (p - q)
thus a #Q (p - q) = a #Q (p + (- q))
.= (a #Q p) * (a #Q (- q)) by A1, Th53
.= (a #Q p) * (1 / (a #Q q)) by A1, Th54
.= ((a #Q p) * 1) / (a #Q q)
.= (a #Q p) / (a #Q q) ; ::_thesis: verum
end;
theorem Th56: :: PREPOWER:56
for a, b being real number
for p being Rational st a > 0 & b > 0 holds
(a * b) #Q p = (a #Q p) * (b #Q p)
proof
let a, b be real number ; ::_thesis: for p being Rational st a > 0 & b > 0 holds
(a * b) #Q p = (a #Q p) * (b #Q p)
let p be Rational; ::_thesis: ( a > 0 & b > 0 implies (a * b) #Q p = (a #Q p) * (b #Q p) )
assume that
A1: a > 0 and
A2: b > 0 ; ::_thesis: (a * b) #Q p = (a #Q p) * (b #Q p)
A3: a #Z (numerator p) >= 0 by A1, Th39;
A4: b #Z (numerator p) >= 0 by A2, Th39;
thus (a * b) #Q p = (denominator p) -Root ((a #Z (numerator p)) * (b #Z (numerator p))) by Th40
.= (a #Q p) * (b #Q p) by A3, A4, Th22, RAT_1:11 ; ::_thesis: verum
end;
theorem Th57: :: PREPOWER:57
for a being real number
for p being Rational st a > 0 holds
(1 / a) #Q p = 1 / (a #Q p)
proof
let a be real number ; ::_thesis: for p being Rational st a > 0 holds
(1 / a) #Q p = 1 / (a #Q p)
let p be Rational; ::_thesis: ( a > 0 implies (1 / a) #Q p = 1 / (a #Q p) )
assume A1: a > 0 ; ::_thesis: (1 / a) #Q p = 1 / (a #Q p)
thus (1 / a) #Q p = (denominator p) -Root (1 / (a #Z (numerator p))) by Th42
.= (denominator p) -Root (a #Z (- (numerator p))) by Th41
.= (denominator p) -Root (a #Z (numerator (- p))) by RAT_1:43
.= a #Q (- p) by RAT_1:43
.= 1 / (a #Q p) by A1, Th54 ; ::_thesis: verum
end;
theorem Th58: :: PREPOWER:58
for a, b being real number
for p being Rational st a > 0 & b > 0 holds
(a / b) #Q p = (a #Q p) / (b #Q p)
proof
let a, b be real number ; ::_thesis: for p being Rational st a > 0 & b > 0 holds
(a / b) #Q p = (a #Q p) / (b #Q p)
let p be Rational; ::_thesis: ( a > 0 & b > 0 implies (a / b) #Q p = (a #Q p) / (b #Q p) )
assume that
A1: a > 0 and
A2: b > 0 ; ::_thesis: (a / b) #Q p = (a #Q p) / (b #Q p)
thus (a / b) #Q p = (a * (1 / b)) #Q p
.= (a #Q p) * ((1 / b) #Q p) by A1, A2, Th56
.= (a #Q p) * (1 / (b #Q p)) by A2, Th57
.= (a #Q p) / (b #Q p) ; ::_thesis: verum
end;
theorem Th59: :: PREPOWER:59
for a being real number
for p, q being Rational st a > 0 holds
(a #Q p) #Q q = a #Q (p * q)
proof
let a be real number ; ::_thesis: for p, q being Rational st a > 0 holds
(a #Q p) #Q q = a #Q (p * q)
let p, q be Rational; ::_thesis: ( a > 0 implies (a #Q p) #Q q = a #Q (p * q) )
A1: denominator p >= 1 by RAT_1:11;
A2: denominator q <> 0 by RAT_1:def_3;
A3: denominator p <> 0 by RAT_1:def_3;
then A4: (denominator p) * (denominator q) <> 0 by A2, XCMPLX_1:6;
p = (numerator p) / (denominator p) by RAT_1:15;
then p * q = ((numerator p) / (denominator p)) * ((numerator q) / (denominator q)) by RAT_1:15
.= (((numerator p) / (denominator p)) * (numerator q)) / (denominator q)
.= ((numerator p) * (numerator q)) / ((denominator p) * (denominator q)) by XCMPLX_1:83 ;
then consider n being Element of NAT such that
A5: (numerator p) * (numerator q) = (numerator (p * q)) * n and
A6: (denominator p) * (denominator q) = (denominator (p * q)) * n by A3, A2, RAT_1:27, XCMPLX_1:6;
A7: (denominator (p * q)) * n >= 0 + 1 by A4, A6, NAT_1:13;
n > 0 by A4, A6;
then A8: n >= 0 + 1 by NAT_1:13;
reconsider k = n as Integer ;
A9: denominator q >= 1 by RAT_1:11;
A10: denominator (p * q) >= 1 by RAT_1:11;
assume A11: a > 0 ; ::_thesis: (a #Q p) #Q q = a #Q (p * q)
then A12: a #Z ((numerator p) * (numerator q)) >= 0 by Th39;
A13: a #Q (p * q) > 0 by A11, Th52;
A14: a #Z (numerator (p * q)) > 0 by A11, Th39;
a #Z (numerator p) > 0 by A11, Th39;
hence (a #Q p) #Q q = (denominator q) -Root ((denominator p) -Root ((a #Z (numerator p)) #Z (numerator q))) by Th46, RAT_1:11
.= (denominator q) -Root ((denominator p) -Root (a #Z ((numerator p) * (numerator q)))) by Th45
.= ((denominator (p * q)) * n) -Root (a #Z ((numerator (p * q)) * k)) by A1, A9, A12, A5, A6, Th25
.= ((denominator (p * q)) * n) -Root ((a #Z (numerator (p * q))) #Z k) by Th45
.= (((denominator (p * q)) * n) -Root (a #Z (numerator (p * q)))) #Z k by A14, A7, Th46
.= ((n * (denominator (p * q))) -Root (a #Z (numerator (p * q)))) |^ n by Th36
.= (n -Root (a #Q (p * q))) |^ n by A8, A10, A14, Th25
.= a #Q (p * q) by A8, A13, Lm2 ;
::_thesis: verum
end;
theorem Th60: :: PREPOWER:60
for a being real number
for p being Rational st a >= 1 & p >= 0 holds
a #Q p >= 1
proof
let a be real number ; ::_thesis: for p being Rational st a >= 1 & p >= 0 holds
a #Q p >= 1
let p be Rational; ::_thesis: ( a >= 1 & p >= 0 implies a #Q p >= 1 )
assume that
A1: a >= 1 and
A2: p >= 0 ; ::_thesis: a #Q p >= 1
numerator p >= 0 by A2, RAT_1:37;
then reconsider n = numerator p as Element of NAT by INT_1:3;
A3: a #Z (numerator p) = a |^ n by Th36;
a |^ n >= 1 |^ n by A1, Th9;
then A4: a #Z (numerator p) >= 1 by A3, NEWTON:10;
denominator p >= 1 by RAT_1:11;
hence a #Q p >= 1 by A4, Th29; ::_thesis: verum
end;
theorem Th61: :: PREPOWER:61
for a being real number
for p being Rational st a >= 1 & p <= 0 holds
a #Q p <= 1
proof
let a be real number ; ::_thesis: for p being Rational st a >= 1 & p <= 0 holds
a #Q p <= 1
let p be Rational; ::_thesis: ( a >= 1 & p <= 0 implies a #Q p <= 1 )
assume that
A1: a >= 1 and
A2: p <= 0 ; ::_thesis: a #Q p <= 1
a #Q (- p) >= 1 by A1, A2, Th60;
then 1 / (a #Q p) >= 1 by A1, Th54;
hence a #Q p <= 1 by XREAL_1:191; ::_thesis: verum
end;
theorem Th62: :: PREPOWER:62
for a being real number
for p being Rational st a > 1 & p > 0 holds
a #Q p > 1
proof
let a be real number ; ::_thesis: for p being Rational st a > 1 & p > 0 holds
a #Q p > 1
let p be Rational; ::_thesis: ( a > 1 & p > 0 implies a #Q p > 1 )
assume that
A1: a > 1 and
A2: p > 0 ; ::_thesis: a #Q p > 1
A3: numerator p > 0 by A2, RAT_1:38;
then reconsider n = numerator p as Element of NAT by INT_1:3;
n >= 0 + 1 by A3, NAT_1:13;
then A4: a |^ n > 1 |^ n by A1, Lm1;
a #Z (numerator p) = a |^ n by Th36;
then a #Z (numerator p) > 1 by A4, NEWTON:10;
then (denominator p) -Root (a #Z (numerator p)) > (denominator p) -Root 1 by Th28, RAT_1:11;
hence a #Q p > 1 by Th20, RAT_1:11; ::_thesis: verum
end;
theorem Th63: :: PREPOWER:63
for a being real number
for p, q being Rational st a >= 1 & p >= q holds
a #Q p >= a #Q q
proof
let a be real number ; ::_thesis: for p, q being Rational st a >= 1 & p >= q holds
a #Q p >= a #Q q
let p, q be Rational; ::_thesis: ( a >= 1 & p >= q implies a #Q p >= a #Q q )
assume that
A1: a >= 1 and
A2: p >= q ; ::_thesis: a #Q p >= a #Q q
percases ( p = q or p > q ) by A2, XXREAL_0:1;
suppose p = q ; ::_thesis: a #Q p >= a #Q q
hence a #Q p >= a #Q q ; ::_thesis: verum
end;
suppose p > q ; ::_thesis: a #Q p >= a #Q q
then A3: p - q >= 0 by XREAL_1:50;
A4: a #Q q <> 0 by A1, Th52;
A5: (a #Q p) / (a #Q q) = a #Q (p - q) by A1, Th55;
a #Q q >= 0 by A1, Th52;
then ((a #Q p) / (a #Q q)) * (a #Q q) >= 1 * (a #Q q) by A1, A3, A5, Th60, XREAL_1:64;
hence a #Q p >= a #Q q by A4, XCMPLX_1:87; ::_thesis: verum
end;
end;
end;
theorem Th64: :: PREPOWER:64
for a being real number
for p, q being Rational st a > 1 & p > q holds
a #Q p > a #Q q
proof
let a be real number ; ::_thesis: for p, q being Rational st a > 1 & p > q holds
a #Q p > a #Q q
let p, q be Rational; ::_thesis: ( a > 1 & p > q implies a #Q p > a #Q q )
assume that
A1: a > 1 and
A2: p > q ; ::_thesis: a #Q p > a #Q q
A3: p - q > 0 by A2, XREAL_1:50;
A4: (a #Q p) / (a #Q q) = a #Q (p - q) by A1, Th55;
A5: a #Q q <> 0 by A1, Th52;
a #Q q > 0 by A1, Th52;
then ((a #Q p) / (a #Q q)) * (a #Q q) > 1 * (a #Q q) by A1, A3, A4, Th62, XREAL_1:68;
hence a #Q p > a #Q q by A5, XCMPLX_1:87; ::_thesis: verum
end;
theorem Th65: :: PREPOWER:65
for a being real number
for p being Rational st a > 0 & a < 1 & p > 0 holds
a #Q p < 1
proof
let a be real number ; ::_thesis: for p being Rational st a > 0 & a < 1 & p > 0 holds
a #Q p < 1
let p be Rational; ::_thesis: ( a > 0 & a < 1 & p > 0 implies a #Q p < 1 )
reconsider q = 0 as Rational ;
assume that
A1: a > 0 and
A2: a < 1 and
A3: p > 0 ; ::_thesis: a #Q p < 1
1 / a > 1 by A1, A2, Lm4, XREAL_1:88;
then (1 / a) #Q p > (1 / a) #Q q by A3, Th64;
then (1 / a) #Q p > 1 by Th47;
then 1 / (a #Q p) > 1 by A1, Th57;
hence a #Q p < 1 by XREAL_1:185; ::_thesis: verum
end;
theorem :: PREPOWER:66
for a being real number
for p being Rational st a > 0 & a <= 1 & p <= 0 holds
a #Q p >= 1
proof
let a be real number ; ::_thesis: for p being Rational st a > 0 & a <= 1 & p <= 0 holds
a #Q p >= 1
let p be Rational; ::_thesis: ( a > 0 & a <= 1 & p <= 0 implies a #Q p >= 1 )
assume that
A1: a > 0 and
A2: a <= 1 and
A3: p <= 0 ; ::_thesis: a #Q p >= 1
1 / a >= 1 by A1, A2, Lm4, XREAL_1:85;
then (1 / a) #Q p <= 1 by A3, Th61;
then A4: 1 / (a #Q p) <= 1 by A1, Th57;
a #Q p > 0 by A1, Th52;
hence a #Q p >= 1 by A4, XREAL_1:187; ::_thesis: verum
end;
registration
cluster Relation-like NAT -defined REAL -valued RAT -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued for Element of K19(K20(NAT,REAL));
existence
ex b1 being Real_Sequence st b1 is RAT -valued
proof
reconsider s = NAT --> 0 as Real_Sequence by FUNCOP_1:45;
take s ; ::_thesis: s is RAT -valued
thus s is RAT -valued ; ::_thesis: verum
end;
end;
definition
canceled;
mode Rational_Sequence is RAT -valued Real_Sequence;
end;
:: deftheorem PREPOWER:def_5_:_
canceled;
theorem Th67: :: PREPOWER:67
for a being real number ex s being Rational_Sequence st
( s is convergent & lim s = a & ( for n being Element of NAT holds s . n <= a ) )
proof
let a be real number ; ::_thesis: ex s being Rational_Sequence st
( s is convergent & lim s = a & ( for n being Element of NAT holds s . n <= a ) )
deffunc H1( Element of NAT ) -> Element of REAL = [\(($1 + 1) * a)/] / ($1 + 1);
consider s being Real_Sequence such that
A1: for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch_1();
rng s c= RAT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s or y in RAT )
assume y in rng s ; ::_thesis: y in RAT
then consider n being Element of NAT such that
A2: s . n = y by FUNCT_2:113;
s . n = H1(n) by A1;
hence y in RAT by A2, RAT_1:def_2; ::_thesis: verum
end;
then reconsider s = s as Rational_Sequence by RELAT_1:def_19;
deffunc H2( Element of NAT ) -> Element of REAL = 1 / ($1 + 1);
consider s2 being Real_Sequence such that
A3: for n being Element of NAT holds s2 . n = H2(n) from SEQ_1:sch_1();
reconsider a1 = a as Real by XREAL_0:def_1;
reconsider s1 = NAT --> a1 as Real_Sequence ;
take s ; ::_thesis: ( s is convergent & lim s = a & ( for n being Element of NAT holds s . n <= a ) )
set s3 = s1 - s2;
A4: s2 is convergent by A3, SEQ_4:30;
then A5: s1 - s2 is convergent by SEQ_2:11;
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_(s1_-_s2)_._n_<=_s_._n_&_s_._n_<=_s1_._n_)
let n be Element of NAT ; ::_thesis: ( (s1 - s2) . n <= s . n & s . n <= s1 . n )
(n + 1) * a <= [\((n + 1) * a)/] + 1 by INT_1:29;
then ((n + 1) * a) - 1 <= ([\((n + 1) * a)/] + 1) - 1 by XREAL_1:9;
then (((n + 1) * a) - 1) * ((n + 1) ") <= [\((n + 1) * a)/] / (n + 1) by XREAL_1:64;
then ((a / (n + 1)) * (n + 1)) - (1 / (n + 1)) <= s . n by A1;
then a - (1 / (n + 1)) <= s . n by XCMPLX_1:87;
then (s1 . n) - (1 / (n + 1)) <= s . n by FUNCOP_1:7;
then A7: (s1 . n) - (s2 . n) <= s . n by A3;
[\((n + 1) * a)/] <= (n + 1) * a by INT_1:def_6;
then [\((n + 1) * a)/] * ((n + 1) ") <= (a * (n + 1)) * ((n + 1) ") by XREAL_1:64;
then [\((n + 1) * a)/] * ((n + 1) ") <= a * ((n + 1) * ((n + 1) ")) ;
then [\((n + 1) * a)/] * ((n + 1) ") <= a * 1 by XCMPLX_0:def_7;
then [\((n + 1) * a)/] / (n + 1) <= s1 . n by FUNCOP_1:7;
hence ( (s1 - s2) . n <= s . n & s . n <= s1 . n ) by A1, A7, RFUNCT_2:1; ::_thesis: verum
end;
lim s2 = 0 by A3, SEQ_4:30;
then A8: lim (s1 - s2) = (s1 . 0) - 0 by A4, SEQ_4:42
.= a by FUNCOP_1:7 ;
A9: lim s1 = s1 . 0 by SEQ_4:26
.= a by FUNCOP_1:7 ;
hence s is convergent by A5, A8, A6, SEQ_2:19; ::_thesis: ( lim s = a & ( for n being Element of NAT holds s . n <= a ) )
thus lim s = a by A5, A8, A9, A6, SEQ_2:20; ::_thesis: for n being Element of NAT holds s . n <= a
let n be Element of NAT ; ::_thesis: s . n <= a
s . n <= s1 . n by A6;
hence s . n <= a by FUNCOP_1:7; ::_thesis: verum
end;
theorem Th68: :: PREPOWER:68
for a being real number ex s being Rational_Sequence st
( s is convergent & lim s = a & ( for n being Element of NAT holds s . n >= a ) )
proof
let a be real number ; ::_thesis: ex s being Rational_Sequence st
( s is convergent & lim s = a & ( for n being Element of NAT holds s . n >= a ) )
deffunc H1( Element of NAT ) -> Element of REAL = [/(($1 + 1) * a)\] / ($1 + 1);
consider s being Real_Sequence such that
A1: for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch_1();
rng s c= RAT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s or y in RAT )
assume y in rng s ; ::_thesis: y in RAT
then consider n being Element of NAT such that
A2: s . n = y by FUNCT_2:113;
s . n = H1(n) by A1;
hence y in RAT by A2, RAT_1:def_2; ::_thesis: verum
end;
then reconsider s = s as Rational_Sequence by RELAT_1:def_19;
deffunc H2( Element of NAT ) -> Element of REAL = 1 / ($1 + 1);
consider s2 being Real_Sequence such that
A3: for n being Element of NAT holds s2 . n = H2(n) from SEQ_1:sch_1();
take s ; ::_thesis: ( s is convergent & lim s = a & ( for n being Element of NAT holds s . n >= a ) )
a in REAL by XREAL_0:def_1;
then reconsider s1 = NAT --> a as Real_Sequence by FUNCOP_1:45;
set s3 = s1 + s2;
A4: s2 is convergent by A3, SEQ_4:30;
then A5: s1 + s2 is convergent by SEQ_2:5;
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_s1_._n_<=_s_._n_&_s_._n_<=_(s1_+_s2)_._n_)
let n be Element of NAT ; ::_thesis: ( s1 . n <= s . n & s . n <= (s1 + s2) . n )
((n + 1) * a) + 1 >= [/((n + 1) * a)\] by INT_1:def_7;
then (((n + 1) * a) + 1) * ((n + 1) ") >= [/((n + 1) * a)\] / (n + 1) by XREAL_1:64;
then ((a / (n + 1)) * (n + 1)) + (1 / (n + 1)) >= s . n by A1;
then a + (1 / (n + 1)) >= s . n by XCMPLX_1:87;
then (s1 . n) + (1 / (n + 1)) >= s . n by FUNCOP_1:7;
then A7: (s1 . n) + (s2 . n) >= s . n by A3;
[/((n + 1) * a)\] >= (n + 1) * a by INT_1:def_7;
then [/((n + 1) * a)\] * ((n + 1) ") >= (a * (n + 1)) * ((n + 1) ") by XREAL_1:64;
then [/((n + 1) * a)\] * ((n + 1) ") >= a * ((n + 1) * ((n + 1) ")) ;
then [/((n + 1) * a)\] * ((n + 1) ") >= a * 1 by XCMPLX_0:def_7;
then [/((n + 1) * a)\] / (n + 1) >= s1 . n by FUNCOP_1:7;
hence ( s1 . n <= s . n & s . n <= (s1 + s2) . n ) by A1, A7, SEQ_1:7; ::_thesis: verum
end;
lim s2 = 0 by A3, SEQ_4:30;
then A8: lim (s1 + s2) = (s1 . 0) + 0 by A4, SEQ_4:42
.= a by FUNCOP_1:7 ;
A9: lim s1 = s1 . 0 by SEQ_4:26
.= a by FUNCOP_1:7 ;
hence s is convergent by A5, A8, A6, SEQ_2:19; ::_thesis: ( lim s = a & ( for n being Element of NAT holds s . n >= a ) )
thus lim s = a by A5, A8, A9, A6, SEQ_2:20; ::_thesis: for n being Element of NAT holds s . n >= a
let n be Element of NAT ; ::_thesis: s . n >= a
s . n >= s1 . n by A6;
hence s . n >= a by FUNCOP_1:7; ::_thesis: verum
end;
definition
let a be real number ;
let s be Rational_Sequence;
funca #Q s -> Real_Sequence means :Def6: :: PREPOWER:def 6
for n being Element of NAT holds it . n = a #Q (s . n);
existence
ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = a #Q (s . n)
proof
deffunc H1( Element of NAT ) -> set = a #Q (s . $1);
consider s1 being Real_Sequence such that
A1: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
take s1 ; ::_thesis: for n being Element of NAT holds s1 . n = a #Q (s . n)
thus for n being Element of NAT holds s1 . n = a #Q (s . n) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = a #Q (s . n) ) & ( for n being Element of NAT holds b2 . n = a #Q (s . n) ) holds
b1 = b2
proof
let s1, s2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s1 . n = a #Q (s . n) ) & ( for n being Element of NAT holds s2 . n = a #Q (s . n) ) implies s1 = s2 )
assume that
A2: for n being Element of NAT holds s1 . n = a #Q (s . n) and
A3: for n being Element of NAT holds s2 . n = a #Q (s . n) ; ::_thesis: s1 = s2
now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_=_s2_._n
let n be Element of NAT ; ::_thesis: s1 . n = s2 . n
thus s1 . n = a #Q (s . n) by A2
.= s2 . n by A3 ; ::_thesis: verum
end;
hence s1 = s2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines #Q PREPOWER:def_6_:_
for a being real number
for s being Rational_Sequence
for b3 being Real_Sequence holds
( b3 = a #Q s iff for n being Element of NAT holds b3 . n = a #Q (s . n) );
Lm6: for s being Rational_Sequence
for a being real number st s is convergent & a >= 1 holds
a #Q s is convergent
proof
let s be Rational_Sequence; ::_thesis: for a being real number st s is convergent & a >= 1 holds
a #Q s is convergent
let a be real number ; ::_thesis: ( s is convergent & a >= 1 implies a #Q s is convergent )
assume that
A1: s is convergent and
A2: a >= 1 ; ::_thesis: a #Q s is convergent
s is bounded by A1, SEQ_2:13;
then consider d being real number such that
0 < d and
A3: for n being Element of NAT holds abs (s . n) < d by SEQ_2:3;
consider m2 being Element of NAT such that
A4: d < m2 by SEQ_4:3;
reconsider m2 = m2 as Rational ;
now__::_thesis:_for_c_being_real_number_st_c_>_0_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_m_>=_n_holds_
abs_(((a_#Q_s)_._m)_-_((a_#Q_s)_._n))_<_c
A5: a #Q m2 >= 0 by A2, Th52;
let c be real number ; ::_thesis: ( c > 0 implies ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs (((a #Q s) . m) - ((a #Q s) . n)) < c )
assume A6: c > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs (((a #Q s) . m) - ((a #Q s) . n)) < c
consider m1 being Element of NAT such that
A7: ((a #Q m2) * (a - 1)) / c < m1 by SEQ_4:3;
m1 + 1 >= m1 by XREAL_1:29;
then ((a #Q m2) * (a - 1)) / c < m1 + 1 by A7, XXREAL_0:2;
then (((a #Q m2) * (a - 1)) / c) * c < c * (m1 + 1) by A6, XREAL_1:68;
then (a #Q m2) * (a - 1) < c * (m1 + 1) by A6, XCMPLX_1:87;
then ((a #Q m2) * (a - 1)) / (m1 + 1) < ((m1 + 1) * c) / (m1 + 1) by XREAL_1:74;
then ((a #Q m2) * (a - 1)) / (m1 + 1) < (c / (m1 + 1)) * (m1 + 1) ;
then A8: ((a #Q m2) * (a - 1)) / (m1 + 1) < c by XCMPLX_1:87;
consider n being Element of NAT such that
A9: for m being Element of NAT st n <= m holds
abs ((s . m) - (s . n)) < (m1 + 1) " by A1, SEQ_4:41;
take n = n; ::_thesis: for m being Element of NAT st m >= n holds
abs (((a #Q s) . m) - ((a #Q s) . n)) < c
let m be Element of NAT ; ::_thesis: ( m >= n implies abs (((a #Q s) . m) - ((a #Q s) . n)) < c )
assume m >= n ; ::_thesis: abs (((a #Q s) . m) - ((a #Q s) . n)) < c
then A10: abs ((s . m) - (s . n)) <= (m1 + 1) " by A9;
A11: m1 + 1 >= 0 + 1 by NAT_1:13;
then ((m1 + 1) -Root a) - 1 <= (a - 1) / (m1 + 1) by A2, Th31;
then A12: (a #Q m2) * (((m1 + 1) -Root a) - 1) <= (a #Q m2) * ((a - 1) / (m1 + 1)) by A5, XREAL_1:64;
A13: a #Q (s . n) <> 0 by A2, Th52;
A14: abs ((a #Q (s . m)) - (a #Q (s . n))) = abs (((a #Q (s . m)) - (a #Q (s . n))) * 1)
.= abs (((a #Q (s . m)) - (a #Q (s . n))) * ((a #Q (s . n)) / (a #Q (s . n)))) by A13, XCMPLX_1:60
.= abs (((a #Q (s . n)) * ((a #Q (s . m)) - (a #Q (s . n)))) / (a #Q (s . n)))
.= abs ((a #Q (s . n)) * (((a #Q (s . m)) - (a #Q (s . n))) / (a #Q (s . n))))
.= (abs (a #Q (s . n))) * (abs (((a #Q (s . m)) - (a #Q (s . n))) / (a #Q (s . n)))) by COMPLEX1:65
.= (abs (a #Q (s . n))) * (abs (((a #Q (s . m)) / (a #Q (s . n))) - ((a #Q (s . n)) / (a #Q (s . n)))))
.= (abs (a #Q (s . n))) * (abs (((a #Q (s . m)) / (a #Q (s . n))) - 1)) by A13, XCMPLX_1:60
.= (abs (a #Q (s . n))) * (abs ((a #Q ((s . m) - (s . n))) - 1)) by A2, Th55 ;
A15: s . n <= abs (s . n) by ABSVALUE:4;
reconsider m3 = (m1 + 1) " as Rational ;
A16: abs ((a #Q ((s . m) - (s . n))) - 1) >= 0 by COMPLEX1:46;
A17: a #Q ((s . m) - (s . n)) <> 0 by A2, Th52;
(s . m) - (s . n) <= abs ((s . m) - (s . n)) by ABSVALUE:4;
then (s . m) - (s . n) <= (m1 + 1) " by A10, XXREAL_0:2;
then a #Q ((s . m) - (s . n)) <= a #Q m3 by A2, Th63;
then a #Q ((s . m) - (s . n)) <= (m1 + 1) -Root a by A11, Th50;
then A18: (a #Q ((s . m) - (s . n))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:9;
A19: a #Q ((s . m) - (s . n)) > 0 by A2, Th52;
A20: now__::_thesis:_abs_((a_#Q_((s_._m)_-_(s_._n)))_-_1)_<=_((m1_+_1)_-Root_a)_-_1
percases ( (s . m) - (s . n) >= 0 or (s . m) - (s . n) < 0 ) ;
suppose (s . m) - (s . n) >= 0 ; ::_thesis: abs ((a #Q ((s . m) - (s . n))) - 1) <= ((m1 + 1) -Root a) - 1
then a #Q ((s . m) - (s . n)) >= 1 by A2, Th60;
then (a #Q ((s . m) - (s . n))) - 1 >= 0 by XREAL_1:48;
hence abs ((a #Q ((s . m) - (s . n))) - 1) <= ((m1 + 1) -Root a) - 1 by A18, ABSVALUE:def_1; ::_thesis: verum
end;
supposeA21: (s . m) - (s . n) < 0 ; ::_thesis: abs ((a #Q ((s . m) - (s . n))) - 1) <= ((m1 + 1) -Root a) - 1
A22: - ((s . m) - (s . n)) <= abs (- ((s . m) - (s . n))) by ABSVALUE:4;
abs ((s . m) - (s . n)) = abs (- ((s . m) - (s . n))) by COMPLEX1:52;
then - ((s . m) - (s . n)) <= m3 by A10, A22, XXREAL_0:2;
then a #Q (- ((s . m) - (s . n))) <= a #Q m3 by A2, Th63;
then a #Q (- ((s . m) - (s . n))) <= (m1 + 1) -Root a by A11, Th50;
then A23: (a #Q (- ((s . m) - (s . n)))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:9;
a #Q (- ((s . m) - (s . n))) >= 1 by A2, A21, Th60;
then (a #Q (- ((s . m) - (s . n)))) - 1 >= 0 by XREAL_1:48;
then A24: abs ((a #Q (- ((s . m) - (s . n)))) - 1) <= ((m1 + 1) -Root a) - 1 by A23, ABSVALUE:def_1;
a #Q ((s . m) - (s . n)) <= 1 by A2, A21, Th61;
then A25: abs (a #Q ((s . m) - (s . n))) <= 1 by A19, ABSVALUE:def_1;
abs ((a #Q (- ((s . m) - (s . n)))) - 1) >= 0 by COMPLEX1:46;
then A26: (abs (a #Q ((s . m) - (s . n)))) * (abs ((a #Q (- ((s . m) - (s . n)))) - 1)) <= 1 * (abs ((a #Q (- ((s . m) - (s . n)))) - 1)) by A25, XREAL_1:64;
abs ((a #Q ((s . m) - (s . n))) - 1) = abs (((a #Q ((s . m) - (s . n))) - 1) * 1)
.= abs (((a #Q ((s . m) - (s . n))) - 1) * ((a #Q ((s . m) - (s . n))) / (a #Q ((s . m) - (s . n))))) by A17, XCMPLX_1:60
.= abs (((a #Q ((s . m) - (s . n))) * ((a #Q ((s . m) - (s . n))) - 1)) / (a #Q ((s . m) - (s . n))))
.= abs ((a #Q ((s . m) - (s . n))) * (((a #Q ((s . m) - (s . n))) - 1) / (a #Q ((s . m) - (s . n)))))
.= (abs (a #Q ((s . m) - (s . n)))) * (abs (((a #Q ((s . m) - (s . n))) - 1) / (a #Q ((s . m) - (s . n))))) by COMPLEX1:65
.= (abs (a #Q ((s . m) - (s . n)))) * (abs (((a #Q ((s . m) - (s . n))) / (a #Q ((s . m) - (s . n)))) - (1 / (a #Q ((s . m) - (s . n))))))
.= (abs (a #Q ((s . m) - (s . n)))) * (abs (1 - (1 / (a #Q ((s . m) - (s . n)))))) by A17, XCMPLX_1:60
.= (abs (a #Q ((s . m) - (s . n)))) * (abs (1 - (a #Q (- ((s . m) - (s . n)))))) by A2, Th54
.= (abs (a #Q ((s . m) - (s . n)))) * (abs (- (1 - (a #Q (- ((s . m) - (s . n))))))) by COMPLEX1:52
.= (abs (a #Q ((s . m) - (s . n)))) * (abs ((a #Q (- ((s . m) - (s . n)))) - 1)) ;
hence abs ((a #Q ((s . m) - (s . n))) - 1) <= ((m1 + 1) -Root a) - 1 by A24, A26, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A27: a #Q (s . n) > 0 by A2, Th52;
abs (s . n) <= m2 by A3, A4, XXREAL_0:2;
then s . n <= m2 by A15, XXREAL_0:2;
then a #Q (s . n) <= a #Q m2 by A2, Th63;
then A28: abs (a #Q (s . n)) <= a #Q m2 by A27, ABSVALUE:def_1;
abs (a #Q (s . n)) >= 0 by A27, ABSVALUE:def_1;
then (abs (a #Q (s . n))) * (abs ((a #Q ((s . m) - (s . n))) - 1)) <= (a #Q m2) * (((m1 + 1) -Root a) - 1) by A20, A16, A28, XREAL_1:66;
then abs ((a #Q (s . m)) - (a #Q (s . n))) <= ((a #Q m2) * (a - 1)) / (m1 + 1) by A14, A12, XXREAL_0:2;
then abs ((a #Q (s . m)) - (a #Q (s . n))) < c by A8, XXREAL_0:2;
then abs (((a #Q s) . m) - (a #Q (s . n))) < c by Def6;
hence abs (((a #Q s) . m) - ((a #Q s) . n)) < c by Def6; ::_thesis: verum
end;
hence a #Q s is convergent by SEQ_4:41; ::_thesis: verum
end;
theorem Th69: :: PREPOWER:69
for a being real number
for s being Rational_Sequence st s is convergent & a > 0 holds
a #Q s is convergent
proof
let a be real number ; ::_thesis: for s being Rational_Sequence st s is convergent & a > 0 holds
a #Q s is convergent
let s be Rational_Sequence; ::_thesis: ( s is convergent & a > 0 implies a #Q s is convergent )
assume that
A1: s is convergent and
A2: a > 0 ; ::_thesis: a #Q s is convergent
percases ( a >= 1 or a < 1 ) ;
suppose a >= 1 ; ::_thesis: a #Q s is convergent
hence a #Q s is convergent by A1, Lm6; ::_thesis: verum
end;
supposeA3: a < 1 ; ::_thesis: a #Q s is convergent
then a / a < 1 / a by A2, XREAL_1:74;
then 1 < 1 / a by A2, XCMPLX_1:60;
then A4: (1 / a) #Q s is convergent by A1, Lm6;
s is bounded by A1, SEQ_2:13;
then consider d being real number such that
0 < d and
A5: for n being Element of NAT holds abs (s . n) < d by SEQ_2:3;
reconsider d = d as Real by XREAL_0:def_1;
consider m1 being Element of NAT such that
A6: 2 * d < m1 by SEQ_4:3;
reconsider m1 = m1 as Rational ;
A7: a #Q m1 > 0 by A2, Th52;
now__::_thesis:_for_c_being_real_number_st_c_>_0_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_m_>=_n_holds_
abs_(((a_#Q_s)_._m)_-_((a_#Q_s)_._n))_<_c
let c be real number ; ::_thesis: ( c > 0 implies ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs (((a #Q s) . m) - ((a #Q s) . n)) < c )
assume A8: c > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs (((a #Q s) . m) - ((a #Q s) . n)) < c
then c * (a #Q m1) > 0 by A7, XREAL_1:129;
then consider n being Element of NAT such that
A9: for m being Element of NAT st n <= m holds
abs ((((1 / a) #Q s) . m) - (((1 / a) #Q s) . n)) < c * (a #Q m1) by A4, SEQ_4:41;
take n = n; ::_thesis: for m being Element of NAT st m >= n holds
abs (((a #Q s) . m) - ((a #Q s) . n)) < c
let m be Element of NAT ; ::_thesis: ( m >= n implies abs (((a #Q s) . m) - ((a #Q s) . n)) < c )
assume m >= n ; ::_thesis: abs (((a #Q s) . m) - ((a #Q s) . n)) < c
then A10: abs ((((1 / a) #Q s) . m) - (((1 / a) #Q s) . n)) < c * (a #Q m1) by A9;
A11: a #Q (s . m) <> 0 by A2, Th52;
A12: a #Q ((s . m) + (s . n)) > 0 by A2, Th52;
abs (s . m) < d by A5;
then A13: (abs (s . m)) + (abs (s . n)) < d + d by A5, XREAL_1:8;
abs ((s . m) + (s . n)) <= (abs (s . m)) + (abs (s . n)) by COMPLEX1:56;
then abs ((s . m) + (s . n)) < d + d by A13, XXREAL_0:2;
then abs ((s . m) + (s . n)) < m1 by A6, XXREAL_0:2;
then A14: abs (- ((s . m) + (s . n))) < m1 by COMPLEX1:52;
- ((s . m) + (s . n)) <= abs (- ((s . m) + (s . n))) by ABSVALUE:4;
then - ((s . m) + (s . n)) < m1 by A14, XXREAL_0:2;
then A15: m1 - (- ((s . m) + (s . n))) > 0 by XREAL_1:50;
A16: a #Q (s . n) <> 0 by A2, Th52;
abs ((((1 / a) #Q s) . m) - (((1 / a) #Q s) . n)) = abs (((1 / a) #Q (s . m)) - (((1 / a) #Q s) . n)) by Def6
.= abs (((1 / a) #Q (s . m)) - ((1 / a) #Q (s . n))) by Def6
.= abs ((1 / (a #Q (s . m))) - ((1 / a) #Q (s . n))) by A2, Th57
.= abs ((1 / (a #Q (s . m))) - (1 / (a #Q (s . n)))) by A2, Th57
.= abs (((a #Q (s . m)) ") - (1 / (a #Q (s . n))))
.= abs (((a #Q (s . m)) ") - ((a #Q (s . n)) "))
.= (abs ((a #Q (s . m)) - (a #Q (s . n)))) / ((abs (a #Q (s . m))) * (abs (a #Q (s . n)))) by A11, A16, SEQ_2:2
.= (abs ((a #Q (s . m)) - (a #Q (s . n)))) / (abs ((a #Q (s . m)) * (a #Q (s . n)))) by COMPLEX1:65
.= (abs ((a #Q (s . m)) - (a #Q (s . n)))) / (abs (a #Q ((s . m) + (s . n)))) by A2, Th53
.= (abs ((a #Q (s . m)) - (a #Q (s . n)))) / (a #Q ((s . m) + (s . n))) by A12, ABSVALUE:def_1 ;
then A17: ((abs ((a #Q (s . m)) - (a #Q (s . n)))) / (a #Q ((s . m) + (s . n)))) * (a #Q ((s . m) + (s . n))) < (c * (a #Q m1)) * (a #Q ((s . m) + (s . n))) by A10, A12, XREAL_1:68;
a #Q ((s . m) + (s . n)) <> 0 by A2, Th52;
then A18: abs ((a #Q (s . m)) - (a #Q (s . n))) < (c * (a #Q m1)) * (a #Q ((s . m) + (s . n))) by A17, XCMPLX_1:87;
(a #Q m1) * (a #Q ((s . m) + (s . n))) = a #Q (m1 + ((s . m) + (s . n))) by A2, Th53;
then c * ((a #Q m1) * (a #Q ((s . m) + (s . n)))) < 1 * c by A2, A3, A8, A15, Th65, XREAL_1:68;
then abs ((a #Q (s . m)) - (a #Q (s . n))) < c by A18, XXREAL_0:2;
then abs (((a #Q s) . m) - (a #Q (s . n))) < c by Def6;
hence abs (((a #Q s) . m) - ((a #Q s) . n)) < c by Def6; ::_thesis: verum
end;
hence a #Q s is convergent by SEQ_4:41; ::_thesis: verum
end;
end;
end;
Lm7: for s1, s2 being Rational_Sequence
for a being real number st s1 is convergent & s2 is convergent & lim s1 = lim s2 & a >= 1 holds
lim (a #Q s1) = lim (a #Q s2)
proof
let s1, s2 be Rational_Sequence; ::_thesis: for a being real number st s1 is convergent & s2 is convergent & lim s1 = lim s2 & a >= 1 holds
lim (a #Q s1) = lim (a #Q s2)
let a be real number ; ::_thesis: ( s1 is convergent & s2 is convergent & lim s1 = lim s2 & a >= 1 implies lim (a #Q s1) = lim (a #Q s2) )
assume that
A1: s1 is convergent and
A2: s2 is convergent and
A3: lim s1 = lim s2 and
A4: a >= 1 ; ::_thesis: lim (a #Q s1) = lim (a #Q s2)
A5: s1 - s2 is convergent by A1, A2, SEQ_2:11;
A6: a #Q s2 is convergent by A2, A4, Th69;
A7: now__::_thesis:_for_n_being_Element_of_NAT_holds_(((a_#Q_s1)_-_(a_#Q_s2))_+_(a_#Q_s2))_._n_=_(a_#Q_s1)_._n
let n be Element of NAT ; ::_thesis: (((a #Q s1) - (a #Q s2)) + (a #Q s2)) . n = (a #Q s1) . n
thus (((a #Q s1) - (a #Q s2)) + (a #Q s2)) . n = (((a #Q s1) - (a #Q s2)) . n) + ((a #Q s2) . n) by SEQ_1:7
.= (((a #Q s1) . n) - ((a #Q s2) . n)) + ((a #Q s2) . n) by RFUNCT_2:1
.= (a #Q s1) . n ; ::_thesis: verum
end;
s2 is bounded by A2, SEQ_2:13;
then consider d being real number such that
0 < d and
A8: for n being Element of NAT holds abs (s2 . n) < d by SEQ_2:3;
consider m2 being Element of NAT such that
A9: d < m2 by SEQ_4:3;
reconsider m2 = m2 as Rational ;
A10: lim (s1 - s2) = (lim s1) - (lim s2) by A1, A2, SEQ_2:12
.= 0 by A3 ;
A11: now__::_thesis:_for_c_being_real_number_st_c_>_0_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_m_>=_n_holds_
abs_((((a_#Q_s1)_-_(a_#Q_s2))_._m)_-_0)_<_c
A12: a #Q m2 >= 0 by A4, Th52;
let c be real number ; ::_thesis: ( c > 0 implies ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs ((((a #Q s1) - (a #Q s2)) . m) - 0) < c )
assume A13: c > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs ((((a #Q s1) - (a #Q s2)) . m) - 0) < c
consider m1 being Element of NAT such that
A14: ((a #Q m2) * (a - 1)) / c < m1 by SEQ_4:3;
m1 + 1 >= m1 by XREAL_1:29;
then ((a #Q m2) * (a - 1)) / c < m1 + 1 by A14, XXREAL_0:2;
then (((a #Q m2) * (a - 1)) / c) * c < c * (m1 + 1) by A13, XREAL_1:68;
then (a #Q m2) * (a - 1) < c * (m1 + 1) by A13, XCMPLX_1:87;
then ((a #Q m2) * (a - 1)) / (m1 + 1) < ((m1 + 1) * c) / (m1 + 1) by XREAL_1:74;
then ((a #Q m2) * (a - 1)) / (m1 + 1) < (c / (m1 + 1)) * (m1 + 1) ;
then A15: ((a #Q m2) * (a - 1)) / (m1 + 1) < c by XCMPLX_1:87;
consider n being Element of NAT such that
A16: for m being Element of NAT st n <= m holds
abs (((s1 - s2) . m) - 0) < (m1 + 1) " by A5, A10, SEQ_2:def_7;
take n = n; ::_thesis: for m being Element of NAT st m >= n holds
abs ((((a #Q s1) - (a #Q s2)) . m) - 0) < c
let m be Element of NAT ; ::_thesis: ( m >= n implies abs ((((a #Q s1) - (a #Q s2)) . m) - 0) < c )
assume m >= n ; ::_thesis: abs ((((a #Q s1) - (a #Q s2)) . m) - 0) < c
then abs (((s1 - s2) . m) - 0) < (m1 + 1) " by A16;
then A17: abs ((s1 . m) - (s2 . m)) <= (m1 + 1) " by RFUNCT_2:1;
A18: m1 + 1 >= 0 + 1 by NAT_1:13;
then ((m1 + 1) -Root a) - 1 <= (a - 1) / (m1 + 1) by A4, Th31;
then A19: (a #Q m2) * (((m1 + 1) -Root a) - 1) <= (a #Q m2) * ((a - 1) / (m1 + 1)) by A12, XREAL_1:64;
A20: a #Q (s2 . m) <> 0 by A4, Th52;
A21: abs ((a #Q (s1 . m)) - (a #Q (s2 . m))) = abs (((a #Q (s1 . m)) - (a #Q (s2 . m))) * 1)
.= abs (((a #Q (s1 . m)) - (a #Q (s2 . m))) * ((a #Q (s2 . m)) / (a #Q (s2 . m)))) by A20, XCMPLX_1:60
.= abs (((a #Q (s2 . m)) * ((a #Q (s1 . m)) - (a #Q (s2 . m)))) / (a #Q (s2 . m)))
.= abs ((a #Q (s2 . m)) * (((a #Q (s1 . m)) - (a #Q (s2 . m))) / (a #Q (s2 . m))))
.= (abs (a #Q (s2 . m))) * (abs (((a #Q (s1 . m)) - (a #Q (s2 . m))) / (a #Q (s2 . m)))) by COMPLEX1:65
.= (abs (a #Q (s2 . m))) * (abs (((a #Q (s1 . m)) / (a #Q (s2 . m))) - ((a #Q (s2 . m)) / (a #Q (s2 . m)))))
.= (abs (a #Q (s2 . m))) * (abs (((a #Q (s1 . m)) / (a #Q (s2 . m))) - 1)) by A20, XCMPLX_1:60
.= (abs (a #Q (s2 . m))) * (abs ((a #Q ((s1 . m) - (s2 . m))) - 1)) by A4, Th55 ;
A22: s2 . m <= abs (s2 . m) by ABSVALUE:4;
reconsider m3 = (m1 + 1) " as Rational ;
A23: abs ((a #Q ((s1 . m) - (s2 . m))) - 1) >= 0 by COMPLEX1:46;
A24: a #Q ((s1 . m) - (s2 . m)) <> 0 by A4, Th52;
(s1 . m) - (s2 . m) <= abs ((s1 . m) - (s2 . m)) by ABSVALUE:4;
then (s1 . m) - (s2 . m) <= (m1 + 1) " by A17, XXREAL_0:2;
then a #Q ((s1 . m) - (s2 . m)) <= a #Q m3 by A4, Th63;
then a #Q ((s1 . m) - (s2 . m)) <= (m1 + 1) -Root a by A18, Th50;
then A25: (a #Q ((s1 . m) - (s2 . m))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:9;
A26: a #Q ((s1 . m) - (s2 . m)) > 0 by A4, Th52;
A27: now__::_thesis:_abs_((a_#Q_((s1_._m)_-_(s2_._m)))_-_1)_<=_((m1_+_1)_-Root_a)_-_1
percases ( (s1 . m) - (s2 . m) >= 0 or (s1 . m) - (s2 . m) < 0 ) ;
suppose (s1 . m) - (s2 . m) >= 0 ; ::_thesis: abs ((a #Q ((s1 . m) - (s2 . m))) - 1) <= ((m1 + 1) -Root a) - 1
then a #Q ((s1 . m) - (s2 . m)) >= 1 by A4, Th60;
then (a #Q ((s1 . m) - (s2 . m))) - 1 >= 0 by XREAL_1:48;
hence abs ((a #Q ((s1 . m) - (s2 . m))) - 1) <= ((m1 + 1) -Root a) - 1 by A25, ABSVALUE:def_1; ::_thesis: verum
end;
supposeA28: (s1 . m) - (s2 . m) < 0 ; ::_thesis: abs ((a #Q ((s1 . m) - (s2 . m))) - 1) <= ((m1 + 1) -Root a) - 1
A29: - ((s1 . m) - (s2 . m)) <= abs (- ((s1 . m) - (s2 . m))) by ABSVALUE:4;
abs ((s1 . m) - (s2 . m)) = abs (- ((s1 . m) - (s2 . m))) by COMPLEX1:52;
then - ((s1 . m) - (s2 . m)) <= m3 by A17, A29, XXREAL_0:2;
then a #Q (- ((s1 . m) - (s2 . m))) <= a #Q m3 by A4, Th63;
then a #Q (- ((s1 . m) - (s2 . m))) <= (m1 + 1) -Root a by A18, Th50;
then A30: (a #Q (- ((s1 . m) - (s2 . m)))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:9;
a #Q (- ((s1 . m) - (s2 . m))) >= 1 by A4, A28, Th60;
then (a #Q (- ((s1 . m) - (s2 . m)))) - 1 >= 0 by XREAL_1:48;
then A31: abs ((a #Q (- ((s1 . m) - (s2 . m)))) - 1) <= ((m1 + 1) -Root a) - 1 by A30, ABSVALUE:def_1;
a #Q ((s1 . m) - (s2 . m)) <= 1 by A4, A28, Th61;
then A32: abs (a #Q ((s1 . m) - (s2 . m))) <= 1 by A26, ABSVALUE:def_1;
abs ((a #Q (- ((s1 . m) - (s2 . m)))) - 1) >= 0 by COMPLEX1:46;
then A33: (abs (a #Q ((s1 . m) - (s2 . m)))) * (abs ((a #Q (- ((s1 . m) - (s2 . m)))) - 1)) <= 1 * (abs ((a #Q (- ((s1 . m) - (s2 . m)))) - 1)) by A32, XREAL_1:64;
abs ((a #Q ((s1 . m) - (s2 . m))) - 1) = abs (((a #Q ((s1 . m) - (s2 . m))) - 1) * 1)
.= abs (((a #Q ((s1 . m) - (s2 . m))) - 1) * ((a #Q ((s1 . m) - (s2 . m))) / (a #Q ((s1 . m) - (s2 . m))))) by A24, XCMPLX_1:60
.= abs (((a #Q ((s1 . m) - (s2 . m))) * ((a #Q ((s1 . m) - (s2 . m))) - 1)) / (a #Q ((s1 . m) - (s2 . m))))
.= abs ((a #Q ((s1 . m) - (s2 . m))) * (((a #Q ((s1 . m) - (s2 . m))) - 1) / (a #Q ((s1 . m) - (s2 . m)))))
.= (abs (a #Q ((s1 . m) - (s2 . m)))) * (abs (((a #Q ((s1 . m) - (s2 . m))) - 1) / (a #Q ((s1 . m) - (s2 . m))))) by COMPLEX1:65
.= (abs (a #Q ((s1 . m) - (s2 . m)))) * (abs (((a #Q ((s1 . m) - (s2 . m))) / (a #Q ((s1 . m) - (s2 . m)))) - (1 / (a #Q ((s1 . m) - (s2 . m))))))
.= (abs (a #Q ((s1 . m) - (s2 . m)))) * (abs (1 - (1 / (a #Q ((s1 . m) - (s2 . m)))))) by A24, XCMPLX_1:60
.= (abs (a #Q ((s1 . m) - (s2 . m)))) * (abs (1 - (a #Q (- ((s1 . m) - (s2 . m)))))) by A4, Th54
.= (abs (a #Q ((s1 . m) - (s2 . m)))) * (abs (- (1 - (a #Q (- ((s1 . m) - (s2 . m))))))) by COMPLEX1:52
.= (abs (a #Q ((s1 . m) - (s2 . m)))) * (abs ((a #Q (- ((s1 . m) - (s2 . m)))) - 1)) ;
hence abs ((a #Q ((s1 . m) - (s2 . m))) - 1) <= ((m1 + 1) -Root a) - 1 by A31, A33, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A34: a #Q (s2 . m) > 0 by A4, Th52;
abs (s2 . m) <= m2 by A8, A9, XXREAL_0:2;
then s2 . m <= m2 by A22, XXREAL_0:2;
then a #Q (s2 . m) <= a #Q m2 by A4, Th63;
then A35: abs (a #Q (s2 . m)) <= a #Q m2 by A34, ABSVALUE:def_1;
abs (a #Q (s2 . m)) >= 0 by A34, ABSVALUE:def_1;
then (abs (a #Q (s2 . m))) * (abs ((a #Q ((s1 . m) - (s2 . m))) - 1)) <= (a #Q m2) * (((m1 + 1) -Root a) - 1) by A27, A23, A35, XREAL_1:66;
then abs ((a #Q (s1 . m)) - (a #Q (s2 . m))) <= ((a #Q m2) * (a - 1)) / (m1 + 1) by A21, A19, XXREAL_0:2;
then abs ((a #Q (s1 . m)) - (a #Q (s2 . m))) < c by A15, XXREAL_0:2;
then abs (((a #Q s1) . m) - (a #Q (s2 . m))) < c by Def6;
then abs (((a #Q s1) . m) - ((a #Q s2) . m)) < c by Def6;
hence abs ((((a #Q s1) - (a #Q s2)) . m) - 0) < c by RFUNCT_2:1; ::_thesis: verum
end;
then A36: (a #Q s1) - (a #Q s2) is convergent by SEQ_2:def_6;
then lim ((a #Q s1) - (a #Q s2)) = 0 by A11, SEQ_2:def_7;
then lim (((a #Q s1) - (a #Q s2)) + (a #Q s2)) = 0 + (lim (a #Q s2)) by A36, A6, SEQ_2:6
.= lim (a #Q s2) ;
hence lim (a #Q s1) = lim (a #Q s2) by A7, FUNCT_2:63; ::_thesis: verum
end;
theorem Th70: :: PREPOWER:70
for s1, s2 being Rational_Sequence
for a being real number st s1 is convergent & s2 is convergent & lim s1 = lim s2 & a > 0 holds
( a #Q s1 is convergent & a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) )
proof
let s1, s2 be Rational_Sequence; ::_thesis: for a being real number st s1 is convergent & s2 is convergent & lim s1 = lim s2 & a > 0 holds
( a #Q s1 is convergent & a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) )
let a be real number ; ::_thesis: ( s1 is convergent & s2 is convergent & lim s1 = lim s2 & a > 0 implies ( a #Q s1 is convergent & a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) ) )
assume that
A1: s1 is convergent and
A2: s2 is convergent and
A3: lim s1 = lim s2 and
A4: a > 0 ; ::_thesis: ( a #Q s1 is convergent & a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) )
thus A5: a #Q s1 is convergent by A1, A4, Th69; ::_thesis: ( a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) )
s2 is bounded by A2, SEQ_2:13;
then consider e being real number such that
0 < e and
A6: for n being Element of NAT holds abs (s2 . n) < e by SEQ_2:3;
s1 is bounded by A1, SEQ_2:13;
then consider d being real number such that
0 < d and
A7: for n being Element of NAT holds abs (s1 . n) < d by SEQ_2:3;
consider m1 being Element of NAT such that
A8: d + e < m1 by SEQ_4:3;
thus A9: a #Q s2 is convergent by A2, A4, Th69; ::_thesis: lim (a #Q s1) = lim (a #Q s2)
reconsider m1 = m1 as Rational ;
A10: a #Q m1 > 0 by A4, Th52;
percases ( a >= 1 or a < 1 ) ;
suppose a >= 1 ; ::_thesis: lim (a #Q s1) = lim (a #Q s2)
hence lim (a #Q s1) = lim (a #Q s2) by A1, A2, A3, Lm7; ::_thesis: verum
end;
supposeA11: a < 1 ; ::_thesis: lim (a #Q s1) = lim (a #Q s2)
then a / a < 1 / a by A4, XREAL_1:74;
then 1 < 1 / a by A4, XCMPLX_1:60;
then A12: lim ((1 / a) #Q s1) = lim ((1 / a) #Q s2) by A1, A2, A3, Lm7;
A13: (1 / a) #Q s2 is convergent by A2, A4, Th69;
A14: (1 / a) #Q s1 is convergent by A1, A4, Th69;
then A15: ((1 / a) #Q s1) - ((1 / a) #Q s2) is convergent by A13, SEQ_2:11;
A16: lim (((1 / a) #Q s1) - ((1 / a) #Q s2)) = (lim ((1 / a) #Q s1)) - (lim ((1 / a) #Q s2)) by A14, A13, SEQ_2:12
.= 0 by A12 ;
A17: now__::_thesis:_for_c_being_real_number_st_c_>_0_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_m_>=_n_holds_
abs_((((a_#Q_s1)_-_(a_#Q_s2))_._m)_-_0)_<_c
let c be real number ; ::_thesis: ( c > 0 implies ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs ((((a #Q s1) - (a #Q s2)) . m) - 0) < c )
assume A18: c > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs ((((a #Q s1) - (a #Q s2)) . m) - 0) < c
then c * (a #Q m1) > 0 by A10, XREAL_1:129;
then consider n being Element of NAT such that
A19: for m being Element of NAT st n <= m holds
abs (((((1 / a) #Q s1) - ((1 / a) #Q s2)) . m) - 0) < c * (a #Q m1) by A15, A16, SEQ_2:def_7;
take n = n; ::_thesis: for m being Element of NAT st m >= n holds
abs ((((a #Q s1) - (a #Q s2)) . m) - 0) < c
let m be Element of NAT ; ::_thesis: ( m >= n implies abs ((((a #Q s1) - (a #Q s2)) . m) - 0) < c )
assume m >= n ; ::_thesis: abs ((((a #Q s1) - (a #Q s2)) . m) - 0) < c
then abs (((((1 / a) #Q s1) - ((1 / a) #Q s2)) . m) - 0) < c * (a #Q m1) by A19;
then A20: abs ((((1 / a) #Q s1) . m) - (((1 / a) #Q s2) . m)) < c * (a #Q m1) by RFUNCT_2:1;
A21: a #Q (s1 . m) <> 0 by A4, Th52;
abs (s1 . m) < d by A7;
then A22: (abs (s1 . m)) + (abs (s2 . m)) < d + e by A6, XREAL_1:8;
abs ((s1 . m) + (s2 . m)) <= (abs (s1 . m)) + (abs (s2 . m)) by COMPLEX1:56;
then abs ((s1 . m) + (s2 . m)) < d + e by A22, XXREAL_0:2;
then abs ((s1 . m) + (s2 . m)) < m1 by A8, XXREAL_0:2;
then A23: abs (- ((s1 . m) + (s2 . m))) < m1 by COMPLEX1:52;
- ((s1 . m) + (s2 . m)) <= abs (- ((s1 . m) + (s2 . m))) by ABSVALUE:4;
then - ((s1 . m) + (s2 . m)) < m1 by A23, XXREAL_0:2;
then A24: m1 - (- ((s1 . m) + (s2 . m))) > 0 by XREAL_1:50;
A25: a #Q (s2 . m) <> 0 by A4, Th52;
A26: a #Q ((s1 . m) + (s2 . m)) > 0 by A4, Th52;
abs ((((1 / a) #Q s1) . m) - (((1 / a) #Q s2) . m)) = abs (((1 / a) #Q (s1 . m)) - (((1 / a) #Q s2) . m)) by Def6
.= abs (((1 / a) #Q (s1 . m)) - ((1 / a) #Q (s2 . m))) by Def6
.= abs ((1 / (a #Q (s1 . m))) - ((1 / a) #Q (s2 . m))) by A4, Th57
.= abs ((1 / (a #Q (s1 . m))) - (1 / (a #Q (s2 . m)))) by A4, Th57
.= abs (((a #Q (s1 . m)) ") - (1 / (a #Q (s2 . m))))
.= abs (((a #Q (s1 . m)) ") - ((a #Q (s2 . m)) "))
.= (abs ((a #Q (s1 . m)) - (a #Q (s2 . m)))) / ((abs (a #Q (s1 . m))) * (abs (a #Q (s2 . m)))) by A21, A25, SEQ_2:2
.= (abs ((a #Q (s1 . m)) - (a #Q (s2 . m)))) / (abs ((a #Q (s1 . m)) * (a #Q (s2 . m)))) by COMPLEX1:65
.= (abs ((a #Q (s1 . m)) - (a #Q (s2 . m)))) / (abs (a #Q ((s1 . m) + (s2 . m)))) by A4, Th53
.= (abs ((a #Q (s1 . m)) - (a #Q (s2 . m)))) / (a #Q ((s1 . m) + (s2 . m))) by A26, ABSVALUE:def_1 ;
then A27: ((abs ((a #Q (s1 . m)) - (a #Q (s2 . m)))) / (a #Q ((s1 . m) + (s2 . m)))) * (a #Q ((s1 . m) + (s2 . m))) < (c * (a #Q m1)) * (a #Q ((s1 . m) + (s2 . m))) by A20, A26, XREAL_1:68;
a #Q ((s1 . m) + (s2 . m)) <> 0 by A4, Th52;
then A28: abs ((a #Q (s1 . m)) - (a #Q (s2 . m))) < (c * (a #Q m1)) * (a #Q ((s1 . m) + (s2 . m))) by A27, XCMPLX_1:87;
(a #Q m1) * (a #Q ((s1 . m) + (s2 . m))) = a #Q (m1 + ((s1 . m) + (s2 . m))) by A4, Th53;
then c * ((a #Q m1) * (a #Q ((s1 . m) + (s2 . m)))) < 1 * c by A4, A11, A18, A24, Th65, XREAL_1:68;
then abs ((a #Q (s1 . m)) - (a #Q (s2 . m))) < c by A28, XXREAL_0:2;
then abs (((a #Q s1) . m) - (a #Q (s2 . m))) < c by Def6;
then abs (((a #Q s1) . m) - ((a #Q s2) . m)) < c by Def6;
hence abs ((((a #Q s1) - (a #Q s2)) . m) - 0) < c by RFUNCT_2:1; ::_thesis: verum
end;
then (a #Q s1) - (a #Q s2) is convergent by SEQ_2:def_6;
then lim ((a #Q s1) - (a #Q s2)) = 0 by A17, SEQ_2:def_7;
then 0 = (lim (a #Q s1)) - (lim (a #Q s2)) by A5, A9, SEQ_2:12;
hence lim (a #Q s1) = lim (a #Q s2) ; ::_thesis: verum
end;
end;
end;
definition
let a, b be real number ;
assume A1: a > 0 ;
funca #R b -> real number means :Def7: :: PREPOWER:def 7
ex s being Rational_Sequence st
( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = it );
existence
ex b1 being real number ex s being Rational_Sequence st
( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b1 )
proof
consider s being Rational_Sequence such that
A2: s is convergent and
A3: lim s = b and
for n being Element of NAT holds s . n <= b by Th67;
take lim (a #Q s) ; ::_thesis: ex s being Rational_Sequence st
( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = lim (a #Q s) )
thus ex s being Rational_Sequence st
( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = lim (a #Q s) ) by A1, A2, A3, Th69; ::_thesis: verum
end;
uniqueness
for b1, b2 being real number st ex s being Rational_Sequence st
( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b1 ) & ex s being Rational_Sequence st
( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b2 ) holds
b1 = b2 by A1, Th70;
end;
:: deftheorem Def7 defines #R PREPOWER:def_7_:_
for a, b being real number st a > 0 holds
for b3 being real number holds
( b3 = a #R b iff ex s being Rational_Sequence st
( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b3 ) );
definition
let a, b be Real;
:: original: #R
redefine funca #R b -> Real;
coherence
a #R b is Real by XREAL_0:def_1;
end;
theorem Th71: :: PREPOWER:71
for a being real number st a > 0 holds
a #R 0 = 1
proof
let a be real number ; ::_thesis: ( a > 0 implies a #R 0 = 1 )
reconsider s = NAT --> 0 as Real_Sequence by FUNCOP_1:45;
reconsider s = s as Rational_Sequence ;
assume A1: a > 0 ; ::_thesis: a #R 0 = 1
s . 0 = 0 by FUNCOP_1:7;
then A2: lim s = 0 by SEQ_4:26;
A3: now__::_thesis:_for_n_being_Nat_holds_(a_#Q_s)_._n_=_1
let n be Nat; ::_thesis: (a #Q s) . n = 1
reconsider nn = n as Element of NAT by ORDINAL1:def_12;
thus (a #Q s) . n = a #Q (s . nn) by Def6
.= 1 by Th47, FUNCOP_1:7 ; ::_thesis: verum
end;
then A4: a #Q s is constant by VALUED_0:def_18;
(a #Q s) . 0 = 1 by A3;
then lim (a #Q s) = 1 by A4, SEQ_4:26;
hence a #R 0 = 1 by A1, A2, A4, Def7; ::_thesis: verum
end;
theorem :: PREPOWER:72
for a being real number st a > 0 holds
a #R 1 = a
proof
let a be real number ; ::_thesis: ( a > 0 implies a #R 1 = a )
reconsider s = NAT --> 1 as Real_Sequence by FUNCOP_1:45;
reconsider s = s as Rational_Sequence ;
s . 0 = 1 by FUNCOP_1:7;
then A1: lim s = 1 by SEQ_4:26;
assume A2: a > 0 ; ::_thesis: a #R 1 = a
A3: now__::_thesis:_for_n_being_Nat_holds_(a_#Q_s)_._n_=_a
let n be Nat; ::_thesis: (a #Q s) . n = a
reconsider nn = n as Element of NAT by ORDINAL1:def_12;
thus (a #Q s) . n = a #Q (s . nn) by Def6
.= a by A2, Th48, FUNCOP_1:7 ; ::_thesis: verum
end;
a in REAL by XREAL_0:def_1;
then A4: a #Q s is constant by A3, VALUED_0:def_18;
(a #Q s) . 0 = a by A3;
then lim (a #Q s) = a by A4, SEQ_4:26;
hence a #R 1 = a by A2, A1, A4, Def7; ::_thesis: verum
end;
theorem Th73: :: PREPOWER:73
for a being real number holds 1 #R a = 1
proof
let a be real number ; ::_thesis: 1 #R a = 1
consider s being Rational_Sequence such that
A1: s is convergent and
A2: a = lim s and
for n being Element of NAT holds s . n <= a by Th67;
A3: now__::_thesis:_for_n_being_Nat_holds_(1_#Q_s)_._n_=_1
let n be Nat; ::_thesis: (1 #Q s) . n = 1
reconsider nn = n as Element of NAT by ORDINAL1:def_12;
thus (1 #Q s) . n = 1 #Q (s . nn) by Def6
.= 1 by Th51 ; ::_thesis: verum
end;
then 1 #Q s is constant by VALUED_0:def_18;
then A4: lim (1 #Q s) = (1 #Q s) . 0 by SEQ_4:26
.= 1 by A3 ;
1 #Q s is convergent by A1, Th69;
hence 1 #R a = 1 by A1, A2, A4, Def7; ::_thesis: verum
end;
theorem Th74: :: PREPOWER:74
for a being real number
for p being Rational st a > 0 holds
a #R p = a #Q p
proof
let a be real number ; ::_thesis: for p being Rational st a > 0 holds
a #R p = a #Q p
let p be Rational; ::_thesis: ( a > 0 implies a #R p = a #Q p )
assume A1: a > 0 ; ::_thesis: a #R p = a #Q p
p in REAL by XREAL_0:def_1;
then reconsider s = NAT --> p as Real_Sequence by FUNCOP_1:45;
A2: lim s = s . 0 by SEQ_4:26
.= p by FUNCOP_1:7 ;
reconsider s = s as Rational_Sequence ;
A3: now__::_thesis:_for_n_being_Nat_holds_(a_#Q_s)_._n_=_a_#Q_p
let n be Nat; ::_thesis: (a #Q s) . n = a #Q p
reconsider nn = n as Element of NAT by ORDINAL1:def_12;
thus (a #Q s) . n = a #Q (s . nn) by Def6
.= a #Q p by FUNCOP_1:7 ; ::_thesis: verum
end;
a #Q p in REAL by XREAL_0:def_1;
then A4: a #Q s is constant by A3, VALUED_0:def_18;
then lim (a #Q s) = (a #Q s) . 0 by SEQ_4:26
.= a #Q p by A3 ;
hence a #R p = a #Q p by A1, A2, A4, Def7; ::_thesis: verum
end;
theorem Th75: :: PREPOWER:75
for a, b, c being real number st a > 0 holds
a #R (b + c) = (a #R b) * (a #R c)
proof
let a, b, c be real number ; ::_thesis: ( a > 0 implies a #R (b + c) = (a #R b) * (a #R c) )
consider sb being Rational_Sequence such that
A1: sb is convergent and
A2: b = lim sb and
for n being Element of NAT holds sb . n <= b by Th67;
consider sc being Rational_Sequence such that
A3: sc is convergent and
A4: c = lim sc and
for n being Element of NAT holds sc . n <= c by Th67;
assume A5: a > 0 ; ::_thesis: a #R (b + c) = (a #R b) * (a #R c)
then A6: a #Q sb is convergent by A1, Th69;
A7: a #Q sc is convergent by A5, A3, Th69;
reconsider s = sb + sc as Rational_Sequence ;
A8: lim s = b + c by A1, A2, A3, A4, SEQ_2:6;
A9: now__::_thesis:_for_n_being_Element_of_NAT_holds_(a_#Q_s)_._n_=_((a_#Q_sb)_._n)_*_((a_#Q_sc)_._n)
let n be Element of NAT ; ::_thesis: (a #Q s) . n = ((a #Q sb) . n) * ((a #Q sc) . n)
thus (a #Q s) . n = a #Q (s . n) by Def6
.= a #Q ((sb . n) + (sc . n)) by SEQ_1:7
.= (a #Q (sb . n)) * (a #Q (sc . n)) by A5, Th53
.= (a #Q (sb . n)) * ((a #Q sc) . n) by Def6
.= ((a #Q sb) . n) * ((a #Q sc) . n) by Def6 ; ::_thesis: verum
end;
A10: s is convergent by A1, A3, SEQ_2:5;
then a #Q s is convergent by A5, Th69;
hence a #R (b + c) = lim (a #Q s) by A5, A10, A8, Def7
.= lim ((a #Q sb) (#) (a #Q sc)) by A9, SEQ_1:8
.= (lim (a #Q sb)) * (lim (a #Q sc)) by A6, A7, SEQ_2:15
.= (a #R b) * (lim (a #Q sc)) by A5, A1, A2, A6, Def7
.= (a #R b) * (a #R c) by A5, A3, A4, A7, Def7 ;
::_thesis: verum
end;
Lm8: for a, b being real number st a > 0 holds
a #R b >= 0
proof
let a, b be real number ; ::_thesis: ( a > 0 implies a #R b >= 0 )
consider s being Rational_Sequence such that
A1: s is convergent and
A2: b = lim s and
for n being Element of NAT holds s . n <= b by Th67;
assume A3: a > 0 ; ::_thesis: a #R b >= 0
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_(a_#Q_s)_._n_>=_0
let n be Element of NAT ; ::_thesis: (a #Q s) . n >= 0
(a #Q s) . n = a #Q (s . n) by Def6;
hence (a #Q s) . n >= 0 by A3, Th52; ::_thesis: verum
end;
a #Q s is convergent by A3, A1, Th69;
then a #R b = lim (a #Q s) by A3, A1, A2, Def7;
hence a #R b >= 0 by A3, A1, A4, Th69, SEQ_2:17; ::_thesis: verum
end;
Lm9: for a, b being real number st a > 0 holds
a #R b <> 0
proof
let a, b be real number ; ::_thesis: ( a > 0 implies a #R b <> 0 )
assume A1: a > 0 ; ::_thesis: a #R b <> 0
assume a #R b = 0 ; ::_thesis: contradiction
then 0 = (a #R b) * (a #R (- b))
.= a #R (b + (- b)) by A1, Th75
.= 1 by A1, Th71 ;
hence contradiction ; ::_thesis: verum
end;
theorem Th76: :: PREPOWER:76
for a, c being real number st a > 0 holds
a #R (- c) = 1 / (a #R c)
proof
let a, c be real number ; ::_thesis: ( a > 0 implies a #R (- c) = 1 / (a #R c) )
assume A1: a > 0 ; ::_thesis: a #R (- c) = 1 / (a #R c)
then 1 = a #R (c + (- c)) by Th71
.= (a #R (- c)) * (a #R c) by A1, Th75 ;
then 1 / (a #R c) = (a #R (- c)) * ((a #R c) / (a #R c)) by XCMPLX_1:74
.= (a #R (- c)) * 1 by A1, Lm9, XCMPLX_1:60 ;
hence a #R (- c) = 1 / (a #R c) ; ::_thesis: verum
end;
theorem Th77: :: PREPOWER:77
for a, b, c being real number st a > 0 holds
a #R (b - c) = (a #R b) / (a #R c)
proof
let a, b, c be real number ; ::_thesis: ( a > 0 implies a #R (b - c) = (a #R b) / (a #R c) )
assume A1: a > 0 ; ::_thesis: a #R (b - c) = (a #R b) / (a #R c)
thus a #R (b - c) = a #R (b + (- c))
.= (a #R b) * (a #R (- c)) by A1, Th75
.= (a #R b) * (1 / (a #R c)) by A1, Th76
.= (a #R b) * (1 * ((a #R c) "))
.= (a #R b) / (a #R c) ; ::_thesis: verum
end;
theorem Th78: :: PREPOWER:78
for a, b, c being real number st a > 0 & b > 0 holds
(a * b) #R c = (a #R c) * (b #R c)
proof
let a, b, c be real number ; ::_thesis: ( a > 0 & b > 0 implies (a * b) #R c = (a #R c) * (b #R c) )
assume that
A1: a > 0 and
A2: b > 0 ; ::_thesis: (a * b) #R c = (a #R c) * (b #R c)
A3: a * b > 0 by A1, A2, XREAL_1:129;
consider s1 being Rational_Sequence such that
A4: s1 is convergent and
A5: c = lim s1 and
for n being Element of NAT holds s1 . n >= c by Th68;
A6: a #Q s1 is convergent by A1, A4, Th69;
A7: b #Q s1 is convergent by A2, A4, Th69;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((a_*_b)_#Q_s1)_._n_=_((a_#Q_s1)_._n)_*_((b_#Q_s1)_._n)
let n be Element of NAT ; ::_thesis: ((a * b) #Q s1) . n = ((a #Q s1) . n) * ((b #Q s1) . n)
thus ((a * b) #Q s1) . n = (a * b) #Q (s1 . n) by Def6
.= (a #Q (s1 . n)) * (b #Q (s1 . n)) by A1, A2, Th56
.= ((a #Q s1) . n) * (b #Q (s1 . n)) by Def6
.= ((a #Q s1) . n) * ((b #Q s1) . n) by Def6 ; ::_thesis: verum
end;
then A8: (a * b) #Q s1 = (a #Q s1) (#) (b #Q s1) by SEQ_1:8;
then (a * b) #Q s1 is convergent by A6, A7, SEQ_2:14;
hence (a * b) #R c = lim ((a * b) #Q s1) by A3, A4, A5, Def7
.= (lim (a #Q s1)) * (lim (b #Q s1)) by A6, A7, A8, SEQ_2:15
.= (a #R c) * (lim (b #Q s1)) by A1, A4, A5, A6, Def7
.= (a #R c) * (b #R c) by A2, A4, A5, A7, Def7 ;
::_thesis: verum
end;
theorem Th79: :: PREPOWER:79
for a, c being real number st a > 0 holds
(1 / a) #R c = 1 / (a #R c)
proof
let a, c be real number ; ::_thesis: ( a > 0 implies (1 / a) #R c = 1 / (a #R c) )
assume A1: a > 0 ; ::_thesis: (1 / a) #R c = 1 / (a #R c)
1 = 1 #R c by Th73
.= ((1 / a) * a) #R c by A1, XCMPLX_1:106
.= ((1 / a) #R c) * (a #R c) by A1, Th78 ;
then 1 / (a #R c) = ((1 / a) #R c) * ((a #R c) / (a #R c)) by XCMPLX_1:74
.= ((1 / a) #R c) * 1 by A1, Lm9, XCMPLX_1:60 ;
hence (1 / a) #R c = 1 / (a #R c) ; ::_thesis: verum
end;
theorem :: PREPOWER:80
for a, b, c being real number st a > 0 & b > 0 holds
(a / b) #R c = (a #R c) / (b #R c)
proof
let a, b, c be real number ; ::_thesis: ( a > 0 & b > 0 implies (a / b) #R c = (a #R c) / (b #R c) )
assume that
A1: a > 0 and
A2: b > 0 ; ::_thesis: (a / b) #R c = (a #R c) / (b #R c)
thus (a / b) #R c = (a * (b ")) #R c
.= (a #R c) * ((b ") #R c) by A1, A2, Th78
.= (a #R c) * ((1 / b) #R c)
.= (a #R c) * (1 / (b #R c)) by A2, Th79
.= ((a #R c) * 1) / (b #R c)
.= (a #R c) / (b #R c) ; ::_thesis: verum
end;
theorem Th81: :: PREPOWER:81
for a, b being real number st a > 0 holds
a #R b > 0
proof
let a, b be real number ; ::_thesis: ( a > 0 implies a #R b > 0 )
assume A1: a > 0 ; ::_thesis: a #R b > 0
then a #R b <> 0 by Lm9;
hence a #R b > 0 by A1, Lm8; ::_thesis: verum
end;
theorem Th82: :: PREPOWER:82
for a, c, b being real number st a >= 1 & c >= b holds
a #R c >= a #R b
proof
let a, c, b be real number ; ::_thesis: ( a >= 1 & c >= b implies a #R c >= a #R b )
assume that
A1: a >= 1 and
A2: c >= b ; ::_thesis: a #R c >= a #R b
consider s1 being Rational_Sequence such that
A3: s1 is convergent and
A4: c = lim s1 and
A5: for n being Element of NAT holds s1 . n >= c by Th68;
A6: a #Q s1 is convergent by A1, A3, Th69;
consider s2 being Rational_Sequence such that
A7: s2 is convergent and
A8: b = lim s2 and
A9: for n being Element of NAT holds s2 . n <= b by Th67;
A10: a #Q s2 is convergent by A1, A7, Th69;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(a_#Q_s1)_._n_>=_(a_#Q_s2)_._n
let n be Element of NAT ; ::_thesis: (a #Q s1) . n >= (a #Q s2) . n
s1 . n >= c by A5;
then A11: s1 . n >= b by A2, XXREAL_0:2;
s2 . n <= b by A9;
then s1 . n >= s2 . n by A11, XXREAL_0:2;
then a #Q (s1 . n) >= a #Q (s2 . n) by A1, Th63;
then a #Q (s1 . n) >= (a #Q s2) . n by Def6;
hence (a #Q s1) . n >= (a #Q s2) . n by Def6; ::_thesis: verum
end;
then lim (a #Q s1) >= lim (a #Q s2) by A6, A10, SEQ_2:18;
then a #R c >= lim (a #Q s2) by A1, A3, A4, A6, Def7;
hence a #R c >= a #R b by A1, A7, A8, A10, Def7; ::_thesis: verum
end;
theorem Th83: :: PREPOWER:83
for a, c, b being real number st a > 1 & c > b holds
a #R c > a #R b
proof
let a, c, b be real number ; ::_thesis: ( a > 1 & c > b implies a #R c > a #R b )
assume that
A1: a > 1 and
A2: c > b ; ::_thesis: a #R c > a #R b
consider p being Rational such that
A3: b < p and
A4: p < c by A2, RAT_1:7;
consider q being Rational such that
A5: b < q and
A6: q < p by A3, RAT_1:7;
consider s2 being Rational_Sequence such that
A7: s2 is convergent and
A8: b = lim s2 and
A9: for n being Element of NAT holds s2 . n <= b by Th67;
A10: a #Q q < a #Q p by A1, A6, Th64;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(a_#Q_s2)_._n_<=_a_#Q_q
let n be Element of NAT ; ::_thesis: (a #Q s2) . n <= a #Q q
s2 . n <= b by A9;
then s2 . n <= q by A5, XXREAL_0:2;
then a #Q (s2 . n) <= a #Q q by A1, Th63;
hence (a #Q s2) . n <= a #Q q by Def6; ::_thesis: verum
end;
then A11: lim (a #Q s2) <= a #Q q by A1, A7, Th2, Th69;
a #Q s2 is convergent by A1, A7, Th69;
then a #R b <= a #Q q by A1, A7, A8, A11, Def7;
then A12: a #R b < a #Q p by A10, XXREAL_0:2;
consider s1 being Rational_Sequence such that
A13: s1 is convergent and
A14: c = lim s1 and
A15: for n being Element of NAT holds s1 . n >= c by Th68;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(a_#Q_s1)_._n_>=_a_#Q_p
let n be Element of NAT ; ::_thesis: (a #Q s1) . n >= a #Q p
s1 . n >= c by A15;
then s1 . n >= p by A4, XXREAL_0:2;
then a #Q (s1 . n) >= a #Q p by A1, Th63;
hence (a #Q s1) . n >= a #Q p by Def6; ::_thesis: verum
end;
then A16: lim (a #Q s1) >= a #Q p by A1, A13, Th1, Th69;
a #Q s1 is convergent by A1, A13, Th69;
then a #R c >= a #Q p by A1, A13, A14, A16, Def7;
hence a #R c > a #R b by A12, XXREAL_0:2; ::_thesis: verum
end;
theorem Th84: :: PREPOWER:84
for a, c, b being real number st a > 0 & a <= 1 & c >= b holds
a #R c <= a #R b
proof
let a, c, b be real number ; ::_thesis: ( a > 0 & a <= 1 & c >= b implies a #R c <= a #R b )
assume that
A1: a > 0 and
A2: a <= 1 and
A3: c >= b ; ::_thesis: a #R c <= a #R b
1 / a >= 1 by A1, A2, Lm4, XREAL_1:85;
then (1 / a) #R c >= (1 / a) #R b by A3, Th82;
then 1 / (a #R c) >= (1 / a) #R b by A1, Th79;
then A4: 1 / (a #R c) >= 1 / (a #R b) by A1, Th79;
a #R b > 0 by A1, Th81;
hence a #R c <= a #R b by A4, XREAL_1:89; ::_thesis: verum
end;
theorem Th85: :: PREPOWER:85
for a, b being real number st a >= 1 & b >= 0 holds
a #R b >= 1
proof
let a, b be real number ; ::_thesis: ( a >= 1 & b >= 0 implies a #R b >= 1 )
assume that
A1: a >= 1 and
A2: b >= 0 ; ::_thesis: a #R b >= 1
consider s being Rational_Sequence such that
A3: s is convergent and
A4: b = lim s and
A5: for n being Element of NAT holds s . n >= b by Th68;
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_(a_#Q_s)_._n_>=_1
let n be Element of NAT ; ::_thesis: (a #Q s) . n >= 1
A7: (a #Q s) . n = a #Q (s . n) by Def6;
s . n >= b by A5;
hence (a #Q s) . n >= 1 by A1, A2, A7, Th60; ::_thesis: verum
end;
a #Q s is convergent by A1, A3, Th69;
then a #R b = lim (a #Q s) by A1, A3, A4, Def7;
hence a #R b >= 1 by A1, A3, A6, Th1, Th69; ::_thesis: verum
end;
theorem Th86: :: PREPOWER:86
for a, b being real number st a > 1 & b > 0 holds
a #R b > 1
proof
let a, b be real number ; ::_thesis: ( a > 1 & b > 0 implies a #R b > 1 )
assume that
A1: a > 1 and
A2: b > 0 ; ::_thesis: a #R b > 1
a #R b > a #R 0 by A1, A2, Th83;
hence a #R b > 1 by A1, Th71; ::_thesis: verum
end;
theorem Th87: :: PREPOWER:87
for a, b being real number st a >= 1 & b <= 0 holds
a #R b <= 1
proof
let a, b be real number ; ::_thesis: ( a >= 1 & b <= 0 implies a #R b <= 1 )
assume that
A1: a >= 1 and
A2: b <= 0 ; ::_thesis: a #R b <= 1
a #R (- b) >= 1 by A1, A2, Th85;
then 1 / (a #R b) >= 1 by A1, Th76;
then 1 / (1 / (a #R b)) <= 1 by XREAL_1:211;
hence a #R b <= 1 ; ::_thesis: verum
end;
theorem :: PREPOWER:88
for a, b being real number st a > 1 & b < 0 holds
a #R b < 1
proof
let a, b be real number ; ::_thesis: ( a > 1 & b < 0 implies a #R b < 1 )
assume that
A1: a > 1 and
A2: b < 0 ; ::_thesis: a #R b < 1
- b > 0 by A2, XREAL_1:58;
then a #R (- b) > 1 by A1, Th86;
then 1 / (a #R b) > 1 by A1, Th76;
then 1 / (1 / (a #R b)) < 1 by XREAL_1:212;
hence a #R b < 1 ; ::_thesis: verum
end;
Lm10: for p being Rational
for s1, s2 being Real_Sequence st s1 is convergent & s2 is convergent & lim s1 > 0 & p >= 0 & ( for n being Element of NAT holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ) holds
lim s2 = (lim s1) #Q p
proof
let p be Rational; ::_thesis: for s1, s2 being Real_Sequence st s1 is convergent & s2 is convergent & lim s1 > 0 & p >= 0 & ( for n being Element of NAT holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ) holds
lim s2 = (lim s1) #Q p
let s1, s2 be Real_Sequence; ::_thesis: ( s1 is convergent & s2 is convergent & lim s1 > 0 & p >= 0 & ( for n being Element of NAT holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ) implies lim s2 = (lim s1) #Q p )
assume that
A1: s1 is convergent and
A2: s2 is convergent and
A3: lim s1 > 0 and
A4: p >= 0 and
A5: for n being Element of NAT holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ; ::_thesis: lim s2 = (lim s1) #Q p
reconsider s = NAT --> (lim s1) as Real_Sequence ;
consider m0 being Element of NAT such that
A6: p < m0 by SEQ_4:3;
A7: lim s = s . 0 by SEQ_4:26
.= lim s1 by FUNCOP_1:7 ;
then A8: s1 /" s is convergent by A1, A3, SEQ_2:23;
deffunc H1( Element of NAT ) -> Element of REAL = ((s /" s1) . $1) |^ m0;
consider s3 being Real_Sequence such that
A9: for n being Element of NAT holds s3 . n = H1(n) from SEQ_1:sch_1();
for n being Element of NAT holds s1 . n <> 0 by A5;
then A10: s1 is non-zero by SEQ_1:5;
then A11: s /" s1 is convergent by A1, A3, SEQ_2:23;
then A12: s3 is convergent by A9, Th18;
reconsider q = m0 as Rational ;
deffunc H2( Element of NAT ) -> Element of REAL = ((s1 /" s) . $1) |^ m0;
consider s4 being Real_Sequence such that
A13: for n being Element of NAT holds s4 . n = H2(n) from SEQ_1:sch_1();
lim (s /" s1) = (lim s) / (lim s1) by A1, A3, A10, SEQ_2:24
.= 1 by A3, A7, XCMPLX_1:60 ;
then lim s3 = 1 |^ m0 by A11, A9, Th18;
then A14: lim s3 = 1 by NEWTON:10;
lim (s1 /" s) = (lim s1) / (lim s) by A1, A3, A7, SEQ_2:24
.= 1 by A3, A7, XCMPLX_1:60 ;
then lim s4 = 1 |^ m0 by A8, A13, Th18;
then A15: lim s4 = 1 by NEWTON:10;
s2 is bounded by A2, SEQ_2:13;
then consider d being real number such that
A16: d > 0 and
A17: for n being Element of NAT holds abs (s2 . n) < d by SEQ_2:3;
A18: s4 is convergent by A8, A13, Th18;
now__::_thesis:_for_c_being_real_number_st_c_>_0_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_m_>=_n_holds_
abs_((s2_._m)_-_((lim_s1)_#Q_p))_<_c
let c be real number ; ::_thesis: ( c > 0 implies ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs ((s2 . m) - ((lim s1) #Q p)) < c )
assume A19: c > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs ((s2 . m) - ((lim s1) #Q p)) < c
then c / d > 0 by A16, XREAL_1:139;
then consider m1 being Element of NAT such that
A20: for m being Element of NAT st m >= m1 holds
abs ((s3 . m) - 1) < c / d by A12, A14, SEQ_2:def_7;
A21: (lim s1) #Q p > 0 by A3, Th52;
then A22: abs ((lim s1) #Q p) > 0 by ABSVALUE:def_1;
then c / (abs ((lim s1) #Q p)) > 0 by A19, XREAL_1:139;
then consider m2 being Element of NAT such that
A23: for m being Element of NAT st m >= m2 holds
abs ((s4 . m) - 1) < c / (abs ((lim s1) #Q p)) by A18, A15, SEQ_2:def_7;
take n = m1 + m2; ::_thesis: for m being Element of NAT st m >= n holds
abs ((s2 . m) - ((lim s1) #Q p)) < c
let m be Element of NAT ; ::_thesis: ( m >= n implies abs ((s2 . m) - ((lim s1) #Q p)) < c )
assume A24: m >= n ; ::_thesis: abs ((s2 . m) - ((lim s1) #Q p)) < c
m2 <= n by NAT_1:11;
then A25: m >= m2 by A24, XXREAL_0:2;
m1 <= n by NAT_1:11;
then A26: m >= m1 by A24, XXREAL_0:2;
now__::_thesis:_abs_((s2_._m)_-_((lim_s1)_#Q_p))_<_c
percases ( s1 . m >= lim s1 or s1 . m <= lim s1 ) ;
supposeA27: s1 . m >= lim s1 ; ::_thesis: abs ((s2 . m) - ((lim s1) #Q p)) < c
A28: (s1 . m) / (lim s1) = (s1 . m) / (s . m) by FUNCOP_1:7
.= (s1 . m) * ((s . m) ")
.= (s1 . m) * ((s ") . m) by VALUED_1:10
.= (s1 /" s) . m by SEQ_1:8 ;
(s1 . m) * ((lim s1) ") >= (lim s1) * ((lim s1) ") by A3, A27, XREAL_1:64;
then A29: (s1 /" s) . m >= 1 by A3, A28, XCMPLX_0:def_7;
then ((s1 /" s) . m) #Q p <= ((s1 /" s) . m) #Q q by A6, Th63;
then ((s1 /" s) . m) #Q p <= ((s1 /" s) . m) |^ m0 by A29, Th49;
then A30: (((s1 /" s) . m) #Q p) - 1 <= (((s1 /" s) . m) |^ m0) - 1 by XREAL_1:9;
((s1 /" s) . m) #Q p >= 1 by A4, A29, Th60;
then (((s1 /" s) . m) #Q p) - 1 >= 1 - 1 by XREAL_1:9;
then A31: (((s1 /" s) . m) #Q p) - 1 = abs ((((s1 /" s) . m) #Q p) - 1) by ABSVALUE:def_1;
A32: (lim s1) #Q p <> 0 by A3, Th52;
A33: abs ((s4 . m) - 1) < c / (abs ((lim s1) #Q p)) by A23, A25;
A34: s1 . m > 0 by A5;
((s1 /" s) . m) |^ m0 >= 1 by A29, Th11;
then (((s1 /" s) . m) |^ m0) - 1 >= 1 - 1 by XREAL_1:9;
then abs ((((s1 /" s) . m) #Q p) - 1) <= abs ((((s1 /" s) . m) |^ m0) - 1) by A30, A31, ABSVALUE:def_1;
then abs ((((s1 /" s) . m) #Q p) - 1) <= abs ((s4 . m) - 1) by A13;
then A35: abs ((((s1 /" s) . m) #Q p) - 1) < c / (abs ((lim s1) #Q p)) by A33, XXREAL_0:2;
A36: abs ((lim s1) #Q p) <> 0 by A21, ABSVALUE:def_1;
abs ((s2 . m) - ((lim s1) #Q p)) = abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) * 1) by A5
.= abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) * (((lim s1) #Q p) / ((lim s1) #Q p))) by A32, XCMPLX_1:60
.= abs ((((lim s1) #Q p) * (((s1 . m) #Q p) - ((lim s1) #Q p))) / ((lim s1) #Q p))
.= abs (((lim s1) #Q p) * ((((s1 . m) #Q p) - ((lim s1) #Q p)) / ((lim s1) #Q p)))
.= (abs ((lim s1) #Q p)) * (abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) / ((lim s1) #Q p))) by COMPLEX1:65
.= (abs ((lim s1) #Q p)) * (abs ((((s1 . m) #Q p) / ((lim s1) #Q p)) - (((lim s1) #Q p) / ((lim s1) #Q p))))
.= (abs ((lim s1) #Q p)) * (abs ((((s1 . m) #Q p) / ((lim s1) #Q p)) - 1)) by A32, XCMPLX_1:60
.= (abs ((lim s1) #Q p)) * (abs ((((s1 . m) / (lim s1)) #Q p) - 1)) by A3, A34, Th58 ;
then abs ((s2 . m) - ((lim s1) #Q p)) < (abs ((lim s1) #Q p)) * (c / (abs ((lim s1) #Q p))) by A22, A28, A35, XREAL_1:68;
hence abs ((s2 . m) - ((lim s1) #Q p)) < c by A36, XCMPLX_1:87; ::_thesis: verum
end;
supposeA37: s1 . m <= lim s1 ; ::_thesis: abs ((s2 . m) - ((lim s1) #Q p)) < c
A38: (lim s1) / (s1 . m) = (s . m) / (s1 . m) by FUNCOP_1:7
.= (s . m) * ((s1 . m) ")
.= (s . m) * ((s1 ") . m) by VALUED_1:10
.= (s /" s1) . m by SEQ_1:8 ;
A39: s1 . m <> 0 by A5;
A40: s1 . m > 0 by A5;
then (s1 . m) * ((s1 . m) ") <= (lim s1) * ((s1 . m) ") by A37, XREAL_1:64;
then A41: (s /" s1) . m >= 1 by A39, A38, XCMPLX_0:def_7;
then ((s /" s1) . m) #Q p <= ((s /" s1) . m) #Q q by A6, Th63;
then ((s /" s1) . m) #Q p <= ((s /" s1) . m) |^ m0 by A41, Th49;
then A42: (((s /" s1) . m) #Q p) - 1 <= (((s /" s1) . m) |^ m0) - 1 by XREAL_1:9;
(s1 . m) #Q p > 0 by A5, Th52;
then A43: abs ((s1 . m) #Q p) > 0 by ABSVALUE:def_1;
A44: abs ((s3 . m) - 1) < c / d by A20, A26;
((s /" s1) . m) #Q p >= 1 by A4, A41, Th60;
then (((s /" s1) . m) #Q p) - 1 >= 1 - 1 by XREAL_1:9;
then A45: (((s /" s1) . m) #Q p) - 1 = abs ((((s /" s1) . m) #Q p) - 1) by ABSVALUE:def_1;
((s /" s1) . m) |^ m0 >= 1 by A41, Th11;
then (((s /" s1) . m) |^ m0) - 1 >= 1 - 1 by XREAL_1:9;
then abs ((((s /" s1) . m) #Q p) - 1) <= abs ((((s /" s1) . m) |^ m0) - 1) by A42, A45, ABSVALUE:def_1;
then abs ((((s /" s1) . m) #Q p) - 1) <= abs ((s3 . m) - 1) by A9;
then A46: abs ((((s /" s1) . m) #Q p) - 1) < c / d by A44, XXREAL_0:2;
abs (s2 . m) < d by A17;
then abs ((s1 . m) #Q p) < d by A5;
then (abs ((s1 . m) #Q p)) / d < d / d by A16, XREAL_1:74;
then (abs ((s1 . m) #Q p)) / d < 1 by A16, XCMPLX_1:60;
then A47: c * ((abs ((s1 . m) #Q p)) / d) < c * 1 by A19, XREAL_1:68;
A48: (s1 . m) #Q p <> 0 by A5, Th52;
abs ((s2 . m) - ((lim s1) #Q p)) = abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) * 1) by A5
.= abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) * (((s1 . m) #Q p) / ((s1 . m) #Q p))) by A48, XCMPLX_1:60
.= abs ((((s1 . m) #Q p) * (((s1 . m) #Q p) - ((lim s1) #Q p))) / ((s1 . m) #Q p))
.= abs (((s1 . m) #Q p) * ((((s1 . m) #Q p) - ((lim s1) #Q p)) / ((s1 . m) #Q p)))
.= (abs ((s1 . m) #Q p)) * (abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) / ((s1 . m) #Q p))) by COMPLEX1:65
.= (abs ((s1 . m) #Q p)) * (abs ((((s1 . m) #Q p) / ((s1 . m) #Q p)) - (((lim s1) #Q p) / ((s1 . m) #Q p))))
.= (abs ((s1 . m) #Q p)) * (abs (1 - (((lim s1) #Q p) / ((s1 . m) #Q p)))) by A48, XCMPLX_1:60
.= (abs ((s1 . m) #Q p)) * (abs (- (1 - (((lim s1) #Q p) / ((s1 . m) #Q p))))) by COMPLEX1:52
.= (abs ((s1 . m) #Q p)) * (abs ((((lim s1) #Q p) / ((s1 . m) #Q p)) - 1))
.= (abs ((s1 . m) #Q p)) * (abs ((((lim s1) / (s1 . m)) #Q p) - 1)) by A3, A40, Th58 ;
then abs ((s2 . m) - ((lim s1) #Q p)) < (abs ((s1 . m) #Q p)) * (c / d) by A43, A38, A46, XREAL_1:68;
hence abs ((s2 . m) - ((lim s1) #Q p)) < c by A47, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence abs ((s2 . m) - ((lim s1) #Q p)) < c ; ::_thesis: verum
end;
hence lim s2 = (lim s1) #Q p by A2, SEQ_2:def_7; ::_thesis: verum
end;
theorem Th89: :: PREPOWER:89
for p being Rational
for s1, s2 being Real_Sequence st s1 is convergent & s2 is convergent & lim s1 > 0 & ( for n being Element of NAT holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ) holds
lim s2 = (lim s1) #Q p
proof
let p be Rational; ::_thesis: for s1, s2 being Real_Sequence st s1 is convergent & s2 is convergent & lim s1 > 0 & ( for n being Element of NAT holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ) holds
lim s2 = (lim s1) #Q p
let s1, s2 be Real_Sequence; ::_thesis: ( s1 is convergent & s2 is convergent & lim s1 > 0 & ( for n being Element of NAT holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ) implies lim s2 = (lim s1) #Q p )
assume that
A1: s1 is convergent and
A2: s2 is convergent and
A3: lim s1 > 0 and
A4: for n being Element of NAT holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ; ::_thesis: lim s2 = (lim s1) #Q p
percases ( p >= 0 or p <= 0 ) ;
suppose p >= 0 ; ::_thesis: lim s2 = (lim s1) #Q p
hence lim s2 = (lim s1) #Q p by A1, A2, A3, A4, Lm10; ::_thesis: verum
end;
supposeA5: p <= 0 ; ::_thesis: lim s2 = (lim s1) #Q p
s1 is bounded by A1, SEQ_2:13;
then consider d being real number such that
A6: d > 0 and
A7: for n being Element of NAT holds abs (s1 . n) < d by SEQ_2:3;
reconsider d = d as Real by XREAL_0:def_1;
A8: d #Q p > 0 by A6, Th52;
A9: now__::_thesis:_not_lim_s2_=_0
assume lim s2 = 0 ; ::_thesis: contradiction
then consider n being Element of NAT such that
A10: for m being Element of NAT st m >= n holds
abs ((s2 . m) - 0) < d #Q p by A2, A8, SEQ_2:def_7;
now__::_thesis:_for_m_being_Element_of_NAT_holds_not_m_>=_n
let m be Element of NAT ; ::_thesis: not m >= n
A11: s1 . m > 0 by A4;
A12: s1 . m <> 0 by A4;
A13: (s1 . m) #Q p > 0 by A4, Th52;
abs (s1 . m) < d by A7;
then s1 . m < d by A11, ABSVALUE:def_1;
then (s1 . m) / (s1 . m) < d / (s1 . m) by A11, XREAL_1:74;
then 1 <= d / (s1 . m) by A12, XCMPLX_1:60;
then (d / (s1 . m)) #Q p <= 1 by A5, Th61;
then (d #Q p) / ((s1 . m) #Q p) <= 1 by A6, A11, Th58;
then A14: ((d #Q p) / ((s1 . m) #Q p)) * ((s1 . m) #Q p) <= 1 * ((s1 . m) #Q p) by A13, XREAL_1:64;
A15: (s1 . m) #Q p <> 0 by A4, Th52;
assume m >= n ; ::_thesis: contradiction
then abs ((s2 . m) - 0) < d #Q p by A10;
then abs ((s1 . m) #Q p) < d #Q p by A4;
then (s1 . m) #Q p < d #Q p by A13, ABSVALUE:def_1;
hence contradiction by A15, A14, XCMPLX_1:87; ::_thesis: verum
end;
hence contradiction ; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_s2_._n_<>_0
let n be Element of NAT ; ::_thesis: s2 . n <> 0
(s1 . n) #Q p <> 0 by A4, Th52;
hence s2 . n <> 0 by A4; ::_thesis: verum
end;
then A16: s2 is non-zero by SEQ_1:5;
then A17: lim (s2 ") = (lim s2) " by A2, A9, SEQ_2:22;
deffunc H1( Element of NAT ) -> Element of REAL = (s2 . $1) " ;
consider s being Real_Sequence such that
A18: for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch_1();
A19: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_s1_._n_>_0_&_s_._n_=_(s1_._n)_#Q_(-_p)_)
let n be Element of NAT ; ::_thesis: ( s1 . n > 0 & s . n = (s1 . n) #Q (- p) )
s . n = (s2 . n) " by A18
.= ((s1 . n) #Q p) " by A4
.= 1 / ((s1 . n) #Q p)
.= (s1 . n) #Q (- p) by A4, Th54 ;
hence ( s1 . n > 0 & s . n = (s1 . n) #Q (- p) ) by A4; ::_thesis: verum
end;
A20: dom s2 = NAT by FUNCT_2:def_1;
A21: dom s = NAT by FUNCT_2:def_1;
then for n being set st n in dom s holds
s . n = (s2 . n) " by A18;
then A22: s = s2 " by A21, A20, VALUED_1:def_7;
s2 " is convergent by A2, A16, A9, SEQ_2:21;
then (lim s2) " = (lim s1) #Q (- p) by A1, A3, A5, A17, A22, A19, Lm10;
then 1 / (lim s2) = 1 / ((lim s1) #Q p) by A3, Th54;
hence lim s2 = (lim s1) #Q p by XCMPLX_1:59; ::_thesis: verum
end;
end;
end;
Lm11: for a, b being real number
for p being Rational st a > 0 holds
(a #R b) #Q p = a #R (b * p)
proof
let a, b be real number ; ::_thesis: for p being Rational st a > 0 holds
(a #R b) #Q p = a #R (b * p)
let p be Rational; ::_thesis: ( a > 0 implies (a #R b) #Q p = a #R (b * p) )
consider s1 being Rational_Sequence such that
A1: s1 is convergent and
A2: b = lim s1 and
for n being Element of NAT holds s1 . n >= b by Th68;
reconsider s2 = p (#) s1 as Rational_Sequence ;
assume A3: a > 0 ; ::_thesis: (a #R b) #Q p = a #R (b * p)
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_(a_#Q_s1)_._n_>_0_&_((a_#Q_s1)_._n)_#Q_p_=_(a_#Q_s2)_._n_)
let n be Element of NAT ; ::_thesis: ( (a #Q s1) . n > 0 & ((a #Q s1) . n) #Q p = (a #Q s2) . n )
A5: a #Q (s1 . n) > 0 by A3, Th52;
((a #Q s1) . n) #Q p = (a #Q (s1 . n)) #Q p by Def6
.= a #Q (p * (s1 . n)) by A3, Th59
.= a #Q (s2 . n) by SEQ_1:9
.= (a #Q s2) . n by Def6 ;
hence ( (a #Q s1) . n > 0 & ((a #Q s1) . n) #Q p = (a #Q s2) . n ) by A5, Def6; ::_thesis: verum
end;
A6: s2 is convergent by A1, SEQ_2:7;
then A7: a #Q s2 is convergent by A3, Th69;
lim s2 = b * p by A1, A2, SEQ_2:8;
then A8: a #R (b * p) = lim (a #Q s2) by A3, A6, A7, Def7;
A9: a #Q s1 is convergent by A3, A1, Th69;
then a #R b = lim (a #Q s1) by A3, A1, A2, Def7;
hence (a #R b) #Q p = a #R (b * p) by A3, A9, A7, A8, A4, Th81, Th89; ::_thesis: verum
end;
Lm12: for a being real number
for s1, s2 being Real_Sequence st a >= 1 & s1 is convergent & s2 is convergent & ( for n being Element of NAT holds s2 . n = a #R (s1 . n) ) holds
lim s2 = a #R (lim s1)
proof
let a be real number ; ::_thesis: for s1, s2 being Real_Sequence st a >= 1 & s1 is convergent & s2 is convergent & ( for n being Element of NAT holds s2 . n = a #R (s1 . n) ) holds
lim s2 = a #R (lim s1)
let s1, s2 be Real_Sequence; ::_thesis: ( a >= 1 & s1 is convergent & s2 is convergent & ( for n being Element of NAT holds s2 . n = a #R (s1 . n) ) implies lim s2 = a #R (lim s1) )
assume that
A1: a >= 1 and
A2: s1 is convergent and
A3: s2 is convergent and
A4: for n being Element of NAT holds s2 . n = a #R (s1 . n) ; ::_thesis: lim s2 = a #R (lim s1)
set d = (abs (lim s1)) + 1;
A5: abs (lim s1) < (abs (lim s1)) + 1 by XREAL_1:29;
now__::_thesis:_for_c_being_real_number_st_c_>_0_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_m_>=_n_holds_
abs_((s2_._m)_-_(a_#R_(lim_s1)))_<_c
lim s1 <= abs (lim s1) by ABSVALUE:4;
then lim s1 <= (abs (lim s1)) + 1 by A5, XXREAL_0:2;
then A6: a #R (lim s1) <= a #R ((abs (lim s1)) + 1) by A1, Th82;
a #R (lim s1) > 0 by A1, Th81;
then A7: abs (a #R (lim s1)) <= a #R ((abs (lim s1)) + 1) by A6, ABSVALUE:def_1;
A8: a #R ((abs (lim s1)) + 1) >= 0 by A1, Th81;
let c be real number ; ::_thesis: ( c > 0 implies ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs ((s2 . m) - (a #R (lim s1))) < c )
assume A9: c > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs ((s2 . m) - (a #R (lim s1))) < c
consider m1 being Element of NAT such that
A10: ((a #R ((abs (lim s1)) + 1)) * (a - 1)) / c < m1 by SEQ_4:3;
m1 + 1 >= m1 by XREAL_1:29;
then ((a #R ((abs (lim s1)) + 1)) * (a - 1)) / c < m1 + 1 by A10, XXREAL_0:2;
then (((a #R ((abs (lim s1)) + 1)) * (a - 1)) / c) * c < c * (m1 + 1) by A9, XREAL_1:68;
then (a #R ((abs (lim s1)) + 1)) * (a - 1) < c * (m1 + 1) by A9, XCMPLX_1:87;
then ((a #R ((abs (lim s1)) + 1)) * (a - 1)) / (m1 + 1) < ((m1 + 1) * c) / (m1 + 1) by XREAL_1:74;
then ((a #R ((abs (lim s1)) + 1)) * (a - 1)) / (m1 + 1) < (c / (m1 + 1)) * (m1 + 1) ;
then A11: ((a #R ((abs (lim s1)) + 1)) * (a - 1)) / (m1 + 1) < c by XCMPLX_1:87;
reconsider m3 = (m1 + 1) " as Rational ;
A12: abs (a #R (lim s1)) >= 0 by COMPLEX1:46;
consider n being Element of NAT such that
A13: for m being Element of NAT st n <= m holds
abs ((s1 . m) - (lim s1)) < (m1 + 1) " by A2, SEQ_2:def_7;
take n = n; ::_thesis: for m being Element of NAT st m >= n holds
abs ((s2 . m) - (a #R (lim s1))) < c
let m be Element of NAT ; ::_thesis: ( m >= n implies abs ((s2 . m) - (a #R (lim s1))) < c )
assume m >= n ; ::_thesis: abs ((s2 . m) - (a #R (lim s1))) < c
then A14: abs ((s1 . m) - (lim s1)) <= (m1 + 1) " by A13;
A15: m1 + 1 >= 0 + 1 by NAT_1:13;
then ((m1 + 1) -Root a) - 1 <= (a - 1) / (m1 + 1) by A1, Th31;
then A16: (a #R ((abs (lim s1)) + 1)) * (((m1 + 1) -Root a) - 1) <= (a #R ((abs (lim s1)) + 1)) * ((a - 1) / (m1 + 1)) by A8, XREAL_1:64;
(s1 . m) - (lim s1) <= abs ((s1 . m) - (lim s1)) by ABSVALUE:4;
then (s1 . m) - (lim s1) <= (m1 + 1) " by A14, XXREAL_0:2;
then a #R ((s1 . m) - (lim s1)) <= a #R m3 by A1, Th82;
then a #R ((s1 . m) - (lim s1)) <= a #Q m3 by A1, Th74;
then a #R ((s1 . m) - (lim s1)) <= (m1 + 1) -Root a by A15, Th50;
then A17: (a #R ((s1 . m) - (lim s1))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:9;
A18: a #R ((s1 . m) - (lim s1)) <> 0 by A1, Th81;
A19: a #R ((s1 . m) - (lim s1)) > 0 by A1, Th81;
A20: now__::_thesis:_abs_((a_#R_((s1_._m)_-_(lim_s1)))_-_1)_<=_((m1_+_1)_-Root_a)_-_1
percases ( (s1 . m) - (lim s1) >= 0 or (s1 . m) - (lim s1) < 0 ) ;
suppose (s1 . m) - (lim s1) >= 0 ; ::_thesis: abs ((a #R ((s1 . m) - (lim s1))) - 1) <= ((m1 + 1) -Root a) - 1
then a #R ((s1 . m) - (lim s1)) >= 1 by A1, Th85;
then (a #R ((s1 . m) - (lim s1))) - 1 >= 0 by XREAL_1:48;
hence abs ((a #R ((s1 . m) - (lim s1))) - 1) <= ((m1 + 1) -Root a) - 1 by A17, ABSVALUE:def_1; ::_thesis: verum
end;
supposeA21: (s1 . m) - (lim s1) < 0 ; ::_thesis: abs ((a #R ((s1 . m) - (lim s1))) - 1) <= ((m1 + 1) -Root a) - 1
A22: - ((s1 . m) - (lim s1)) <= abs (- ((s1 . m) - (lim s1))) by ABSVALUE:4;
abs ((s1 . m) - (lim s1)) = abs (- ((s1 . m) - (lim s1))) by COMPLEX1:52;
then - ((s1 . m) - (lim s1)) <= m3 by A14, A22, XXREAL_0:2;
then a #R (- ((s1 . m) - (lim s1))) <= a #R m3 by A1, Th82;
then a #R (- ((s1 . m) - (lim s1))) <= a #Q m3 by A1, Th74;
then a #R (- ((s1 . m) - (lim s1))) <= (m1 + 1) -Root a by A15, Th50;
then A23: (a #R (- ((s1 . m) - (lim s1)))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:9;
a #R (- ((s1 . m) - (lim s1))) >= 1 by A1, A21, Th85;
then (a #R (- ((s1 . m) - (lim s1)))) - 1 >= 0 by XREAL_1:48;
then A24: abs ((a #R (- ((s1 . m) - (lim s1)))) - 1) <= ((m1 + 1) -Root a) - 1 by A23, ABSVALUE:def_1;
a #R ((s1 . m) - (lim s1)) <= 1 by A1, A21, Th87;
then A25: abs (a #R ((s1 . m) - (lim s1))) <= 1 by A19, ABSVALUE:def_1;
abs ((a #R (- ((s1 . m) - (lim s1)))) - 1) >= 0 by COMPLEX1:46;
then A26: (abs (a #R ((s1 . m) - (lim s1)))) * (abs ((a #R (- ((s1 . m) - (lim s1)))) - 1)) <= 1 * (abs ((a #R (- ((s1 . m) - (lim s1)))) - 1)) by A25, XREAL_1:64;
abs ((a #R ((s1 . m) - (lim s1))) - 1) = abs (((a #R ((s1 . m) - (lim s1))) - 1) * 1)
.= abs (((a #R ((s1 . m) - (lim s1))) - 1) * ((a #R ((s1 . m) - (lim s1))) / (a #R ((s1 . m) - (lim s1))))) by A18, XCMPLX_1:60
.= abs (((a #R ((s1 . m) - (lim s1))) * ((a #R ((s1 . m) - (lim s1))) - 1)) / (a #R ((s1 . m) - (lim s1))))
.= abs ((a #R ((s1 . m) - (lim s1))) * (((a #R ((s1 . m) - (lim s1))) - 1) / (a #R ((s1 . m) - (lim s1)))))
.= (abs (a #R ((s1 . m) - (lim s1)))) * (abs (((a #R ((s1 . m) - (lim s1))) - 1) / (a #R ((s1 . m) - (lim s1))))) by COMPLEX1:65
.= (abs (a #R ((s1 . m) - (lim s1)))) * (abs (((a #R ((s1 . m) - (lim s1))) / (a #R ((s1 . m) - (lim s1)))) - (1 / (a #R ((s1 . m) - (lim s1))))))
.= (abs (a #R ((s1 . m) - (lim s1)))) * (abs (1 - (1 / (a #R ((s1 . m) - (lim s1)))))) by A18, XCMPLX_1:60
.= (abs (a #R ((s1 . m) - (lim s1)))) * (abs (1 - (a #R (- ((s1 . m) - (lim s1)))))) by A1, Th76
.= (abs (a #R ((s1 . m) - (lim s1)))) * (abs (- (1 - (a #R (- ((s1 . m) - (lim s1))))))) by COMPLEX1:52
.= (abs (a #R ((s1 . m) - (lim s1)))) * (abs ((a #R (- ((s1 . m) - (lim s1)))) - 1)) ;
hence abs ((a #R ((s1 . m) - (lim s1))) - 1) <= ((m1 + 1) -Root a) - 1 by A24, A26, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
abs ((a #R ((s1 . m) - (lim s1))) - 1) >= 0 by COMPLEX1:46;
then A27: (abs (a #R (lim s1))) * (abs ((a #R ((s1 . m) - (lim s1))) - 1)) <= (a #R ((abs (lim s1)) + 1)) * (((m1 + 1) -Root a) - 1) by A20, A12, A7, XREAL_1:66;
abs ((a #R (s1 . m)) - (a #R (lim s1))) = abs (((a #R (s1 . m)) - (a #R (lim s1))) * 1)
.= abs (((a #R (s1 . m)) - (a #R (lim s1))) * ((a #R (lim s1)) / (a #R (lim s1)))) by A1, Lm9, XCMPLX_1:60
.= abs (((a #R (lim s1)) * ((a #R (s1 . m)) - (a #R (lim s1)))) / (a #R (lim s1)))
.= abs ((a #R (lim s1)) * (((a #R (s1 . m)) - (a #R (lim s1))) / (a #R (lim s1))))
.= (abs (a #R (lim s1))) * (abs (((a #R (s1 . m)) - (a #R (lim s1))) / (a #R (lim s1)))) by COMPLEX1:65
.= (abs (a #R (lim s1))) * (abs (((a #R (s1 . m)) / (a #R (lim s1))) - ((a #R (lim s1)) / (a #R (lim s1)))))
.= (abs (a #R (lim s1))) * (abs (((a #R (s1 . m)) / (a #R (lim s1))) - 1)) by A1, Lm9, XCMPLX_1:60
.= (abs (a #R (lim s1))) * (abs ((a #R ((s1 . m) - (lim s1))) - 1)) by A1, Th77 ;
then abs ((a #R (s1 . m)) - (a #R (lim s1))) <= ((a #R ((abs (lim s1)) + 1)) * (a - 1)) / (m1 + 1) by A27, A16, XXREAL_0:2;
then abs ((a #R (s1 . m)) - (a #R (lim s1))) < c by A11, XXREAL_0:2;
hence abs ((s2 . m) - (a #R (lim s1))) < c by A4; ::_thesis: verum
end;
hence lim s2 = a #R (lim s1) by A3, SEQ_2:def_7; ::_thesis: verum
end;
theorem Th90: :: PREPOWER:90
for a being real number
for s1, s2 being Real_Sequence st a > 0 & s1 is convergent & s2 is convergent & ( for n being Element of NAT holds s2 . n = a #R (s1 . n) ) holds
lim s2 = a #R (lim s1)
proof
let a be real number ; ::_thesis: for s1, s2 being Real_Sequence st a > 0 & s1 is convergent & s2 is convergent & ( for n being Element of NAT holds s2 . n = a #R (s1 . n) ) holds
lim s2 = a #R (lim s1)
let s1, s2 be Real_Sequence; ::_thesis: ( a > 0 & s1 is convergent & s2 is convergent & ( for n being Element of NAT holds s2 . n = a #R (s1 . n) ) implies lim s2 = a #R (lim s1) )
assume that
A1: a > 0 and
A2: s1 is convergent and
A3: s2 is convergent and
A4: for n being Element of NAT holds s2 . n = a #R (s1 . n) ; ::_thesis: lim s2 = a #R (lim s1)
percases ( a >= 1 or a < 1 ) ;
suppose a >= 1 ; ::_thesis: lim s2 = a #R (lim s1)
hence lim s2 = a #R (lim s1) by A2, A3, A4, Lm12; ::_thesis: verum
end;
supposeA5: a < 1 ; ::_thesis: lim s2 = a #R (lim s1)
A6: now__::_thesis:_not_lim_s2_=_0
assume A7: lim s2 = 0 ; ::_thesis: contradiction
a #R ((lim s1) + 1) > 0 by A1, Th81;
then consider n being Element of NAT such that
A8: for m being Element of NAT st m >= n holds
abs ((s2 . m) - 0) < a #R ((lim s1) + 1) by A3, A7, SEQ_2:def_7;
consider n1 being Element of NAT such that
A9: for m being Element of NAT st m >= n1 holds
abs ((s1 . m) - (lim s1)) < 1 by A2, SEQ_2:def_7;
now__::_thesis:_for_m_being_Element_of_NAT_holds_not_m_>=_n_+_n1
let m be Element of NAT ; ::_thesis: not m >= n + n1
assume A10: m >= n + n1 ; ::_thesis: contradiction
n + n1 >= n1 by NAT_1:12;
then m >= n1 by A10, XXREAL_0:2;
then A11: abs ((s1 . m) - (lim s1)) < 1 by A9;
(s1 . m) - (lim s1) <= abs ((s1 . m) - (lim s1)) by ABSVALUE:4;
then (s1 . m) - (lim s1) < 1 by A11, XXREAL_0:2;
then A12: ((s1 . m) - (lim s1)) + (lim s1) < (lim s1) + 1 by XREAL_1:6;
n + n1 >= n by NAT_1:12;
then m >= n by A10, XXREAL_0:2;
then abs ((s2 . m) - 0) < a #R ((lim s1) + 1) by A8;
then A13: abs (a #R (s1 . m)) < a #R ((lim s1) + 1) by A4;
a #R (s1 . m) > 0 by A1, Th81;
then a #R (s1 . m) < a #R ((lim s1) + 1) by A13, ABSVALUE:def_1;
hence contradiction by A1, A5, A12, Th84; ::_thesis: verum
end;
hence contradiction ; ::_thesis: verum
end;
A14: now__::_thesis:_for_n_being_Element_of_NAT_holds_(s2_")_._n_=_(1_/_a)_#R_(s1_._n)
let n be Element of NAT ; ::_thesis: (s2 ") . n = (1 / a) #R (s1 . n)
thus (s2 ") . n = (s2 . n) " by VALUED_1:10
.= (a #R (s1 . n)) " by A4
.= 1 / (a #R (s1 . n))
.= (1 / a) #R (s1 . n) by A1, Th79 ; ::_thesis: verum
end;
a * (1 / a) <= 1 * (1 / a) by A1, A5, XREAL_1:64;
then A15: 1 <= 1 / a by A1, XCMPLX_1:106;
A16: a #R (lim s1) <> 0 by A1, Th81;
now__::_thesis:_for_n_being_Element_of_NAT_holds_s2_._n_<>_0
let n be Element of NAT ; ::_thesis: s2 . n <> 0
s2 . n = a #R (s1 . n) by A4;
hence s2 . n <> 0 by A1, Th81; ::_thesis: verum
end;
then A17: s2 is non-zero by SEQ_1:5;
then A18: lim (s2 ") = (lim s2) " by A3, A6, SEQ_2:22;
s2 " is convergent by A3, A6, A17, SEQ_2:21;
then (lim s2) " = (1 / a) #R (lim s1) by A2, A15, A18, A14, Lm12
.= 1 / (a #R (lim s1)) by A1, Th79 ;
then 1 = (1 / (a #R (lim s1))) * (lim s2) by A6, XCMPLX_0:def_7;
then a #R (lim s1) = (a #R (lim s1)) * ((1 / (a #R (lim s1))) * (lim s2))
.= ((a #R (lim s1)) * (1 / (a #R (lim s1)))) * (lim s2)
.= 1 * (lim s2) by A16, XCMPLX_1:106 ;
hence lim s2 = a #R (lim s1) ; ::_thesis: verum
end;
end;
end;
theorem :: PREPOWER:91
for a, b, c being real number st a > 0 holds
(a #R b) #R c = a #R (b * c)
proof
let a, b, c be real number ; ::_thesis: ( a > 0 implies (a #R b) #R c = a #R (b * c) )
consider s being Rational_Sequence such that
A1: s is convergent and
A2: c = lim s and
for n being Element of NAT holds s . n <= c by Th67;
A3: lim (b (#) s) = b * c by A1, A2, SEQ_2:8;
A4: b (#) s is convergent by A1, SEQ_2:7;
assume A5: a > 0 ; ::_thesis: (a #R b) #R c = a #R (b * c)
then A6: (a #R b) #Q s is convergent by A1, Th69, Th81;
A7: now__::_thesis:_for_n_being_Element_of_NAT_holds_((a_#R_b)_#Q_s)_._n_=_a_#R_((b_(#)_s)_._n)
let n be Element of NAT ; ::_thesis: ((a #R b) #Q s) . n = a #R ((b (#) s) . n)
thus ((a #R b) #Q s) . n = (a #R b) #Q (s . n) by Def6
.= a #R (b * (s . n)) by A5, Lm11
.= a #R ((b (#) s) . n) by SEQ_1:9 ; ::_thesis: verum
end;
a #R b > 0 by A5, Th81;
then (a #R b) #R c = lim ((a #R b) #Q s) by A1, A2, A6, Def7;
hence (a #R b) #R c = a #R (b * c) by A5, A6, A4, A3, A7, Th90; ::_thesis: verum
end;
begin
theorem :: PREPOWER:92
for r, u being real number st r > 0 & u > 0 holds
ex k being Element of NAT st u / (2 |^ k) <= r
proof
let r, u be real number ; ::_thesis: ( r > 0 & u > 0 implies ex k being Element of NAT st u / (2 |^ k) <= r )
defpred S1[ Element of NAT ] means $1 <= 2 |^ $1;
assume that
A1: r > 0 and
A2: u > 0 ; ::_thesis: ex k being Element of NAT st u / (2 |^ k) <= r
set t = 1 / r;
reconsider t = 1 / r as Real ;
consider n being Element of NAT such that
A3: u * t < n by SEQ_4:3;
A4: 0 < u * t by A1, A2, XREAL_1:129;
then A5: u / (u * t) > u / n by A2, A3, XREAL_1:76;
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume k <= 2 |^ k ; ::_thesis: S1[k + 1]
then A7: (2 |^ k) + 1 >= k + 1 by XREAL_1:7;
2 |^ k >= 1 by Th11;
then A8: (2 |^ k) + (2 |^ k) >= (2 |^ k) + 1 by XREAL_1:7;
2 |^ (k + 1) = (2 |^ k) * (2 |^ 1) by NEWTON:8
.= (2 |^ k) * 2 by NEWTON:5
.= (2 |^ k) + (2 |^ k) ;
hence S1[k + 1] by A8, A7, XXREAL_0:2; ::_thesis: verum
end;
take n ; ::_thesis: u / (2 |^ n) <= r
A9: r = 1 / t
.= (u * 1) / (u * t) by A2, XCMPLX_1:91
.= u / (u * t) ;
A10: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A10, A6);
then u / n >= u / (2 |^ n) by A2, A3, A4, XREAL_1:118;
hence u / (2 |^ n) <= r by A9, A5, XXREAL_0:2; ::_thesis: verum
end;
theorem :: PREPOWER:93
for n being Element of NAT
for r being real number
for k being Nat st k >= n & r >= 1 holds
r |^ k >= r |^ n
proof
let n be Element of NAT ; ::_thesis: for r being real number
for k being Nat st k >= n & r >= 1 holds
r |^ k >= r |^ n
let r be real number ; ::_thesis: for k being Nat st k >= n & r >= 1 holds
r |^ k >= r |^ n
let k be Nat; ::_thesis: ( k >= n & r >= 1 implies r |^ k >= r |^ n )
assume that
A1: k >= n and
A2: r >= 1 ; ::_thesis: r |^ k >= r |^ n
consider m being Nat such that
A3: k = n + m by A1, NAT_1:10;
A4: r |^ k = (r |^ n) * (r |^ m) by A3, NEWTON:8;
r |^ n >= 1 by A2, Th11;
hence r |^ k >= r |^ n by A2, A4, Th11, XREAL_1:151; ::_thesis: verum
end;
theorem Th94: :: PREPOWER:94
for n, m, l being Element of NAT st n divides m & n divides l holds
n divides m - l
proof
let n, m, l be Element of NAT ; ::_thesis: ( n divides m & n divides l implies n divides m - l )
assume that
A1: n divides m and
A2: n divides l ; ::_thesis: n divides m - l
A3: - l = - (n * (l div n)) by A2, NAT_D:3
.= n * (- (l div n)) ;
m = n * (m div n) by A1, NAT_D:3;
then m - l = n * ((m div n) + (- (l div n))) by A3;
hence n divides m - l by INT_1:def_3; ::_thesis: verum
end;
theorem :: PREPOWER:95
for m, n being Element of NAT holds
( m divides n iff m divides n ) ;
theorem Th96: :: PREPOWER:96
for m, n being Element of NAT holds m gcd n = m gcd (abs (n - m))
proof
let m, n be Element of NAT ; ::_thesis: m gcd n = m gcd (abs (n - m))
set x = m gcd n;
set y = m gcd (abs (n - m));
A1: m gcd n divides m by NAT_D:def_5;
A2: m gcd n divides n by NAT_D:def_5;
A3: m gcd (abs (n - m)) divides m by NAT_D:def_5;
percases ( n - m >= 0 or n - m < 0 ) ;
suppose n - m >= 0 ; ::_thesis: m gcd n = m gcd (abs (n - m))
then reconsider nm = n - m as Element of NAT by INT_1:3;
A4: abs (n - m) = nm by ABSVALUE:def_1;
then m gcd (abs (n - m)) divides nm by NAT_D:def_5;
then m gcd (abs (n - m)) divides nm + m by A3, NAT_D:8;
then A5: m gcd (abs (n - m)) divides m gcd n by A3, NAT_D:def_5;
m gcd n divides n - m by A1, A2, Th94;
then m gcd n divides m gcd (abs (n - m)) by A1, A4, NAT_D:def_5;
hence m gcd n = m gcd (abs (n - m)) by A5, NAT_D:5; ::_thesis: verum
end;
supposeA6: n - m < 0 ; ::_thesis: m gcd n = m gcd (abs (n - m))
reconsider nn = n as Integer ;
A7: abs (n - m) = - (n - m) by A6, ABSVALUE:def_1
.= m - n ;
then reconsider mn = m - n as Element of NAT ;
m gcd (abs (n - m)) divides mn by A7, NAT_D:def_5;
then m gcd (abs (n - m)) divides mn - m by A3, Th94;
then m gcd (abs (n - m)) divides nn by INT_2:10;
then A8: m gcd (abs (n - m)) divides m gcd n by A3, NAT_D:def_5;
m gcd n divides m - n by A1, A2, Th94;
then m gcd n divides m gcd (abs (n - m)) by A1, A7, NAT_D:def_5;
hence m gcd n = m gcd (abs (n - m)) by A8, NAT_D:5; ::_thesis: verum
end;
end;
end;
theorem :: PREPOWER:97
for a, b being Integer st a >= 0 & b >= 0 holds
a gcd b = a gcd (b - a)
proof
let a, b be Integer; ::_thesis: ( a >= 0 & b >= 0 implies a gcd b = a gcd (b - a) )
assume that
A1: a >= 0 and
A2: b >= 0 ; ::_thesis: a gcd b = a gcd (b - a)
thus a gcd b = (abs a) gcd (abs b) by INT_2:34
.= (abs a) gcd (abs ((abs b) - (abs a))) by Th96
.= (abs a) gcd (abs (b - (abs a))) by A2, ABSVALUE:def_1
.= (abs a) gcd (abs (b - a)) by A1, ABSVALUE:def_1
.= a gcd (b - a) by INT_2:34 ; ::_thesis: verum
end;
theorem :: PREPOWER:98
for a being real number
for l being Integer st a >= 0 holds
a #Z l >= 0 by Lm5;
theorem :: PREPOWER:99
for a being real number
for l being Integer st a > 0 holds
a #Q l = a #Z l
proof
let a be real number ; ::_thesis: for l being Integer st a > 0 holds
a #Q l = a #Z l
let l be Integer; ::_thesis: ( a > 0 implies a #Q l = a #Z l )
assume a > 0 ; ::_thesis: a #Q l = a #Z l
then a #Z l > 0 by Th39;
then A1: a #Z l = (1 -Root (a #Z l)) |^ 1 by Def2;
denominator l = 1 by RAT_1:17;
hence a #Q l = 1 -Root (a #Z l) by RAT_1:17
.= a #Z l by A1, NEWTON:5 ;
::_thesis: verum
end;
theorem :: PREPOWER:100
for l being Integer st l <> 0 holds
0 #Z l = 0
proof
let l be Integer; ::_thesis: ( l <> 0 implies 0 #Z l = 0 )
assume A1: l <> 0 ; ::_thesis: 0 #Z l = 0
percases ( l > 0 or l < 0 ) by A1;
supposeA2: l > 0 ; ::_thesis: 0 #Z l = 0
then reconsider l = l as Element of NAT by INT_1:3;
l >= 0 + 1 by A2, NAT_1:13;
then A3: 0 |^ l = 0 by NEWTON:11;
abs l = l by ABSVALUE:def_1;
hence 0 #Z l = 0 by A3, Def3; ::_thesis: verum
end;
supposeA4: l < 0 ; ::_thesis: 0 #Z l = 0
then reconsider k = - l as Element of NAT by INT_1:3;
k > - 0 by A4, XREAL_1:58;
then k >= 0 + 1 by NAT_1:13;
then A5: 0 |^ k = 0 by NEWTON:11;
abs l = k by A4, ABSVALUE:def_1;
then (0 |^ (abs l)) " = 0 by A5;
hence 0 #Z l = 0 by A4, Def3; ::_thesis: verum
end;
end;
end;