A5: gcd (s1,s2,Amp) = 1. R by A2, Th44;
A6: ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) ) )

proof

assume that
A7: ( r1 = 0. R or s1 = 0. R ) and
A8: s2 <> 0. R and
r2 = 1. R ; :: thesis: for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) )

now

per cases ( r1 = 0. R or s1 = 0. R ) by A7;

case r1 = 0. R ; :: thesis: for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) )

then gcd (r1,s2,Amp) = s2 by A4, Th31;
hence for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) ) by A8, Th9; :: thesis: verum

end;

case A9: s1 = 0. R ; :: thesis: for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) )

A10: 1. R <> 0. R ;
A11: 1. R = s2 by A4, A5, A9, Th31;
then gcd (r1,s2,Amp) = 1. R by Th33;
hence for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) ) by A11, A10, Th9; :: thesis: verum

end;

end;

end;

hence for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) ) ; :: thesis: verum

end;

A12: ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R implies for z being Element of R holds
( z = s2 / (gcd (r1,s2,Amp)) iff z = r2 / (gcd (s1,r2,Amp)) ) )

proof

assume that
s2 <> 0. R and
A13: r2 = 1. R and
r2 <> 0. R and
A14: s2 = 1. R ; :: thesis: for z being Element of R holds
( z = s2 / (gcd (r1,s2,Amp)) iff z = r2 / (gcd (s1,r2,Amp)) )
gcd (r1,s2,Amp) = 1. R by A14, Th33;
hence for z being Element of R holds
( z = s2 / (gcd (r1,s2,Amp)) iff z = r2 / (gcd (s1,r2,Amp)) ) by A13, A14, Th33; :: thesis: verum

end;

A15: gcd (r1,r2,Amp) = 1. R by A1, Th44;
A16: ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) )

proof

assume that
A17: ( r1 = 0. R or s1 = 0. R ) and
A18: r2 <> 0. R and
s2 = 1. R ; :: thesis: for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) )

now

per cases ( s1 = 0. R or r1 = 0. R ) by A17;

case s1 = 0. R ; :: thesis: for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) )

then gcd (s1,r2,Amp) = r2 by A3, Th31;
hence for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) by A18, Th9; :: thesis: verum

end;

case A19: r1 = 0. R ; :: thesis: for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) )

A20: 1. R <> 0. R ;
A21: 1. R = r2 by A3, A15, A19, Th31;
then gcd (s1,r2,Amp) = 1. R by Th33;
hence for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) by A21, A20, Th9; :: thesis: verum

end;

end;

end;

hence for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) ; :: thesis: verum

end;

A22: ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) )

proof

assume that
A23: r2 = 1. R and
s2 = 1. R and
A24: r2 <> 0. R and
s2 = 1. R ; :: thesis: for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) )
gcd (s1,r2,Amp) = 1. R by A23, Th33;
hence for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) by A23, A24, Th9; :: thesis: verum

end;

( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) ) )

proof

assume that
r2 = 1. R and
A25: s2 = 1. R and
A26: s2 <> 0. R and
r2 = 1. R ; :: thesis: for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) )
gcd (r1,s2,Amp) = 1. R by A25, Th33;
hence for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) ) by A25, A26, Th9; :: thesis: verum

end;

hence for b₁ being Element of R holds
( ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies ( b₁ = 1. R iff b₁ = 1. R ) ) & ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies ( b₁ = 1. R iff b₁ = s2 / (gcd (r1,s2,Amp)) ) ) & ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies ( b₁ = 1. R iff b₁ = r2 / (gcd (s1,r2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies ( b₁ = 1. R iff b₁ = s2 / (gcd (r1,s2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b₁ = 1. R iff b₁ = r2 / (gcd (s1,r2,Amp)) ) ) & ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b₁ = s2 / (gcd (r1,s2,Amp)) iff b₁ = r2 / (gcd (s1,r2,Amp)) ) ) ) by A6, A16, A22, A12; :: thesis: verum