This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xmulrid

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

Ref Expression
Assertion xmulrid ( 𝐴 ∈ ℝ* → ( 𝐴 ·e 1 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 elxr ⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
2 1re ⊢ 1 ∈ ℝ
3 rexmul ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐴 ·e 1 ) = ( 𝐴 · 1 ) )
4 2 3 mpan2 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ·e 1 ) = ( 𝐴 · 1 ) )
5 ax-1rid ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )
6 4 5 eqtrd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ·e 1 ) = 𝐴 )
7 1xr ⊢ 1 ∈ ℝ*
8 0lt1 ⊢ 0 < 1
9 xmulpnf2 ⊢ ( ( 1 ∈ ℝ* ∧ 0 < 1 ) → ( +∞ ·e 1 ) = +∞ )
10 7 8 9 mp2an ⊢ ( +∞ ·e 1 ) = +∞
11 oveq1 ⊢ ( 𝐴 = +∞ → ( 𝐴 ·e 1 ) = ( +∞ ·e 1 ) )
12 id ⊢ ( 𝐴 = +∞ → 𝐴 = +∞ )
13 10 11 12 3eqtr4a ⊢ ( 𝐴 = +∞ → ( 𝐴 ·e 1 ) = 𝐴 )
14 xmulmnf2 ⊢ ( ( 1 ∈ ℝ* ∧ 0 < 1 ) → ( -∞ ·e 1 ) = -∞ )
15 7 8 14 mp2an ⊢ ( -∞ ·e 1 ) = -∞
16 oveq1 ⊢ ( 𝐴 = -∞ → ( 𝐴 ·e 1 ) = ( -∞ ·e 1 ) )
17 id ⊢ ( 𝐴 = -∞ → 𝐴 = -∞ )
18 15 16 17 3eqtr4a ⊢ ( 𝐴 = -∞ → ( 𝐴 ·e 1 ) = 𝐴 )
19 6 13 18 3jaoi ⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) → ( 𝐴 ·e 1 ) = 𝐴 )
20 1 19 sylbi ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ·e 1 ) = 𝐴 )