:: 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;