:: Countable Sets and Hessenberg's Theorem
:: by Grzegorz Bancerek
::
:: Received September 5, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem :: CARD_4:1
canceled;
theorem :: CARD_4:2
canceled;
theorem :: CARD_4:3
canceled;
theorem :: CARD_4:4
canceled;
theorem :: CARD_4:5
canceled;
theorem :: CARD_4:6
canceled;
theorem :: CARD_4:7
canceled;
theorem :: CARD_4:8
canceled;
theorem :: CARD_4:9
canceled;
theorem :: CARD_4:10
canceled;
theorem :: CARD_4:11
canceled;
theorem :: CARD_4:12
canceled;
theorem :: CARD_4:13
canceled;
theorem :: CARD_4:14
canceled;
theorem :: CARD_4:15
canceled;
theorem :: CARD_4:16
canceled;
theorem :: CARD_4:17
canceled;
theorem :: CARD_4:18
canceled;
theorem :: CARD_4:19
canceled;
theorem :: CARD_4:20
canceled;
theorem :: CARD_4:21
canceled;
theorem :: CARD_4:22
canceled;
theorem :: CARD_4:23
canceled;
theorem :: CARD_4:24
canceled;
theorem :: CARD_4:25
canceled;
theorem :: CARD_4:26
canceled;
theorem :: CARD_4:27
canceled;
theorem :: CARD_4:28
canceled;
theorem :: CARD_4:29
canceled;
theorem :: CARD_4:30
canceled;
theorem :: CARD_4:31
canceled;
theorem :: CARD_4:32
canceled;
theorem :: CARD_4:33
canceled;
theorem :: CARD_4:34
canceled;
theorem :: CARD_4:35
canceled;
theorem :: CARD_4:36
canceled;
theorem :: CARD_4:37
canceled;
theorem :: CARD_4:38
canceled;
theorem :: CARD_4:39
canceled;
theorem :: CARD_4:40
canceled;
theorem :: CARD_4:41
canceled;
theorem :: CARD_4:42
canceled;
theorem :: CARD_4:43
theorem :: CARD_4:44
theorem :: CARD_4:45
canceled;
theorem :: CARD_4:46
canceled;
theorem :: CARD_4:47
canceled;
theorem :: CARD_4:48
canceled;
theorem :: CARD_4:49
canceled;
theorem :: CARD_4:50
canceled;
theorem Th51: :: CARD_4:51
Lm3:
for n1, m1, n2, m2 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
n1 <= n2
theorem Th52: :: CARD_4:52
for
n1,
m1,
n2,
m2 being
Nat st
(2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
(
n1 = n2 &
m1 = m2 )
Lm4:
for x being set st x in [:NAT ,NAT :] holds
ex n1, n2 being Element of NAT st x = [n1,n2]
theorem Th53: :: CARD_4:53
theorem Th54: :: CARD_4:54
theorem Th55: :: CARD_4:55
theorem Th56: :: CARD_4:56
theorem Th57: :: CARD_4:57
theorem Th58: :: CARD_4:58
theorem :: CARD_4:59
canceled;
theorem :: CARD_4:60
canceled;
theorem Th61: :: CARD_4:61
theorem :: CARD_4:62
theorem :: CARD_4:63
canceled;
theorem :: CARD_4:64
canceled;
theorem :: CARD_4:65
theorem :: CARD_4:66
theorem :: CARD_4:67
canceled;
theorem :: CARD_4:68
canceled;
theorem :: CARD_4:69
canceled;
theorem :: CARD_4:70
canceled;
theorem :: CARD_4:71
canceled;
theorem :: CARD_4:72
canceled;
theorem :: CARD_4:73
canceled;
theorem :: CARD_4:74
canceled;
theorem :: CARD_4:75
canceled;
theorem :: CARD_4:76
canceled;
theorem Th77: :: CARD_4:77
theorem Th78: :: CARD_4:78
theorem Th79: :: CARD_4:79
theorem :: CARD_4:80
theorem :: CARD_4:81
theorem :: CARD_4:82
theorem :: CARD_4:83
canceled;
theorem Th84: :: CARD_4:84
theorem :: CARD_4:85
theorem Th86: :: CARD_4:86
theorem :: CARD_4:87