:: INT_2 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem :: INT_2:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: INT_2:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th3: :: INT_2:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th4: :: INT_2:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b being
Nat holds
( (
a = 0 or
b = 0 ) iff
a lcm b = 0 )
theorem :: INT_2:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b being
Nat holds
( (
a = 0 &
b = 0 ) iff
a hcf b = 0 )
theorem :: INT_2:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INT_2:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th8: :: INT_2:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
n being
Nat holds
(
- n is
Nat iff
n = 0 )
theorem Th9: :: INT_2:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th10: :: INT_2:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th11: :: INT_2:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th12: :: INT_2:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th13: :: INT_2:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th14: :: INT_2:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INT_2:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th16: :: INT_2:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th17: :: INT_2:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INT_2:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INT_2:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INT_2:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th21: :: INT_2:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem INT_2:def 1 :
canceled;
:: deftheorem defines lcm' INT_2:def 2 :
theorem :: INT_2:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: INT_2:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INT_2:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th25: :: INT_2:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INT_2:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th27: :: INT_2:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem defines gcd INT_2:def 3 :
theorem :: INT_2:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: INT_2:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INT_2:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th31: :: INT_2:31
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INT_2:32
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th33: :: INT_2:33
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INT_2:34
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th35: :: INT_2:35
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b being
Integer holds
( (
a = 0 &
b = 0 ) iff
a gcd b = 0 )
:: deftheorem Def4 defines are_relative_prime INT_2:def 4 :
theorem :: INT_2:36
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: INT_2:37
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: INT_2:38
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th39: :: INT_2:39
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th40: :: INT_2:40
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INT_2:41
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def5 defines prime INT_2:def 5 :
for
p being
Nat holds
(
p is
prime iff (
p > 1 & ( for
n being
Nat holds
( not
n divides p or
n = 1 or
n = p ) ) ) );
:: deftheorem Def6 defines are_relative_prime INT_2:def 6 :
theorem :: INT_2:42
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: INT_2:43
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: INT_2:44
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INT_2:45
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: INT_2:46
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INT_2:47
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INT_2:48
:: Showing IDV graph ... (Click the Palm Tree again to close it) 