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

Metamath Proof Explorer

Theorem xmulasslem2

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

		Ref	Expression
	Assertion	xmulasslem2	$⊢ (0 < A \land A = −∞) \to φ$

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