defpred S_{1}[ Nat] means for m, n being Element of NAT st $1 gcd m = 1 holds

$1 gcd (m * n) = $1 gcd n;

A1: for k being Nat st ( for a being Nat st a < k holds

S_{1}[a] ) holds

S_{1}[k]
_{1}[k]
from NAT_1:sch 4(A1);

hence for k, m, n being Element of NAT st k gcd m = 1 holds

k gcd (m * n) = k gcd n ; :: thesis: verum

$1 gcd (m * n) = $1 gcd n;

A1: for k being Nat st ( for a being Nat st a < k holds

S

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( ( for a being Nat st a < k holds

S_{1}[a] ) implies S_{1}[k] )

assume A2: for a being Nat st a < k holds

S_{1}[a]
; :: thesis: S_{1}[k]

end;S

assume A2: for a being Nat st a < k holds

S

per cases
( k = 0 or k = 1 or k > 1 )
by NAT_1:25;

end;

suppose A3:
k = 0
; :: thesis: S_{1}[k]

let m, n be Element of NAT ; :: thesis: ( k gcd m = 1 implies k gcd (m * n) = k gcd n )

assume k gcd m = 1 ; :: thesis: k gcd (m * n) = k gcd n

then 1 = m by A3, NEWTON:52;

hence k gcd (m * n) = k gcd n ; :: thesis: verum

end;assume k gcd m = 1 ; :: thesis: k gcd (m * n) = k gcd n

then 1 = m by A3, NEWTON:52;

hence k gcd (m * n) = k gcd n ; :: thesis: verum

suppose A4:
k = 1
; :: thesis: S_{1}[k]

let m, n be Element of NAT ; :: thesis: ( k gcd m = 1 implies k gcd (m * n) = k gcd n )

assume k gcd m = 1 ; :: thesis: k gcd (m * n) = k gcd n

k gcd (m * n) = 1 by A4, NEWTON:51;

hence k gcd (m * n) = k gcd n by A4, NEWTON:51; :: thesis: verum

end;assume k gcd m = 1 ; :: thesis: k gcd (m * n) = k gcd n

k gcd (m * n) = 1 by A4, NEWTON:51;

hence k gcd (m * n) = k gcd n by A4, NEWTON:51; :: thesis: verum

suppose A5:
k > 1
; :: thesis: S_{1}[k]

let m, n be Element of NAT ; :: thesis: ( k gcd m = 1 implies k gcd (m * n) = k gcd n )

set b = k gcd (m * n);

assume A6: k gcd m = 1 ; :: thesis: k gcd (m * n) = k gcd n

thus k gcd (m * n) = k gcd n :: thesis: verum

end;set b = k gcd (m * n);

assume A6: k gcd m = 1 ; :: thesis: k gcd (m * n) = k gcd n

thus k gcd (m * n) = k gcd n :: thesis: verum

proof
end;

per cases
( k gcd (m * n) = 0 or k gcd (m * n) = 1 or k gcd (m * n) > 1 )
by NAT_1:25;

end;

suppose
k gcd (m * n) = 0
; :: thesis: k gcd (m * n) = k gcd n

then
0 divides k
by NAT_D:def 5;

then k = 0 by INT_2:3;

hence k gcd (m * n) = k gcd n by A5; :: thesis: verum

end;then k = 0 by INT_2:3;

hence k gcd (m * n) = k gcd n by A5; :: thesis: verum

suppose A7:
k gcd (m * n) = 1
; :: thesis: k gcd (m * n) = k gcd n

set c = k gcd n;

A8: k gcd n divides k by NAT_D:def 5;

A9: n divides m * n by NAT_D:def 3;

k gcd n divides n by NAT_D:def 5;

then k gcd n divides m * n by A9, NAT_D:4;

then k gcd n divides 1 by A7, A8, NAT_D:def 5;

hence k gcd (m * n) = k gcd n by A7, WSIERP_1:15; :: thesis: verum

end;A8: k gcd n divides k by NAT_D:def 5;

A9: n divides m * n by NAT_D:def 3;

k gcd n divides n by NAT_D:def 5;

then k gcd n divides m * n by A9, NAT_D:4;

then k gcd n divides 1 by A7, A8, NAT_D:def 5;

hence k gcd (m * n) = k gcd n by A7, WSIERP_1:15; :: thesis: verum

suppose
k gcd (m * n) > 1
; :: thesis: k gcd (m * n) = k gcd n

then
k gcd (m * n) >= 1 + 1
by NAT_1:13;

then consider p being Element of NAT such that

A10: p is prime and

A11: p divides k gcd (m * n) by INT_2:31;

k gcd (m * n) divides k by NAT_D:def 5;

then A12: p divides k by A11, NAT_D:4;

then consider s being Nat such that

A13: k = p * s by NAT_D:def 3;

A14: not p divides m

then p divides m * n by A11, NAT_D:4;

then p divides n by A10, A14, NEWTON:80;

then consider r being Nat such that

A15: n = p * r by NAT_D:def 3;

reconsider s = s as Element of NAT by ORDINAL1:def 12;

A16: s + 1 > s by XREAL_1:29;

p > 1 by A10, INT_2:def 4;

then p >= 1 + 1 by NAT_1:13;

then A17: s * p >= s * (1 + 1) by NAT_1:4;

s <> 0 by A5, A13;

then s + s > s by XREAL_1:29;

then s + s >= s + 1 by NAT_1:13;

then k >= s + 1 by A13, A17, XXREAL_0:2;

then A18: s < k by A16, XXREAL_0:2;

A19: s gcd m = 1

A22: k gcd n = p * (s gcd r) by A13, A15, PYTHTRIP:8;

k gcd (m * n) = (p * s) gcd (p * (m * r)) by A13, A15

.= p * (s gcd (m * r)) by PYTHTRIP:8 ;

hence k gcd (m * n) = k gcd n by A2, A18, A19, A22; :: thesis: verum

end;then consider p being Element of NAT such that

A10: p is prime and

A11: p divides k gcd (m * n) by INT_2:31;

k gcd (m * n) divides k by NAT_D:def 5;

then A12: p divides k by A11, NAT_D:4;

then consider s being Nat such that

A13: k = p * s by NAT_D:def 3;

A14: not p divides m

proof

k gcd (m * n) divides m * n
by NAT_D:def 5;
assume
p divides m
; :: thesis: contradiction

then p divides 1 by A6, A12, NAT_D:def 5;

then p = 1 by WSIERP_1:15;

hence contradiction by A10, INT_2:def 4; :: thesis: verum

end;then p divides 1 by A6, A12, NAT_D:def 5;

then p = 1 by WSIERP_1:15;

hence contradiction by A10, INT_2:def 4; :: thesis: verum

then p divides m * n by A11, NAT_D:4;

then p divides n by A10, A14, NEWTON:80;

then consider r being Nat such that

A15: n = p * r by NAT_D:def 3;

reconsider s = s as Element of NAT by ORDINAL1:def 12;

A16: s + 1 > s by XREAL_1:29;

p > 1 by A10, INT_2:def 4;

then p >= 1 + 1 by NAT_1:13;

then A17: s * p >= s * (1 + 1) by NAT_1:4;

s <> 0 by A5, A13;

then s + s > s by XREAL_1:29;

then s + s >= s + 1 by NAT_1:13;

then k >= s + 1 by A13, A17, XXREAL_0:2;

then A18: s < k by A16, XXREAL_0:2;

A19: s gcd m = 1

proof

reconsider r = r as Element of NAT by ORDINAL1:def 12;
set c = s gcd m;

A20: s gcd m divides s by NAT_D:def 5;

A21: s gcd m divides m by NAT_D:def 5;

s divides k by A13, NAT_D:def 3;

then s gcd m divides k by A20, NAT_D:4;

then s gcd m divides 1 by A6, A21, NAT_D:def 5;

hence s gcd m = 1 by WSIERP_1:15; :: thesis: verum

end;A20: s gcd m divides s by NAT_D:def 5;

A21: s gcd m divides m by NAT_D:def 5;

s divides k by A13, NAT_D:def 3;

then s gcd m divides k by A20, NAT_D:4;

then s gcd m divides 1 by A6, A21, NAT_D:def 5;

hence s gcd m = 1 by WSIERP_1:15; :: thesis: verum

A22: k gcd n = p * (s gcd r) by A13, A15, PYTHTRIP:8;

k gcd (m * n) = (p * s) gcd (p * (m * r)) by A13, A15

.= p * (s gcd (m * r)) by PYTHTRIP:8 ;

hence k gcd (m * n) = k gcd n by A2, A18, A19, A22; :: thesis: verum

hence for k, m, n being Element of NAT st k gcd m = 1 holds

k gcd (m * n) = k gcd n ; :: thesis: verum