Metamath Proof Explorer

Theorem redvr

Description: The division operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017)

Ref Expression
Assertion redvr 
|- ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( A ( /r ` RRfld ) B ) = ( A / B ) )

Proof

Step Hyp Ref Expression
1 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
2 1 simpli 
 |-  RR e. ( SubRing ` CCfld )
3 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> A e. RR )
4 3simpc 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( B e. RR /\ B =/= 0 ) )
5 1 simpri 
 |-  RRfld e. DivRing
6 rebase 
 |-  RR = ( Base ` RRfld )
7 eqid 
 |-  ( Unit ` RRfld ) = ( Unit ` RRfld )
8 re0g 
 |-  0 = ( 0g ` RRfld )
9 6 7 8 drngunit 
 |-  ( RRfld e. DivRing -> ( B e. ( Unit ` RRfld ) <-> ( B e. RR /\ B =/= 0 ) ) )
10 5 9 ax-mp 
 |-  ( B e. ( Unit ` RRfld ) <-> ( B e. RR /\ B =/= 0 ) )
11 4 10 sylibr 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> B e. ( Unit ` RRfld ) )
12 df-refld 
 |-  RRfld = ( CCfld |`s RR )
13 cnflddiv 
 |-  / = ( /r ` CCfld )
14 eqid 
 |-  ( /r ` RRfld ) = ( /r ` RRfld )
15 12 13 7 14 subrgdv 
 |-  ( ( RR e. ( SubRing ` CCfld ) /\ A e. RR /\ B e. ( Unit ` RRfld ) ) -> ( A / B ) = ( A ( /r ` RRfld ) B ) )
16 2 3 11 15 mp3an2i 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( A / B ) = ( A ( /r ` RRfld ) B ) )
17 16 eqcomd 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( A ( /r ` RRfld ) B ) = ( A / B ) )