:: Integers
:: by Micha{\l} J. Trybulec
::
:: Received February 7, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for z being set st z in [:{0 },NAT :] \ {[0 ,0 ]} holds
ex k being Element of NAT st z = - k
Lm2:
for x being set
for k being Element of NAT st x = - k & k <> x holds
x in [:{0 },NAT :] \ {[0 ,0 ]}
:: deftheorem Def1 defines INT INT_1:def 1 :
for
b1 being
set holds
(
b1 = INT iff for
x being
set holds
(
x in b1 iff ex
k being
Element of
NAT st
(
x = k or
x = - k ) ) );
:: deftheorem Def2 defines integer INT_1:def 2 :
theorem :: INT_1:1
canceled;
theorem :: INT_1:2
canceled;
theorem :: INT_1:3
canceled;
theorem :: INT_1:4
canceled;
theorem :: INT_1:5
canceled;
theorem :: INT_1:6
canceled;
theorem Th7: :: INT_1:7
theorem Th8: :: INT_1:8
Lm3:
for x being set st x in INT holds
x in REAL
by NUMBERS:15;
theorem :: INT_1:9
canceled;
theorem :: INT_1:10
canceled;
theorem :: INT_1:11
canceled;
theorem :: INT_1:12
canceled;
theorem :: INT_1:13
canceled;
theorem :: INT_1:14
canceled;
theorem :: INT_1:15
canceled;
theorem Th16: :: INT_1:16
theorem :: INT_1:17
theorem Th18: :: INT_1:18
theorem Th19: :: INT_1:19
Lm4:
for j being Element of NAT st j < 1 holds
j = 0
Lm5:
for i1 being Integer st 0 < i1 holds
1 <= i1
theorem Th20: :: INT_1:20
theorem Th21: :: INT_1:21
theorem Th22: :: INT_1:22
for
i1,
i2 being
Integer holds
(
i1 * i2 = 1 iff ( (
i1 = 1 &
i2 = 1 ) or (
i1 = - 1 &
i2 = - 1 ) ) )
theorem :: INT_1:23
for
i1,
i2 being
Integer holds
(
i1 * i2 = - 1 iff ( (
i1 = - 1 &
i2 = 1 ) or (
i1 = 1 &
i2 = - 1 ) ) )
Lm6:
for i0, i1 being Integer st i0 <= i1 holds
ex k being Element of NAT st i0 + k = i1
Lm7:
for i0, i1 being Integer st i0 <= i1 holds
ex k being Element of NAT st i1 - k = i0
:: deftheorem Def3 defines are_congruent_mod INT_1:def 3 :
theorem :: INT_1:24
canceled;
theorem :: INT_1:25
canceled;
theorem :: INT_1:26
canceled;
theorem :: INT_1:27
canceled;
theorem :: INT_1:28
canceled;
theorem :: INT_1:29
canceled;
theorem :: INT_1:30
canceled;
theorem :: INT_1:31
canceled;
theorem :: INT_1:32
theorem :: INT_1:33
theorem :: INT_1:34
theorem :: INT_1:35
theorem :: INT_1:36
theorem :: INT_1:37
theorem :: INT_1:38
theorem :: INT_1:39
theorem :: INT_1:40
theorem :: INT_1:41
theorem :: INT_1:42
theorem :: INT_1:43
theorem Th44: :: INT_1:44
theorem Th45: :: INT_1:45
Lm8:
for r being real number ex n being Element of NAT st r < n
:: deftheorem Def4 defines [\ INT_1:def 4 :
theorem :: INT_1:46
canceled;
theorem Th47: :: INT_1:47
theorem Th48: :: INT_1:48
theorem :: INT_1:49
canceled;
theorem :: INT_1:50
theorem Th51: :: INT_1:51
theorem Th52: :: INT_1:52
:: deftheorem Def5 defines [/ INT_1:def 5 :
theorem :: INT_1:53
canceled;
theorem Th54: :: INT_1:54
theorem Th55: :: INT_1:55
theorem :: INT_1:56
canceled;
theorem :: INT_1:57
theorem :: INT_1:58
theorem Th59: :: INT_1:59
theorem Th60: :: INT_1:60
theorem :: INT_1:61
theorem :: INT_1:62
theorem :: INT_1:63
theorem :: INT_1:64
theorem :: INT_1:65
theorem :: INT_1:66
:: deftheorem defines frac INT_1:def 6 :
theorem :: INT_1:67
canceled;
theorem :: INT_1:68
theorem Th69: :: INT_1:69
theorem :: INT_1:70
theorem Th71: :: INT_1:71
theorem :: INT_1:72
:: deftheorem defines div INT_1:def 7 :
:: deftheorem Def8 defines mod INT_1:def 8 :
:: deftheorem Def9 defines divides INT_1:def 9 :
theorem :: INT_1:73
canceled;
theorem Th74: :: INT_1:74
theorem :: INT_1:75
theorem :: INT_1:76
theorem :: INT_1:77
theorem :: INT_1:78
theorem Th79: :: INT_1:79
theorem :: INT_1:80
theorem Th81: :: INT_1:81
theorem :: INT_1:82
theorem :: INT_1:83
theorem :: INT_1:84
theorem :: INT_1:85
theorem :: INT_1:86
theorem :: INT_1:87
theorem :: INT_1:88
theorem :: INT_1:89
theorem :: INT_1:90
theorem :: INT_1:91
theorem :: INT_1:92