let a, b, c be Nat; :: thesis: (a + (b * c)) gcd b = a gcd b
defpred S₁[ Nat] means (a + (b * $1)) gcd b = a gcd b;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let kk be Nat; :: thesis: ( S₁[kk] implies S₁[kk + 1] )
assume A2: (a + (b * kk)) gcd b = a gcd b ; :: thesis: S₁[kk + 1]

now

per cases ( b = 0 or b > 0 ) ;

suppose b = 0 ; :: thesis: (a + (b * (kk + 1))) gcd b = a gcd b

hence (a + (b * (kk + 1))) gcd b = a gcd b ; :: thesis: verum

end;

suppose A3: b > 0 ; :: thesis: (a + (b * (kk + 1))) gcd b = a gcd b

set T = a gcd b;
A4: a gcd b > 0 by A3, NEWTON:58;
A5: a gcd b divides a + (b * kk) by A2, NAT_D:def 5;
then A6: a + (b * kk) = (a gcd b) * ((a + (b * kk)) div (a gcd b)) by NAT_D:3;

now

per cases ( a + (b * kk) = 0 or a + (b * kk) > 0 ) ;

suppose A7: a + (b * kk) = 0 ; :: thesis: (a + (b * (kk + 1))) gcd b = a gcd b

then a gcd b = 0 gcd b by NAT_1:7
.= b by NEWTON:52 ;
hence (a + (b * (kk + 1))) gcd b = a gcd b by A7, NAT_D:32; :: thesis: verum

end;

suppose A8: a + (b * kk) > 0 ; :: thesis: (a + (b * (kk + 1))) gcd b = a gcd b

set T2 = b div (a gcd b);
set T1 = (a + (b * kk)) div (a gcd b);
A9: (a + (b * kk)) div (a gcd b) <> 0 by A6, A8;
a gcd b divides b by NAT_D:def 5;
then A10: b = (a gcd b) * (b div (a gcd b)) by NAT_D:3;
then (((a + (b * kk)) div (a gcd b)) * (a gcd b)) gcd ((b div (a gcd b)) * (a gcd b)) = a gcd b by A2, A5, NAT_D:3;
then (a + (b * kk)) div (a gcd b),b div (a gcd b) are_relative_prime by A4, A9, Th7;
then ((a + (b * kk)) div (a gcd b)) gcd (b div (a gcd b)) = 1 by INT_2:def 3;
then A11: (((a + (b * kk)) div (a gcd b)) + (b div (a gcd b))) gcd (b div (a gcd b)) = 1 by Th8;
(a + (b * (kk + 1))) gcd b = ((a + (b * kk)) + b) gcd b
.= (((a gcd b) * ((a + (b * kk)) div (a gcd b))) + ((a gcd b) * (b div (a gcd b)))) gcd ((a gcd b) * (b div (a gcd b))) by A5, A10, NAT_D:3
.= ((a gcd b) * (((a + (b * kk)) div (a gcd b)) + (b div (a gcd b)))) gcd ((a gcd b) * (b div (a gcd b)))
.= a gcd b by A11, Th6 ;
hence (a + (b * (kk + 1))) gcd b = a gcd b ; :: thesis: verum

end;

end;

end;

hence (a + (b * (kk + 1))) gcd b = a gcd b ; :: thesis: verum

end;

end;

end;

hence S₁[kk + 1] ; :: thesis: verum

end;

A12: S₁[ 0 ] ;
for c being Nat holds S₁[c] from NAT_1:sch 2(A12, A1);
hence (a + (b * c)) gcd b = a gcd b ; :: thesis: verum