A5: gcd (s1,s2,Amp) = 1. R by A2, Th43;
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 :: thesis: ( ( r1 = 0. R & ( for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) ) ) ) or ( s1 = 0. R & ( for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) ) ) ) )

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, Th30;
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, Th30;
then gcd (r1,s2,Amp) = 1. R by Th32;
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: gcd (r1,r2,Amp) = 1. R by A1, Th43;
A13: ( ( 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
A14: ( r1 = 0. R or s1 = 0. R ) and
A15: 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 :: thesis: ( ( s1 = 0. R & ( for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) ) ) or ( r1 = 0. R & ( for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) ) ) )

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

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, Th30;
hence for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) by A15, Th9; :: thesis: verum

end;

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

A17: 1. R <> 0. R ;
A18: 1. R = r2 by A3, A12, A16, Th30;
then gcd (s1,r2,Amp) = 1. R by Th32;
hence for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) by A18, A17, 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;

A19: ( 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
A20: r2 = 1. R and
s2 = 1. R and
A21: 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 A20, Th32;
hence for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) by A20, A21, 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
A22: s2 = 1. R and
A23: 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 A22, Th32;
hence for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) ) by A22, A23, 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, A13, A19; :: thesis: verum