Theorem xlesubadd 9507

Description: Under certain conditions, the conclusion of lesubadd 8063 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 952	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 𝐴 ∈ ℝ*)
2		simpl2 953	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 𝐵 ∈ ℝ*)
3	2	xnegcld 9479	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → -𝑒𝐵 ∈ ℝ*)
4		xaddcl 9484	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ -𝑒𝐵 ∈ ℝ*) → (𝐴 +𝑒 -𝑒𝐵) ∈ ℝ*)
5	1, 3, 4	syl2anc 406	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐴 +𝑒 -𝑒𝐵) ∈ ℝ*)
6	5	adantr 272	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 -𝑒𝐵) ∈ ℝ*)
7		simpll3 990	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 ∈ ℝ) → 𝐶 ∈ ℝ*)
8		simpr 109	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
9		xleadd1 9499	. . . 4 ⊢ (((𝐴 +𝑒 -𝑒𝐵) ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐵)))
10	6, 7, 8, 9	syl3anc 1184	. . 3 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐵)))
11		xnpcan 9496	. . . . 5 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴)
12	1, 11	sylan 279	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴)
13	12	breq1d 3885	. . 3 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 ∈ ℝ) → (((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐵) ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵)))
14	10, 13	bitrd 187	. 2 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵)))
15		simpr3 957	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 0 ≤ 𝐶)
16		oveq1 5713	. . . . . . . . 9 ⊢ (𝐴 = +∞ → (𝐴 +𝑒 -∞) = (+∞ +𝑒 -∞))
17		pnfaddmnf 9474	. . . . . . . . 9 ⊢ (+∞ +𝑒 -∞) = 0
18	16, 17	syl6eq 2148	. . . . . . . 8 ⊢ (𝐴 = +∞ → (𝐴 +𝑒 -∞) = 0)
19	18	breq1d 3885	. . . . . . 7 ⊢ (𝐴 = +∞ → ((𝐴 +𝑒 -∞) ≤ 𝐶 ↔ 0 ≤ 𝐶))
20	15, 19	syl5ibrcom 156	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐴 = +∞ → (𝐴 +𝑒 -∞) ≤ 𝐶))
21		xaddmnf1 9472	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) = -∞)
22	21	ex 114	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≠ +∞ → (𝐴 +𝑒 -∞) = -∞))
23	1, 22	syl 14	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐴 ≠ +∞ → (𝐴 +𝑒 -∞) = -∞))
24		simpl3 954	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 𝐶 ∈ ℝ*)
25		mnfle 9419	. . . . . . . . 9 ⊢ (𝐶 ∈ ℝ* → -∞ ≤ 𝐶)
26	24, 25	syl 14	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → -∞ ≤ 𝐶)
27		breq1 3878	. . . . . . . 8 ⊢ ((𝐴 +𝑒 -∞) = -∞ → ((𝐴 +𝑒 -∞) ≤ 𝐶 ↔ -∞ ≤ 𝐶))
28	26, 27	syl5ibrcom 156	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +𝑒 -∞) = -∞ → (𝐴 +𝑒 -∞) ≤ 𝐶))
29	23, 28	syld 45	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐴 ≠ +∞ → (𝐴 +𝑒 -∞) ≤ 𝐶))
30		xrpnfdc 9466	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ* → DECID 𝐴 = +∞)
31		dcne 2278	. . . . . . . 8 ⊢ (DECID 𝐴 = +∞ ↔ (𝐴 = +∞ ∨ 𝐴 ≠ +∞))
32	30, 31	sylib 121	. . . . . . 7 ⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ∨ 𝐴 ≠ +∞))
33	1, 32	syl 14	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐴 = +∞ ∨ 𝐴 ≠ +∞))
34	20, 29, 33	mpjaod 679	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐴 +𝑒 -∞) ≤ 𝐶)
35		pnfge 9416	. . . . . . 7 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)
36	1, 35	syl 14	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 𝐴 ≤ +∞)
37		ge0nemnf 9448	. . . . . . . 8 ⊢ ((𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶) → 𝐶 ≠ -∞)
38	24, 15, 37	syl2anc 406	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 𝐶 ≠ -∞)
39		xaddpnf1 9470	. . . . . . 7 ⊢ ((𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞) → (𝐶 +𝑒 +∞) = +∞)
40	24, 38, 39	syl2anc 406	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐶 +𝑒 +∞) = +∞)
41	36, 40	breqtrrd 3901	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 𝐴 ≤ (𝐶 +𝑒 +∞))
42	34, 41	2thd 174	. . . 4 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +𝑒 -∞) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 +∞)))
43		xnegeq 9451	. . . . . . . 8 ⊢ (𝐵 = +∞ → -𝑒𝐵 = -𝑒+∞)
44		xnegpnf 9452	. . . . . . . 8 ⊢ -𝑒+∞ = -∞
45	43, 44	syl6eq 2148	. . . . . . 7 ⊢ (𝐵 = +∞ → -𝑒𝐵 = -∞)
46	45	oveq2d 5722	. . . . . 6 ⊢ (𝐵 = +∞ → (𝐴 +𝑒 -𝑒𝐵) = (𝐴 +𝑒 -∞))
47	46	breq1d 3885	. . . . 5 ⊢ (𝐵 = +∞ → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ (𝐴 +𝑒 -∞) ≤ 𝐶))
48		oveq2 5714	. . . . . 6 ⊢ (𝐵 = +∞ → (𝐶 +𝑒 𝐵) = (𝐶 +𝑒 +∞))
49	48	breq2d 3887	. . . . 5 ⊢ (𝐵 = +∞ → (𝐴 ≤ (𝐶 +𝑒 𝐵) ↔ 𝐴 ≤ (𝐶 +𝑒 +∞)))
50	47, 49	bibi12d 234	. . . 4 ⊢ (𝐵 = +∞ → (((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵)) ↔ ((𝐴 +𝑒 -∞) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 +∞))))
51	42, 50	syl5ibrcom 156	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐵 = +∞ → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵))))
52	51	imp 123	. 2 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) ∧ 𝐵 = +∞) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵)))
53		simpr2 956	. . . 4 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → 𝐵 ≠ -∞)
54	2, 53	jca 302	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞))
55		xrnemnf 9405	. . 3 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞))
56	54, 55	sylib 121	. 2 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞))
57	14, 52, 56	mpjaodan 753	1 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 670  DECID wdc 786   ∧ w3a 930   = wceq 1299   ∈ wcel 1448   ≠ wne 2267   class class class wbr 3875  (class class class)co 5706  ℝcr 7499  0cc0 7500  +∞cpnf 7669  -∞cmnf 7670  ℝ^*cxr 7671   ≤ cle 7673  -_𝑒cxne 9397   +_𝑒 cxad 9398

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-pr 4069  ax-un 4293  ax-setind 4390  ax-cnex 7586  ax-resscn 7587  ax-1cn 7588  ax-1re 7589  ax-icn 7590  ax-addcl 7591  ax-addrcl 7592  ax-mulcl 7593  ax-addcom 7595  ax-addass 7597  ax-distr 7599  ax-i2m1 7600  ax-0id 7603  ax-rnegex 7604  ax-cnre 7606  ax-pre-ltirr 7607  ax-pre-ltwlin 7608  ax-pre-lttrn 7609  ax-pre-apti 7610  ax-pre-ltadd 7611

This theorem depends on definitions:  df-bi 116  df-dc 787  df-3or 931  df-3an 932  df-tru 1302  df-fal 1305  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ne 2268  df-nel 2363  df-ral 2380  df-rex 2381  df-reu 2382  df-rab 2384  df-v 2643  df-sbc 2863  df-csb 2956  df-dif 3023  df-un 3025  df-in 3027  df-ss 3034  df-if 3422  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-iun 3762  df-br 3876  df-opab 3930  df-mpt 3931  df-id 4153  df-po 4156  df-iso 4157  df-xp 4483  df-rel 4484  df-cnv 4485  df-co 4486  df-dm 4487  df-rn 4488  df-res 4489  df-ima 4490  df-iota 5024  df-fun 5061  df-fn 5062  df-f 5063  df-fv 5067  df-riota 5662  df-ov 5709  df-oprab 5710  df-mpo 5711  df-1st 5969  df-2nd 5970  df-pnf 7674  df-mnf 7675  df-xr 7676  df-ltxr 7677  df-le 7678  df-sub 7806  df-neg 7807  df-xneg 9400  df-xadd 9401

This theorem is referenced by:  xmetrtri  12304