A5: ( gcd (r2,s2,Amp) = 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies for z being Element of R holds
( z = r2 * s2 iff z = 1. R ) )
proof
assume that
A6: gcd (r2,s2,Amp) = 1. R and
A7: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; :: thesis: for z being Element of R holds
( z = r2 * s2 iff z = 1. R )
A8: 0. R = (r1 * s2) + (s1 * (r2 / (1. R))) by A6, A7, Th10
.= (r1 * s2) + (s1 * r2) by Th10 ;
then A9: r1 * s2 = - (s1 * r2) by RLVECT_1:6;
A10: s1 * r2 = - (r1 * s2) by A8, RLVECT_1:6;
gcd (s2,s1,Amp) = 1. R by A2, Th43;
then gcd (s2,(s1 * r2),Amp) = gcd (s2,r2,Amp) by Th37
.= 1. R by A6, Th29 ;
then 1. R = gcd (((1. R) * s2),(- (r1 * s2)),Amp) by A10
.= gcd (((1. R) * s2),((- r1) * s2),Amp) by VECTSP_1:8 ;
then A11: 1. R is_associated_to s2 * (gcd ((1. R),(- r1),Amp)) by Th36;
let z be Element of R; :: thesis: ( z = r2 * s2 iff z = 1. R )
A12: 1. R in Amp by Th22;
gcd (r2,r1,Amp) = 1. R by A1, Th43;
then gcd (r2,(r1 * s2),Amp) = 1. R by A6, Th37;
then 1. R = gcd (((1. R) * r2),(- (s1 * r2)),Amp) by A9
.= gcd (((1. R) * r2),((- s1) * r2),Amp) by VECTSP_1:8 ;
then A13: 1. R is_associated_to r2 * (gcd ((1. R),(- s1),Amp)) by Th36;
s2 * (gcd ((1. R),(- r1),Amp)) = s2 * (1. R) by Th32
.= s2 ;
then A14: s2 = 1. R by A4, A12, A11, Def9;
r2 * (gcd ((1. R),(- s1),Amp)) = r2 * (1. R) by Th32
.= r2 ;
then r2 = 1. R by A3, A13, A12, Def9;
hence ( z = r2 * s2 iff z = 1. R ) by A14; :: thesis: verum
end;
A15: gcd (r1,r2,Amp) = 1. R by A1, Th43;
A16: ( r1 = 0. R & gcd (r2,s2,Amp) = 1. R implies for z being Element of R holds
( z = s2 iff z = r2 * s2 ) )
proof
assume that
A17: r1 = 0. R and
gcd (r2,s2,Amp) = 1. R ; :: thesis: for z being Element of R holds
( z = s2 iff z = r2 * s2 )
let z be Element of R; :: thesis: ( z = s2 iff z = r2 * s2 )
r2 = 1. R by A3, A15, A17, Th30;
hence ( z = s2 iff z = r2 * s2 ) ; :: thesis: verum
end;
A18: gcd (s1,s2,Amp) = 1. R by A2, Th43;
A19: ( s1 = 0. R & gcd (r2,s2,Amp) = 1. R implies for z being Element of R holds
( z = r2 iff z = r2 * s2 ) )
proof
assume that
A20: s1 = 0. R and
gcd (r2,s2,Amp) = 1. R ; :: thesis: for z being Element of R holds
( z = r2 iff z = r2 * s2 )
let z be Element of R; :: thesis: ( z = r2 iff z = r2 * s2 )
s2 = 1. R by A4, A18, A20, Th30;
hence ( z = r2 iff z = r2 * s2 ) ; :: thesis: verum
end;
A21: ( s1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies for z being Element of R holds
( z = r2 iff z = 1. R ) )
proof
A22: 1. R <> 0. R ;
assume that
A23: s1 = 0. R and
A24: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; :: thesis: for z being Element of R holds
( z = r2 iff z = 1. R )
let z be Element of R; :: thesis: ( z = r2 iff z = 1. R )
A25: s2 = 1. R by A4, A18, A23, Th30;
then A26: gcd (r2,s2,Amp) = 1. R by Th32;
0. R = (r1 * (s2 / (gcd (r2,s2,Amp)))) + (0. R) by A23, A24
.= r1 * ((1. R) / (gcd (r2,s2,Amp))) by A25, RLVECT_1:4
.= r1 * (1. R) by A26, A22, Th9
.= r1 ;
hence ( z = r2 iff z = 1. R ) by A3, A15, Th30; :: thesis: verum
end;
A27: ( r1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies for z being Element of R holds
( z = s2 iff z = 1. R ) )
proof
A28: 1. R <> 0. R ;
assume that
A29: r1 = 0. R and
A30: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; :: thesis: for z being Element of R holds
( z = s2 iff z = 1. R )
let z be Element of R; :: thesis: ( z = s2 iff z = 1. R )
A31: r2 = 1. R by A3, A15, A29, Th30;
then A32: gcd (r2,s2,Amp) = 1. R by Th32;
0. R = (0. R) + (s1 * (r2 / (gcd (r2,s2,Amp)))) by A29, A30
.= s1 * ((1. R) / (gcd (r2,s2,Amp))) by A31, RLVECT_1:4
.= s1 * (1. R) by A32, A28, Th9
.= s1 ;
hence ( z = s2 iff z = 1. R ) by A4, A18, Th30; :: thesis: verum
end;
( r1 = 0. R & s1 = 0. R implies for z being Element of R holds
( z = s2 iff z = r2 ) )
proof
assume that
A33: r1 = 0. R and
A34: s1 = 0. R ; :: thesis: for z being Element of R holds
( z = s2 iff z = r2 )
let z be Element of R; :: thesis: ( z = s2 iff z = r2 )
r2 = 1. R by A3, A15, A33, Th30;
hence ( z = s2 iff z = r2 ) by A4, A18, A34, Th30; :: thesis: verum
end;
hence for b1 being Element of R holds
( ( r1 = 0. R & s1 = 0. R implies ( b1 = s2 iff b1 = r2 ) ) & ( r1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b1 = s2 iff b1 = r2 * s2 ) ) & ( r1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b1 = s2 iff b1 = 1. R ) ) & ( s1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b1 = r2 iff b1 = r2 * s2 ) ) & ( s1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b1 = r2 iff b1 = 1. R ) ) & ( gcd (r2,s2,Amp) = 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b1 = r2 * s2 iff b1 = 1. R ) ) ) by A16, A27, A19, A21, A5; :: thesis: verum