Metamath Proof Explorer

Theorem divrec

Description: Relationship between division and reciprocal. Theorem I.9 of Apostol p. 18. (Contributed by NM, 2-Aug-2004) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> B e. CC )
2 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> A e. CC )
3 reccl 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( 1 / B ) e. CC )
4 3 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( 1 / B ) e. CC )
5 1 2 4 mul12d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B x. ( A x. ( 1 / B ) ) ) = ( A x. ( B x. ( 1 / B ) ) ) )
6 recid 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( B x. ( 1 / B ) ) = 1 )
7 6 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B x. ( 1 / B ) ) = 1 )
8 7 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A x. ( B x. ( 1 / B ) ) ) = ( A x. 1 ) )
9 2 mulid1d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A x. 1 ) = A )
10 5 8 9 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B x. ( A x. ( 1 / B ) ) ) = A )
11 2 4 mulcld 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A x. ( 1 / B ) ) e. CC )
12 3simpc 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B e. CC /\ B =/= 0 ) )
13 divmul 
 |-  ( ( A e. CC /\ ( A x. ( 1 / B ) ) e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) = ( A x. ( 1 / B ) ) <-> ( B x. ( A x. ( 1 / B ) ) ) = A ) )
14 2 11 12 13 syl3anc 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) = ( A x. ( 1 / B ) ) <-> ( B x. ( A x. ( 1 / B ) ) ) = A ) )
15 10 14 mpbird 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( A x. ( 1 / B ) ) )