Theorem xlesubadd 12644

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

Assertion

Ref	Expression
xlesubadd	⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵)))

Proof of Theorem xlesubadd

Step	Hyp	Ref	Expression
1		simpl1 1188	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 𝐴 ∈ ℝ*)
2		simpl2 1189	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 𝐵 ∈ ℝ*)
3		xnegcl 12594	. . . . . . 7 ⊢ (𝐵 ∈ ℝ* → -𝑒𝐵 ∈ ℝ*)
4	2, 3	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → -𝑒𝐵 ∈ ℝ*)
5		xaddcl 12620	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ -𝑒𝐵 ∈ ℝ*) → (𝐴 +𝑒 -𝑒𝐵) ∈ ℝ*)
6	1, 4, 5	syl2anc 587	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐴 +𝑒 -𝑒𝐵) ∈ ℝ*)
7	6	adantr 484	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 -𝑒𝐵) ∈ ℝ*)
8		simpll3 1211	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 ∈ ℝ) → 𝐶 ∈ ℝ*)
9		simpr 488	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
10		xleadd1 12636	. . . 4 ⊢ (((𝐴 +𝑒 -𝑒𝐵) ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐵)))
11	7, 8, 9, 10	syl3anc 1368	. . 3 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐵)))
12		xnpcan 12633	. . . . 5 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴)
13	1, 12	sylan 583	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴)
14	13	breq1d 5040	. . 3 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 ∈ ℝ) → (((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐵) ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵)))
15	11, 14	bitrd 282	. 2 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵)))
16		simpr3 1193	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 0 ≤ 𝐶)
17		oveq1 7142	. . . . . . . . 9 ⊢ (𝐴 = +∞ → (𝐴 +𝑒 -∞) = (+∞ +𝑒 -∞))
18		pnfaddmnf 12611	. . . . . . . . 9 ⊢ (+∞ +𝑒 -∞) = 0
19	17, 18	eqtrdi 2849	. . . . . . . 8 ⊢ (𝐴 = +∞ → (𝐴 +𝑒 -∞) = 0)
20	19	breq1d 5040	. . . . . . 7 ⊢ (𝐴 = +∞ → ((𝐴 +𝑒 -∞) ≤ 𝐶 ↔ 0 ≤ 𝐶))
21	16, 20	syl5ibrcom 250	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐴 = +∞ → (𝐴 +𝑒 -∞) ≤ 𝐶))
22		xaddmnf1 12609	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) = -∞)
23	22	ex 416	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≠ +∞ → (𝐴 +𝑒 -∞) = -∞))
24	1, 23	syl 17	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐴 ≠ +∞ → (𝐴 +𝑒 -∞) = -∞))
25		simpl3 1190	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 𝐶 ∈ ℝ*)
26		mnfle 12517	. . . . . . . . 9 ⊢ (𝐶 ∈ ℝ* → -∞ ≤ 𝐶)
27	25, 26	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → -∞ ≤ 𝐶)
28		breq1 5033	. . . . . . . 8 ⊢ ((𝐴 +𝑒 -∞) = -∞ → ((𝐴 +𝑒 -∞) ≤ 𝐶 ↔ -∞ ≤ 𝐶))
29	27, 28	syl5ibrcom 250	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +𝑒 -∞) = -∞ → (𝐴 +𝑒 -∞) ≤ 𝐶))
30	24, 29	syld 47	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐴 ≠ +∞ → (𝐴 +𝑒 -∞) ≤ 𝐶))
31	21, 30	pm2.61dne 3073	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐴 +𝑒 -∞) ≤ 𝐶)
32		pnfge 12513	. . . . . . 7 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)
33	1, 32	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 𝐴 ≤ +∞)
34		ge0nemnf 12554	. . . . . . . 8 ⊢ ((𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶) → 𝐶 ≠ -∞)
35	25, 16, 34	syl2anc 587	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 𝐶 ≠ -∞)
36		xaddpnf1 12607	. . . . . . 7 ⊢ ((𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞) → (𝐶 +𝑒 +∞) = +∞)
37	25, 35, 36	syl2anc 587	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐶 +𝑒 +∞) = +∞)
38	33, 37	breqtrrd 5058	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 𝐴 ≤ (𝐶 +𝑒 +∞))
39	31, 38	2thd 268	. . . 4 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +𝑒 -∞) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 +∞)))
40		xnegeq 12588	. . . . . . . 8 ⊢ (𝐵 = +∞ → -𝑒𝐵 = -𝑒+∞)
41		xnegpnf 12590	. . . . . . . 8 ⊢ -𝑒+∞ = -∞
42	40, 41	eqtrdi 2849	. . . . . . 7 ⊢ (𝐵 = +∞ → -𝑒𝐵 = -∞)
43	42	oveq2d 7151	. . . . . 6 ⊢ (𝐵 = +∞ → (𝐴 +𝑒 -𝑒𝐵) = (𝐴 +𝑒 -∞))
44	43	breq1d 5040	. . . . 5 ⊢ (𝐵 = +∞ → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ (𝐴 +𝑒 -∞) ≤ 𝐶))
45		oveq2 7143	. . . . . 6 ⊢ (𝐵 = +∞ → (𝐶 +𝑒 𝐵) = (𝐶 +𝑒 +∞))
46	45	breq2d 5042	. . . . 5 ⊢ (𝐵 = +∞ → (𝐴 ≤ (𝐶 +𝑒 𝐵) ↔ 𝐴 ≤ (𝐶 +𝑒 +∞)))
47	44, 46	bibi12d 349	. . . 4 ⊢ (𝐵 = +∞ → (((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵)) ↔ ((𝐴 +𝑒 -∞) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 +∞))))
48	39, 47	syl5ibrcom 250	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐵 = +∞ → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵))))
49	48	imp 410	. 2 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 = +∞) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵)))
50		simpr2 1192	. . . 4 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 𝐵 ≠ -∞)
51	2, 50	jca 515	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞))
52		xrnemnf 12500	. . 3 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞))
53	51, 52	sylib 221	. 2 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞))
54	15, 49, 53	mpjaodan 956	1 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987   class class class wbr 5030  (class class class)co 7135  ℝcr 10525  0cc0 10526  +∞cpnf 10661  -∞cmnf 10662  ℝ^*cxr 10663   ≤ cle 10665  -_𝑒cxne 12492   +_𝑒 cxad 12493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-po 5438  df-so 5439  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-1st 7671  df-2nd 7672  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-xneg 12495  df-xadd 12496

This theorem is referenced by:  xmetrtri  22962  metdstri  23456  metdscnlem  23460