A2: ( gcd r1,r2,Amp = 1. R & gcd s1,s2,Amp = 1. R ) by A1, Th44;
A3: ( ( 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 A4: ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & 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 A4;

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 A1, Th31;
hence for z being Element of R holds
( z = 1. R iff z = s2 / (gcd r1,s2,Amp) ) by A4, Th9; :: thesis: verum

end;

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

then A5: 1. R = s2 by A1, A2, Th31;
then A6: gcd r1,s2,Amp = 1. R by Th33;
1. R <> 0. R ;
hence for z being Element of R holds
( z = 1. R iff z = s2 / (gcd r1,s2,Amp) ) by A5, A6, 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;

A7: ( ( 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 A8: ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & 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 A8;

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

end;

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

then A9: 1. R = r2 by A1, A2, Th31;
then A10: gcd s1,r2,Amp = 1. R by Th33;
1. R <> 0. R ;
hence for z being Element of R holds
( z = 1. R iff z = r2 / (gcd s1,r2,Amp) ) by A9, A10, 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;

A11: ( 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 A12: ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R ) ; :: thesis: for z being Element of R holds
( z = 1. R iff z = s2 / (gcd r1,s2,Amp) )
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 A12, Th9; :: thesis: verum

end;

A13: ( 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 A14: ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R ) ; :: thesis: for z being Element of R holds
( z = 1. R iff z = r2 / (gcd s1,r2,Amp) )
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 A14, Th9; :: thesis: verum

end;

( 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 A15: ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R ) ; :: thesis: for z being Element of R holds
( z = s2 / (gcd r1,s2,Amp) iff z = r2 / (gcd s1,r2,Amp) )
then gcd r1,s2,Amp = 1. R by Th33;
hence for z being Element of R holds
( z = s2 / (gcd r1,s2,Amp) iff z = r2 / (gcd s1,r2,Amp) ) by A15, Th33; :: 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 A3, A7, A11, A13; :: thesis: verum