Step |
Hyp |
Ref |
Expression |
1 |
|
simp2 |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> B e. RR ) |
2 |
1
|
rexrd |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> B e. RR* ) |
3 |
|
simp1 |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> A e. RR* ) |
4 |
|
1xr |
|- 1 e. RR* |
5 |
4
|
a1i |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> 1 e. RR* ) |
6 |
|
simp3 |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> B =/= 0 ) |
7 |
5 1 6
|
xdivcld |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( 1 /e B ) e. RR* ) |
8 |
3 7
|
xmulcld |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( A *e ( 1 /e B ) ) e. RR* ) |
9 |
|
xmulcom |
|- ( ( B e. RR* /\ ( A *e ( 1 /e B ) ) e. RR* ) -> ( B *e ( A *e ( 1 /e B ) ) ) = ( ( A *e ( 1 /e B ) ) *e B ) ) |
10 |
2 8 9
|
syl2anc |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( B *e ( A *e ( 1 /e B ) ) ) = ( ( A *e ( 1 /e B ) ) *e B ) ) |
11 |
|
xmulass |
|- ( ( A e. RR* /\ ( 1 /e B ) e. RR* /\ B e. RR* ) -> ( ( A *e ( 1 /e B ) ) *e B ) = ( A *e ( ( 1 /e B ) *e B ) ) ) |
12 |
3 7 2 11
|
syl3anc |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( ( A *e ( 1 /e B ) ) *e B ) = ( A *e ( ( 1 /e B ) *e B ) ) ) |
13 |
|
xmulcom |
|- ( ( ( 1 /e B ) e. RR* /\ B e. RR* ) -> ( ( 1 /e B ) *e B ) = ( B *e ( 1 /e B ) ) ) |
14 |
7 2 13
|
syl2anc |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( ( 1 /e B ) *e B ) = ( B *e ( 1 /e B ) ) ) |
15 |
|
eqid |
|- ( 1 /e B ) = ( 1 /e B ) |
16 |
|
xdivmul |
|- ( ( 1 e. RR* /\ ( 1 /e B ) e. RR* /\ ( B e. RR /\ B =/= 0 ) ) -> ( ( 1 /e B ) = ( 1 /e B ) <-> ( B *e ( 1 /e B ) ) = 1 ) ) |
17 |
5 7 1 6 16
|
syl112anc |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( ( 1 /e B ) = ( 1 /e B ) <-> ( B *e ( 1 /e B ) ) = 1 ) ) |
18 |
15 17
|
mpbii |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( B *e ( 1 /e B ) ) = 1 ) |
19 |
14 18
|
eqtrd |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( ( 1 /e B ) *e B ) = 1 ) |
20 |
19
|
oveq2d |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( A *e ( ( 1 /e B ) *e B ) ) = ( A *e 1 ) ) |
21 |
10 12 20
|
3eqtrd |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( B *e ( A *e ( 1 /e B ) ) ) = ( A *e 1 ) ) |
22 |
|
xmulid1 |
|- ( A e. RR* -> ( A *e 1 ) = A ) |
23 |
3 22
|
syl |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( A *e 1 ) = A ) |
24 |
21 23
|
eqtrd |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( B *e ( A *e ( 1 /e B ) ) ) = A ) |
25 |
|
xdivmul |
|- ( ( A e. RR* /\ ( A *e ( 1 /e B ) ) e. RR* /\ ( B e. RR /\ B =/= 0 ) ) -> ( ( A /e B ) = ( A *e ( 1 /e B ) ) <-> ( B *e ( A *e ( 1 /e B ) ) ) = A ) ) |
26 |
3 8 1 6 25
|
syl112anc |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( ( A /e B ) = ( A *e ( 1 /e B ) ) <-> ( B *e ( A *e ( 1 /e B ) ) ) = A ) ) |
27 |
24 26
|
mpbird |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( A /e B ) = ( A *e ( 1 /e B ) ) ) |