Theorem xmulasslem2

Description: Lemma for xmulass . (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xmulasslem2	⊢ ( ( 0 < 𝐴 ∧ 𝐴 = -∞ ) → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝐴 = -∞ → ( 0 < 𝐴 ↔ 0 < -∞ ) )
2		0xr	⊢ 0 ∈ ℝ*
3		nltmnf	⊢ ( 0 ∈ ℝ* → ¬ 0 < -∞ )
4	2 3	ax-mp	⊢ ¬ 0 < -∞
5	4	pm2.21i	⊢ ( 0 < -∞ → 𝜑 )
6	1 5	biimtrdi	⊢ ( 𝐴 = -∞ → ( 0 < 𝐴 → 𝜑 ) )
7	6	impcom	⊢ ( ( 0 < 𝐴 ∧ 𝐴 = -∞ ) → 𝜑 )