Metamath Proof Explorer

Theorem rexdiv

Description: The extended real division operation when both arguments are real. (Contributed by Thierry Arnoux, 18-Dec-2016)

Ref Expression
Assertion rexdiv 
|- ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( A /e B ) = ( A / B ) )

Proof

Step Hyp Ref Expression
1 redivcl 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( A / B ) e. RR )
2 recn 
 |-  ( A e. RR -> A e. CC )
3 recn 
 |-  ( B e. RR -> B e. CC )
4 id 
 |-  ( B =/= 0 -> B =/= 0 )
5 2 3 4 3anim123i 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( A e. CC /\ B e. CC /\ B =/= 0 ) )
6 divcan2 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B x. ( A / B ) ) = A )
7 5 6 syl 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( B x. ( A / B ) ) = A )
8 oveq2 
 |-  ( x = ( A / B ) -> ( B x. x ) = ( B x. ( A / B ) ) )
9 8 eqeq1d 
 |-  ( x = ( A / B ) -> ( ( B x. x ) = A <-> ( B x. ( A / B ) ) = A ) )
10 9 rspcev 
 |-  ( ( ( A / B ) e. RR /\ ( B x. ( A / B ) ) = A ) -> E. x e. RR ( B x. x ) = A )
11 1 7 10 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> E. x e. RR ( B x. x ) = A )
12 receu 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> E! x e. CC ( B x. x ) = A )
13 5 12 syl 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> E! x e. CC ( B x. x ) = A )
14 ax-resscn 
 |-  RR C_ CC
15 id 
 |-  ( ( B x. x ) = A -> ( B x. x ) = A )
16 15 rgenw 
 |-  A. x e. RR ( ( B x. x ) = A -> ( B x. x ) = A )
17 riotass2 
 |-  ( ( ( RR C_ CC /\ A. x e. RR ( ( B x. x ) = A -> ( B x. x ) = A ) ) /\ ( E. x e. RR ( B x. x ) = A /\ E! x e. CC ( B x. x ) = A ) ) -> ( iota_ x e. RR ( B x. x ) = A ) = ( iota_ x e. CC ( B x. x ) = A ) )
18 14 16 17 mpanl12 
 |-  ( ( E. x e. RR ( B x. x ) = A /\ E! x e. CC ( B x. x ) = A ) -> ( iota_ x e. RR ( B x. x ) = A ) = ( iota_ x e. CC ( B x. x ) = A ) )
19 11 13 18 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( iota_ x e. RR ( B x. x ) = A ) = ( iota_ x e. CC ( B x. x ) = A ) )
20 rexr 
 |-  ( A e. RR -> A e. RR* )
21 xdivval 
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( A /e B ) = ( iota_ x e. RR* ( B *e x ) = A ) )
22 20 21 syl3an1 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( A /e B ) = ( iota_ x e. RR* ( B *e x ) = A ) )
23 ressxr 
 |-  RR C_ RR*
24 23 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> RR C_ RR* )
25 rexmul 
 |-  ( ( B e. RR /\ x e. RR ) -> ( B *e x ) = ( B x. x ) )
26 25 eqeq1d 
 |-  ( ( B e. RR /\ x e. RR ) -> ( ( B *e x ) = A <-> ( B x. x ) = A ) )
27 26 biimprd 
 |-  ( ( B e. RR /\ x e. RR ) -> ( ( B x. x ) = A -> ( B *e x ) = A ) )
28 27 ralrimiva 
 |-  ( B e. RR -> A. x e. RR ( ( B x. x ) = A -> ( B *e x ) = A ) )
29 28 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> A. x e. RR ( ( B x. x ) = A -> ( B *e x ) = A ) )
30 xreceu 
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> E! x e. RR* ( B *e x ) = A )
31 20 30 syl3an1 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> E! x e. RR* ( B *e x ) = A )
32 riotass2 
 |-  ( ( ( RR C_ RR* /\ A. x e. RR ( ( B x. x ) = A -> ( B *e x ) = A ) ) /\ ( E. x e. RR ( B x. x ) = A /\ E! x e. RR* ( B *e x ) = A ) ) -> ( iota_ x e. RR ( B x. x ) = A ) = ( iota_ x e. RR* ( B *e x ) = A ) )
33 24 29 11 31 32 syl22anc 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( iota_ x e. RR ( B x. x ) = A ) = ( iota_ x e. RR* ( B *e x ) = A ) )
34 22 33 eqtr4d 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( A /e B ) = ( iota_ x e. RR ( B x. x ) = A ) )
35 divval 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( iota_ x e. CC ( B x. x ) = A ) )
36 5 35 syl 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( A / B ) = ( iota_ x e. CC ( B x. x ) = A ) )
37 19 34 36 3eqtr4d 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( A /e B ) = ( A / B ) )