defpred S₁[ Nat] means for m, n being 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:25;

suppose A3: k = 0 ; :: thesis: S₁[k]

let m, n be 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;

suppose A4: k = 1 ; :: thesis: S₁[k]

let m, n be 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;

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

let m, n be 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

proof

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

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: 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;

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

proof

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;

k gcd (m * n) divides m * n by NAT_D:def 5;
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

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;

reconsider r = r as Element of NAT by ORDINAL1:def 12;
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;

end;

end;

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 4(A1);
hence for k, m, n being Nat st k gcd m = 1 holds
k gcd (m * n) = k gcd n ; :: thesis: verum