defpred S1[ 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
S1[a] ) holds
S1[k]
proof
let k be Nat; :: thesis: ( ( for a being Nat st a < k holds
S1[a] ) implies S1[k] )

assume A2: for a being Nat st a < k holds
S1[a] ; :: thesis: S1[k]
per cases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25;
suppose A3: k = 0 ; :: thesis: S1[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 ;
hence k gcd (m * n) = k gcd n ; :: thesis: verum
end;
suppose A4: k = 1 ; :: thesis: S1[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 ;
hence k gcd (m * n) = k gcd n by ; :: thesis: verum
end;
suppose A5: k > 1 ; :: thesis: S1[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
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 ;
then k gcd n divides 1 by ;
hence k gcd (m * n) = k gcd n by ; :: 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 ;
then consider s being Nat such that
A13: k = p * s by NAT_D:def 3;
A14: not p divides m k gcd (m * n) divides m * n by NAT_D:def 5;
then p divides m * n by ;
then p divides n by ;
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 ;
then p >= 1 + 1 by NAT_1:13;
then A17: s * p >= s * (1 + 1) by NAT_1:4;
s <> 0 by ;
then s + s > s by XREAL_1:29;
then s + s >= s + 1 by NAT_1:13;
then k >= s + 1 by ;
then A18: s < k by ;
A19: s gcd m = 1 reconsider r = r as Element of NAT by ORDINAL1:def 12;
A22: k gcd n = p * (s gcd r) by ;
k gcd (m * n) = (p * s) gcd (p * (m * r)) by
.= 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 S1[k] from hence for k, m, n being Element of NAT st k gcd m = 1 holds
k gcd (m * n) = k gcd n ; :: thesis: verum