:: Series
:: by Konrad Raczkowski and Andrzej N\c{e}dzusiak
::
:: Received October 15, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
( 1 / 1 = 1 & 1 / (- 1) = - 1 )
;
theorem Th1: :: SERIES_1:1
theorem Th2: :: SERIES_1:2
theorem Th3: :: SERIES_1:3
:: deftheorem Def1 defines Partial_Sums SERIES_1:def 1 :
:: deftheorem Def2 defines summable SERIES_1:def 2 :
:: deftheorem defines Sum SERIES_1:def 3 :
theorem :: SERIES_1:4
canceled;
theorem :: SERIES_1:5
canceled;
theorem :: SERIES_1:6
canceled;
theorem Th7: :: SERIES_1:7
theorem Th8: :: SERIES_1:8
theorem Th9: :: SERIES_1:9
theorem :: SERIES_1:10
theorem :: SERIES_1:11
theorem Th12: :: SERIES_1:12
theorem Th13: :: SERIES_1:13
theorem Th14: :: SERIES_1:14
theorem Th15: :: SERIES_1:15
theorem Th16: :: SERIES_1:16
theorem Th17: :: SERIES_1:17
theorem :: SERIES_1:18
theorem Th19: :: SERIES_1:19
theorem Th20: :: SERIES_1:20
theorem :: SERIES_1:21
theorem Th22: :: SERIES_1:22
theorem :: SERIES_1:23
canceled;
theorem :: SERIES_1:24
theorem Th25: :: SERIES_1:25
theorem Th26: :: SERIES_1:26
theorem :: SERIES_1:27
theorem Th28: :: SERIES_1:28
theorem :: SERIES_1:29
theorem Th30: :: SERIES_1:30
theorem :: SERIES_1:31
theorem Th32: :: SERIES_1:32
theorem Th33: :: SERIES_1:33
theorem :: SERIES_1:34
theorem Th35: :: SERIES_1:35
theorem :: SERIES_1:36
theorem :: SERIES_1:37
:: deftheorem SERIES_1:def 4 :
canceled;
:: deftheorem Def5 defines absolutely_summable SERIES_1:def 5 :
theorem :: SERIES_1:38
canceled;
theorem Th39: :: SERIES_1:39
theorem :: SERIES_1:40
theorem :: SERIES_1:41
theorem :: SERIES_1:42
theorem Th43: :: SERIES_1:43
theorem :: SERIES_1:44
theorem :: SERIES_1:45
theorem :: SERIES_1:46
theorem :: SERIES_1:47
:: deftheorem defines Sum SERIES_1:def 6 :
:: deftheorem defines Sum SERIES_1:def 7 :