xsubge0 - Intuitionistic Logic Explorer

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

Theorem xsubge0 10301

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

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

**Proof of Theorem xsubge0**
Step	Hyp	Ref	Expression
1		elxr 10196	. 2 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
2		0xr 8379	. . . . 5 ⊢ 0 ∈ ℝ^*
3		rexr 8378	. . . . . 6 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
4		xnegcl 10252	. . . . . . 7 ⊢ (𝐵 ∈ ℝ^* → -_e𝐵 ∈ ℝ^*)
5		xaddcl 10280	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ -_e𝐵 ∈ ℝ^) → (𝐴 +_e -_e𝐵) ∈ ℝ^)
6	4, 5	sylan2 286	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐴 +_e -_e𝐵) ∈ ℝ^)
7	3, 6	sylan2 286	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐴 +_e -_e𝐵) ∈ ℝ^*)
8		simpr 110	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
9		xleadd1 10295	. . . . 5 ⊢ ((0 ∈ ℝ^* ∧ (𝐴 +_e -_e𝐵) ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 +_e -_e𝐵) ↔ (0 +_e 𝐵) ≤ ((𝐴 +_e -_e𝐵) +_e 𝐵)))
10	2, 7, 8, 9	mp3an2i 1383	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 +_e -_e𝐵) ↔ (0 +_e 𝐵) ≤ ((𝐴 +_e -_e𝐵) +_e 𝐵)))
11	3	adantl 277	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ^*)
12		xaddid2 10283	. . . . . 6 ⊢ (𝐵 ∈ ℝ^* → (0 +_e 𝐵) = 𝐵)
13	11, 12	syl 14	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (0 +_e 𝐵) = 𝐵)
14		xnpcan 10292	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → ((𝐴 +_e -_e𝐵) +_e 𝐵) = 𝐴)
15	13, 14	breq12d 4144	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → ((0 +_e 𝐵) ≤ ((𝐴 +_e -_e𝐵) +_e 𝐵) ↔ 𝐵 ≤ 𝐴))
16	10, 15	bitrd 188	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 +_e -_e𝐵) ↔ 𝐵 ≤ 𝐴))
17		pnfxr 8385	. . . . . . 7 ⊢ +∞ ∈ ℝ^*
18		xrletri3 10224	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (𝐴 = +∞ ↔ (𝐴 ≤ +∞ ∧ +∞ ≤ 𝐴)))
19	17, 18	mpan2 429	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → (𝐴 = +∞ ↔ (𝐴 ≤ +∞ ∧ +∞ ≤ 𝐴)))
20		rexr 8378	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
21		renepnf 8380	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
22		xaddmnf1 10268	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ +∞) → (𝐴 +_e -∞) = -∞)
23	20, 21, 22	syl2anc 415	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → (𝐴 +_e -∞) = -∞)
24		mnflt0 10204	. . . . . . . . . . . . 13 ⊢ -∞ < 0
25		mnfxr 8389	. . . . . . . . . . . . . . 15 ⊢ -∞ ∈ ℝ^*
26		xrlenlt 8397	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ^* ∧ -∞ ∈ ℝ^*) → (0 ≤ -∞ ↔ ¬ -∞ < 0))
27	2, 25, 26	mp2an 430	. . . . . . . . . . . . . 14 ⊢ (0 ≤ -∞ ↔ ¬ -∞ < 0)
28	27	biimpi 120	. . . . . . . . . . . . 13 ⊢ (0 ≤ -∞ → ¬ -∞ < 0)
29	24, 28	mt2 649	. . . . . . . . . . . 12 ⊢ ¬ 0 ≤ -∞
30		breq2 4135	. . . . . . . . . . . 12 ⊢ ((𝐴 +_e -∞) = -∞ → (0 ≤ (𝐴 +_e -∞) ↔ 0 ≤ -∞))
31	29, 30	mtbiri 686	. . . . . . . . . . 11 ⊢ ((𝐴 +_e -∞) = -∞ → ¬ 0 ≤ (𝐴 +_e -∞))
32	31	pm2.21d 628	. . . . . . . . . 10 ⊢ ((𝐴 +_e -∞) = -∞ → (0 ≤ (𝐴 +_e -∞) → 𝐴 = +∞))
33	23, 32	syl 14	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → (0 ≤ (𝐴 +_e -∞) → 𝐴 = +∞))
34	33	adantl 277	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ∈ ℝ) → (0 ≤ (𝐴 +_e -∞) → 𝐴 = +∞))
35		simpr 110	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 = +∞) → 𝐴 = +∞)
36	35	a1d 22	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 = +∞) → (0 ≤ (𝐴 +_e -∞) → 𝐴 = +∞))
37		eleq1 2301	. . . . . . . . . . . 12 ⊢ (𝐴 = -∞ → (𝐴 ∈ ℝ^* ↔ -∞ ∈ ℝ^*))
38	25, 37	mpbiri 168	. . . . . . . . . . 11 ⊢ (𝐴 = -∞ → 𝐴 ∈ ℝ^*)
39		mnfnepnf 8388	. . . . . . . . . . . 12 ⊢ -∞ ≠ +∞
40		neeq1 2433	. . . . . . . . . . . 12 ⊢ (𝐴 = -∞ → (𝐴 ≠ +∞ ↔ -∞ ≠ +∞))
41	39, 40	mpbiri 168	. . . . . . . . . . 11 ⊢ (𝐴 = -∞ → 𝐴 ≠ +∞)
42	38, 41, 22	syl2anc 415	. . . . . . . . . 10 ⊢ (𝐴 = -∞ → (𝐴 +_e -∞) = -∞)
43	42, 32	syl 14	. . . . . . . . 9 ⊢ (𝐴 = -∞ → (0 ≤ (𝐴 +_e -∞) → 𝐴 = +∞))
44	43	adantl 277	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 = -∞) → (0 ≤ (𝐴 +_e -∞) → 𝐴 = +∞))
45		elxr 10196	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
46	45	biimpi 120	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ^* → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
47	34, 36, 44, 46	mpjao3dan 1348	. . . . . . 7 ⊢ (𝐴 ∈ ℝ^* → (0 ≤ (𝐴 +_e -∞) → 𝐴 = +∞))
48		0le0 9403	. . . . . . . 8 ⊢ 0 ≤ 0
49		oveq1 6095	. . . . . . . . 9 ⊢ (𝐴 = +∞ → (𝐴 +_e -∞) = (+∞ +_e -∞))
50		pnfaddmnf 10270	. . . . . . . . 9 ⊢ (+∞ +_e -∞) = 0
51	49, 50	eqtrdi 2287	. . . . . . . 8 ⊢ (𝐴 = +∞ → (𝐴 +_e -∞) = 0)
52	48, 51	breqtrrid 4169	. . . . . . 7 ⊢ (𝐴 = +∞ → 0 ≤ (𝐴 +_e -∞))
53	47, 52	impbid1 142	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → (0 ≤ (𝐴 +_e -∞) ↔ 𝐴 = +∞))
54		pnfge 10209	. . . . . . 7 ⊢ (𝐴 ∈ ℝ^* → 𝐴 ≤ +∞)
55	54	biantrurd 305	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → (+∞ ≤ 𝐴 ↔ (𝐴 ≤ +∞ ∧ +∞ ≤ 𝐴)))
56	19, 53, 55	3bitr4d 220	. . . . 5 ⊢ (𝐴 ∈ ℝ^* → (0 ≤ (𝐴 +_e -∞) ↔ +∞ ≤ 𝐴))
57	56	adantr 276	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → (0 ≤ (𝐴 +_e -∞) ↔ +∞ ≤ 𝐴))
58		xnegeq 10247	. . . . . . . 8 ⊢ (𝐵 = +∞ → -_e𝐵 = -_e+∞)
59		xnegpnf 10248	. . . . . . . 8 ⊢ -_e+∞ = -∞
60	58, 59	eqtrdi 2287	. . . . . . 7 ⊢ (𝐵 = +∞ → -_e𝐵 = -∞)
61	60	adantl 277	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → -_e𝐵 = -∞)
62	61	oveq2d 6104	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → (𝐴 +_e -_e𝐵) = (𝐴 +_e -∞))
63	62	breq2d 4143	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → (0 ≤ (𝐴 +_e -_e𝐵) ↔ 0 ≤ (𝐴 +_e -∞)))
64		breq1 4134	. . . . 5 ⊢ (𝐵 = +∞ → (𝐵 ≤ 𝐴 ↔ +∞ ≤ 𝐴))
65	64	adantl 277	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → (𝐵 ≤ 𝐴 ↔ +∞ ≤ 𝐴))
66	57, 63, 65	3bitr4d 220	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → (0 ≤ (𝐴 +_e -_e𝐵) ↔ 𝐵 ≤ 𝐴))
67		oveq1 6095	. . . . . . . . . 10 ⊢ (𝐴 = -∞ → (𝐴 +_e +∞) = (-∞ +_e +∞))
68		mnfaddpnf 10271	. . . . . . . . . 10 ⊢ (-∞ +_e +∞) = 0
69	67, 68	eqtrdi 2287	. . . . . . . . 9 ⊢ (𝐴 = -∞ → (𝐴 +_e +∞) = 0)
70	69	adantl 277	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 = -∞) → (𝐴 +_e +∞) = 0)
71	48, 70	breqtrrid 4169	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 = -∞) → 0 ≤ (𝐴 +_e +∞))
72		df-ne 2421	. . . . . . . 8 ⊢ (𝐴 ≠ -∞ ↔ ¬ 𝐴 = -∞)
73		0lepnf 10210	. . . . . . . . 9 ⊢ 0 ≤ +∞
74		xaddpnf1 10266	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞) → (𝐴 +_e +∞) = +∞)
75	73, 74	breqtrrid 4169	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞) → 0 ≤ (𝐴 +_e +∞))
76	72, 75	sylan2br 288	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ ¬ 𝐴 = -∞) → 0 ≤ (𝐴 +_e +∞))
77		xrmnfdc 10263	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ^* → DECID 𝐴 = -∞)
78		exmiddc 848	. . . . . . . 8 ⊢ (DECID 𝐴 = -∞ → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
79	77, 78	syl 14	. . . . . . 7 ⊢ (𝐴 ∈ ℝ^* → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
80	71, 76, 79	mpjaodan 810	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → 0 ≤ (𝐴 +_e +∞))
81		mnfle 10212	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → -∞ ≤ 𝐴)
82	80, 81	2thd 175	. . . . 5 ⊢ (𝐴 ∈ ℝ^* → (0 ≤ (𝐴 +_e +∞) ↔ -∞ ≤ 𝐴))
83	82	adantr 276	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (0 ≤ (𝐴 +_e +∞) ↔ -∞ ≤ 𝐴))
84		xnegeq 10247	. . . . . . . 8 ⊢ (𝐵 = -∞ → -_e𝐵 = -_e-∞)
85		xnegmnf 10249	. . . . . . . 8 ⊢ -_e-∞ = +∞
86	84, 85	eqtrdi 2287	. . . . . . 7 ⊢ (𝐵 = -∞ → -_e𝐵 = +∞)
87	86	adantl 277	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → -_e𝐵 = +∞)
88	87	oveq2d 6104	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐴 +_e -_e𝐵) = (𝐴 +_e +∞))
89	88	breq2d 4143	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (0 ≤ (𝐴 +_e -_e𝐵) ↔ 0 ≤ (𝐴 +_e +∞)))
90		breq1 4134	. . . . 5 ⊢ (𝐵 = -∞ → (𝐵 ≤ 𝐴 ↔ -∞ ≤ 𝐴))
91	90	adantl 277	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐵 ≤ 𝐴 ↔ -∞ ≤ 𝐴))
92	83, 89, 91	3bitr4d 220	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (0 ≤ (𝐴 +_e -_e𝐵) ↔ 𝐵 ≤ 𝐴))
93	16, 66, 92	3jaodan 1347	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (0 ≤ (𝐴 +_e -_e𝐵) ↔ 𝐵 ≤ 𝐴))
94	1, 93	sylan2b 287	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (0 ≤ (𝐴 +_e -_e𝐵) ↔ 𝐵 ≤ 𝐴))

Colors of variables: wff set class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 DECID wdc 846 ∨ w3o 1008 = wceq 1402 ∈ wcel 2209 ≠ wne 2420 class class class wbr 4131 (class class class)co 6088 ℝcr 8185 0cc0 8186 +∞cpnf 8364 -∞cmnf 8365 ℝ^*cxr 8366 < clt 8367 ≤ cle 8368 -_ecxne 10189 +_e cxad 10190

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-sep 4251 ax-pow 4313 ax-pr 4348 ax-un 4580 ax-setind 4686 ax-cnex 8277 ax-resscn 8278 ax-1cn 8279 ax-1re 8280 ax-icn 8281 ax-addcl 8282 ax-addrcl 8283 ax-mulcl 8284 ax-addcom 8286 ax-addass 8288 ax-distr 8290 ax-i2m1 8291 ax-0id 8294 ax-rnegex 8295 ax-cnre 8297 ax-pre-ltirr 8298 ax-pre-apti 8301 ax-pre-ltadd 8302

This proof depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-iun 4014 df-br 4132 df-opab 4194 df-mpt 4195 df-id 4440 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-res 4788 df-ima 4789 df-iota 5340 df-fun 5382 df-fn 5383 df-f 5384 df-fv 5388 df-riota 6041 df-ov 6091 df-oprab 6092 df-mpo 6093 df-1st 6378 df-2nd 6379 df-pnf 8369 df-mnf 8370 df-xr 8371 df-ltxr 8372 df-le 8373 df-sub 8507 df-neg 8508 df-xneg 10192 df-xadd 10193

This theorem is used by: ssblps 15663 ssbl 15664

W3C validator