Theorem xmulid1

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

	Ref	Expression
Assertion	xmulid1	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ·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 ) = 𝐴 )