:: The {C}atalan Numbers. {P}art {II}
:: by Karol P\c{a}k
::
:: Received October 31, 2006
:: Copyright (c) 2006 Association of Mizar Users
theorem Th1: :: CATALAN2:1
theorem Th2: :: CATALAN2:2
theorem Th3: :: CATALAN2:3
theorem Th4: :: CATALAN2:4
theorem Th5: :: CATALAN2:5
:: deftheorem Def1 defines dominated_by_0 CATALAN2:def 1 :
theorem Th6: :: CATALAN2:6
theorem Th7: :: CATALAN2:7
Lm1:
for n, m, k being Element of NAT st n <= m holds
(m --> k) | n = n --> k
Lm2:
for k, m being Element of NAT holds Sum (k --> m) = k * m
Lm3:
for k being Element of NAT holds k --> 0 is dominated_by_0
theorem :: CATALAN2:8
Lm4:
for p, q being XFinSequence of NAT holds Sum (p ^ q) = (Sum p) + (Sum q)
theorem Th9: :: CATALAN2:9
theorem Th10: :: CATALAN2:10
theorem Th11: :: CATALAN2:11
theorem Th12: :: CATALAN2:12
theorem Th13: :: CATALAN2:13
theorem Th14: :: CATALAN2:14
theorem Th15: :: CATALAN2:15
theorem Th16: :: CATALAN2:16
theorem Th17: :: CATALAN2:17
theorem Th18: :: CATALAN2:18
theorem Th19: :: CATALAN2:19
theorem Th20: :: CATALAN2:20
theorem Th21: :: CATALAN2:21
theorem Th22: :: CATALAN2:22
theorem :: CATALAN2:23
:: deftheorem Def2 defines Domin_0 CATALAN2:def 2 :
theorem Th24: :: CATALAN2:24
theorem Th25: :: CATALAN2:25
theorem Th26: :: CATALAN2:26
theorem Th27: :: CATALAN2:27
theorem Th28: :: CATALAN2:28
theorem Th29: :: CATALAN2:29
theorem Th30: :: CATALAN2:30
theorem Th31: :: CATALAN2:31
theorem Th32: :: CATALAN2:32
theorem Th33: :: CATALAN2:33
theorem Th34: :: CATALAN2:34
theorem :: CATALAN2:35
theorem :: CATALAN2:36
theorem Th37: :: CATALAN2:37
theorem Th38: :: CATALAN2:38
Lm5:
for D being set holds D ^omega is functional
:: deftheorem Def3 defines OMEGA CATALAN2:def 3 :
theorem :: CATALAN2:39
theorem Th40: :: CATALAN2:40
theorem Th41: :: CATALAN2:41
theorem Th42: :: CATALAN2:42
theorem Th43: :: CATALAN2:43
theorem Th44: :: CATALAN2:44
theorem :: CATALAN2:45
theorem :: CATALAN2:46
:: deftheorem defines Sum CATALAN2:def 4 :
Lm6:
for Fr being XFinSequence of REAL st dom Fr = 0 holds
Sum Fr = 0
Lm7:
for Fr being XFinSequence of REAL st ( dom Fr = 1 or len Fr = 1 ) holds
Sum Fr = Fr . 0
Lm8:
for Fr being XFinSequence of REAL
for n being Element of NAT st n in dom Fr holds
(Sum (Fr | n)) + (Fr . n) = Sum (Fr | (n + 1))
Lm9:
for Fr1, Fr2 being XFinSequence of REAL st dom Fr1 = dom Fr2 & ( for n being Element of NAT st n in len Fr1 holds
Fr1 . n = Fr2 . ((len Fr1) -' (1 + n)) ) holds
Sum Fr1 = Sum Fr2
:: deftheorem Def5 defines (##) CATALAN2:def 5 :
theorem :: CATALAN2:47
theorem :: CATALAN2:48
theorem Th49: :: CATALAN2:49
theorem :: CATALAN2:50
theorem :: CATALAN2:51
theorem Th52: :: CATALAN2:52
theorem Th53: :: CATALAN2:53
theorem Th54: :: CATALAN2:54
theorem Th55: :: CATALAN2:55
theorem Th56: :: CATALAN2:56
theorem Th57: :: CATALAN2:57
theorem Th58: :: CATALAN2:58
theorem Th59: :: CATALAN2:59
theorem :: CATALAN2:60