defpred S₁[ 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₁[a] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for a being Nat st a < k holds
S₁[a] ) implies S₁[k] )
assume A2: for a being Nat st a < k holds
S₁[a] ; :: thesis: S₁[k]

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

suppose A3: k = 0 ; :: thesis: S₁[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:65;
hence k gcd (m * n) = k gcd n ; :: thesis: verum

end;

suppose A4: k = 1 ; :: thesis: S₁[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:64;
hence k gcd (m * n) = k gcd n by A4, NEWTON:64; :: thesis: verum

end;

suppose A5: k > 1 ; :: thesis: S₁[k]

let m, n be Element of NAT ; :: thesis: ( k gcd m = 1 implies k gcd (m * n) = k gcd n )
assume A6: k gcd m = 1 ; :: thesis: k gcd (m * n) = k gcd n
set b = k gcd (m * n);
thus k gcd (m * n) = k gcd n :: thesis: verum

proof

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

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;

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: k gcd n divides n by NAT_D:def 5;
n divides m * n by NAT_D:def 3;
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:20; :: thesis: verum

end;

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:48;
A12: p divides k

proof

k gcd (m * n) divides k by NAT_D:def 5;
hence p divides k by A11, NAT_D:4; :: thesis: verum

end;

then consider s being Nat such that
A13: k = p * s by NAT_D:def 3;
reconsider s = s as Element of NAT by ORDINAL1:def 13;
A14: s < k

proof

p > 1 by A10, INT_2:def 5;
then p >= 1 + 1 by NAT_1:13;
then A15: s * p >= s * (1 + 1) by NAT_1:4;
s <> 0 by A5, A13;
then s + s > s by NAT_1:3, XREAL_1:31;
then s + s >= s + 1 by NAT_1:13;
then A16: k >= s + 1 by A13, A15, XXREAL_0:2;
s + 1 > s by XREAL_1:31;
hence s < k by A16, XXREAL_0:2; :: thesis: verum

end;

A17: not p divides m

proof

assume p divides m ; :: thesis: contradiction
then p divides 1 by A6, A12, NAT_D:def 5;
then p = 1 by WSIERP_1:20;
hence contradiction by A10, INT_2:def 5; :: thesis: verum

end;

p divides m * n

proof

k gcd (m * n) divides m * n by NAT_D:def 5;
hence p divides m * n by A11, NAT_D:4; :: thesis: verum

end;

then p divides n by A10, A17, NEWTON:98;
then consider r being Nat such that
A18: n = p * r by NAT_D:def 3;
reconsider r = r as Element of NAT by ORDINAL1:def 13;
A19: s gcd m = 1

proof

set c = s gcd m;
A20: s gcd m divides s by NAT_D:def 5;
s divides k by A13, NAT_D:def 3;
then A21: s gcd m divides k by A20, NAT_D:4;
s gcd m divides m by NAT_D:def 5;
then s gcd m divides 1 by A6, A21, NAT_D:def 5;
hence s gcd m = 1 by WSIERP_1:20; :: thesis: verum

end;

A22: k gcd (m * n) = (p * s) gcd (p * (m * r)) by A13, A18
.= p * (s gcd (m * r)) by PYTHTRIP:8 ;
k gcd n = p * (s gcd r) by A13, A18, PYTHTRIP:8;
hence k gcd (m * n) = k gcd n by A2, A14, A19, A22; :: thesis: verum

end;

end;

end;

end;

end;

end;

for k being Nat holds S₁[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