xlesubadd

Description: Under certain conditions, the conclusion of lesubadd is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015)

		Ref	Expression
	Assertion	xlesubadd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to (A +_{𝑒} (- B) \leq C \leftrightarrow A \leq C +_{𝑒} B)$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to A \in ℝ^{}$
2		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to B \in ℝ^{}$
3		xnegcl	$⊢ B \in ℝ^{} \to - B \in ℝ^{}$
4	2 3	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to - B \in ℝ^{}$
5		xaddcl	$⊢ (A \in ℝ^{} \land - B \in ℝ^{}) \to A +_{𝑒} (- B) \in ℝ^{*}$
6	1 4 5	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to A +_{𝑒} (- B) \in ℝ^{}$
7	6	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \land B \in ℝ) \to A +_{𝑒} (- B) \in ℝ^{}$
8		simpll3	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \land B \in ℝ) \to C \in ℝ^{}$
9		simpr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \land B \in ℝ) \to B \in ℝ$
10		xleadd1	$⊢ (A +_{𝑒} (- B) \in ℝ^{} \land C \in ℝ^{} \land B \in ℝ) \to (A +_{𝑒} (- B) \leq C \leftrightarrow (A +_{𝑒} (- B)) +_{𝑒} B \leq C +_{𝑒} B)$
11	7 8 9 10	syl3anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \land B \in ℝ) \to (A +_{𝑒} (- B) \leq C \leftrightarrow (A +_{𝑒} (- B)) +_{𝑒} B \leq C +_{𝑒} B)$
12		xnpcan	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A +_{𝑒} (- B)) +_{𝑒} B = A$
13	1 12	sylan	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \land B \in ℝ) \to (A +_{𝑒} (- B)) +_{𝑒} B = A$
14	13	breq1d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \land B \in ℝ) \to ((A +_{𝑒} (- B)) +_{𝑒} B \leq C +_{𝑒} B \leftrightarrow A \leq C +_{𝑒} B)$
15	11 14	bitrd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \land B \in ℝ) \to (A +_{𝑒} (- B) \leq C \leftrightarrow A \leq C +_{𝑒} B)$
16		simpr3	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to 0 \leq C$
17		oveq1	$⊢ A = +∞ \to A +_{𝑒} −∞ = +∞ +_{𝑒} −∞$
18		pnfaddmnf	$⊢ +∞ +_{𝑒} −∞ = 0$
19	17 18	syl6eq	$⊢ A = +∞ \to A +_{𝑒} −∞ = 0$
20	19	breq1d	$⊢ A = +∞ \to (A +_{𝑒} −∞ \leq C \leftrightarrow 0 \leq C)$
21	16 20	syl5ibrcom	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to (A = +∞ \to A +_{𝑒} −∞ \leq C)$
22		xaddmnf1	$⊢ (A \in ℝ^{*} \land A \neq +∞) \to A +_{𝑒} −∞ = −∞$
23	22	ex	$⊢ A \in ℝ^{*} \to (A \neq +∞ \to A +_{𝑒} −∞ = −∞)$
24	1 23	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to (A \neq +∞ \to A +_{𝑒} −∞ = −∞)$
25		simpl3	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to C \in ℝ^{}$
26		mnfle	$⊢ C \in ℝ^{*} \to −∞ \leq C$
27	25 26	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to −∞ \leq C$
28		breq1	$⊢ A +_{𝑒} −∞ = −∞ \to (A +_{𝑒} −∞ \leq C \leftrightarrow −∞ \leq C)$
29	27 28	syl5ibrcom	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to (A +_{𝑒} −∞ = −∞ \to A +_{𝑒} −∞ \leq C)$
30	24 29	syld	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to (A \neq +∞ \to A +_{𝑒} −∞ \leq C)$
31	21 30	pm2.61dne	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to A +_{𝑒} −∞ \leq C$
32		pnfge	$⊢ A \in ℝ^{*} \to A \leq +∞$
33	1 32	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to A \leq +∞$
34		ge0nemnf	$⊢ (C \in ℝ^{*} \land 0 \leq C) \to C \neq −∞$
35	25 16 34	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to C \neq −∞$
36		xaddpnf1	$⊢ (C \in ℝ^{*} \land C \neq −∞) \to C +_{𝑒} +∞ = +∞$
37	25 35 36	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to C +_{𝑒} +∞ = +∞$
38	33 37	breqtrrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to A \leq C +_{𝑒} +∞$
39	31 38	2thd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to (A +_{𝑒} −∞ \leq C \leftrightarrow A \leq C +_{𝑒} +∞)$
40		xnegeq	$⊢ B = +∞ \to - B = - +∞$
41		xnegpnf	$⊢ - +∞ = −∞$
42	40 41	syl6eq	$⊢ B = +∞ \to - B = −∞$
43	42	oveq2d	$⊢ B = +∞ \to A +_{𝑒} (- B) = A +_{𝑒} −∞$
44	43	breq1d	$⊢ B = +∞ \to (A +_{𝑒} (- B) \leq C \leftrightarrow A +_{𝑒} −∞ \leq C)$
45		oveq2	$⊢ B = +∞ \to C +_{𝑒} B = C +_{𝑒} +∞$
46	45	breq2d	$⊢ B = +∞ \to (A \leq C +_{𝑒} B \leftrightarrow A \leq C +_{𝑒} +∞)$
47	44 46	bibi12d	$⊢ B = +∞ \to ((A +_{𝑒} (- B) \leq C \leftrightarrow A \leq C +_{𝑒} B) \leftrightarrow (A +_{𝑒} −∞ \leq C \leftrightarrow A \leq C +_{𝑒} +∞))$
48	39 47	syl5ibrcom	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to (B = +∞ \to (A +_{𝑒} (- B) \leq C \leftrightarrow A \leq C +_{𝑒} B))$
49	48	imp	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \land B = +∞) \to (A +_{𝑒} (- B) \leq C \leftrightarrow A \leq C +_{𝑒} B)$
50		simpr2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to B \neq −∞$
51	2 50	jca	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to (B \in ℝ^{} \land B \neq −∞)$
52		xrnemnf	$⊢ (B \in ℝ^{*} \land B \neq −∞) \leftrightarrow (B \in ℝ \lor B = +∞)$
53	51 52	sylib	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to (B \in ℝ \lor B = +∞)$
54	15 49 53	mpjaodan	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (0 \leq A \land B \neq −∞ \land 0 \leq C)) \to (A +_{𝑒} (- B) \leq C \leftrightarrow A \leq C +_{𝑒} B)$

Metamath Proof Explorer

Theorem xlesubadd

Proof