xmulpnf1

Description: Multiplication by plus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xmulpnf1	$⊢ (A \in ℝ^{*} \land 0 < A) \to A \cdot_{𝑒} +∞ = +∞$

Proof

Step	Hyp	Ref	Expression
1		pnfxr	$⊢ +∞ \in ℝ^{*}$
2		xmulval	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{}) \to A \cdot_{𝑒} +∞ = if ((A = 0 \lor +∞ = 0), 0, if ((((0 < +∞ \land A = +∞) \lor (+∞ < 0 \land A = −∞)) \lor ((0 < A \land +∞ = +∞) \lor (A < 0 \land +∞ = −∞))), +∞, if ((((0 < +∞ \land A = −∞) \lor (+∞ < 0 \land A = +∞)) \lor ((0 < A \land +∞ = −∞) \lor (A < 0 \land +∞ = +∞))), −∞, A +∞)))$
3	1 2	mpan2	$⊢ A \in ℝ^{*} \to A \cdot_{𝑒} +∞ = if ((A = 0 \lor +∞ = 0), 0, if ((((0 < +∞ \land A = +∞) \lor (+∞ < 0 \land A = −∞)) \lor ((0 < A \land +∞ = +∞) \lor (A < 0 \land +∞ = −∞))), +∞, if ((((0 < +∞ \land A = −∞) \lor (+∞ < 0 \land A = +∞)) \lor ((0 < A \land +∞ = −∞) \lor (A < 0 \land +∞ = +∞))), −∞, A +∞)))$
4	3	adantr	$⊢ (A \in ℝ^{*} \land 0 < A) \to A \cdot_{𝑒} +∞ = if ((A = 0 \lor +∞ = 0), 0, if ((((0 < +∞ \land A = +∞) \lor (+∞ < 0 \land A = −∞)) \lor ((0 < A \land +∞ = +∞) \lor (A < 0 \land +∞ = −∞))), +∞, if ((((0 < +∞ \land A = −∞) \lor (+∞ < 0 \land A = +∞)) \lor ((0 < A \land +∞ = −∞) \lor (A < 0 \land +∞ = +∞))), −∞, A +∞)))$
5		0xr	$⊢ 0 \in ℝ^{*}$
6		xrltne	$⊢ (0 \in ℝ^{} \land A \in ℝ^{} \land 0 < A) \to A \neq 0$
7	5 6	mp3an1	$⊢ (A \in ℝ^{*} \land 0 < A) \to A \neq 0$
8		0re	$⊢ 0 \in ℝ$
9		renepnf	$⊢ 0 \in ℝ \to 0 \neq +∞$
10	8 9	ax-mp	$⊢ 0 \neq +∞$
11	10	necomi	$⊢ +∞ \neq 0$
12		neanior	$⊢ (A \neq 0 \land +∞ \neq 0) \leftrightarrow \neg (A = 0 \lor +∞ = 0)$
13	7 11 12	sylanblc	$⊢ (A \in ℝ^{*} \land 0 < A) \to \neg (A = 0 \lor +∞ = 0)$
14	13	iffalsed	$⊢ (A \in ℝ^{*} \land 0 < A) \to if ((A = 0 \lor +∞ = 0), 0, if ((((0 < +∞ \land A = +∞) \lor (+∞ < 0 \land A = −∞)) \lor ((0 < A \land +∞ = +∞) \lor (A < 0 \land +∞ = −∞))), +∞, if ((((0 < +∞ \land A = −∞) \lor (+∞ < 0 \land A = +∞)) \lor ((0 < A \land +∞ = −∞) \lor (A < 0 \land +∞ = +∞))), −∞, A +∞))) = if ((((0 < +∞ \land A = +∞) \lor (+∞ < 0 \land A = −∞)) \lor ((0 < A \land +∞ = +∞) \lor (A < 0 \land +∞ = −∞))), +∞, if ((((0 < +∞ \land A = −∞) \lor (+∞ < 0 \land A = +∞)) \lor ((0 < A \land +∞ = −∞) \lor (A < 0 \land +∞ = +∞))), −∞, A +∞))$
15		simpr	$⊢ (A \in ℝ^{*} \land 0 < A) \to 0 < A$
16		eqid	$⊢ +∞ = +∞$
17	15 16	jctir	$⊢ (A \in ℝ^{*} \land 0 < A) \to (0 < A \land +∞ = +∞)$
18	17	orcd	$⊢ (A \in ℝ^{*} \land 0 < A) \to ((0 < A \land +∞ = +∞) \lor (A < 0 \land +∞ = −∞))$
19	18	olcd	$⊢ (A \in ℝ^{*} \land 0 < A) \to (((0 < +∞ \land A = +∞) \lor (+∞ < 0 \land A = −∞)) \lor ((0 < A \land +∞ = +∞) \lor (A < 0 \land +∞ = −∞)))$
20	19	iftrued	$⊢ (A \in ℝ^{*} \land 0 < A) \to if ((((0 < +∞ \land A = +∞) \lor (+∞ < 0 \land A = −∞)) \lor ((0 < A \land +∞ = +∞) \lor (A < 0 \land +∞ = −∞))), +∞, if ((((0 < +∞ \land A = −∞) \lor (+∞ < 0 \land A = +∞)) \lor ((0 < A \land +∞ = −∞) \lor (A < 0 \land +∞ = +∞))), −∞, A +∞)) = +∞$
21	4 14 20	3eqtrd	$⊢ (A \in ℝ^{*} \land 0 < A) \to A \cdot_{𝑒} +∞ = +∞$

Metamath Proof Explorer

Theorem xmulpnf1

Proof