:: Factorial and Newton coefficients
:: by Rafa{\l} Kwiatek
::
:: Received July 27, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem :: NEWTON:1
canceled;
theorem :: NEWTON:2
canceled;
theorem Th3: :: NEWTON:3
theorem :: NEWTON:4
canceled;
theorem Th5: :: NEWTON:5
theorem Th6: :: NEWTON:6
theorem Th7: :: NEWTON:7
:: deftheorem defines |^ NEWTON:def 1 :
theorem :: NEWTON:8
canceled;
theorem Th9: :: NEWTON:9
theorem Th10: :: NEWTON:10
theorem Th11: :: NEWTON:11
theorem :: NEWTON:12
theorem Th13: :: NEWTON:13
theorem :: NEWTON:14
theorem Th15: :: NEWTON:15
for
s being
Nat holds 1
|^ s = 1
theorem Th16: :: NEWTON:16
:: deftheorem defines ! NEWTON:def 2 :
theorem :: NEWTON:17
canceled;
theorem Th18: :: NEWTON:18
theorem :: NEWTON:19
theorem :: NEWTON:20
theorem Th21: :: NEWTON:21
for
s being
Nat holds
(s + 1) ! = (s ! ) * (s + 1)
theorem Th22: :: NEWTON:22
theorem Th23: :: NEWTON:23
theorem :: NEWTON:24
canceled;
theorem Th25: :: NEWTON:25
for
s,
t being
Nat holds
(s ! ) * (t ! ) <> 0
:: deftheorem Def3 defines choose NEWTON:def 3 :
for
k,
n being
Nat for
b3 being
set holds
( (
n >= k implies (
b3 = n choose k iff for
l being
Nat st
l = n - k holds
b3 = (n ! ) / ((k ! ) * (l ! )) ) ) & ( not
n >= k implies (
b3 = n choose k iff
b3 = 0 ) ) );
theorem :: NEWTON:26
canceled;
theorem Th27: :: NEWTON:27
theorem :: NEWTON:28
canceled;
theorem Th29: :: NEWTON:29
theorem Th30: :: NEWTON:30
theorem Th31: :: NEWTON:31
theorem Th32: :: NEWTON:32
theorem Th33: :: NEWTON:33
theorem :: NEWTON:34
theorem Th35: :: NEWTON:35
theorem :: NEWTON:36
definition
let a,
b be
real number ;
let n be
Nat;
func a,
b In_Power n -> FinSequence of
REAL means :
Def4:
:: NEWTON:def 4
(
len it = n + 1 & ( for
i,
l,
m being
Nat st
i in dom it &
m = i - 1 &
l = n - m holds
it . i = ((n choose m) * (a |^ l)) * (b |^ m) ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = n + 1 & ( for i, l, m being Nat st i in dom b1 & m = i - 1 & l = n - m holds
b1 . i = ((n choose m) * (a |^ l)) * (b |^ m) ) )
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = n + 1 & ( for i, l, m being Nat st i in dom b1 & m = i - 1 & l = n - m holds
b1 . i = ((n choose m) * (a |^ l)) * (b |^ m) ) & len b2 = n + 1 & ( for i, l, m being Nat st i in dom b2 & m = i - 1 & l = n - m holds
b2 . i = ((n choose m) * (a |^ l)) * (b |^ m) ) holds
b1 = b2
end;
:: deftheorem Def4 defines In_Power NEWTON:def 4 :
theorem :: NEWTON:37
canceled;
theorem Th38: :: NEWTON:38
theorem Th39: :: NEWTON:39
theorem Th40: :: NEWTON:40
theorem Th41: :: NEWTON:41
:: deftheorem Def5 defines Newton_Coeff NEWTON:def 5 :
theorem :: NEWTON:42
canceled;
theorem Th43: :: NEWTON:43
theorem :: NEWTON:44
theorem Th45: :: NEWTON:45
for
l,
k being
Nat st
l >= 1 holds
k * l >= k
theorem Th46: :: NEWTON:46
for
l,
n,
k being
Nat st
l >= 1 &
n >= k * l holds
n >= k
theorem Th47: :: NEWTON:47
theorem :: NEWTON:48
for
n being
Nat st
n <> 0 holds
(n + 1) / n > 1
theorem Th49: :: NEWTON:49
for
k being
Nat holds
k / (k + 1) < 1
theorem Th50: :: NEWTON:50
for
l being
Nat holds
l ! >= l
theorem Th51: :: NEWTON:51
theorem :: NEWTON:52
canceled;
theorem Th53: :: NEWTON:53
theorem Th54: :: NEWTON:54
theorem :: NEWTON:55
theorem :: NEWTON:56
theorem Th57: :: NEWTON:57
theorem :: NEWTON:58
theorem :: NEWTON:59
theorem Th60: :: NEWTON:60
theorem :: NEWTON:61
theorem Th62: :: NEWTON:62
theorem :: NEWTON:63
theorem :: NEWTON:64
theorem :: NEWTON:65
theorem Th66: :: NEWTON:66
theorem Th67: :: NEWTON:67
theorem :: NEWTON:68
theorem :: NEWTON:69
theorem :: NEWTON:70
theorem Th71: :: NEWTON:71
theorem :: NEWTON:72
canceled;
theorem :: NEWTON:73
theorem :: NEWTON:74
theorem :: NEWTON:75
theorem :: NEWTON:76
theorem :: NEWTON:77
theorem :: NEWTON:78
theorem :: NEWTON:79
theorem :: NEWTON:80
theorem :: NEWTON:81
:: deftheorem Def6 defines SetPrimes NEWTON:def 6 :
:: deftheorem Def7 defines SetPrimenumber NEWTON:def 7 :
theorem Th82: :: NEWTON:82
theorem :: NEWTON:83
theorem Th84: :: NEWTON:84
theorem Th85: :: NEWTON:85
theorem Th86: :: NEWTON:86
theorem :: NEWTON:87
theorem Th88: :: NEWTON:88
theorem :: NEWTON:89
theorem :: NEWTON:90
theorem :: NEWTON:91
theorem :: NEWTON:92
theorem :: NEWTON:93
theorem Th94: :: NEWTON:94
theorem :: NEWTON:95
Lm1:
for n being Nat holds SetPrimenumber n = { k where k is Element of NAT : ( k < n & k is prime ) }
:: deftheorem Def8 defines primenumber NEWTON:def 8 :
theorem :: NEWTON:96
theorem Th97: :: NEWTON:97
theorem :: NEWTON:98
theorem :: NEWTON:99
canceled;
theorem :: NEWTON:100
theorem :: NEWTON:101
theorem :: NEWTON:102
theorem :: NEWTON:103
defpred S1[ Nat] means 2 |^ $1 >= $1 + 1;
Lm2:
S1[ 0 ]
by RVSUM_1:124;
Lm3:
for n being Nat st S1[n] holds
S1[n + 1]
theorem Th104: :: NEWTON:104
theorem :: NEWTON:105
for
n being
Nat holds 2
|^ n > n
theorem Th106: :: NEWTON:106
Lm3:
for n1, m1, n2, m2 being natural number st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
n1 <= n2
theorem :: NEWTON:107