:: Convergence and the Limit of Complex Sequences. Series
:: by Yasunari Shidama and Artur Korni{\l}owicz
::
:: Received June 25, 1997
:: Copyright (c) 1997 Association of Mizar Users
Lm1:
0c = 0 + (0 * <i> )
;
theorem :: COMSEQ_3:1
theorem Th2: :: COMSEQ_3:2
theorem Th3: :: COMSEQ_3:3
reconsider C = NAT --> 0 as Real_Sequence by FUNCOP_1:57;
Lm2:
for n being Element of NAT holds C . n = 0
by FUNCOP_1:13;
theorem :: COMSEQ_3:4
theorem :: COMSEQ_3:5
theorem :: COMSEQ_3:6
theorem :: COMSEQ_3:7
theorem :: COMSEQ_3:8
theorem :: COMSEQ_3:9
theorem :: COMSEQ_3:10
Lm3:
for seq being Complex_Sequence
for n being Element of NAT holds
( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n )
:: deftheorem Def1 defines GeoSeq COMSEQ_3:def 1 :
:: deftheorem defines #N COMSEQ_3:def 2 :
theorem :: COMSEQ_3:11
:: deftheorem Def3 defines Re COMSEQ_3:def 3 :
:: deftheorem Def4 defines Im COMSEQ_3:def 4 :
theorem Th12: :: COMSEQ_3:12
theorem Th13: :: COMSEQ_3:13
theorem Th14: :: COMSEQ_3:14
theorem Th15: :: COMSEQ_3:15
theorem Th16: :: COMSEQ_3:16
theorem Th17: :: COMSEQ_3:17
theorem Th18: :: COMSEQ_3:18
theorem :: COMSEQ_3:19
theorem :: COMSEQ_3:20
theorem :: COMSEQ_3:21
theorem Th22: :: COMSEQ_3:22
theorem Th23: :: COMSEQ_3:23
:: deftheorem COMSEQ_3:def 5 :
canceled;
:: deftheorem COMSEQ_3:def 6 :
canceled;
:: deftheorem Def7 defines Partial_Sums COMSEQ_3:def 7 :
:: deftheorem defines Sum COMSEQ_3:def 8 :
theorem Th24: :: COMSEQ_3:24
theorem Th25: :: COMSEQ_3:25
theorem Th26: :: COMSEQ_3:26
theorem Th27: :: COMSEQ_3:27
theorem Th28: :: COMSEQ_3:28
theorem Th29: :: COMSEQ_3:29
theorem :: COMSEQ_3:30
theorem Th31: :: COMSEQ_3:31
theorem Th32: :: COMSEQ_3:32
theorem :: COMSEQ_3:33
theorem Th34: :: COMSEQ_3:34
theorem :: COMSEQ_3:35
theorem Th36: :: COMSEQ_3:36
theorem Th37: :: COMSEQ_3:37
theorem Th38: :: COMSEQ_3:38
theorem Th39: :: COMSEQ_3:39
theorem Th40: :: COMSEQ_3:40
theorem Th41: :: COMSEQ_3:41
theorem Th42: :: COMSEQ_3:42
theorem Th43: :: COMSEQ_3:43
theorem Th44: :: COMSEQ_3:44
theorem :: COMSEQ_3:45
theorem Th46: :: COMSEQ_3:46
theorem :: COMSEQ_3:47
theorem :: COMSEQ_3:48
theorem :: COMSEQ_3:49
theorem :: COMSEQ_3:50
canceled;
theorem :: COMSEQ_3:51
:: deftheorem COMSEQ_3:def 9 :
canceled;
:: deftheorem Def10 defines summable COMSEQ_3:def 10 :
set D = NAT --> 0c ;
:: deftheorem Def11 defines absolutely_summable COMSEQ_3:def 11 :
theorem Th52: :: COMSEQ_3:52
theorem Th53: :: COMSEQ_3:53
theorem Th54: :: COMSEQ_3:54
theorem Th55: :: COMSEQ_3:55
theorem Th56: :: COMSEQ_3:56
theorem Th57: :: COMSEQ_3:57
theorem Th58: :: COMSEQ_3:58
theorem Th59: :: COMSEQ_3:59
theorem :: COMSEQ_3:60
theorem :: COMSEQ_3:61
theorem Th62: :: COMSEQ_3:62
theorem Th63: :: COMSEQ_3:63
theorem Th64: :: COMSEQ_3:64
theorem Th65: :: COMSEQ_3:65
theorem :: COMSEQ_3:66
theorem :: COMSEQ_3:67
theorem :: COMSEQ_3:68
theorem :: COMSEQ_3:69
theorem :: COMSEQ_3:70
theorem :: COMSEQ_3:71
theorem :: COMSEQ_3:72
theorem :: COMSEQ_3:73
theorem :: COMSEQ_3:74
theorem :: COMSEQ_3:75
theorem :: COMSEQ_3:76
theorem :: COMSEQ_3:77