xsubge0 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > xsubge0		GIF version

Theorem xsubge0 9505

Description: Extended real version of subge0 8104. (Contributed by Mario Carneiro, 24-Aug-2015.)

**Assertion**
Ref	Expression
xsubge0	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ 𝐵 ≤ 𝐴))

**Proof of Theorem xsubge0**
Step	Hyp	Ref	Expression
1		elxr 9404	. 2 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
2		0xr 7684	. . . . 5 ⊢ 0 ∈ ℝ^*
3		rexr 7683	. . . . . 6 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
4		xnegcl 9456	. . . . . . 7 ⊢ (𝐵 ∈ ℝ^* → -_𝑒𝐵 ∈ ℝ^*)
5		xaddcl 9484	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ -_𝑒𝐵 ∈ ℝ^) → (𝐴 +_𝑒 -_𝑒𝐵) ∈ ℝ^)
6	4, 5	sylan2 282	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐴 +_𝑒 -_𝑒𝐵) ∈ ℝ^)
7	3, 6	sylan2 282	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐴 +_𝑒 -_𝑒𝐵) ∈ ℝ^*)
8		simpr 109	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
9		xleadd1 9499	. . . . 5 ⊢ ((0 ∈ ℝ^* ∧ (𝐴 +_𝑒 -_𝑒𝐵) ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ (0 +_𝑒 𝐵) ≤ ((𝐴 +_𝑒 -_𝑒𝐵) +_𝑒 𝐵)))
10	2, 7, 8, 9	mp3an2i 1288	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ (0 +_𝑒 𝐵) ≤ ((𝐴 +_𝑒 -_𝑒𝐵) +_𝑒 𝐵)))
11	3	adantl 273	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ^*)
12		xaddid2 9487	. . . . . 6 ⊢ (𝐵 ∈ ℝ^* → (0 +_𝑒 𝐵) = 𝐵)
13	11, 12	syl 14	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (0 +_𝑒 𝐵) = 𝐵)
14		xnpcan 9496	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → ((𝐴 +_𝑒 -_𝑒𝐵) +_𝑒 𝐵) = 𝐴)
15	13, 14	breq12d 3888	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → ((0 +_𝑒 𝐵) ≤ ((𝐴 +_𝑒 -_𝑒𝐵) +_𝑒 𝐵) ↔ 𝐵 ≤ 𝐴))
16	10, 15	bitrd 187	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ 𝐵 ≤ 𝐴))
17		pnfxr 7690	. . . . . . 7 ⊢ +∞ ∈ ℝ^*
18		xrletri3 9429	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (𝐴 = +∞ ↔ (𝐴 ≤ +∞ ∧ +∞ ≤ 𝐴)))
19	17, 18	mpan2 419	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → (𝐴 = +∞ ↔ (𝐴 ≤ +∞ ∧ +∞ ≤ 𝐴)))
20		rexr 7683	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
21		renepnf 7685	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
22		xaddmnf1 9472	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ +∞) → (𝐴 +_𝑒 -∞) = -∞)
23	20, 21, 22	syl2anc 406	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → (𝐴 +_𝑒 -∞) = -∞)
24		mnflt0 9411	. . . . . . . . . . . . 13 ⊢ -∞ < 0
25		mnfxr 7694	. . . . . . . . . . . . . . 15 ⊢ -∞ ∈ ℝ^*
26		xrlenlt 7701	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ^* ∧ -∞ ∈ ℝ^*) → (0 ≤ -∞ ↔ ¬ -∞ < 0))
27	2, 25, 26	mp2an 420	. . . . . . . . . . . . . 14 ⊢ (0 ≤ -∞ ↔ ¬ -∞ < 0)
28	27	biimpi 119	. . . . . . . . . . . . 13 ⊢ (0 ≤ -∞ → ¬ -∞ < 0)
29	24, 28	mt2 609	. . . . . . . . . . . 12 ⊢ ¬ 0 ≤ -∞
30		breq2 3879	. . . . . . . . . . . 12 ⊢ ((𝐴 +_𝑒 -∞) = -∞ → (0 ≤ (𝐴 +_𝑒 -∞) ↔ 0 ≤ -∞))
31	29, 30	mtbiri 641	. . . . . . . . . . 11 ⊢ ((𝐴 +_𝑒 -∞) = -∞ → ¬ 0 ≤ (𝐴 +_𝑒 -∞))
32	31	pm2.21d 589	. . . . . . . . . 10 ⊢ ((𝐴 +_𝑒 -∞) = -∞ → (0 ≤ (𝐴 +_𝑒 -∞) → 𝐴 = +∞))
33	23, 32	syl 14	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → (0 ≤ (𝐴 +_𝑒 -∞) → 𝐴 = +∞))
34	33	adantl 273	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ∈ ℝ) → (0 ≤ (𝐴 +_𝑒 -∞) → 𝐴 = +∞))
35		simpr 109	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 = +∞) → 𝐴 = +∞)
36	35	a1d 22	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 = +∞) → (0 ≤ (𝐴 +_𝑒 -∞) → 𝐴 = +∞))
37		eleq1 2162	. . . . . . . . . . . 12 ⊢ (𝐴 = -∞ → (𝐴 ∈ ℝ^* ↔ -∞ ∈ ℝ^*))
38	25, 37	mpbiri 167	. . . . . . . . . . 11 ⊢ (𝐴 = -∞ → 𝐴 ∈ ℝ^*)
39		mnfnepnf 7693	. . . . . . . . . . . 12 ⊢ -∞ ≠ +∞
40		neeq1 2280	. . . . . . . . . . . 12 ⊢ (𝐴 = -∞ → (𝐴 ≠ +∞ ↔ -∞ ≠ +∞))
41	39, 40	mpbiri 167	. . . . . . . . . . 11 ⊢ (𝐴 = -∞ → 𝐴 ≠ +∞)
42	38, 41, 22	syl2anc 406	. . . . . . . . . 10 ⊢ (𝐴 = -∞ → (𝐴 +_𝑒 -∞) = -∞)
43	42, 32	syl 14	. . . . . . . . 9 ⊢ (𝐴 = -∞ → (0 ≤ (𝐴 +_𝑒 -∞) → 𝐴 = +∞))
44	43	adantl 273	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 = -∞) → (0 ≤ (𝐴 +_𝑒 -∞) → 𝐴 = +∞))
45		elxr 9404	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
46	45	biimpi 119	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ^* → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
47	34, 36, 44, 46	mpjao3dan 1253	. . . . . . 7 ⊢ (𝐴 ∈ ℝ^* → (0 ≤ (𝐴 +_𝑒 -∞) → 𝐴 = +∞))
48		0le0 8667	. . . . . . . 8 ⊢ 0 ≤ 0
49		oveq1 5713	. . . . . . . . 9 ⊢ (𝐴 = +∞ → (𝐴 +_𝑒 -∞) = (+∞ +_𝑒 -∞))
50		pnfaddmnf 9474	. . . . . . . . 9 ⊢ (+∞ +_𝑒 -∞) = 0
51	49, 50	syl6eq 2148	. . . . . . . 8 ⊢ (𝐴 = +∞ → (𝐴 +_𝑒 -∞) = 0)
52	48, 51	syl5breqr 3911	. . . . . . 7 ⊢ (𝐴 = +∞ → 0 ≤ (𝐴 +_𝑒 -∞))
53	47, 52	impbid1 141	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → (0 ≤ (𝐴 +_𝑒 -∞) ↔ 𝐴 = +∞))
54		pnfge 9416	. . . . . . 7 ⊢ (𝐴 ∈ ℝ^* → 𝐴 ≤ +∞)
55	54	biantrurd 301	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → (+∞ ≤ 𝐴 ↔ (𝐴 ≤ +∞ ∧ +∞ ≤ 𝐴)))
56	19, 53, 55	3bitr4d 219	. . . . 5 ⊢ (𝐴 ∈ ℝ^* → (0 ≤ (𝐴 +_𝑒 -∞) ↔ +∞ ≤ 𝐴))
57	56	adantr 272	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → (0 ≤ (𝐴 +_𝑒 -∞) ↔ +∞ ≤ 𝐴))
58		xnegeq 9451	. . . . . . . 8 ⊢ (𝐵 = +∞ → -_𝑒𝐵 = -_𝑒+∞)
59		xnegpnf 9452	. . . . . . . 8 ⊢ -_𝑒+∞ = -∞
60	58, 59	syl6eq 2148	. . . . . . 7 ⊢ (𝐵 = +∞ → -_𝑒𝐵 = -∞)
61	60	adantl 273	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → -_𝑒𝐵 = -∞)
62	61	oveq2d 5722	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → (𝐴 +_𝑒 -_𝑒𝐵) = (𝐴 +_𝑒 -∞))
63	62	breq2d 3887	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ 0 ≤ (𝐴 +_𝑒 -∞)))
64		breq1 3878	. . . . 5 ⊢ (𝐵 = +∞ → (𝐵 ≤ 𝐴 ↔ +∞ ≤ 𝐴))
65	64	adantl 273	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → (𝐵 ≤ 𝐴 ↔ +∞ ≤ 𝐴))
66	57, 63, 65	3bitr4d 219	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ 𝐵 ≤ 𝐴))
67		oveq1 5713	. . . . . . . . . 10 ⊢ (𝐴 = -∞ → (𝐴 +_𝑒 +∞) = (-∞ +_𝑒 +∞))
68		mnfaddpnf 9475	. . . . . . . . . 10 ⊢ (-∞ +_𝑒 +∞) = 0
69	67, 68	syl6eq 2148	. . . . . . . . 9 ⊢ (𝐴 = -∞ → (𝐴 +_𝑒 +∞) = 0)
70	69	adantl 273	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 = -∞) → (𝐴 +_𝑒 +∞) = 0)
71	48, 70	syl5breqr 3911	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 = -∞) → 0 ≤ (𝐴 +_𝑒 +∞))
72		df-ne 2268	. . . . . . . 8 ⊢ (𝐴 ≠ -∞ ↔ ¬ 𝐴 = -∞)
73		0lepnf 9417	. . . . . . . . 9 ⊢ 0 ≤ +∞
74		xaddpnf1 9470	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞) → (𝐴 +_𝑒 +∞) = +∞)
75	73, 74	syl5breqr 3911	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞) → 0 ≤ (𝐴 +_𝑒 +∞))
76	72, 75	sylan2br 284	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ ¬ 𝐴 = -∞) → 0 ≤ (𝐴 +_𝑒 +∞))
77		xrmnfdc 9467	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ^* → DECID 𝐴 = -∞)
78		exmiddc 788	. . . . . . . 8 ⊢ (DECID 𝐴 = -∞ → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
79	77, 78	syl 14	. . . . . . 7 ⊢ (𝐴 ∈ ℝ^* → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
80	71, 76, 79	mpjaodan 753	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → 0 ≤ (𝐴 +_𝑒 +∞))
81		mnfle 9419	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → -∞ ≤ 𝐴)
82	80, 81	2thd 174	. . . . 5 ⊢ (𝐴 ∈ ℝ^* → (0 ≤ (𝐴 +_𝑒 +∞) ↔ -∞ ≤ 𝐴))
83	82	adantr 272	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (0 ≤ (𝐴 +_𝑒 +∞) ↔ -∞ ≤ 𝐴))
84		xnegeq 9451	. . . . . . . 8 ⊢ (𝐵 = -∞ → -_𝑒𝐵 = -_𝑒-∞)
85		xnegmnf 9453	. . . . . . . 8 ⊢ -_𝑒-∞ = +∞
86	84, 85	syl6eq 2148	. . . . . . 7 ⊢ (𝐵 = -∞ → -_𝑒𝐵 = +∞)
87	86	adantl 273	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → -_𝑒𝐵 = +∞)
88	87	oveq2d 5722	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐴 +_𝑒 -_𝑒𝐵) = (𝐴 +_𝑒 +∞))
89	88	breq2d 3887	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ 0 ≤ (𝐴 +_𝑒 +∞)))
90		breq1 3878	. . . . 5 ⊢ (𝐵 = -∞ → (𝐵 ≤ 𝐴 ↔ -∞ ≤ 𝐴))
91	90	adantl 273	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐵 ≤ 𝐴 ↔ -∞ ≤ 𝐴))
92	83, 89, 91	3bitr4d 219	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ 𝐵 ≤ 𝐴))
93	16, 66, 92	3jaodan 1252	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ 𝐵 ≤ 𝐴))
94	1, 93	sylan2b 283	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ 𝐵 ≤ 𝐴))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 670 DECID wdc 786 ∨ w3o 929 = 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 < clt 7672 ≤ 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-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-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: ssblps 12353 ssbl 12354

W3C validator