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