let i be Nat; :: thesis: ( i is prime implies for m, n being Nat holds
( not i divides m * n or i divides m or i divides n ) )
defpred S1[ Nat] means ( $1 is prime & ex m, n being Nat st
( $1 divides m * n & not $1 divides m & not $1 divides n ) );
assume A1: i is prime ; :: thesis: for m, n being Nat holds
( not i divides m * n or i divides m or i divides n )
given m, n being Nat such that A2: i divides m * n and
A3: ( not i divides m & not i divides n ) ; :: thesis: contradiction
A4: ex i being Nat st S1[i] by A1, A2, A3;
consider p9 being Nat such that
A5: S1[p9] and
A6: for p1 being Nat st S1[p1] holds
p9 <= p1 from NAT_1:sch 5(A4);
 defpred S2[ Nat] means ex n being Nat st
( p9 divides $1 * n & not p9 divides $1 & not p9 divides n );
A7: ex i being Nat st S2[i] by A5;
consider m being Nat such that
A8: S2[m] and
A9: for m1 being Nat st S2[m1] holds
m <= m1 from NAT_1:sch 5(A7);
 A10: m > 0 by A8;
consider n being Nat such that
A11: p9 divides m * n and
A12: not p9 divides m and
A13: not p9 divides n by A8;
A14: m < p9
proof
set m1 = m mod p9;
assume A15: m >= p9 ; :: thesis: contradiction
A16: p9 > 0 by A5, INT_2:def 4;
then m = (p9 * (m div p9)) + (m mod p9) by NAT_D:2;
then A17: m * n = ((p9 * (m div p9)) * n) + ((m mod p9) * n) ;
m mod p9 < p9 by A16, NAT_D:1;
then A18: m mod p9 < m by A15, XXREAL_0:2;
A19: p9 divides p9 * (m div p9) by NAT_D:def 3;
p9 divides p9 * ((m div p9) * n) by NAT_D:def 3;
then A20: p9 divides (m mod p9) * n by A11, A17, NAT_D:10;
m = (p9 * (m div p9)) + (m mod p9) by A16, NAT_D:2;
then not p9 divides m mod p9 by A12, A19, NAT_D:8;
hence contradiction by A9, A13, A18, A20; :: thesis: verum
end;
A21: m < 2
proof
assume m >= 2 ; :: thesis: contradiction
then consider p1 being Element of NAT such that
A22: p1 is prime and
A23: p1 divides m by INT_2:31;
A24: p1 > 1 by A22, INT_2:def 4;
A25: not p1 divides p9
proof
assume p1 divides p9 ; :: thesis: contradiction
then ( p1 = 1 or p1 = p9 ) by A5, INT_2:def 4;
hence contradiction by A8, A22, A23, INT_2:def 4; :: thesis: verum
end;
p1 <= m by A10, A23, NAT_D:7;
then A26: not p9 <= p1 by A14, XXREAL_0:2;
A27: p1 <> 0 by A22, INT_2:def 4;
consider k being Nat such that
A28: m * n = p9 * k by A11, NAT_D:def 3;
p1 divides p9 * k by A23, A28, NAT_D:9;
then p1 divides k by A6, A22, A26, A25;
then consider k1 being Nat such that
A29: k = p1 * k1 by NAT_D:def 3;
consider m1 being Nat such that
A30: m = p1 * m1 by A23, NAT_D:def 3;
A31: m1 > 0 by A8, A30;
A32: m1 <> m
proof
assume m1 = m ; :: thesis: contradiction
then m = 1 * m1 ;
hence contradiction by A24, A30, A31, XREAL_1:68; :: thesis: verum
end;
m1 divides m by A30, NAT_D:def 3;
then m1 <= m by A10, NAT_D:7;
then A33: m1 < m by A32, XXREAL_0:1;
(p9 * k1) * p1 = p1 * (m1 * n) by A28, A29, A30;
then m1 * n = p9 * k1 by A27, XCMPLX_1:5;
then A34: p9 divides m1 * n by NAT_D:def 3;
not p9 divides m1 by A12, A30, NAT_D:9;
hence contradiction by A9, A13, A33, A34; :: thesis: verum
end;
m >= 2
proof
A35: m >= 0 + 1 by A10, NAT_1:13;
assume A36: m < 2 ; :: thesis: contradiction
then m <= 1 + 1 ;
then m = 1 by A36, A35, NAT_1:9;
hence contradiction by A11, A13; :: thesis: verum
end;
hence contradiction by A21; :: thesis: verum