let R be gcdDomain; 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
mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
let Amp be 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
mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
let r1, r2, s1, s2 be Element of R; ( Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp )
assume that
A1:
Amp is multiplicative
and
A2:
r1,r2 are_normalized_wrt Amp
and
A3:
s1,s2 are_normalized_wrt Amp
; mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
A4:
gcd (r1,r2,Amp) = 1. R
by A2;
then A5:
r1,r2 are_co-prime
;
s2 in Amp
by A3;
then A6:
s2 = NF (s2,Amp)
by Def9;
r2 in Amp
by A2;
then A7:
r2 = NF (r2,Amp)
by Def9;
A8:
r2 <> 0. R
by A2;
then A9:
gcd (s1,r2,Amp) <> 0. R
by Th33;
A10:
gcd (s1,s2,Amp) = 1. R
by A3;
then A11:
s1,s2 are_co-prime
;
A12:
s2 <> 0. R
by A3;
then A13:
gcd (r1,s2,Amp) <> 0. R
by Th33;
now ( ( ( r1 = 0. R or s1 = 0. R ) & mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp ) or ( r2 = 1. R & s2 = 1. R & mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp ) or ( s2 <> 0. R & r2 = 1. R & mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp ) or ( r2 <> 0. R & s2 = 1. R & mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp ) or ( not r1 = 0. R & not s1 = 0. R & ( not r2 = 1. R or not s2 = 1. R ) & ( not s2 <> 0. R or not r2 = 1. R ) & ( not r2 <> 0. R or not s2 = 1. R ) & mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp ) )per cases
( r1 = 0. R or s1 = 0. R or ( r2 = 1. R & s2 = 1. R ) or ( s2 <> 0. R & r2 = 1. R ) or ( r2 <> 0. R & s2 = 1. R ) or ( not r1 = 0. R & not s1 = 0. R & ( not r2 = 1. R or not s2 = 1. R ) & ( not s2 <> 0. R or not r2 = 1. R ) & ( not r2 <> 0. R or not s2 = 1. R ) ) )
;
case A14:
(
r1 = 0. R or
s1 = 0. R )
;
mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt AmpA15:
(
1. R in Amp &
1. R <> 0. R )
by Th22;
A16:
mult2 (
r1,
r2,
s1,
s2,
Amp)
= 1. R
by A5, A11, A7, A6, A14, Def19;
then
gcd (
(mult1 (r1,r2,s1,s2,Amp)),
(mult2 (r1,r2,s1,s2,Amp)),
Amp)
= 1. R
by Th32;
hence
mult1 (
r1,
r2,
s1,
s2,
Amp),
mult2 (
r1,
r2,
s1,
s2,
Amp)
are_normalized_wrt Amp
by A16, A15;
verum end; case A17:
(
r2 = 1. R &
s2 = 1. R )
;
mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt AmpA18:
(
1. R in Amp &
1. R <> 0. R )
by Th22;
A19:
mult2 (
r1,
r2,
s1,
s2,
Amp)
= 1. R
by A5, A11, A7, A17, Def19;
then
gcd (
(mult1 (r1,r2,s1,s2,Amp)),
(mult2 (r1,r2,s1,s2,Amp)),
Amp)
= 1. R
by Th32;
hence
mult1 (
r1,
r2,
s1,
s2,
Amp),
mult2 (
r1,
r2,
s1,
s2,
Amp)
are_normalized_wrt Amp
by A19, A18;
verum end; case A20:
(
s2 <> 0. R &
r2 = 1. R )
;
mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Ampthen A21:
gcd (
s1,
r2,
Amp)
= 1. R
by Th32;
then
r2 / (gcd (s1,r2,Amp)) = 1. R
by A20, Th9;
then A22:
s2 / (gcd (r1,s2,Amp)) = (s2 / (gcd (r1,s2,Amp))) * (r2 / (gcd (s1,r2,Amp)))
;
A23:
gcd (
r1,
s2,
Amp)
divides r1
by Def12;
then
gcd (
r1,
s2,
Amp)
divides r1 * s1
by Th7;
then A24:
(r1 * s1) / (gcd (r1,s2,Amp)) =
(r1 / (gcd (r1,s2,Amp))) * s1
by A13, A23, Th11
.=
(r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))
by A21, Th10
;
A25:
mult2 (
r1,
r2,
s1,
s2,
Amp)
= s2 / (gcd (r1,s2,Amp))
by A5, A11, A7, A6, A20, Def19;
reconsider zz =
gcd (
r1,
s2,
Amp) as
Element of
Amp by Def12;
A26:
(
gcd (
r1,
s2,
Amp)
divides s2 &
gcd (
r1,
s2,
Amp)
<> 0. R )
by A12, Def12, Th33;
then A27:
s2 / (gcd (r1,s2,Amp)) <> 0. R
by A12, Th8;
mult1 (
r1,
r2,
s1,
s2,
Amp)
= (r1 * s1) / (gcd (r1,s2,Amp))
by A20, Def18;
then A28:
gcd (
(mult1 (r1,r2,s1,s2,Amp)),
(mult2 (r1,r2,s1,s2,Amp)),
Amp)
= 1. R
by A4, A10, A8, A12, A25, A24, A22, Th41;
reconsider s2 =
s2 as
Element of
Amp by A3;
s2 / zz in Amp
by A1, A26, Th27;
hence
mult1 (
r1,
r2,
s1,
s2,
Amp),
mult2 (
r1,
r2,
s1,
s2,
Amp)
are_normalized_wrt Amp
by A25, A28, A27;
verum end; case A29:
(
r2 <> 0. R &
s2 = 1. R )
;
mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Ampthen A30:
gcd (
r1,
s2,
Amp)
= 1. R
by Th32;
then
s2 / (gcd (r1,s2,Amp)) = 1. R
by A29, Th9;
then A31:
r2 / (gcd (s1,r2,Amp)) = (r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)))
;
A32:
gcd (
s1,
r2,
Amp)
divides s1
by Def12;
then
gcd (
s1,
r2,
Amp)
divides r1 * s1
by Th7;
then A33:
(r1 * s1) / (gcd (s1,r2,Amp)) =
r1 * (s1 / (gcd (s1,r2,Amp)))
by A9, A32, Th11
.=
(r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))
by A30, Th10
;
A34:
mult2 (
r1,
r2,
s1,
s2,
Amp)
= r2 / (gcd (s1,r2,Amp))
by A5, A11, A7, A6, A29, Def19;
reconsider zz =
gcd (
s1,
r2,
Amp) as
Element of
Amp by Def12;
A35:
(
gcd (
s1,
r2,
Amp)
divides r2 &
gcd (
s1,
r2,
Amp)
<> 0. R )
by A8, Def12, Th33;
then A36:
r2 / (gcd (s1,r2,Amp)) <> 0. R
by A8, Th8;
mult1 (
r1,
r2,
s1,
s2,
Amp)
= (r1 * s1) / (gcd (s1,r2,Amp))
by A29, Def18;
then A37:
gcd (
(mult1 (r1,r2,s1,s2,Amp)),
(mult2 (r1,r2,s1,s2,Amp)),
Amp)
= 1. R
by A4, A10, A8, A12, A34, A33, A31, Th41;
reconsider r2 =
r2 as
Element of
Amp by A2;
r2 / zz in Amp
by A1, A35, Th27;
hence
mult1 (
r1,
r2,
s1,
s2,
Amp),
mult2 (
r1,
r2,
s1,
s2,
Amp)
are_normalized_wrt Amp
by A34, A37, A36;
verum end; case A38:
( not
r1 = 0. R & not
s1 = 0. R & ( not
r2 = 1. R or not
s2 = 1. R ) & ( not
s2 <> 0. R or not
r2 = 1. R ) & ( not
r2 <> 0. R or not
s2 = 1. R ) )
;
mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Ampreconsider z2 =
gcd (
s1,
r2,
Amp) as
Element of
Amp by Def12;
reconsider z1 =
gcd (
r1,
s2,
Amp) as
Element of
Amp by Def12;
A39:
(
gcd (
r1,
s2,
Amp)
divides s2 &
gcd (
r1,
s2,
Amp)
<> 0. R )
by A12, Def12, Th33;
then A40:
s2 / (gcd (r1,s2,Amp)) <> 0. R
by A12, Th8;
A41:
mult2 (
r1,
r2,
s1,
s2,
Amp)
= (r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)))
by A5, A11, A7, A6, A38, Def19;
mult1 (
r1,
r2,
s1,
s2,
Amp)
= (r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))
by A38, Def18;
then A42:
gcd (
(mult1 (r1,r2,s1,s2,Amp)),
(mult2 (r1,r2,s1,s2,Amp)),
Amp)
= 1. R
by A4, A10, A8, A12, A41, Th41;
A43:
(
gcd (
s1,
r2,
Amp)
divides r2 &
gcd (
s1,
r2,
Amp)
<> 0. R )
by A8, Def12, Th33;
then A44:
r2 / (gcd (s1,r2,Amp)) <> 0. R
by A8, Th8;
reconsider s2 =
s2 as
Element of
Amp by A3;
reconsider u =
s2 / z1 as
Element of
Amp by A1, A39, Th27;
reconsider r2 =
r2 as
Element of
Amp by A2;
reconsider v =
r2 / z2 as
Element of
Amp by A1, A43, Th27;
A45:
v * u <> 0. R
by A40, A44, VECTSP_2:def 1;
v * u in Amp
by A1;
hence
mult1 (
r1,
r2,
s1,
s2,
Amp),
mult2 (
r1,
r2,
s1,
s2,
Amp)
are_normalized_wrt Amp
by A41, A42, A45;
verum end; end; end;
hence
mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
; verum