Theorem xmulasslem2

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

	Ref	Expression
Assertion	xmulasslem2	|- ( ( 0 < A /\ A = -oo ) -> ph )

Proof

Step	Hyp	Ref	Expression
1		breq2	|- ( A = -oo -> ( 0 < A <-> 0 < -oo ) )
2		0xr	|- 0 e. RR*
3		nltmnf	|- ( 0 e. RR* -> -. 0 < -oo )
4	2 3	ax-mp	|- -. 0 < -oo
5	4	pm2.21i	|- ( 0 < -oo -> ph )
6	1 5	syl6bi	|- ( A = -oo -> ( 0 < A -> ph ) )
7	6	impcom	|- ( ( 0 < A /\ A = -oo ) -> ph )