let a, b, c be Nat; :: thesis: (a + (b * c)) gcd b = a gcd b
defpred S1[ Nat] means (a + (b * \$1)) gcd b = a gcd b;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let kk be Nat; :: thesis: ( S1[kk] implies S1[kk + 1] )
assume A2: (a + (b * kk)) gcd b = a gcd b ; :: thesis: S1[kk + 1]
now :: thesis: (a + (b * (kk + 1))) gcd b = a gcd b
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 ;
A5: a gcd b divides a + (b * kk) by ;
then A6: a + (b * kk) = (a gcd b) * ((a + (b * kk)) div (a gcd b)) by NAT_D:3;
now :: thesis: (a + (b * (kk + 1))) gcd b = a gcd b
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 ; :: 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 ;
then (a + (b * kk)) div (a gcd b),b div (a gcd b) are_coprime by A4, A9, Th6;
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 Th7;
(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
.= ((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 ;
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 S1[kk + 1] ; :: thesis: verum
end;
A12: S1[ 0 ] ;
for c being Nat holds S1[c] from NAT_1:sch 2(A12, A1);
hence (a + (b * c)) gcd b = a gcd b ; :: thesis: verum