Metamath Proof Explorer

Theorem xmulid1

Description: Extended real version of mulid1 . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmulid1 
|- ( A e. RR* -> ( A *e 1 ) = A )

Proof

Step Hyp Ref Expression
1 elxr 
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
2 1re 
 |-  1 e. RR
3 rexmul 
 |-  ( ( A e. RR /\ 1 e. RR ) -> ( A *e 1 ) = ( A x. 1 ) )
4 2 3 mpan2 
 |-  ( A e. RR -> ( A *e 1 ) = ( A x. 1 ) )
5 ax-1rid 
 |-  ( A e. RR -> ( A x. 1 ) = A )
6 4 5 eqtrd 
 |-  ( A e. RR -> ( A *e 1 ) = A )
7 1xr 
 |-  1 e. RR*
8 0lt1 
 |-  0 < 1
9 xmulpnf2 
 |-  ( ( 1 e. RR* /\ 0 < 1 ) -> ( +oo *e 1 ) = +oo )
10 7 8 9 mp2an 
 |-  ( +oo *e 1 ) = +oo
11 oveq1 
 |-  ( A = +oo -> ( A *e 1 ) = ( +oo *e 1 ) )
12 id 
 |-  ( A = +oo -> A = +oo )
13 10 11 12 3eqtr4a 
 |-  ( A = +oo -> ( A *e 1 ) = A )
14 xmulmnf2 
 |-  ( ( 1 e. RR* /\ 0 < 1 ) -> ( -oo *e 1 ) = -oo )
15 7 8 14 mp2an 
 |-  ( -oo *e 1 ) = -oo
16 oveq1 
 |-  ( A = -oo -> ( A *e 1 ) = ( -oo *e 1 ) )
17 id 
 |-  ( A = -oo -> A = -oo )
18 15 16 17 3eqtr4a 
 |-  ( A = -oo -> ( A *e 1 ) = A )
19 6 13 18 3jaoi 
 |-  ( ( A e. RR \/ A = +oo \/ A = -oo ) -> ( A *e 1 ) = A )
20 1 19 sylbi 
 |-  ( A e. RR* -> ( A *e 1 ) = A )