let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp holds
(add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))
let Amp be AmpleSet of R; :: thesis: for r1, r2, s1, s2 being Element of R st r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp holds
(add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))
let r1, r2, s1, s2 be Element of R; :: thesis: ( r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) )
assume that
A1: r1,r2 are_normalized_wrt Amp and
A2: s1,s2 are_normalized_wrt Amp ; :: thesis: (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))
gcd (r1,r2,Amp) = 1. R by A1;
then A3: r1,r2 are_co-prime ;
s2 in Amp by A2;
then A4: s2 = NF (s2,Amp) by Def9;
gcd (s1,s2,Amp) = 1. R by A2;
then A5: s1,s2 are_co-prime ;
r2 in Amp by A1;
then A6: r2 = NF (r2,Amp) by Def9;
A7: r2 <> 0. R by A1;
now :: thesis: ( ( r1 = 0. R & (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) ) or ( s1 = 0. R & (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) ) or ( gcd (r2,s2,Amp) = 1. R & (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) ) or ( (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R & (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) ) or ( r1 <> 0. R & s1 <> 0. R & gcd (r2,s2,Amp) <> 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) <> 0. R & (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) ) )
per cases ( r1 = 0. R or s1 = 0. R or gcd (r2,s2,Amp) = 1. R or (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R or ( r1 <> 0. R & s1 <> 0. R & gcd (r2,s2,Amp) <> 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) <> 0. R ) ) ;
case A8: r1 = 0. R ; :: thesis: (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))
then A9: add1 (r1,r2,s1,s2,Amp) = s1 by A3, A5, A6, A4, Def16;
add2 (r1,r2,s1,s2,Amp) = s2 by A3, A5, A6, A4, A8, Def17;
then (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) = s2 * ((0. R) + (s1 * r2)) by A8
.= s2 * (s1 * r2) by RLVECT_1:4
.= (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) by A9, GROUP_1:def 3 ;
hence (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) ; :: thesis: verum
end;
case A10: s1 = 0. R ; :: thesis: (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))
then A11: add1 (r1,r2,s1,s2,Amp) = r1 by A3, A5, A6, A4, Def16;
add2 (r1,r2,s1,s2,Amp) = r2 by A3, A5, A6, A4, A10, Def17;
then (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) = r2 * ((r1 * s2) + (0. R)) by A10
.= r2 * (r1 * s2) by RLVECT_1:4
.= (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) by A11, GROUP_1:def 3 ;
hence (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) ; :: thesis: verum
end;
case A12: gcd (r2,s2,Amp) = 1. R ; :: thesis: (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))
then add2 (r1,r2,s1,s2,Amp) = r2 * s2 by A3, A5, A6, A4, Def17;
hence (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) by A3, A5, A6, A4, A12, Def16; :: thesis: verum
end;
case A13: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; :: thesis: (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))
A14: (r1 * s2) + (s1 * r2) = 0. R
proof
A15: gcd (r2,s2,Amp) divides r2 by Def12;
then A16: gcd (r2,s2,Amp) divides s1 * r2 by Th7;
A17: gcd (r2,s2,Amp) divides s2 by Def12;
then consider f being Element of R such that
A18: (gcd (r2,s2,Amp)) * f = s2 ;
A19: gcd (r2,s2,Amp) <> 0. R by A7, Th33;
consider e being Element of R such that
A20: (gcd (r2,s2,Amp)) * e = r2 by A15;
(gcd (r2,s2,Amp)) * ((e * s1) + (f * r1)) = ((gcd (r2,s2,Amp)) * (e * s1)) + ((gcd (r2,s2,Amp)) * (f * r1)) by VECTSP_1:def 2
.= (((gcd (r2,s2,Amp)) * e) * s1) + ((gcd (r2,s2,Amp)) * (f * r1)) by GROUP_1:def 3
.= (r1 * s2) + (s1 * r2) by A20, A18, GROUP_1:def 3 ;
then A21: gcd (r2,s2,Amp) divides (r1 * s2) + (s1 * r2) ;
A22: gcd (r2,s2,Amp) divides r1 * s2 by A17, Th7;
then 0. R = ((r1 * s2) / (gcd (r2,s2,Amp))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) by A13, A19, A17, Th11
.= ((r1 * s2) / (gcd (r2,s2,Amp))) + ((s1 * r2) / (gcd (r2,s2,Amp))) by A19, A15, A16, Th11 ;
then A23: 0. R = ((r1 * s2) + (s1 * r2)) / (gcd (r2,s2,Amp)) by A19, A22, A16, A21, Th12;
0. R = (0. R) * (gcd (r2,s2,Amp))
.= (r1 * s2) + (s1 * r2) by A19, A21, A23, Def4 ;
hence (r1 * s2) + (s1 * r2) = 0. R ; :: thesis: verum
end;
add1 (r1,r2,s1,s2,Amp) = 0. R by A3, A5, A6, A4, A13, Def16;
then (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = 0. R
.= (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) by A14 ;
hence (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) ; :: thesis: verum
end;
case A24: ( r1 <> 0. R & s1 <> 0. R & gcd (r2,s2,Amp) <> 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) <> 0. R ) ; :: thesis: (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))
A25: gcd (r2,s2,Amp) divides s2 by Def12;
then A26: gcd (r2,s2,Amp) divides r1 * s2 by Th7;
then A27: gcd (r2,s2,Amp) divides (r1 * s2) * r2 by Th7;
then A28: gcd (r2,s2,Amp) divides ((r1 * s2) * r2) * s2 by Th7;
A29: add1 (r1,r2,s1,s2,Amp) = ((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))) / (gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp)) by A3, A5, A6, A4, A24, Def16;
A30: gcd (r2,s2,Amp) divides r2 by Def12;
then A31: gcd (r2,s2,Amp) divides s1 * r2 by Th7;
gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) divides gcd (r2,s2,Amp) by Def12;
then gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) divides r2 by A30, Th2;
then A32: gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) divides r2 * (s2 / (gcd (r2,s2,Amp))) by Th7;
then A33: gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) divides (r2 * (s2 / (gcd (r2,s2,Amp)))) * ((r1 * s2) + (s1 * r2)) by Th7;
A34: gcd (r2,s2,Amp) divides (s1 * r2) * r2 by A30, Th7;
then A35: gcd (r2,s2,Amp) divides ((s1 * r2) * r2) * s2 by Th7;
A36: gcd (r2,s2,Amp) divides r2 * s2 by A30, Th7;
then A37: gcd (r2,s2,Amp) divides (r2 * s2) * r1 by Th7;
then A38: gcd (r2,s2,Amp) divides ((r2 * s2) * r1) * s2 by Th7;
A39: gcd (r2,s2,Amp) divides (r2 * s2) * s1 by A36, Th7;
then A40: gcd (r2,s2,Amp) divides ((r2 * s2) * s1) * r2 by Th7;
A41: add2 (r1,r2,s1,s2,Amp) = (r2 * (s2 / (gcd (r2,s2,Amp)))) / (gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp)) by A3, A5, A6, A4, A24, Def17;
A42: gcd (r2,s2,Amp) <> 0. R by A7, Th33;
then A43: gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) <> 0. R by Th33;
A44: (r2 * (s2 / (gcd (r2,s2,Amp)))) * ((r1 * s2) + (s1 * r2)) = ((r2 * (s2 / (gcd (r2,s2,Amp)))) * (r1 * s2)) + ((r2 * (s2 / (gcd (r2,s2,Amp)))) * (s1 * r2)) by VECTSP_1:def 2
.= (((r2 * (s2 / (gcd (r2,s2,Amp)))) * r1) * s2) + ((r2 * (s2 / (gcd (r2,s2,Amp)))) * (s1 * r2)) by GROUP_1:def 3
.= (((r2 * (s2 / (gcd (r2,s2,Amp)))) * r1) * s2) + (((r2 * (s2 / (gcd (r2,s2,Amp)))) * s1) * r2) by GROUP_1:def 3
.= ((((r2 * s2) / (gcd (r2,s2,Amp))) * r1) * s2) + (((r2 * (s2 / (gcd (r2,s2,Amp)))) * s1) * r2) by A42, A25, A36, Th11
.= ((((r2 * s2) / (gcd (r2,s2,Amp))) * r1) * s2) + ((((r2 * s2) / (gcd (r2,s2,Amp))) * s1) * r2) by A42, A25, A36, Th11
.= ((((r2 * s2) * r1) / (gcd (r2,s2,Amp))) * s2) + ((((r2 * s2) / (gcd (r2,s2,Amp))) * s1) * r2) by A42, A36, A37, Th11
.= ((((r2 * s2) * r1) / (gcd (r2,s2,Amp))) * s2) + ((((r2 * s2) * s1) / (gcd (r2,s2,Amp))) * r2) by A42, A36, A39, Th11
.= ((((r2 * s2) * r1) * s2) / (gcd (r2,s2,Amp))) + ((((r2 * s2) * s1) / (gcd (r2,s2,Amp))) * r2) by A42, A37, A38, Th11
.= (((r1 * (s2 * r2)) * s2) / (gcd (r2,s2,Amp))) + ((((r2 * s2) * s1) * r2) / (gcd (r2,s2,Amp))) by A42, A39, A40, Th11
.= ((((r1 * s2) * r2) * s2) / (gcd (r2,s2,Amp))) + ((((r2 * s2) * s1) * r2) / (gcd (r2,s2,Amp))) by GROUP_1:def 3
.= ((((r1 * s2) * r2) * s2) / (gcd (r2,s2,Amp))) + ((s1 * ((r2 * s2) * r2)) / (gcd (r2,s2,Amp))) by GROUP_1:def 3
.= ((((r1 * s2) * r2) * s2) / (gcd (r2,s2,Amp))) + ((s1 * ((r2 * r2) * s2)) / (gcd (r2,s2,Amp))) by GROUP_1:def 3
.= ((((r1 * s2) * r2) * s2) / (gcd (r2,s2,Amp))) + (((s1 * (r2 * r2)) * s2) / (gcd (r2,s2,Amp))) by GROUP_1:def 3
.= ((((r1 * s2) * r2) * s2) / (gcd (r2,s2,Amp))) + ((((s1 * r2) * r2) * s2) / (gcd (r2,s2,Amp))) by GROUP_1:def 3 ;
A45: ((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))) * (r2 * s2) = ((r1 * (s2 / (gcd (r2,s2,Amp)))) * (r2 * s2)) + ((s1 * (r2 / (gcd (r2,s2,Amp)))) * (r2 * s2)) by VECTSP_1:def 7
.= (((r1 * s2) / (gcd (r2,s2,Amp))) * (r2 * s2)) + ((s1 * (r2 / (gcd (r2,s2,Amp)))) * (r2 * s2)) by A42, A25, A26, Th11
.= (((r1 * s2) / (gcd (r2,s2,Amp))) * (r2 * s2)) + (((s1 * r2) / (gcd (r2,s2,Amp))) * (r2 * s2)) by A42, A30, A31, Th11
.= ((((r1 * s2) / (gcd (r2,s2,Amp))) * r2) * s2) + (((s1 * r2) / (gcd (r2,s2,Amp))) * (r2 * s2)) by GROUP_1:def 3
.= ((((r1 * s2) / (gcd (r2,s2,Amp))) * r2) * s2) + ((((s1 * r2) / (gcd (r2,s2,Amp))) * r2) * s2) by GROUP_1:def 3
.= ((((r1 * s2) * r2) / (gcd (r2,s2,Amp))) * s2) + ((((s1 * r2) / (gcd (r2,s2,Amp))) * r2) * s2) by A42, A26, A27, Th11
.= ((((r1 * s2) * r2) / (gcd (r2,s2,Amp))) * s2) + ((((s1 * r2) * r2) / (gcd (r2,s2,Amp))) * s2) by A42, A31, A34, Th11
.= ((((r1 * s2) * r2) * s2) / (gcd (r2,s2,Amp))) + ((((s1 * r2) * r2) / (gcd (r2,s2,Amp))) * s2) by A42, A27, A28, Th11
.= ((((r1 * s2) * r2) * s2) / (gcd (r2,s2,Amp))) + ((((s1 * r2) * r2) * s2) / (gcd (r2,s2,Amp))) by A42, A34, A35, Th11 ;
A46: gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) divides (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) by Def12;
then gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) divides ((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))) * (r2 * s2) by Th7;
then (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))) * (r2 * s2)) / (gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp)) by A29, A43, A46, Th11
.= (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) by A41, A45, A44, A43, A32, A33, Th11 ;
hence (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) ; :: thesis: verum
end;
end;
end;
hence (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) ; :: thesis: verum