:: The Sum and Product of Finite Sequences of Real Numbers
:: by Czes{\l}aw Byli\'nski
::
:: Received May 11, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for a, b being real number holds multreal . a,b = a * b
Lm2:
for a, b being complex number holds multcomplex . a,b = a * b
theorem :: RVSUM_1:1
canceled;
theorem :: RVSUM_1:2
canceled;
theorem :: RVSUM_1:3
:: deftheorem defines diffreal RVSUM_1:def 1 :
:: deftheorem Def2 defines sqrreal RVSUM_1:def 2 :
theorem :: RVSUM_1:4
canceled;
theorem :: RVSUM_1:5
canceled;
theorem :: RVSUM_1:6
canceled;
theorem :: RVSUM_1:7
canceled;
theorem :: RVSUM_1:8
canceled;
theorem :: RVSUM_1:9
canceled;
theorem :: RVSUM_1:10
canceled;
theorem :: RVSUM_1:11
canceled;
theorem :: RVSUM_1:12
canceled;
theorem :: RVSUM_1:13
theorem :: RVSUM_1:14
canceled;
theorem :: RVSUM_1:15
canceled;
theorem Th16: :: RVSUM_1:16
theorem Th17: :: RVSUM_1:17
:: deftheorem defines multreal RVSUM_1:def 3 :
Lm3:
for r, r1 being real number holds (multreal [;] r,(id REAL )) . r1 = r * r1
theorem :: RVSUM_1:18
canceled;
theorem :: RVSUM_1:19
theorem :: RVSUM_1:20
theorem Th21: :: RVSUM_1:21
theorem Th22: :: RVSUM_1:22
theorem Th23: :: RVSUM_1:23
theorem :: RVSUM_1:24
Lm4:
for F being real-valued FinSequence holds F is FinSequence of REAL
:: deftheorem defines + RVSUM_1:def 4 :
theorem :: RVSUM_1:25
canceled;
theorem :: RVSUM_1:26
canceled;
theorem Th27: :: RVSUM_1:27
theorem :: RVSUM_1:28
theorem :: RVSUM_1:29
theorem :: RVSUM_1:30
theorem :: RVSUM_1:31
canceled;
theorem Th32: :: RVSUM_1:32
theorem :: RVSUM_1:33
theorem :: RVSUM_1:34
canceled;
theorem Th35: :: RVSUM_1:35
:: deftheorem defines - RVSUM_1:def 5 :
theorem :: RVSUM_1:36
theorem :: RVSUM_1:37
theorem :: RVSUM_1:38
theorem Th39: :: RVSUM_1:39
theorem :: RVSUM_1:40
theorem :: RVSUM_1:41
theorem :: RVSUM_1:42
canceled;
theorem :: RVSUM_1:43
theorem :: RVSUM_1:44
theorem Th45: :: RVSUM_1:45
:: deftheorem defines - RVSUM_1:def 6 :
theorem :: RVSUM_1:46
canceled;
theorem :: RVSUM_1:47
canceled;
theorem :: RVSUM_1:48
theorem :: RVSUM_1:49
theorem :: RVSUM_1:50
theorem :: RVSUM_1:51
theorem Th52: :: RVSUM_1:52
theorem :: RVSUM_1:53
theorem :: RVSUM_1:54
theorem :: RVSUM_1:55
theorem :: RVSUM_1:56
theorem Th57: :: RVSUM_1:57
theorem Th58: :: RVSUM_1:58
theorem :: RVSUM_1:59
theorem :: RVSUM_1:60
theorem Th61: :: RVSUM_1:61
theorem :: RVSUM_1:62
theorem :: RVSUM_1:63
theorem :: RVSUM_1:64
theorem :: RVSUM_1:65
canceled;
theorem Th66: :: RVSUM_1:66
:: deftheorem defines * RVSUM_1:def 7 :
theorem :: RVSUM_1:67
theorem :: RVSUM_1:68
theorem :: RVSUM_1:69
theorem Th70: :: RVSUM_1:70
theorem Th71: :: RVSUM_1:71
theorem :: RVSUM_1:72
theorem :: RVSUM_1:73
theorem :: RVSUM_1:74
theorem :: RVSUM_1:75
theorem Th76: :: RVSUM_1:76
:: deftheorem defines sqr RVSUM_1:def 8 :
theorem :: RVSUM_1:77
canceled;
theorem :: RVSUM_1:78
canceled;
theorem :: RVSUM_1:79
canceled;
theorem :: RVSUM_1:80
canceled;
theorem :: RVSUM_1:81
theorem :: RVSUM_1:82
theorem Th83: :: RVSUM_1:83
theorem Th84: :: RVSUM_1:84
:: deftheorem defines mlt RVSUM_1:def 9 :
theorem :: RVSUM_1:85
canceled;
theorem Th86: :: RVSUM_1:86
theorem Th87: :: RVSUM_1:87
theorem :: RVSUM_1:88
theorem :: RVSUM_1:89
theorem :: RVSUM_1:90
canceled;
theorem :: RVSUM_1:91
canceled;
theorem Th92: :: RVSUM_1:92
theorem :: RVSUM_1:93
theorem Th94: :: RVSUM_1:94
theorem :: RVSUM_1:95
canceled;
theorem :: RVSUM_1:96
theorem Th97: :: RVSUM_1:97
theorem Th98: :: RVSUM_1:98
theorem Th99: :: RVSUM_1:99
theorem :: RVSUM_1:100
:: deftheorem RVSUM_1:def 10 :
canceled;
:: deftheorem Def11 defines Sum RVSUM_1:def 11 :
theorem Th101: :: RVSUM_1:101
:: deftheorem defines Sum RVSUM_1:def 12 :
:: deftheorem defines Sum RVSUM_1:def 13 :
theorem Th102: :: RVSUM_1:102
theorem :: RVSUM_1:103
theorem Th104: :: RVSUM_1:104
theorem Th105: :: RVSUM_1:105
theorem :: RVSUM_1:106
theorem Th107: :: RVSUM_1:107
theorem :: RVSUM_1:108
theorem :: RVSUM_1:109
theorem Th110: :: RVSUM_1:110
theorem Th111: :: RVSUM_1:111
theorem Th112: :: RVSUM_1:112
theorem Th113: :: RVSUM_1:113
theorem Th114: :: RVSUM_1:114
theorem Th115: :: RVSUM_1:115
theorem Th116: :: RVSUM_1:116
theorem Th117: :: RVSUM_1:117
theorem :: RVSUM_1:118
theorem Th119: :: RVSUM_1:119
theorem Th120: :: RVSUM_1:120
theorem :: RVSUM_1:121
theorem :: RVSUM_1:122
:: deftheorem Def14 defines Product RVSUM_1:def 14 :
theorem Th123: :: RVSUM_1:123
:: deftheorem defines Product RVSUM_1:def 15 :
:: deftheorem defines Product RVSUM_1:def 16 :
Lm5:
for F being empty FinSequence holds Product F = 1
theorem Th124: :: RVSUM_1:124
theorem Th125: :: RVSUM_1:125
theorem Th126: :: RVSUM_1:126
theorem Th127: :: RVSUM_1:127
theorem :: RVSUM_1:128
theorem Th129: :: RVSUM_1:129
theorem :: RVSUM_1:130
theorem :: RVSUM_1:131
theorem :: RVSUM_1:132
Lm6:
for p being complex-yielding FinSequence st len p <> 0 holds
ex q being complex-yielding FinSequence ex d being complex number st p = q ^ <*d*>
theorem :: RVSUM_1:133
theorem :: RVSUM_1:134
theorem :: RVSUM_1:135
theorem :: RVSUM_1:136
theorem Th137: :: RVSUM_1:137
theorem :: RVSUM_1:138
theorem :: RVSUM_1:139
theorem :: RVSUM_1:140
theorem :: RVSUM_1:141
theorem :: RVSUM_1:142
theorem :: RVSUM_1:143