:: The Divisibility of Integers and Integer Relatively Primes
:: by Rafa{\l} Kwiatek and Grzegorz Zwara
::
:: Received July 10, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: INT_2:1
theorem Th2: :: INT_2:2
theorem Th3: :: INT_2:3
Lm1:
for a being Integer holds
( a divides - a & - a divides a )
Lm2:
for a, b, c being Integer st a divides b & b divides c holds
a divides c
Lm3:
for a, b being Integer holds
( a divides b iff a divides - b )
Lm4:
for a, b being Integer holds
( a divides b iff - a divides b )
Lm5:
for a being Integer holds
( a divides 0 & 1 divides a & - 1 divides a )
Lm6:
for a, b, c being Integer st a divides b & a divides c holds
a divides b mod c
Lm7:
for k, l being Nat holds
( k divides l iff ex t being Nat st l = k * t )
Lm8:
for i, j being Nat st i divides j & j divides i holds
i = j
:: deftheorem INT_2:def 1 :
canceled;
:: deftheorem Def2 defines lcm INT_2:def 2 :
theorem Th4: :: INT_2:4
Lm9:
for j, i being Nat st 0 < j & i divides j holds
i <= j
:: deftheorem Def3 defines gcd INT_2:def 3 :
theorem Th5: :: INT_2:5
theorem :: INT_2:6
canceled;
theorem :: INT_2:7
canceled;
theorem Th8: :: INT_2:8
theorem :: INT_2:9
theorem :: INT_2:10
theorem :: INT_2:11
theorem Th12: :: INT_2:12
theorem :: INT_2:13
theorem Th14: :: INT_2:14
theorem :: INT_2:15
theorem :: INT_2:16
theorem Th17: :: INT_2:17
theorem :: INT_2:18
theorem :: INT_2:19
theorem :: INT_2:20
theorem :: INT_2:21
theorem :: INT_2:22
canceled;
theorem :: INT_2:23
theorem :: INT_2:24
canceled;
theorem :: INT_2:25
theorem :: INT_2:26
theorem :: INT_2:27
theorem :: INT_2:28
canceled;
theorem :: INT_2:29
theorem :: INT_2:30
canceled;
theorem Th31: :: INT_2:31
theorem :: INT_2:32
theorem :: INT_2:33
theorem :: INT_2:34
theorem Th35: :: INT_2:35
:: deftheorem Def4 defines are_relative_prime INT_2:def 4 :
theorem :: INT_2:36
canceled;
theorem :: INT_2:37
canceled;
theorem :: INT_2:38
theorem Th39: :: INT_2:39
theorem Th40: :: INT_2:40
theorem :: INT_2:41
:: deftheorem Def5 defines prime INT_2:def 5 :
theorem :: INT_2:42
canceled;
theorem Th43: :: INT_2:43
theorem Th44: :: INT_2:44
theorem :: INT_2:45
canceled;
theorem Th46: :: INT_2:46
theorem :: INT_2:47
theorem :: INT_2:48
theorem :: INT_2:49
theorem :: INT_2:50
theorem :: INT_2:51