:: Ordinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received March 1, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem :: ORDINAL3:1
theorem :: ORDINAL3:2
theorem :: ORDINAL3:3
canceled;
theorem :: ORDINAL3:4
canceled;
theorem :: ORDINAL3:5
theorem :: ORDINAL3:6
theorem Th7: :: ORDINAL3:7
theorem Th8: :: ORDINAL3:8
theorem Th9: :: ORDINAL3:9
theorem Th10: :: ORDINAL3:10
theorem :: ORDINAL3:11
theorem :: ORDINAL3:12
theorem :: ORDINAL3:13
theorem :: ORDINAL3:14
canceled;
theorem :: ORDINAL3:15
theorem :: ORDINAL3:16
Lm1:
1 = succ {}
;
theorem Th17: :: ORDINAL3:17
theorem :: ORDINAL3:18
theorem Th19: :: ORDINAL3:19
theorem :: ORDINAL3:20
theorem :: ORDINAL3:21
theorem Th22: :: ORDINAL3:22
theorem :: ORDINAL3:23
theorem Th24: :: ORDINAL3:24
theorem Th25: :: ORDINAL3:25
theorem Th26: :: ORDINAL3:26
theorem Th27: :: ORDINAL3:27
theorem :: ORDINAL3:28
theorem Th29: :: ORDINAL3:29
theorem Th30: :: ORDINAL3:30
theorem Th31: :: ORDINAL3:31
theorem Th32: :: ORDINAL3:32
theorem Th33: :: ORDINAL3:33
theorem :: ORDINAL3:34
theorem :: ORDINAL3:35
theorem Th36: :: ORDINAL3:36
theorem Th37: :: ORDINAL3:37
theorem Th38: :: ORDINAL3:38
theorem Th39: :: ORDINAL3:39
theorem :: ORDINAL3:40
canceled;
theorem :: ORDINAL3:41
for
A,
B being
Ordinal st
A *^ B = 1 holds
(
A = 1 &
B = 1 )
theorem Th42: :: ORDINAL3:42
:: deftheorem ORDINAL3:def 1 :
canceled;
:: deftheorem Def2 defines +^ ORDINAL3:def 2 :
:: deftheorem defines +^ ORDINAL3:def 3 :
:: deftheorem defines *^ ORDINAL3:def 4 :
:: deftheorem Def5 defines *^ ORDINAL3:def 5 :
theorem :: ORDINAL3:43
canceled;
theorem :: ORDINAL3:44
canceled;
theorem :: ORDINAL3:45
canceled;
theorem :: ORDINAL3:46
canceled;
theorem Th47: :: ORDINAL3:47
theorem Th48: :: ORDINAL3:48
theorem Th49: :: ORDINAL3:49
theorem Th50: :: ORDINAL3:50
theorem Th51: :: ORDINAL3:51
theorem Th52: :: ORDINAL3:52
theorem Th53: :: ORDINAL3:53
theorem Th54: :: ORDINAL3:54
theorem Th55: :: ORDINAL3:55
theorem Th56: :: ORDINAL3:56
for
A,
C1,
D1,
C2,
D2 being
Ordinal st
(C1 *^ A) +^ D1 = (C2 *^ A) +^ D2 &
D1 in A &
D2 in A holds
(
C1 = C2 &
D1 = D2 )
theorem Th57: :: ORDINAL3:57
theorem :: ORDINAL3:58
:: deftheorem Def6 defines -^ ORDINAL3:def 6 :
for
A,
B,
b3 being
Ordinal holds
( (
B c= A implies (
b3 = A -^ B iff
A = B +^ b3 ) ) & ( not
B c= A implies (
b3 = A -^ B iff
b3 = {} ) ) );
:: deftheorem Def7 defines div^ ORDINAL3:def 7 :
:: deftheorem defines mod^ ORDINAL3:def 8 :
theorem :: ORDINAL3:59
canceled;
theorem :: ORDINAL3:60
theorem :: ORDINAL3:61
canceled;
theorem :: ORDINAL3:62
canceled;
theorem :: ORDINAL3:63
canceled;
theorem :: ORDINAL3:64
canceled;
theorem Th65: :: ORDINAL3:65
theorem Th66: :: ORDINAL3:66
theorem Th67: :: ORDINAL3:67
theorem :: ORDINAL3:68
theorem Th69: :: ORDINAL3:69
theorem :: ORDINAL3:70
theorem :: ORDINAL3:71
theorem :: ORDINAL3:72
theorem :: ORDINAL3:73
theorem :: ORDINAL3:74
theorem :: ORDINAL3:75
theorem :: ORDINAL3:76
theorem Th77: :: ORDINAL3:77
theorem Th78: :: ORDINAL3:78
theorem :: ORDINAL3:79
theorem :: ORDINAL3:80
theorem Th81: :: ORDINAL3:81
theorem :: ORDINAL3:82
theorem :: ORDINAL3:83
theorem :: ORDINAL3:84
theorem :: ORDINAL3:85
theorem :: ORDINAL3:86
theorem Th87: :: ORDINAL3:87
theorem :: ORDINAL3:88