xrpxdivcld

Description: Closure law for extended division of positive extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016)

	Ref	Expression
Hypotheses	xrpxdivcld.1	$⊢ φ \to A \in [0, +∞]$
	xrpxdivcld.2	$⊢ φ \to B \in ℝ^{+}$
Assertion	xrpxdivcld	$⊢ φ \to A \div_{𝑒} B \in [0, +∞]$

Proof

Step	Hyp	Ref	Expression
1		xrpxdivcld.1	$⊢ φ \to A \in [0, +∞]$
2		xrpxdivcld.2	$⊢ φ \to B \in ℝ^{+}$
3		oveq1	$⊢ A = 0 \to A \div_{𝑒} B = 0 \div_{𝑒} B$
4		xdiv0rp	$⊢ B \in ℝ^{+} \to 0 \div_{𝑒} B = 0$
5	2 4	syl	$⊢ φ \to 0 \div_{𝑒} B = 0$
6	3 5	sylan9eqr	$⊢ (φ \land A = 0) \to A \div_{𝑒} B = 0$
7		elxrge02	$⊢ A \div_{𝑒} B \in [0, +∞] \leftrightarrow (A \div_{𝑒} B = 0 \lor A \div_{𝑒} B \in ℝ^{+} \lor A \div_{𝑒} B = +∞)$
8	7	biimpri	$⊢ (A \div_{𝑒} B = 0 \lor A \div_{𝑒} B \in ℝ^{+} \lor A \div_{𝑒} B = +∞) \to A \div_{𝑒} B \in [0, +∞]$
9	8	3o1cs	$⊢ A \div_{𝑒} B = 0 \to A \div_{𝑒} B \in [0, +∞]$
10	6 9	syl	$⊢ (φ \land A = 0) \to A \div_{𝑒} B \in [0, +∞]$
11		simpr	$⊢ (φ \land A \in ℝ^{+}) \to A \in ℝ^{+}$
12	2	adantr	$⊢ (φ \land A \in ℝ^{+}) \to B \in ℝ^{+}$
13	11 12	rpxdivcld	$⊢ (φ \land A \in ℝ^{+}) \to A \div_{𝑒} B \in ℝ^{+}$
14	8	3o2cs	$⊢ A \div_{𝑒} B \in ℝ^{+} \to A \div_{𝑒} B \in [0, +∞]$
15	13 14	syl	$⊢ (φ \land A \in ℝ^{+}) \to A \div_{𝑒} B \in [0, +∞]$
16		oveq1	$⊢ A = +∞ \to A \div_{𝑒} B = +∞ \div_{𝑒} B$
17		xdivpnfrp	$⊢ B \in ℝ^{+} \to +∞ \div_{𝑒} B = +∞$
18	2 17	syl	$⊢ φ \to +∞ \div_{𝑒} B = +∞$
19	16 18	sylan9eqr	$⊢ (φ \land A = +∞) \to A \div_{𝑒} B = +∞$
20	8	3o3cs	$⊢ A \div_{𝑒} B = +∞ \to A \div_{𝑒} B \in [0, +∞]$
21	19 20	syl	$⊢ (φ \land A = +∞) \to A \div_{𝑒} B \in [0, +∞]$
22		elxrge02	$⊢ A \in [0, +∞] \leftrightarrow (A = 0 \lor A \in ℝ^{+} \lor A = +∞)$
23	1 22	sylib	$⊢ φ \to (A = 0 \lor A \in ℝ^{+} \lor A = +∞)$
24	10 15 21 23	mpjao3dan	$⊢ φ \to A \div_{𝑒} B \in [0, +∞]$

Metamath Proof Explorer

Theorem xrpxdivcld

Proof