:: TOPRNS_1 semantic presentation begin definition let N be Nat; mode Real_Sequence of N is sequence of (TOP-REAL N); end; theorem Th1: :: TOPRNS_1:1 for N being Element of NAT for f being Function holds ( f is Real_Sequence of N iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Point of (TOP-REAL N) ) ) ) proof let N be Element of NAT ; ::_thesis: for f being Function holds ( f is Real_Sequence of N iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Point of (TOP-REAL N) ) ) ) let f be Function; ::_thesis: ( f is Real_Sequence of N iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Point of (TOP-REAL N) ) ) ) thus ( f is Real_Sequence of N implies ( dom f = NAT & ( for n being Element of NAT holds f . n is Point of (TOP-REAL N) ) ) ) by NORMSP_1:12; ::_thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n is Point of (TOP-REAL N) ) implies f is Real_Sequence of N ) assume that A1: dom f = NAT and A2: for n being Element of NAT holds f . n is Point of (TOP-REAL N) ; ::_thesis: f is Real_Sequence of N for x being set st x in NAT holds f . x is Point of (TOP-REAL N) by A2; hence f is Real_Sequence of N by A1, NORMSP_1:12; ::_thesis: verum end; definition let N be Element of NAT ; let IT be Real_Sequence of N; attrIT is non-zero means :Def1: :: TOPRNS_1:def 1 rng IT c= NonZero (TOP-REAL N); end; :: deftheorem Def1 defines non-zero TOPRNS_1:def_1_:_ for N being Element of NAT for IT being Real_Sequence of N holds ( IT is non-zero iff rng IT c= NonZero (TOP-REAL N) ); theorem Th2: :: TOPRNS_1:2 for N being Element of NAT for seq being Real_Sequence of N holds ( seq is non-zero iff for x being set st x in NAT holds seq . x <> 0. (TOP-REAL N) ) proof let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N holds ( seq is non-zero iff for x being set st x in NAT holds seq . x <> 0. (TOP-REAL N) ) let seq be Real_Sequence of N; ::_thesis: ( seq is non-zero iff for x being set st x in NAT holds seq . x <> 0. (TOP-REAL N) ) thus ( seq is non-zero implies for x being set st x in NAT holds seq . x <> 0. (TOP-REAL N) ) ::_thesis: ( ( for x being set st x in NAT holds seq . x <> 0. (TOP-REAL N) ) implies seq is non-zero ) proof assume seq is non-zero ; ::_thesis: for x being set st x in NAT holds seq . x <> 0. (TOP-REAL N) then A1: rng seq c= NonZero (TOP-REAL N) by Def1; let x be set ; ::_thesis: ( x in NAT implies seq . x <> 0. (TOP-REAL N) ) assume x in NAT ; ::_thesis: seq . x <> 0. (TOP-REAL N) then x in dom seq by Th1; then seq . x in rng seq by FUNCT_1:def_3; then not seq . x in {(0. (TOP-REAL N))} by A1, XBOOLE_0:def_5; hence seq . x <> 0. (TOP-REAL N) by TARSKI:def_1; ::_thesis: verum end; assume A2: for x being set st x in NAT holds seq . x <> 0. (TOP-REAL N) ; ::_thesis: seq is non-zero now__::_thesis:_for_y_being_set_st_y_in_rng_seq_holds_ y_in_NonZero_(TOP-REAL_N) let y be set ; ::_thesis: ( y in rng seq implies y in NonZero (TOP-REAL N) ) assume y in rng seq ; ::_thesis: y in NonZero (TOP-REAL N) then consider x being set such that A3: x in dom seq and A4: seq . x = y by FUNCT_1:def_3; A5: x in NAT by A3, NORMSP_1:12; then y <> 0. (TOP-REAL N) by A2, A4; then A6: not y in {(0. (TOP-REAL N))} by TARSKI:def_1; y is Point of (TOP-REAL N) by A4, A5, NORMSP_1:12; hence y in NonZero (TOP-REAL N) by A6, XBOOLE_0:def_5; ::_thesis: verum end; then rng seq c= NonZero (TOP-REAL N) by TARSKI:def_3; hence seq is non-zero by Def1; ::_thesis: verum end; theorem Th3: :: TOPRNS_1:3 for N being Element of NAT for seq being Real_Sequence of N holds ( seq is non-zero iff for n being Element of NAT holds seq . n <> 0. (TOP-REAL N) ) proof let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N holds ( seq is non-zero iff for n being Element of NAT holds seq . n <> 0. (TOP-REAL N) ) let seq be Real_Sequence of N; ::_thesis: ( seq is non-zero iff for n being Element of NAT holds seq . n <> 0. (TOP-REAL N) ) thus ( seq is non-zero implies for n being Element of NAT holds seq . n <> 0. (TOP-REAL N) ) by Th2; ::_thesis: ( ( for n being Element of NAT holds seq . n <> 0. (TOP-REAL N) ) implies seq is non-zero ) assume for n being Element of NAT holds seq . n <> 0. (TOP-REAL N) ; ::_thesis: seq is non-zero then for x being set st x in NAT holds seq . x <> 0. (TOP-REAL N) ; hence seq is non-zero by Th2; ::_thesis: verum end; definition let N be Nat; let seq1, seq2 be Real_Sequence of N; funcseq1 + seq2 -> Real_Sequence of N equals :: TOPRNS_1:def 2 seq1 + seq2; coherence seq1 + seq2 is Real_Sequence of N proof A1: ( dom seq1 = NAT & dom seq2 = NAT ) by FUNCT_2:def_1; dom (seq1 + seq2) = (dom seq1) /\ (dom seq2) by VFUNCT_1:def_1; hence seq1 + seq2 is Real_Sequence of N by A1, FUNCT_2:67; ::_thesis: verum end; end; :: deftheorem defines + TOPRNS_1:def_2_:_ for N being Nat for seq1, seq2 being Real_Sequence of N holds seq1 + seq2 = seq1 + seq2; definition let r be Real; let N be Nat; let seq be Real_Sequence of N; funcr * seq -> Real_Sequence of N equals :: TOPRNS_1:def 3 r (#) seq; coherence r (#) seq is Real_Sequence of N proof A1: dom seq = NAT by FUNCT_2:def_1; dom (r (#) seq) = dom seq by VFUNCT_1:def_4; hence r (#) seq is Real_Sequence of N by A1, FUNCT_2:67; ::_thesis: verum end; end; :: deftheorem defines * TOPRNS_1:def_3_:_ for r being Real for N being Nat for seq being Real_Sequence of N holds r * seq = r (#) seq; definition let N be Nat; let seq be Real_Sequence of N; func - seq -> Real_Sequence of N equals :: TOPRNS_1:def 4 - seq; coherence - seq is Real_Sequence of N proof A1: dom seq = NAT by FUNCT_2:def_1; dom (- seq) = dom seq by VFUNCT_1:def_5; hence - seq is Real_Sequence of N by A1, FUNCT_2:67; ::_thesis: verum end; end; :: deftheorem defines - TOPRNS_1:def_4_:_ for N being Nat for seq being Real_Sequence of N holds - seq = - seq; definition let N be Nat; let seq1, seq2 be Real_Sequence of N; funcseq1 - seq2 -> Real_Sequence of N equals :: TOPRNS_1:def 5 seq1 + (- seq2); correctness coherence seq1 + (- seq2) is Real_Sequence of N; ; end; :: deftheorem defines - TOPRNS_1:def_5_:_ for N being Nat for seq1, seq2 being Real_Sequence of N holds seq1 - seq2 = seq1 + (- seq2); definition let N be Nat; let seq be Real_Sequence of N; func|.seq.| -> Real_Sequence means :Def6: :: TOPRNS_1:def 6 for n being Element of NAT holds it . n = |.(seq . n).|; existence ex b1 being Real_Sequence st for n being Element of NAT holds b1 . n = |.(seq . n).| proof deffunc H1( Element of NAT ) -> Element of REAL = |.(seq . \$1).|; thus ex s being Real_Sequence st for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = |.(seq . n).| ) & ( for n being Element of NAT holds b2 . n = |.(seq . n).| ) holds b1 = b2 proof let seq8, seq9 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq8 . n = |.(seq . n).| ) & ( for n being Element of NAT holds seq9 . n = |.(seq . n).| ) implies seq8 = seq9 ) assume that A1: for n being Element of NAT holds seq8 . n = |.(seq . n).| and A2: for n being Element of NAT holds seq9 . n = |.(seq . n).| ; ::_thesis: seq8 = seq9 let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: seq8 . n = seq9 . n seq9 . n = |.(seq . n).| by A2; hence seq8 . n = seq9 . n by A1; ::_thesis: verum end; end; :: deftheorem Def6 defines |. TOPRNS_1:def_6_:_ for N being Nat for seq being Real_Sequence of N for b3 being Real_Sequence holds ( b3 = |.seq.| iff for n being Element of NAT holds b3 . n = |.(seq . n).| ); theorem Th4: :: TOPRNS_1:4 for N, n being Nat for seq1, seq2 being Real_Sequence of N holds (seq1 + seq2) . n = (seq1 . n) + (seq2 . n) proof let N, n be Nat; ::_thesis: for seq1, seq2 being Real_Sequence of N holds (seq1 + seq2) . n = (seq1 . n) + (seq2 . n) let seq1, seq2 be Real_Sequence of N; ::_thesis: (seq1 + seq2) . n = (seq1 . n) + (seq2 . n) reconsider m = n as Element of NAT by ORDINAL1:def_12; A1: dom (seq1 + seq2) = NAT by FUNCT_2:def_1; thus (seq1 + seq2) . n = (seq1 + seq2) /. m .= (seq1 /. m) + (seq2 /. m) by A1, VFUNCT_1:def_1 .= (seq1 . n) + (seq2 . n) ; ::_thesis: verum end; theorem Th5: :: TOPRNS_1:5 for r being Real for N, n being Nat for seq being Real_Sequence of N holds (r * seq) . n = r * (seq . n) proof let r be Real; ::_thesis: for N, n being Nat for seq being Real_Sequence of N holds (r * seq) . n = r * (seq . n) let N, n be Nat; ::_thesis: for seq being Real_Sequence of N holds (r * seq) . n = r * (seq . n) let seq be Real_Sequence of N; ::_thesis: (r * seq) . n = r * (seq . n) reconsider m = n as Element of NAT by ORDINAL1:def_12; A1: dom (r * seq) = NAT by FUNCT_2:def_1; thus (r * seq) . n = (r * seq) /. m .= r * (seq /. m) by A1, VFUNCT_1:def_4 .= r * (seq . n) ; ::_thesis: verum end; theorem Th6: :: TOPRNS_1:6 for N, n being Nat for seq being Real_Sequence of N holds (- seq) . n = - (seq . n) proof let N, n be Nat; ::_thesis: for seq being Real_Sequence of N holds (- seq) . n = - (seq . n) let seq be Real_Sequence of N; ::_thesis: (- seq) . n = - (seq . n) reconsider m = n as Element of NAT by ORDINAL1:def_12; A1: dom (- seq) = NAT by FUNCT_2:def_1; thus (- seq) . n = (- seq) /. m .= - (seq /. m) by A1, VFUNCT_1:def_5 .= - (seq . n) ; ::_thesis: verum end; theorem Th7: :: TOPRNS_1:7 for N being Element of NAT for r being Real for w being Point of (TOP-REAL N) holds (abs r) * |.w.| = |.(r * w).| by EUCLID:11; theorem :: TOPRNS_1:8 for N being Element of NAT for r being Real for seq being Real_Sequence of N holds |.(r * seq).| = (abs r) (#) |.seq.| proof let N be Element of NAT ; ::_thesis: for r being Real for seq being Real_Sequence of N holds |.(r * seq).| = (abs r) (#) |.seq.| let r be Real; ::_thesis: for seq being Real_Sequence of N holds |.(r * seq).| = (abs r) (#) |.seq.| let seq be Real_Sequence of N; ::_thesis: |.(r * seq).| = (abs r) (#) |.seq.| let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: |.(r * seq).| . n = ((abs r) (#) |.seq.|) . n thus |.(r * seq).| . n = |.((r * seq) . n).| by Def6 .= |.(r * (seq . n)).| by Th5 .= (abs r) * |.(seq . n).| by Th7 .= (abs r) * (|.seq.| . n) by Def6 .= ((abs r) (#) |.seq.|) . n by SEQ_1:9 ; ::_thesis: verum end; theorem :: TOPRNS_1:9 for N being Element of NAT for seq1, seq2 being Real_Sequence of N holds seq1 + seq2 = seq2 + seq1 proof let N be Element of NAT ; ::_thesis: for seq1, seq2 being Real_Sequence of N holds seq1 + seq2 = seq2 + seq1 let seq1, seq2 be Real_Sequence of N; ::_thesis: seq1 + seq2 = seq2 + seq1 let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (seq1 + seq2) . n = (seq2 + seq1) . n thus (seq1 + seq2) . n = (seq1 . n) + (seq2 . n) by Th4 .= (seq2 + seq1) . n by Th4 ; ::_thesis: verum end; theorem Th10: :: TOPRNS_1:10 for N being Element of NAT for seq1, seq2, seq3 being Real_Sequence of N holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3) proof let N be Element of NAT ; ::_thesis: for seq1, seq2, seq3 being Real_Sequence of N holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3) let seq1, seq2, seq3 be Real_Sequence of N; ::_thesis: (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3) let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((seq1 + seq2) + seq3) . n = (seq1 + (seq2 + seq3)) . n thus ((seq1 + seq2) + seq3) . n = ((seq1 + seq2) . n) + (seq3 . n) by Th4 .= ((seq1 . n) + (seq2 . n)) + (seq3 . n) by Th4 .= (seq1 . n) + ((seq2 . n) + (seq3 . n)) by EUCLID:26 .= (seq1 . n) + ((seq2 + seq3) . n) by Th4 .= (seq1 + (seq2 + seq3)) . n by Th4 ; ::_thesis: verum end; theorem Th11: :: TOPRNS_1:11 for N being Element of NAT for seq being Real_Sequence of N holds - seq = (- 1) * seq proof let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N holds - seq = (- 1) * seq let seq be Real_Sequence of N; ::_thesis: - seq = (- 1) * seq let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (- seq) . n = ((- 1) * seq) . n thus ((- 1) * seq) . n = (- 1) * (seq . n) by Th5 .= - (seq . n) by EUCLID:39 .= (- seq) . n by Th6 ; ::_thesis: verum end; theorem Th12: :: TOPRNS_1:12 for N being Element of NAT for r being Real for seq1, seq2 being Real_Sequence of N holds r * (seq1 + seq2) = (r * seq1) + (r * seq2) proof let N be Element of NAT ; ::_thesis: for r being Real for seq1, seq2 being Real_Sequence of N holds r * (seq1 + seq2) = (r * seq1) + (r * seq2) let r be Real; ::_thesis: for seq1, seq2 being Real_Sequence of N holds r * (seq1 + seq2) = (r * seq1) + (r * seq2) let seq1, seq2 be Real_Sequence of N; ::_thesis: r * (seq1 + seq2) = (r * seq1) + (r * seq2) let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (r * (seq1 + seq2)) . n = ((r * seq1) + (r * seq2)) . n thus (r * (seq1 + seq2)) . n = r * ((seq1 + seq2) . n) by Th5 .= r * ((seq1 . n) + (seq2 . n)) by Th4 .= (r * (seq1 . n)) + (r * (seq2 . n)) by EUCLID:32 .= ((r * seq1) . n) + (r * (seq2 . n)) by Th5 .= ((r * seq1) . n) + ((r * seq2) . n) by Th5 .= ((r * seq1) + (r * seq2)) . n by Th4 ; ::_thesis: verum end; theorem Th13: :: TOPRNS_1:13 for N being Element of NAT for r, q being Real for seq being Real_Sequence of N holds (r * q) * seq = r * (q * seq) proof let N be Element of NAT ; ::_thesis: for r, q being Real for seq being Real_Sequence of N holds (r * q) * seq = r * (q * seq) let r, q be Real; ::_thesis: for seq being Real_Sequence of N holds (r * q) * seq = r * (q * seq) let seq be Real_Sequence of N; ::_thesis: (r * q) * seq = r * (q * seq) let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((r * q) * seq) . n = (r * (q * seq)) . n thus ((r * q) * seq) . n = (r * q) * (seq . n) by Th5 .= r * (q * (seq . n)) by EUCLID:30 .= r * ((q * seq) . n) by Th5 .= (r * (q * seq)) . n by Th5 ; ::_thesis: verum end; theorem Th14: :: TOPRNS_1:14 for N being Element of NAT for r being Real for seq1, seq2 being Real_Sequence of N holds r * (seq1 - seq2) = (r * seq1) - (r * seq2) proof let N be Element of NAT ; ::_thesis: for r being Real for seq1, seq2 being Real_Sequence of N holds r * (seq1 - seq2) = (r * seq1) - (r * seq2) let r be Real; ::_thesis: for seq1, seq2 being Real_Sequence of N holds r * (seq1 - seq2) = (r * seq1) - (r * seq2) let seq1, seq2 be Real_Sequence of N; ::_thesis: r * (seq1 - seq2) = (r * seq1) - (r * seq2) thus r * (seq1 - seq2) = (r * seq1) + (r * (- seq2)) by Th12 .= (r * seq1) + (r * ((- 1) * seq2)) by Th11 .= (r * seq1) + (((- 1) * r) * seq2) by Th13 .= (r * seq1) + ((- 1) * (r * seq2)) by Th13 .= (r * seq1) - (r * seq2) by Th11 ; ::_thesis: verum end; theorem :: TOPRNS_1:15 for N being Element of NAT for seq1, seq2, seq3 being Real_Sequence of N holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3 proof let N be Element of NAT ; ::_thesis: for seq1, seq2, seq3 being Real_Sequence of N holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3 let seq1, seq2, seq3 be Real_Sequence of N; ::_thesis: seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3 thus seq1 - (seq2 + seq3) = seq1 + ((- 1) * (seq2 + seq3)) by Th11 .= seq1 + (((- 1) * seq2) + ((- 1) * seq3)) by Th12 .= seq1 + ((- seq2) + ((- 1) * seq3)) by Th11 .= seq1 + ((- seq2) + (- seq3)) by Th11 .= (seq1 - seq2) - seq3 by Th10 ; ::_thesis: verum end; theorem Th16: :: TOPRNS_1:16 for N being Element of NAT for seq being Real_Sequence of N holds 1 * seq = seq proof let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N holds 1 * seq = seq let seq be Real_Sequence of N; ::_thesis: 1 * seq = seq let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (1 * seq) . n = seq . n thus (1 * seq) . n = 1 * (seq . n) by Th5 .= seq . n by EUCLID:29 ; ::_thesis: verum end; theorem Th17: :: TOPRNS_1:17 for N being Element of NAT for seq being Real_Sequence of N holds - (- seq) = seq proof let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N holds - (- seq) = seq let seq be Real_Sequence of N; ::_thesis: - (- seq) = seq thus - (- seq) = (- 1) * (- seq) by Th11 .= (- 1) * ((- 1) * seq) by Th11 .= ((- 1) * (- 1)) * seq by Th13 .= seq by Th16 ; ::_thesis: verum end; theorem :: TOPRNS_1:18 for N being Element of NAT for seq1, seq2 being Real_Sequence of N holds seq1 - (- seq2) = seq1 + seq2 by Th17; theorem :: TOPRNS_1:19 for N being Element of NAT for seq1, seq2, seq3 being Real_Sequence of N holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3 proof let N be Element of NAT ; ::_thesis: for seq1, seq2, seq3 being Real_Sequence of N holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3 let seq1, seq2, seq3 be Real_Sequence of N; ::_thesis: seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3 thus seq1 - (seq2 - seq3) = seq1 + ((- 1) * (seq2 - seq3)) by Th11 .= seq1 + (((- 1) * seq2) - ((- 1) * seq3)) by Th14 .= seq1 + ((- seq2) - ((- 1) * seq3)) by Th11 .= seq1 + ((- seq2) - (- seq3)) by Th11 .= seq1 + ((- seq2) + seq3) by Th17 .= (seq1 - seq2) + seq3 by Th10 ; ::_thesis: verum end; theorem :: TOPRNS_1:20 for N being Element of NAT for seq1, seq2, seq3 being Real_Sequence of N holds seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3 by Th10; theorem Th21: :: TOPRNS_1:21 for N being Element of NAT for r being Real for seq being Real_Sequence of N st r <> 0 & seq is non-zero holds r * seq is non-zero proof let N be Element of NAT ; ::_thesis: for r being Real for seq being Real_Sequence of N st r <> 0 & seq is non-zero holds r * seq is non-zero let r be Real; ::_thesis: for seq being Real_Sequence of N st r <> 0 & seq is non-zero holds r * seq is non-zero let seq be Real_Sequence of N; ::_thesis: ( r <> 0 & seq is non-zero implies r * seq is non-zero ) assume that A1: r <> 0 and A2: seq is non-zero and A3: not r * seq is non-zero ; ::_thesis: contradiction consider n1 being Element of NAT such that A4: (r * seq) . n1 = 0. (TOP-REAL N) by A3, Th3; A5: seq . n1 <> 0. (TOP-REAL N) by A2, Th3; r * (seq . n1) = 0. (TOP-REAL N) by A4, Th5; hence contradiction by A1, A5, EUCLID:31; ::_thesis: verum end; theorem :: TOPRNS_1:22 for N being Element of NAT for seq being Real_Sequence of N st seq is non-zero holds - seq is non-zero proof let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N st seq is non-zero holds - seq is non-zero let seq be Real_Sequence of N; ::_thesis: ( seq is non-zero implies - seq is non-zero ) assume seq is non-zero ; ::_thesis: - seq is non-zero then (- 1) * seq is non-zero by Th21; hence - seq is non-zero by Th11; ::_thesis: verum end; theorem Th23: :: TOPRNS_1:23 for N being Element of NAT holds |.(0. (TOP-REAL N)).| = 0 proof let N be Element of NAT ; ::_thesis: |.(0. (TOP-REAL N)).| = 0 thus |.(0. (TOP-REAL N)).| = |.(0* N).| by EUCLID:70 .= 0 by EUCLID:7 ; ::_thesis: verum end; theorem Th24: :: TOPRNS_1:24 for N being Element of NAT for w being Point of (TOP-REAL N) st |.w.| = 0 holds w = 0. (TOP-REAL N) proof let N be Element of NAT ; ::_thesis: for w being Point of (TOP-REAL N) st |.w.| = 0 holds w = 0. (TOP-REAL N) let w be Point of (TOP-REAL N); ::_thesis: ( |.w.| = 0 implies w = 0. (TOP-REAL N) ) reconsider s = w as Element of REAL N by EUCLID:22; assume |.w.| = 0 ; ::_thesis: w = 0. (TOP-REAL N) then s = 0* N by EUCLID:8 .= 0. (TOP-REAL N) by EUCLID:70 ; hence w = 0. (TOP-REAL N) ; ::_thesis: verum end; theorem :: TOPRNS_1:25 for N being Element of NAT for w being Point of (TOP-REAL N) holds |.w.| >= 0 ; theorem :: TOPRNS_1:26 for N being Element of NAT for w being Point of (TOP-REAL N) holds |.(- w).| = |.w.| by EUCLID:71; theorem Th27: :: TOPRNS_1:27 for N being Element of NAT for w1, w2 being Point of (TOP-REAL N) holds |.(w1 - w2).| = |.(w2 - w1).| proof let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) holds |.(w1 - w2).| = |.(w2 - w1).| let w1, w2 be Point of (TOP-REAL N); ::_thesis: |.(w1 - w2).| = |.(w2 - w1).| thus |.(w1 - w2).| = |.(- (w1 - w2)).| by EUCLID:71 .= |.(w2 - w1).| by EUCLID:44 ; ::_thesis: verum end; Lm1: for N being Element of NAT for w1, w2 being Point of (TOP-REAL N) st |.(w1 - w2).| = 0 holds w1 = w2 proof let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) st |.(w1 - w2).| = 0 holds w1 = w2 let w1, w2 be Point of (TOP-REAL N); ::_thesis: ( |.(w1 - w2).| = 0 implies w1 = w2 ) assume |.(w1 - w2).| = 0 ; ::_thesis: w1 = w2 then w1 - w2 = 0. (TOP-REAL N) by Th24; hence w1 = w2 by EUCLID:43; ::_thesis: verum end; Lm2: for N being Element of NAT for w1, w2 being Point of (TOP-REAL N) st w1 = w2 holds |.(w1 - w2).| = 0 proof let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) st w1 = w2 holds |.(w1 - w2).| = 0 let w1, w2 be Point of (TOP-REAL N); ::_thesis: ( w1 = w2 implies |.(w1 - w2).| = 0 ) assume w1 = w2 ; ::_thesis: |.(w1 - w2).| = 0 then |.(w1 - w2).| = |.(0. (TOP-REAL N)).| by EUCLID:42 .= 0 by Th23 ; hence |.(w1 - w2).| = 0 ; ::_thesis: verum end; theorem :: TOPRNS_1:28 for N being Element of NAT for w1, w2 being Point of (TOP-REAL N) holds ( |.(w1 - w2).| = 0 iff w1 = w2 ) by Lm1, Lm2; theorem Th29: :: TOPRNS_1:29 for N being Element of NAT for w1, w2 being Point of (TOP-REAL N) holds |.(w1 + w2).| <= |.w1.| + |.w2.| proof let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) holds |.(w1 + w2).| <= |.w1.| + |.w2.| let w1, w2 be Point of (TOP-REAL N); ::_thesis: |.(w1 + w2).| <= |.w1.| + |.w2.| reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22; w1 + w2 = s1 + s2 ; hence |.(w1 + w2).| <= |.w1.| + |.w2.| by EUCLID:12; ::_thesis: verum end; theorem :: TOPRNS_1:30 for N being Element of NAT for w1, w2 being Point of (TOP-REAL N) holds |.(w1 - w2).| <= |.w1.| + |.w2.| proof let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) holds |.(w1 - w2).| <= |.w1.| + |.w2.| let w1, w2 be Point of (TOP-REAL N); ::_thesis: |.(w1 - w2).| <= |.w1.| + |.w2.| reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22; w1 - w2 = s1 - s2 ; hence |.(w1 - w2).| <= |.w1.| + |.w2.| by EUCLID:13; ::_thesis: verum end; theorem :: TOPRNS_1:31 for N being Element of NAT for w1, w2 being Point of (TOP-REAL N) holds |.w1.| - |.w2.| <= |.(w1 + w2).| proof let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) holds |.w1.| - |.w2.| <= |.(w1 + w2).| let w1, w2 be Point of (TOP-REAL N); ::_thesis: |.w1.| - |.w2.| <= |.(w1 + w2).| reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22; w1 + w2 = s1 + s2 ; hence |.w1.| - |.w2.| <= |.(w1 + w2).| by EUCLID:14; ::_thesis: verum end; theorem Th32: :: TOPRNS_1:32 for N being Element of NAT for w1, w2 being Point of (TOP-REAL N) holds |.w1.| - |.w2.| <= |.(w1 - w2).| proof let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) holds |.w1.| - |.w2.| <= |.(w1 - w2).| let w1, w2 be Point of (TOP-REAL N); ::_thesis: |.w1.| - |.w2.| <= |.(w1 - w2).| reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22; w1 - w2 = s1 - s2 ; hence |.w1.| - |.w2.| <= |.(w1 - w2).| by EUCLID:15; ::_thesis: verum end; theorem :: TOPRNS_1:33 for N being Element of NAT for w1, w2 being Point of (TOP-REAL N) st w1 <> w2 holds |.(w1 - w2).| > 0 proof let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) st w1 <> w2 holds |.(w1 - w2).| > 0 let w1, w2 be Point of (TOP-REAL N); ::_thesis: ( w1 <> w2 implies |.(w1 - w2).| > 0 ) reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22; s1 - s2 = w1 - w2 ; hence ( w1 <> w2 implies |.(w1 - w2).| > 0 ) by EUCLID:17; ::_thesis: verum end; theorem :: TOPRNS_1:34 for N being Element of NAT for w1, w2, w being Point of (TOP-REAL N) holds |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).| proof let N be Element of NAT ; ::_thesis: for w1, w2, w being Point of (TOP-REAL N) holds |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).| let w1, w2, w be Point of (TOP-REAL N); ::_thesis: |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).| 0. (TOP-REAL N) = w - w by EUCLID:42 .= (- w) + w by EUCLID:41 ; then |.(w1 - w2).| = |.((w1 + ((- w) + w)) - w2).| by EUCLID:27 .= |.(((w1 + (- w)) + w) - w2).| by EUCLID:26 .= |.(((w1 - w) + w) - w2).| by EUCLID:41 .= |.((w1 - w) + (w - w2)).| by EUCLID:45 ; hence |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).| by Th29; ::_thesis: verum end; definition let N be Element of NAT ; let IT be Real_Sequence of N; attrIT is bounded means :Def7: :: TOPRNS_1:def 7 ex r being Real st for n being Element of NAT holds |.(IT . n).| < r; end; :: deftheorem Def7 defines bounded TOPRNS_1:def_7_:_ for N being Element of NAT for IT being Real_Sequence of N holds ( IT is bounded iff ex r being Real st for n being Element of NAT holds |.(IT . n).| < r ); theorem Th35: :: TOPRNS_1:35 for N being Element of NAT for seq being Real_Sequence of N for n being Element of NAT ex r being Real st ( 0 < r & ( for m being Element of NAT st m <= n holds |.(seq . m).| < r ) ) proof let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N for n being Element of NAT ex r being Real st ( 0 < r & ( for m being Element of NAT st m <= n holds |.(seq . m).| < r ) ) let seq be Real_Sequence of N; ::_thesis: for n being Element of NAT ex r being Real st ( 0 < r & ( for m being Element of NAT st m <= n holds |.(seq . m).| < r ) ) defpred S1[ Element of NAT ] means ex r1 being Real st ( 0 < r1 & ( for m being Element of NAT st m <= \$1 holds |.(seq . m).| < r1 ) ); A1: 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] ) given r1 being Real such that A2: 0 < r1 and A3: for m being Element of NAT st m <= n holds |.(seq . m).| < r1 ; ::_thesis: S1[n + 1] A4: now__::_thesis:_(_r1_<=_|.(seq_._(n_+_1)).|_implies_ex_r_being_Element_of_REAL_st_ (_0_<_r_&_(_for_m_being_Element_of_NAT_st_m_<=_n_+_1_holds_ |.(seq_._m).|_<_r_)_)_) assume A5: r1 <= |.(seq . (n + 1)).| ; ::_thesis: ex r being Element of REAL st ( 0 < r & ( for m being Element of NAT st m <= n + 1 holds |.(seq . m).| < r ) ) take r = |.(seq . (n + 1)).| + 1; ::_thesis: ( 0 < r & ( for m being Element of NAT st m <= n + 1 holds |.(seq . m).| < r ) ) thus 0 < r ; ::_thesis: for m being Element of NAT st m <= n + 1 holds |.(seq . m).| < r let m be Element of NAT ; ::_thesis: ( m <= n + 1 implies |.(seq . m).| < r ) assume A6: m <= n + 1 ; ::_thesis: |.(seq . m).| < r A7: now__::_thesis:_(_m_<=_n_implies_|.(seq_._m).|_<_r_) assume m <= n ; ::_thesis: |.(seq . m).| < r then |.(seq . m).| < r1 by A3; then |.(seq . m).| < |.(seq . (n + 1)).| by A5, XXREAL_0:2; then |.(seq . m).| + 0 < r by XREAL_1:8; hence |.(seq . m).| < r ; ::_thesis: verum end; now__::_thesis:_(_m_=_n_+_1_implies_|.(seq_._m).|_<_r_) assume m = n + 1 ; ::_thesis: |.(seq . m).| < r then |.(seq . m).| + 0 < r by XREAL_1:8; hence |.(seq . m).| < r ; ::_thesis: verum end; hence |.(seq . m).| < r by A6, A7, NAT_1:8; ::_thesis: verum end; now__::_thesis:_(_|.(seq_._(n_+_1)).|_<=_r1_implies_ex_r_being_Element_of_REAL_st_ (_0_<_r_&_(_for_m_being_Element_of_NAT_st_m_<=_n_+_1_holds_ |.(seq_._m).|_<_r_)_)_) assume A8: |.(seq . (n + 1)).| <= r1 ; ::_thesis: ex r being Element of REAL st ( 0 < r & ( for m being Element of NAT st m <= n + 1 holds |.(seq . m).| < r ) ) take r = r1 + 1; ::_thesis: ( 0 < r & ( for m being Element of NAT st m <= n + 1 holds |.(seq . m).| < r ) ) thus 0 < r by A2; ::_thesis: for m being Element of NAT st m <= n + 1 holds |.(seq . m).| < r let m be Element of NAT ; ::_thesis: ( m <= n + 1 implies |.(seq . m).| < r ) assume A9: m <= n + 1 ; ::_thesis: |.(seq . m).| < r A10: now__::_thesis:_(_m_<=_n_implies_|.(seq_._m).|_<_r_) assume m <= n ; ::_thesis: |.(seq . m).| < r then A11: |.(seq . m).| < r1 by A3; r1 + 0 < r by XREAL_1:8; hence |.(seq . m).| < r by A11, XXREAL_0:2; ::_thesis: verum end; now__::_thesis:_(_m_=_n_+_1_implies_|.(seq_._m).|_<_r_) A12: r1 + 0 < r by XREAL_1:8; assume m = n + 1 ; ::_thesis: |.(seq . m).| < r hence |.(seq . m).| < r by A8, A12, XXREAL_0:2; ::_thesis: verum end; hence |.(seq . m).| < r by A9, A10, NAT_1:8; ::_thesis: verum end; hence S1[n + 1] by A4; ::_thesis: verum end; A13: S1[ 0 ] proof take r = |.(seq . 0).| + 1; ::_thesis: ( 0 < r & ( for m being Element of NAT st m <= 0 holds |.(seq . m).| < r ) ) thus 0 < r ; ::_thesis: for m being Element of NAT st m <= 0 holds |.(seq . m).| < r let m be Element of NAT ; ::_thesis: ( m <= 0 implies |.(seq . m).| < r ) assume m <= 0 ; ::_thesis: |.(seq . m).| < r then 0 = m ; then |.(seq . m).| + 0 < r by XREAL_1:8; hence |.(seq . m).| < r ; ::_thesis: verum end; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A13, A1); ::_thesis: verum end; definition let N be Element of NAT ; let IT be Real_Sequence of N; attrIT is convergent means :Def8: :: TOPRNS_1:def 8 ex g being Point of (TOP-REAL N) st for r being Real st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((IT . m) - g).| < r; end; :: deftheorem Def8 defines convergent TOPRNS_1:def_8_:_ for N being Element of NAT for IT being Real_Sequence of N holds ( IT is convergent iff ex g being Point of (TOP-REAL N) st for r being Real st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((IT . m) - g).| < r ); definition let N be Element of NAT ; let seq be Real_Sequence of N; assume A1: seq is convergent ; func lim seq -> Point of (TOP-REAL N) means :Def9: :: TOPRNS_1:def 9 for r being Real st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - it).| < r; existence ex b1 being Point of (TOP-REAL N) st for r being Real st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - b1).| < r by A1, Def8; uniqueness for b1, b2 being Point of (TOP-REAL N) st ( for r being Real st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - b1).| < r ) & ( for r being Real st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - b2).| < r ) holds b1 = b2 proof given g1, g2 being Point of (TOP-REAL N) such that A2: for r being Real st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - g1).| < r and A3: for r being Real st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - g2).| < r and A4: g1 <> g2 ; ::_thesis: contradiction A5: now__::_thesis:_not_|.(g1_-_g2).|_=_0 assume |.(g1 - g2).| = 0 ; ::_thesis: contradiction then (0. (TOP-REAL N)) + g2 = (g1 - g2) + g2 by Th24; then g2 = (g1 - g2) + g2 by EUCLID:27 .= g1 - (g2 - g2) by EUCLID:47 .= g1 - (0. (TOP-REAL N)) by EUCLID:42 .= g1 + (- (0. (TOP-REAL N))) by EUCLID:41 .= g1 + ((- 1) * (0. (TOP-REAL N))) by EUCLID:39 .= g1 + (0. (TOP-REAL N)) by EUCLID:28 .= g1 by EUCLID:27 ; hence contradiction by A4; ::_thesis: verum end; then consider n1 being Element of NAT such that A6: for m being Element of NAT st n1 <= m holds |.((seq . m) - g1).| < |.(g1 - g2).| / 4 by A2, XREAL_1:224; consider n2 being Element of NAT such that A7: for m being Element of NAT st n2 <= m holds |.((seq . m) - g2).| < |.(g1 - g2).| / 4 by A3, A5, XREAL_1:224; A8: |.((seq . (n1 + n2)) - g2).| < |.(g1 - g2).| / 4 by A7, NAT_1:12; |.((seq . (n1 + n2)) - g1).| < |.(g1 - g2).| / 4 by A6, NAT_1:12; then A9: |.((seq . (n1 + n2)) - g2).| + |.((seq . (n1 + n2)) - g1).| < (|.(g1 - g2).| / 4) + (|.(g1 - g2).| / 4) by A8, XREAL_1:8; |.(g1 - g2).| = |.((g1 - g2) + (0. (TOP-REAL N))).| by EUCLID:27 .= |.((g1 - g2) + ((- 1) * (0. (TOP-REAL N)))).| by EUCLID:28 .= |.((g1 - g2) + (- (0. (TOP-REAL N)))).| by EUCLID:39 .= |.((g1 - g2) - (0. (TOP-REAL N))).| by EUCLID:41 .= |.((g1 - g2) - ((seq . (n1 + n2)) - (seq . (n1 + n2)))).| by EUCLID:42 .= |.(((g1 - g2) - (seq . (n1 + n2))) + (seq . (n1 + n2))).| by EUCLID:47 .= |.((g1 - ((seq . (n1 + n2)) + g2)) + (seq . (n1 + n2))).| by EUCLID:46 .= |.(((g1 - (seq . (n1 + n2))) - g2) + (seq . (n1 + n2))).| by EUCLID:46 .= |.((g1 - (seq . (n1 + n2))) - (g2 - (seq . (n1 + n2)))).| by EUCLID:47 .= |.((g1 - (seq . (n1 + n2))) + (- (g2 - (seq . (n1 + n2))))).| by EUCLID:41 .= |.((g1 - (seq . (n1 + n2))) + ((seq . (n1 + n2)) - g2)).| by EUCLID:44 .= |.((- ((seq . (n1 + n2)) - g1)) + ((seq . (n1 + n2)) - g2)).| by EUCLID:44 ; then |.(g1 - g2).| <= |.(- ((seq . (n1 + n2)) - g1)).| + |.((seq . (n1 + n2)) - g2).| by Th29; then A10: |.(g1 - g2).| <= |.((seq . (n1 + n2)) - g1).| + |.((seq . (n1 + n2)) - g2).| by EUCLID:71; |.(g1 - g2).| / 2 < |.(g1 - g2).| by A5, XREAL_1:216; hence contradiction by A9, A10, XXREAL_0:2; ::_thesis: verum end; end; :: deftheorem Def9 defines lim TOPRNS_1:def_9_:_ for N being Element of NAT for seq being Real_Sequence of N st seq is convergent holds for b3 being Point of (TOP-REAL N) holds ( b3 = lim seq iff for r being Real st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - b3).| < r ); theorem Th36: :: TOPRNS_1:36 for N being Element of NAT for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds seq + seq9 is convergent proof let N be Element of NAT ; ::_thesis: for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds seq + seq9 is convergent let seq, seq9 be Real_Sequence of N; ::_thesis: ( seq is convergent & seq9 is convergent implies seq + seq9 is convergent ) assume that A1: seq is convergent and A2: seq9 is convergent ; ::_thesis: seq + seq9 is convergent consider g1 being Point of (TOP-REAL N) such that A3: for r being Real st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - g1).| < r by A1, Def8; consider g2 being Point of (TOP-REAL N) such that A4: for r being Real st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq9 . m) - g2).| < r by A2, Def8; take g = g1 + g2; :: according to TOPRNS_1:def_8 ::_thesis: for r being Real st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((seq + seq9) . m) - g).| < r let r be Real; ::_thesis: ( 0 < r implies ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((seq + seq9) . m) - g).| < r ) assume A5: 0 < r ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((seq + seq9) . m) - g).| < r then consider n1 being Element of NAT such that A6: for m being Element of NAT st n1 <= m holds |.((seq . m) - g1).| < r / 2 by A3, XREAL_1:215; consider n2 being Element of NAT such that A7: for m being Element of NAT st n2 <= m holds |.((seq9 . m) - g2).| < r / 2 by A4, A5, XREAL_1:215; take k = n1 + n2; ::_thesis: for m being Element of NAT st k <= m holds |.(((seq + seq9) . m) - g).| < r let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((seq + seq9) . m) - g).| < r ) assume A8: k <= m ; ::_thesis: |.(((seq + seq9) . m) - g).| < r n2 <= k by NAT_1:12; then n2 <= m by A8, XXREAL_0:2; then A9: |.((seq9 . m) - g2).| < r / 2 by A7; A10: |.(((seq + seq9) . m) - g).| = |.(((seq . m) + (seq9 . m)) - (g1 + g2)).| by Th4 .= |.((seq . m) + ((seq9 . m) - (g1 + g2))).| by EUCLID:45 .= |.((seq . m) + ((- (g1 + g2)) + (seq9 . m))).| by EUCLID:41 .= |.(((seq . m) + (- (g1 + g2))) + (seq9 . m)).| by EUCLID:26 .= |.(((seq . m) - (g1 + g2)) + (seq9 . m)).| by EUCLID:41 .= |.((((seq . m) - g1) - g2) + (seq9 . m)).| by EUCLID:46 .= |.((((seq . m) - g1) + (- g2)) + (seq9 . m)).| by EUCLID:41 .= |.(((seq . m) - g1) + ((seq9 . m) + (- g2))).| by EUCLID:26 .= |.(((seq . m) - g1) + ((seq9 . m) - g2)).| by EUCLID:41 ; A11: |.(((seq . m) - g1) + ((seq9 . m) - g2)).| <= |.((seq . m) - g1).| + |.((seq9 . m) - g2).| by Th29; n1 <= n1 + n2 by NAT_1:12; then n1 <= m by A8, XXREAL_0:2; then |.((seq . m) - g1).| < r / 2 by A6; then |.((seq . m) - g1).| + |.((seq9 . m) - g2).| < (r / 2) + (r / 2) by A9, XREAL_1:8; hence |.(((seq + seq9) . m) - g).| < r by A10, A11, XXREAL_0:2; ::_thesis: verum end; theorem Th37: :: TOPRNS_1:37 for N being Element of NAT for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds lim (seq + seq9) = (lim seq) + (lim seq9) proof let N be Element of NAT ; ::_thesis: for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds lim (seq + seq9) = (lim seq) + (lim seq9) let seq, seq9 be Real_Sequence of N; ::_thesis: ( seq is convergent & seq9 is convergent implies lim (seq + seq9) = (lim seq) + (lim seq9) ) assume that A1: seq is convergent and A2: seq9 is convergent ; ::_thesis: lim (seq + seq9) = (lim seq) + (lim seq9) A3: now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ |.(((seq_+_seq9)_._m)_-_((lim_seq)_+_(lim_seq9))).|_<_r let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r ) assume 0 < r ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r then A4: 0 < r / 2 by XREAL_1:215; then consider n1 being Element of NAT such that A5: for m being Element of NAT st n1 <= m holds |.((seq . m) - (lim seq)).| < r / 2 by A1, Def9; consider n2 being Element of NAT such that A6: for m being Element of NAT st n2 <= m holds |.((seq9 . m) - (lim seq9)).| < r / 2 by A2, A4, Def9; take k = n1 + n2; ::_thesis: for m being Element of NAT st k <= m holds |.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r ) assume A7: k <= m ; ::_thesis: |.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r n2 <= k by NAT_1:12; then n2 <= m by A7, XXREAL_0:2; then A8: |.((seq9 . m) - (lim seq9)).| < r / 2 by A6; A9: |.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| = |.((((seq + seq9) . m) - (lim seq)) - (lim seq9)).| by EUCLID:46 .= |.((((seq . m) + (seq9 . m)) - (lim seq)) - (lim seq9)).| by Th4 .= |.(((seq . m) + ((seq9 . m) - (lim seq))) - (lim seq9)).| by EUCLID:45 .= |.(((seq . m) + ((- (lim seq)) + (seq9 . m))) - (lim seq9)).| by EUCLID:41 .= |.((((seq . m) + (- (lim seq))) + (seq9 . m)) - (lim seq9)).| by EUCLID:26 .= |.((((seq . m) - (lim seq)) + (seq9 . m)) - (lim seq9)).| by EUCLID:41 .= |.(((seq . m) - (lim seq)) + ((seq9 . m) - (lim seq9))).| by EUCLID:45 ; A10: |.(((seq . m) - (lim seq)) + ((seq9 . m) - (lim seq9))).| <= |.((seq . m) - (lim seq)).| + |.((seq9 . m) - (lim seq9)).| by Th29; n1 <= n1 + n2 by NAT_1:12; then n1 <= m by A7, XXREAL_0:2; then |.((seq . m) - (lim seq)).| < r / 2 by A5; then |.((seq . m) - (lim seq)).| + |.((seq9 . m) - (lim seq9)).| < (r / 2) + (r / 2) by A8, XREAL_1:8; hence |.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r by A9, A10, XXREAL_0:2; ::_thesis: verum end; seq + seq9 is convergent by A1, A2, Th36; hence lim (seq + seq9) = (lim seq) + (lim seq9) by A3, Def9; ::_thesis: verum end; theorem Th38: :: TOPRNS_1:38 for N being Element of NAT for r being Real for seq being Real_Sequence of N st seq is convergent holds r * seq is convergent proof let N be Element of NAT ; ::_thesis: for r being Real for seq being Real_Sequence of N st seq is convergent holds r * seq is convergent let r be Real; ::_thesis: for seq being Real_Sequence of N st seq is convergent holds r * seq is convergent let seq be Real_Sequence of N; ::_thesis: ( seq is convergent implies r * seq is convergent ) assume seq is convergent ; ::_thesis: r * seq is convergent then consider g1 being Point of (TOP-REAL N) such that A1: for q being Real st 0 < q holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - g1).| < q by Def8; set g = r * g1; A2: now__::_thesis:_(_r_<>_0_implies_for_q_being_Real_st_0_<_q_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ |.(((r_*_seq)_._m)_-_(r_*_g1)).|_<_q_) A3: 0 / (abs r) = 0 ; assume A4: r <> 0 ; ::_thesis: for q being Real st 0 < q holds ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * g1)).| < q then A5: 0 < abs r by COMPLEX1:47; let q be Real; ::_thesis: ( 0 < q implies ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * g1)).| < q ) assume 0 < q ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * g1)).| < q then consider n1 being Element of NAT such that A6: for m being Element of NAT st n1 <= m holds |.((seq . m) - g1).| < q / (abs r) by A1, A5, A3, XREAL_1:74; take k = n1; ::_thesis: for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * g1)).| < q let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((r * seq) . m) - (r * g1)).| < q ) assume k <= m ; ::_thesis: |.(((r * seq) . m) - (r * g1)).| < q then A7: |.((seq . m) - g1).| < q / (abs r) by A6; A8: 0 < abs r by A4, COMPLEX1:47; A9: (abs r) * (q / (abs r)) = (abs r) * (((abs r) ") * q) by XCMPLX_0:def_9 .= ((abs r) * ((abs r) ")) * q .= 1 * q by A8, XCMPLX_0:def_7 .= q ; |.(((r * seq) . m) - (r * g1)).| = |.((r * (seq . m)) - (r * g1)).| by Th5 .= |.(r * ((seq . m) - g1)).| by EUCLID:49 .= (abs r) * |.((seq . m) - g1).| by Th7 ; hence |.(((r * seq) . m) - (r * g1)).| < q by A5, A7, A9, XREAL_1:68; ::_thesis: verum end; now__::_thesis:_(_r_=_0_implies_for_q_being_Real_st_0_<_q_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ |.(((r_*_seq)_._m)_-_(r_*_g1)).|_<_q_) assume A10: r = 0 ; ::_thesis: for q being Real st 0 < q holds ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * g1)).| < q let q be Real; ::_thesis: ( 0 < q implies ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * g1)).| < q ) assume A11: 0 < q ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * g1)).| < q take k = 0 ; ::_thesis: for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * g1)).| < q let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((r * seq) . m) - (r * g1)).| < q ) assume k <= m ; ::_thesis: |.(((r * seq) . m) - (r * g1)).| < q |.(((r * seq) . m) - (r * g1)).| = |.(((0 * seq) . m) - (0. (TOP-REAL N))).| by A10, EUCLID:29 .= |.((0. (TOP-REAL N)) - ((0 * seq) . m)).| by Th27 .= |.((0. (TOP-REAL N)) + (- ((0 * seq) . m))).| by EUCLID:41 .= |.(- ((0 * seq) . m)).| by EUCLID:27 .= |.((0 * seq) . m).| by EUCLID:71 .= |.(0 * (seq . m)).| by Th5 .= |.(0. (TOP-REAL N)).| by EUCLID:29 .= 0 by Th23 ; hence |.(((r * seq) . m) - (r * g1)).| < q by A11; ::_thesis: verum end; hence r * seq is convergent by A2, Def8; ::_thesis: verum end; theorem Th39: :: TOPRNS_1:39 for N being Element of NAT for r being Real for seq being Real_Sequence of N st seq is convergent holds lim (r * seq) = r * (lim seq) proof let N be Element of NAT ; ::_thesis: for r being Real for seq being Real_Sequence of N st seq is convergent holds lim (r * seq) = r * (lim seq) let r be Real; ::_thesis: for seq being Real_Sequence of N st seq is convergent holds lim (r * seq) = r * (lim seq) let seq be Real_Sequence of N; ::_thesis: ( seq is convergent implies lim (r * seq) = r * (lim seq) ) A1: now__::_thesis:_(_r_=_0_implies_for_q_being_Real_st_0_<_q_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ |.(((r_*_seq)_._m)_-_(r_*_(lim_seq))).|_<_q_) assume A2: r = 0 ; ::_thesis: for q being Real st 0 < q holds ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * (lim seq))).| < q let q be Real; ::_thesis: ( 0 < q implies ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * (lim seq))).| < q ) assume A3: 0 < q ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * (lim seq))).| < q take k = 0 ; ::_thesis: for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * (lim seq))).| < q let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((r * seq) . m) - (r * (lim seq))).| < q ) assume k <= m ; ::_thesis: |.(((r * seq) . m) - (r * (lim seq))).| < q r * (lim seq) = 0. (TOP-REAL N) by A2, EUCLID:29; then |.(((r * seq) . m) - (r * (lim seq))).| = |.((0 * (seq . m)) - (0. (TOP-REAL N))).| by A2, Th5 .= |.((0. (TOP-REAL N)) - (0 * (seq . m))).| by Th27 .= |.((0. (TOP-REAL N)) + (- (0 * (seq . m)))).| by EUCLID:41 .= |.(- (0 * (seq . m))).| by EUCLID:27 .= |.(0 * (seq . m)).| by EUCLID:71 .= |.(0. (TOP-REAL N)).| by EUCLID:29 .= 0 by Th23 ; hence |.(((r * seq) . m) - (r * (lim seq))).| < q by A3; ::_thesis: verum end; assume A4: seq is convergent ; ::_thesis: lim (r * seq) = r * (lim seq) A5: now__::_thesis:_(_r_<>_0_implies_for_q_being_Real_st_0_<_q_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ |.(((r_*_seq)_._m)_-_(r_*_(lim_seq))).|_<_q_) A6: 0 / (abs r) = 0 ; assume A7: r <> 0 ; ::_thesis: for q being Real st 0 < q holds ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * (lim seq))).| < q then A8: 0 < abs r by COMPLEX1:47; let q be Real; ::_thesis: ( 0 < q implies ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * (lim seq))).| < q ) assume 0 < q ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * (lim seq))).| < q then 0 < q / (abs r) by A8, A6, XREAL_1:74; then consider n1 being Element of NAT such that A9: for m being Element of NAT st n1 <= m holds |.((seq . m) - (lim seq)).| < q / (abs r) by A4, Def9; take k = n1; ::_thesis: for m being Element of NAT st k <= m holds |.(((r * seq) . m) - (r * (lim seq))).| < q let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((r * seq) . m) - (r * (lim seq))).| < q ) assume k <= m ; ::_thesis: |.(((r * seq) . m) - (r * (lim seq))).| < q then A10: |.((seq . m) - (lim seq)).| < q / (abs r) by A9; A11: 0 <> abs r by A7, COMPLEX1:47; A12: (abs r) * (q / (abs r)) = (abs r) * (((abs r) ") * q) by XCMPLX_0:def_9 .= ((abs r) * ((abs r) ")) * q .= 1 * q by A11, XCMPLX_0:def_7 .= q ; |.(((r * seq) . m) - (r * (lim seq))).| = |.((r * (seq . m)) - (r * (lim seq))).| by Th5 .= |.(r * ((seq . m) - (lim seq))).| by EUCLID:49 .= (abs r) * |.((seq . m) - (lim seq)).| by Th7 ; hence |.(((r * seq) . m) - (r * (lim seq))).| < q by A8, A10, A12, XREAL_1:68; ::_thesis: verum end; r * seq is convergent by A4, Th38; hence lim (r * seq) = r * (lim seq) by A1, A5, Def9; ::_thesis: verum end; theorem Th40: :: TOPRNS_1:40 for N being Element of NAT for seq being Real_Sequence of N st seq is convergent holds - seq is convergent proof let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N st seq is convergent holds - seq is convergent let seq be Real_Sequence of N; ::_thesis: ( seq is convergent implies - seq is convergent ) assume seq is convergent ; ::_thesis: - seq is convergent then (- 1) * seq is convergent by Th38; hence - seq is convergent by Th11; ::_thesis: verum end; theorem Th41: :: TOPRNS_1:41 for N being Element of NAT for seq being Real_Sequence of N st seq is convergent holds lim (- seq) = - (lim seq) proof let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N st seq is convergent holds lim (- seq) = - (lim seq) let seq be Real_Sequence of N; ::_thesis: ( seq is convergent implies lim (- seq) = - (lim seq) ) assume seq is convergent ; ::_thesis: lim (- seq) = - (lim seq) then lim ((- 1) * seq) = (- 1) * (lim seq) by Th39 .= - (1 * (lim seq)) by EUCLID:40 .= - (lim seq) by EUCLID:29 ; hence lim (- seq) = - (lim seq) by Th11; ::_thesis: verum end; theorem :: TOPRNS_1:42 for N being Element of NAT for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds seq - seq9 is convergent proof let N be Element of NAT ; ::_thesis: for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds seq - seq9 is convergent let seq, seq9 be Real_Sequence of N; ::_thesis: ( seq is convergent & seq9 is convergent implies seq - seq9 is convergent ) assume that A1: seq is convergent and A2: seq9 is convergent ; ::_thesis: seq - seq9 is convergent - seq9 is convergent by A2, Th40; hence seq - seq9 is convergent by A1, Th36; ::_thesis: verum end; theorem :: TOPRNS_1:43 for N being Element of NAT for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds lim (seq - seq9) = (lim seq) - (lim seq9) proof let N be Element of NAT ; ::_thesis: for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds lim (seq - seq9) = (lim seq) - (lim seq9) let seq, seq9 be Real_Sequence of N; ::_thesis: ( seq is convergent & seq9 is convergent implies lim (seq - seq9) = (lim seq) - (lim seq9) ) assume that A1: seq is convergent and A2: seq9 is convergent ; ::_thesis: lim (seq - seq9) = (lim seq) - (lim seq9) - seq9 is convergent by A2, Th40; hence lim (seq - seq9) = (lim seq) + (lim (- seq9)) by A1, Th37 .= (lim seq) + (- (lim seq9)) by A2, Th41 .= (lim seq) - (lim seq9) by EUCLID:41 ; ::_thesis: verum end; theorem :: TOPRNS_1:44 for N being Element of NAT for seq being Real_Sequence of N st seq is convergent holds seq is bounded proof let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N st seq is convergent holds seq is bounded let seq be Real_Sequence of N; ::_thesis: ( seq is convergent implies seq is bounded ) assume seq is convergent ; ::_thesis: seq is bounded then consider g being Point of (TOP-REAL N) such that A1: for r being Real st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - g).| < r by Def8; consider n1 being Element of NAT such that A2: for m being Element of NAT st n1 <= m holds |.((seq . m) - g).| < 1 by A1; A3: now__::_thesis:_ex_r_being_Element_of_REAL_st_ (_0_<_r_&_(_for_m_being_Element_of_NAT_st_n1_<=_m_holds_ |.(seq_._m).|_<_r_)_) take r = |.g.| + 1; ::_thesis: ( 0 < r & ( for m being Element of NAT st n1 <= m holds |.(seq . m).| < r ) ) thus 0 < r ; ::_thesis: for m being Element of NAT st n1 <= m holds |.(seq . m).| < r let m be Element of NAT ; ::_thesis: ( n1 <= m implies |.(seq . m).| < r ) A4: (|.(seq . m).| - |.g.|) + |.g.| = |.(seq . m).| ; assume n1 <= m ; ::_thesis: |.(seq . m).| < r then A5: |.((seq . m) - g).| < 1 by A2; |.(seq . m).| - |.g.| <= |.((seq . m) - g).| by Th32; then |.(seq . m).| - |.g.| < 1 by A5, XXREAL_0:2; hence |.(seq . m).| < r by A4, XREAL_1:6; ::_thesis: verum end; now__::_thesis:_ex_r_being_Element_of_REAL_st_ (_0_<_r_&_(_for_m_being_Element_of_NAT_holds_|.(seq_._m).|_<_r_)_) consider r2 being Real such that A6: 0 < r2 and A7: for m being Element of NAT st m <= n1 holds |.(seq . m).| < r2 by Th35; consider r1 being Real such that A8: 0 < r1 and A9: for m being Element of NAT st n1 <= m holds |.(seq . m).| < r1 by A3; take r = r1 + r2; ::_thesis: ( 0 < r & ( for m being Element of NAT holds |.(seq . m).| < r ) ) thus 0 < r by A8, A6; ::_thesis: for m being Element of NAT holds |.(seq . m).| < r let m be Element of NAT ; ::_thesis: |.(seq . m).| < r A10: 0 + r2 < r by A8, XREAL_1:8; A11: now__::_thesis:_(_m_<=_n1_implies_|.(seq_._m).|_<_r_) assume m <= n1 ; ::_thesis: |.(seq . m).| < r then |.(seq . m).| < r2 by A7; hence |.(seq . m).| < r by A10, XXREAL_0:2; ::_thesis: verum end; A12: r1 + 0 < r by A6, XREAL_1:8; now__::_thesis:_(_n1_<=_m_implies_|.(seq_._m).|_<_r_) assume n1 <= m ; ::_thesis: |.(seq . m).| < r then |.(seq . m).| < r1 by A9; hence |.(seq . m).| < r by A12, XXREAL_0:2; ::_thesis: verum end; hence |.(seq . m).| < r by A11; ::_thesis: verum end; hence seq is bounded by Def7; ::_thesis: verum end; theorem :: TOPRNS_1:45 for N being Element of NAT for seq being Real_Sequence of N st seq is convergent & lim seq <> 0. (TOP-REAL N) holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(lim seq).| / 2 < |.(seq . m).| proof let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N st seq is convergent & lim seq <> 0. (TOP-REAL N) holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(lim seq).| / 2 < |.(seq . m).| let seq be Real_Sequence of N; ::_thesis: ( seq is convergent & lim seq <> 0. (TOP-REAL N) implies ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(lim seq).| / 2 < |.(seq . m).| ) assume that A1: seq is convergent and A2: lim seq <> 0. (TOP-REAL N) ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(lim seq).| / 2 < |.(seq . m).| 0 <> |.(lim seq).| by A2, Th24; then 0 < |.(lim seq).| / 2 by XREAL_1:215; then consider n1 being Element of NAT such that A3: for m being Element of NAT st n1 <= m holds |.((seq . m) - (lim seq)).| < |.(lim seq).| / 2 by A1, Def9; take n = n1; ::_thesis: for m being Element of NAT st n <= m holds |.(lim seq).| / 2 < |.(seq . m).| let m be Element of NAT ; ::_thesis: ( n <= m implies |.(lim seq).| / 2 < |.(seq . m).| ) assume n <= m ; ::_thesis: |.(lim seq).| / 2 < |.(seq . m).| then A4: |.((seq . m) - (lim seq)).| < |.(lim seq).| / 2 by A3; ( |.(lim seq).| - |.(seq . m).| <= |.((lim seq) - (seq . m)).| & |.((lim seq) - (seq . m)).| = |.((seq . m) - (lim seq)).| ) by Th27, Th32; then A5: |.(lim seq).| - |.(seq . m).| < |.(lim seq).| / 2 by A4, XXREAL_0:2; ( (|.(lim seq).| / 2) + (|.(seq . m).| - (|.(lim seq).| / 2)) = |.(seq . m).| & (|.(lim seq).| - |.(seq . m).|) + (|.(seq . m).| - (|.(lim seq).| / 2)) = |.(lim seq).| / 2 ) ; hence |.(lim seq).| / 2 < |.(seq . m).| by A5, XREAL_1:6; ::_thesis: verum end;