xsubge0 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > xsubge0		Structured version Visualization version GIF version

Theorem xsubge0 12289

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

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

**Proof of Theorem xsubge0**
Step	Hyp	Ref	Expression
1		elxr 12148	. 2 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
2		0xr 10286	. . . . . 6 ⊢ 0 ∈ ℝ^*
3	2	a1i 11	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → 0 ∈ ℝ^*)
4		rexr 10285	. . . . . 6 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
5		xnegcl 12242	. . . . . . 7 ⊢ (𝐵 ∈ ℝ^* → -_𝑒𝐵 ∈ ℝ^*)
6		xaddcl 12268	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ -_𝑒𝐵 ∈ ℝ^) → (𝐴 +_𝑒 -_𝑒𝐵) ∈ ℝ^)
7	5, 6	sylan2 580	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐴 +_𝑒 -_𝑒𝐵) ∈ ℝ^)
8	4, 7	sylan2 580	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐴 +_𝑒 -_𝑒𝐵) ∈ ℝ^*)
9		simpr 471	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
10		xleadd1 12283	. . . . 5 ⊢ ((0 ∈ ℝ^* ∧ (𝐴 +_𝑒 -_𝑒𝐵) ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ (0 +_𝑒 𝐵) ≤ ((𝐴 +_𝑒 -_𝑒𝐵) +_𝑒 𝐵)))
11	3, 8, 9, 10	syl3anc 1476	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ (0 +_𝑒 𝐵) ≤ ((𝐴 +_𝑒 -_𝑒𝐵) +_𝑒 𝐵)))
12	4	adantl 467	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ^*)
13		xaddid2 12271	. . . . . 6 ⊢ (𝐵 ∈ ℝ^* → (0 +_𝑒 𝐵) = 𝐵)
14	12, 13	syl 17	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (0 +_𝑒 𝐵) = 𝐵)
15		xnpcan 12280	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → ((𝐴 +_𝑒 -_𝑒𝐵) +_𝑒 𝐵) = 𝐴)
16	14, 15	breq12d 4799	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → ((0 +_𝑒 𝐵) ≤ ((𝐴 +_𝑒 -_𝑒𝐵) +_𝑒 𝐵) ↔ 𝐵 ≤ 𝐴))
17	11, 16	bitrd 268	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ 𝐵 ≤ 𝐴))
18		pnfxr 10292	. . . . . . 7 ⊢ +∞ ∈ ℝ^*
19		xrletri3 12183	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (𝐴 = +∞ ↔ (𝐴 ≤ +∞ ∧ +∞ ≤ 𝐴)))
20	18, 19	mpan2 671	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → (𝐴 = +∞ ↔ (𝐴 ≤ +∞ ∧ +∞ ≤ 𝐴)))
21		mnflt0 12157	. . . . . . . . . . 11 ⊢ -∞ < 0
22		mnfxr 10296	. . . . . . . . . . . 12 ⊢ -∞ ∈ ℝ^*
23		xrltnle 10305	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^*) → (-∞ < 0 ↔ ¬ 0 ≤ -∞))
24	22, 2, 23	mp2an 672	. . . . . . . . . . 11 ⊢ (-∞ < 0 ↔ ¬ 0 ≤ -∞)
25	21, 24	mpbi 220	. . . . . . . . . 10 ⊢ ¬ 0 ≤ -∞
26		xaddmnf1 12257	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ +∞) → (𝐴 +_𝑒 -∞) = -∞)
27	26	breq2d 4798	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ +∞) → (0 ≤ (𝐴 +_𝑒 -∞) ↔ 0 ≤ -∞))
28	25, 27	mtbiri 316	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ +∞) → ¬ 0 ≤ (𝐴 +_𝑒 -∞))
29	28	ex 397	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ^* → (𝐴 ≠ +∞ → ¬ 0 ≤ (𝐴 +_𝑒 -∞)))
30	29	necon4ad 2962	. . . . . . 7 ⊢ (𝐴 ∈ ℝ^* → (0 ≤ (𝐴 +_𝑒 -∞) → 𝐴 = +∞))
31		0le0 11310	. . . . . . . 8 ⊢ 0 ≤ 0
32		oveq1 6798	. . . . . . . . 9 ⊢ (𝐴 = +∞ → (𝐴 +_𝑒 -∞) = (+∞ +_𝑒 -∞))
33		pnfaddmnf 12259	. . . . . . . . 9 ⊢ (+∞ +_𝑒 -∞) = 0
34	32, 33	syl6eq 2821	. . . . . . . 8 ⊢ (𝐴 = +∞ → (𝐴 +_𝑒 -∞) = 0)
35	31, 34	syl5breqr 4824	. . . . . . 7 ⊢ (𝐴 = +∞ → 0 ≤ (𝐴 +_𝑒 -∞))
36	30, 35	impbid1 215	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → (0 ≤ (𝐴 +_𝑒 -∞) ↔ 𝐴 = +∞))
37		pnfge 12162	. . . . . . 7 ⊢ (𝐴 ∈ ℝ^* → 𝐴 ≤ +∞)
38	37	biantrurd 522	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → (+∞ ≤ 𝐴 ↔ (𝐴 ≤ +∞ ∧ +∞ ≤ 𝐴)))
39	20, 36, 38	3bitr4d 300	. . . . 5 ⊢ (𝐴 ∈ ℝ^* → (0 ≤ (𝐴 +_𝑒 -∞) ↔ +∞ ≤ 𝐴))
40	39	adantr 466	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → (0 ≤ (𝐴 +_𝑒 -∞) ↔ +∞ ≤ 𝐴))
41		xnegeq 12236	. . . . . . . 8 ⊢ (𝐵 = +∞ → -_𝑒𝐵 = -_𝑒+∞)
42		xnegpnf 12238	. . . . . . . 8 ⊢ -_𝑒+∞ = -∞
43	41, 42	syl6eq 2821	. . . . . . 7 ⊢ (𝐵 = +∞ → -_𝑒𝐵 = -∞)
44	43	adantl 467	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → -_𝑒𝐵 = -∞)
45	44	oveq2d 6807	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → (𝐴 +_𝑒 -_𝑒𝐵) = (𝐴 +_𝑒 -∞))
46	45	breq2d 4798	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ 0 ≤ (𝐴 +_𝑒 -∞)))
47		breq1 4789	. . . . 5 ⊢ (𝐵 = +∞ → (𝐵 ≤ 𝐴 ↔ +∞ ≤ 𝐴))
48	47	adantl 467	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → (𝐵 ≤ 𝐴 ↔ +∞ ≤ 𝐴))
49	40, 46, 48	3bitr4d 300	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = +∞) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ 𝐵 ≤ 𝐴))
50		oveq1 6798	. . . . . . . . . 10 ⊢ (𝐴 = -∞ → (𝐴 +_𝑒 +∞) = (-∞ +_𝑒 +∞))
51		mnfaddpnf 12260	. . . . . . . . . 10 ⊢ (-∞ +_𝑒 +∞) = 0
52	50, 51	syl6eq 2821	. . . . . . . . 9 ⊢ (𝐴 = -∞ → (𝐴 +_𝑒 +∞) = 0)
53	52	adantl 467	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 = -∞) → (𝐴 +_𝑒 +∞) = 0)
54	31, 53	syl5breqr 4824	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 = -∞) → 0 ≤ (𝐴 +_𝑒 +∞))
55		0lepnf 12164	. . . . . . . 8 ⊢ 0 ≤ +∞
56		xaddpnf1 12255	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞) → (𝐴 +_𝑒 +∞) = +∞)
57	55, 56	syl5breqr 4824	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞) → 0 ≤ (𝐴 +_𝑒 +∞))
58	54, 57	pm2.61dane 3030	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → 0 ≤ (𝐴 +_𝑒 +∞))
59		mnfle 12167	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → -∞ ≤ 𝐴)
60	58, 59	2thd 255	. . . . 5 ⊢ (𝐴 ∈ ℝ^* → (0 ≤ (𝐴 +_𝑒 +∞) ↔ -∞ ≤ 𝐴))
61	60	adantr 466	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (0 ≤ (𝐴 +_𝑒 +∞) ↔ -∞ ≤ 𝐴))
62		xnegeq 12236	. . . . . . . 8 ⊢ (𝐵 = -∞ → -_𝑒𝐵 = -_𝑒-∞)
63		xnegmnf 12239	. . . . . . . 8 ⊢ -_𝑒-∞ = +∞
64	62, 63	syl6eq 2821	. . . . . . 7 ⊢ (𝐵 = -∞ → -_𝑒𝐵 = +∞)
65	64	adantl 467	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → -_𝑒𝐵 = +∞)
66	65	oveq2d 6807	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐴 +_𝑒 -_𝑒𝐵) = (𝐴 +_𝑒 +∞))
67	66	breq2d 4798	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ 0 ≤ (𝐴 +_𝑒 +∞)))
68		breq1 4789	. . . . 5 ⊢ (𝐵 = -∞ → (𝐵 ≤ 𝐴 ↔ -∞ ≤ 𝐴))
69	68	adantl 467	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐵 ≤ 𝐴 ↔ -∞ ≤ 𝐴))
70	61, 67, 69	3bitr4d 300	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ 𝐵 ≤ 𝐴))
71	17, 49, 70	3jaodan 1542	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ 𝐵 ≤ 𝐴))
72	1, 71	sylan2b 581	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (0 ≤ (𝐴 +_𝑒 -_𝑒𝐵) ↔ 𝐵 ≤ 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 382 ∨ w3o 1070 = wceq 1631 ∈ wcel 2145 ≠ wne 2943 class class class wbr 4786 (class class class)co 6791 ℝcr 10135 0cc0 10136 +∞cpnf 10271 -∞cmnf 10272 ℝ^*cxr 10273 < clt 10274 ≤ cle 10275 -_𝑒cxne 12141 +_𝑒 cxad 12142

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7094 ax-cnex 10192 ax-resscn 10193 ax-1cn 10194 ax-icn 10195 ax-addcl 10196 ax-addrcl 10197 ax-mulcl 10198 ax-mulrcl 10199 ax-mulcom 10200 ax-addass 10201 ax-mulass 10202 ax-distr 10203 ax-i2m1 10204 ax-1ne0 10205 ax-1rid 10206 ax-rnegex 10207 ax-rrecex 10208 ax-cnre 10209 ax-pre-lttri 10210 ax-pre-lttrn 10211 ax-pre-ltadd 10212

This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-op 4323 df-uni 4575 df-iun 4656 df-br 4787 df-opab 4847 df-mpt 4864 df-id 5157 df-po 5170 df-so 5171 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-iota 5992 df-fun 6031 df-fn 6032 df-f 6033 df-f1 6034 df-fo 6035 df-f1o 6036 df-fv 6037 df-riota 6752 df-ov 6794 df-oprab 6795 df-mpt2 6796 df-1st 7313 df-2nd 7314 df-er 7894 df-en 8108 df-dom 8109 df-sdom 8110 df-pnf 10276 df-mnf 10277 df-xr 10278 df-ltxr 10279 df-le 10280 df-sub 10468 df-neg 10469 df-xneg 12144 df-xadd 12145

This theorem is referenced by: xposdif 12290 ssblps 22440 ssbl 22441 xrsxmet 22825 xrge0subcld 29861 esumle 30453 esumlef 30457

W3C validator