:: Basic Properties of Rational Numbers
:: by Andrzej Kondracki
::
:: Received July 10, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
omega c= ({ [c,d] where c, d is Element of omega : ( c,d are_relative_prime & d <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega
by XBOOLE_1:7;
Lm2:
for i1, j1 being Element of NAT holds quotient i1,j1 = i1 / j1
0 in omega
;
then reconsider 0' = 0 as Element of REAL+ by ARYTM_2:2;
Lm3:
for a being real number
for x' being Element of REAL+ st x' = a holds
0' - x' = - a
Lm4:
for x being set st x in RAT holds
ex m, n being Integer st x = m / n
Lm5:
for x being set
for l being Element of NAT
for m being Integer st x = m / l holds
x in RAT
Lm6:
for x being set
for m, n being Integer st x = m / n holds
x in RAT
:: deftheorem Def1 defines RAT RAT_1:def 1 :
for
b1 being
set holds
(
b1 = RAT iff for
x being
set holds
(
x in b1 iff ex
m,
n being
Integer st
x = m / n ) );
:: deftheorem Def2 defines rational RAT_1:def 2 :
theorem Th1: :: RAT_1:1
theorem :: RAT_1:2
canceled;
theorem Th3: :: RAT_1:3
theorem :: RAT_1:4
canceled;
theorem :: RAT_1:5
canceled;
theorem Th6: :: RAT_1:6
theorem Th7: :: RAT_1:7
theorem :: RAT_1:8
canceled;
theorem :: RAT_1:9
canceled;
theorem :: RAT_1:10
canceled;
theorem :: RAT_1:11
canceled;
theorem :: RAT_1:12
canceled;
theorem :: RAT_1:13
canceled;
theorem :: RAT_1:14
canceled;
theorem :: RAT_1:15
canceled;
theorem Th16: :: RAT_1:16
theorem :: RAT_1:17
canceled;
theorem :: RAT_1:18
canceled;
theorem :: RAT_1:19
canceled;
theorem :: RAT_1:20
canceled;
theorem Th21: :: RAT_1:21
theorem :: RAT_1:22
theorem :: RAT_1:23
canceled;
theorem Th24: :: RAT_1:24
theorem Th25: :: RAT_1:25
:: deftheorem Def3 defines denominator RAT_1:def 3 :
:: deftheorem defines numerator RAT_1:def 4 :
theorem :: RAT_1:26
canceled;
theorem Th27: :: RAT_1:27
theorem :: RAT_1:28
canceled;
theorem Th29: :: RAT_1:29
theorem Th30: :: RAT_1:30
theorem :: RAT_1:31
canceled;
theorem :: RAT_1:32
canceled;
theorem :: RAT_1:33
canceled;
theorem Th34: :: RAT_1:34
theorem :: RAT_1:35
canceled;
theorem Th36: :: RAT_1:36
theorem Th37: :: RAT_1:37
theorem :: RAT_1:38
theorem :: RAT_1:39
canceled;
theorem Th40: :: RAT_1:40
theorem Th41: :: RAT_1:41
theorem :: RAT_1:42
theorem :: RAT_1:43
canceled;
theorem :: RAT_1:44
theorem :: RAT_1:45
Lm7:
1 " = 1
;
theorem :: RAT_1:46
theorem Th47: :: RAT_1:47
theorem Th48: :: RAT_1:48
theorem :: RAT_1:49
theorem Th50: :: RAT_1:50
theorem :: RAT_1:51
canceled;
theorem :: RAT_1:52
canceled;
theorem :: RAT_1:53
canceled;
theorem :: RAT_1:54
canceled;
theorem :: RAT_1:55
canceled;
theorem :: RAT_1:56
canceled;
theorem :: RAT_1:57
canceled;
theorem :: RAT_1:58
canceled;
theorem :: RAT_1:59
canceled;
theorem Th60: :: RAT_1:60
theorem :: RAT_1:61
theorem Th62: :: RAT_1:62
theorem Th63: :: RAT_1:63
theorem Th64: :: RAT_1:64
theorem Th65: :: RAT_1:65
theorem :: RAT_1:66
theorem :: RAT_1:67
theorem :: RAT_1:68
canceled;
theorem :: RAT_1:69
canceled;
theorem :: RAT_1:70
canceled;
theorem :: RAT_1:71
canceled;
theorem Th72: :: RAT_1:72
theorem :: RAT_1:73
theorem :: RAT_1:74
canceled;
theorem :: RAT_1:75
canceled;
theorem :: RAT_1:76
theorem Th77: :: RAT_1:77
theorem :: RAT_1:78
canceled;
theorem :: RAT_1:79
canceled;
theorem Th80: :: RAT_1:80
theorem :: RAT_1:81
theorem :: RAT_1:82
canceled;
theorem :: RAT_1:83
canceled;
theorem :: RAT_1:84
theorem :: RAT_1:85
canceled;
theorem :: RAT_1:86
theorem Th87: :: RAT_1:87
theorem Th88: :: RAT_1:88
theorem :: RAT_1:89