Metamath Proof Explorer

Theorem diveq1

Description: Equality in terms of unit ratio. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion diveq1 
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) = 1 <-> A = B ) )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 divmul2 
 |-  ( ( A e. CC /\ 1 e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) = 1 <-> A = ( B x. 1 ) ) )
3 1 2 mp3an2 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) = 1 <-> A = ( B x. 1 ) ) )
4 3 3impb 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) = 1 <-> A = ( B x. 1 ) ) )
5 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> B e. CC )
6 5 mulid1d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B x. 1 ) = B )
7 6 eqeq2d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A = ( B x. 1 ) <-> A = B ) )
8 4 7 bitrd 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) = 1 <-> A = B ) )