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