Theorem xmulasslem2

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

	Ref	Expression
Assertion	xmulasslem2	$$⊢\left(0<A\wedge A=\mathrm{-\infty }\right)\to \phi$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢A=\mathrm{-\infty }\to \left(0<A\leftrightarrow 0<\mathrm{-\infty }\right)$$
2		0xr	$$⊢0\in {ℝ}^{*}$$
3		nltmnf	$$⊢0\in {ℝ}^{*}\to \neg 0<\mathrm{-\infty }$$
4	2 3	ax-mp	$$⊢\neg 0<\mathrm{-\infty }$$
5	4	pm2.21i	$$⊢0<\mathrm{-\infty }\to \phi$$
6	1 5	biimtrdi	$$⊢A=\mathrm{-\infty }\to \left(0<A\to \phi \right)$$
7	6	impcom	$$⊢\left(0<A\wedge A=\mathrm{-\infty }\right)\to \phi$$