xrlttr - Metamath Proof Explorer

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

Theorem xrlttr 13191

Description: Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.)

**Assertion**
Ref	Expression
xrlttr	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))

**Proof of Theorem xrlttr**
Step	Hyp	Ref	Expression
1		elxr 13167	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		elxr 13167	. . 3 ⊢ (𝐶 ∈ ℝ^* ↔ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))
3		elxr 13167	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
4		lttr 11310	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5	4	3expa 1136	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
6	5	an32s 665	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
7		rexr 11279	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℝ^*)
8		pnfnlt 13179	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ ℝ^* → ¬ +∞ < 𝐶)
9	7, 8	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ ℝ → ¬ +∞ < 𝐶)
10	9	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → ¬ +∞ < 𝐶)
11		breq1 5106	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = +∞ → (𝐵 < 𝐶 ↔ +∞ < 𝐶))
12	11	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 < 𝐶 ↔ +∞ < 𝐶))
13	10, 12	mtbird 328	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → ¬ 𝐵 < 𝐶)
14	13	pm2.21d 122	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 < 𝐶 → 𝐴 < 𝐶))
15	14	adantll 727	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = +∞) → (𝐵 < 𝐶 → 𝐴 < 𝐶))
16	15	adantld 496	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = +∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
17		rexr 11279	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
18		nltmnf 13180	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℝ^* → ¬ 𝐴 < -∞)
19	17, 18	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℝ → ¬ 𝐴 < -∞)
20	19	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
21		breq2 5107	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
22	21	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
23	20, 22	mtbird 328	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
24	23	pm2.21d 122	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → 𝐴 < 𝐶))
25	24	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → 𝐴 < 𝐶))
26	25	adantrd 497	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = -∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
27	6, 16, 26	3jaodan 1458	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
28	3, 27	sylan2b 606	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
29	28	an32s 665	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
30		ltpnf 13171	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)
31	30	adantr 486	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → 𝐴 < +∞)
32		breq2 5107	. . . . . . . . . . 11 ⊢ (𝐶 = +∞ → (𝐴 < 𝐶 ↔ 𝐴 < +∞))
33	32	adantl 487	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → (𝐴 < 𝐶 ↔ 𝐴 < +∞))
34	31, 33	mpbird 260	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
35	34	adantlr 728	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
36	35	a1d 26	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = +∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
37		nltmnf 13180	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ^* → ¬ 𝐵 < -∞)
38	37	adantr 486	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → ¬ 𝐵 < -∞)
39		breq2 5107	. . . . . . . . . . . 12 ⊢ (𝐶 = -∞ → (𝐵 < 𝐶 ↔ 𝐵 < -∞))
40	39	adantl 487	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → (𝐵 < 𝐶 ↔ 𝐵 < -∞))
41	38, 40	mtbird 328	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → ¬ 𝐵 < 𝐶)
42	41	pm2.21d 122	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → (𝐵 < 𝐶 → 𝐴 < 𝐶))
43	42	adantld 496	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
44	43	adantll 727	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = -∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
45	29, 36, 44	3jaodan 1458	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
46	45	anasss 472	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
47		pnfnlt 13179	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ^* → ¬ +∞ < 𝐵)
48	47	adantl 487	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ¬ +∞ < 𝐵)
49		breq1 5106	. . . . . . . . . 10 ⊢ (𝐴 = +∞ → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
50	49	adantr 486	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
51	48, 50	mtbird 328	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ¬ 𝐴 < 𝐵)
52	51	pm2.21d 122	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → 𝐴 < 𝐶))
53	52	adantrd 497	. . . . . 6 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
54	53	adantrr 730	. . . . 5 ⊢ ((𝐴 = +∞ ∧ (𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
55		mnflt 13174	. . . . . . . . . . 11 ⊢ (𝐶 ∈ ℝ → -∞ < 𝐶)
56	55	adantl 487	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → -∞ < 𝐶)
57		breq1 5106	. . . . . . . . . . 11 ⊢ (𝐴 = -∞ → (𝐴 < 𝐶 ↔ -∞ < 𝐶))
58	57	adantr 486	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 ↔ -∞ < 𝐶))
59	56, 58	mpbird 260	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → 𝐴 < 𝐶)
60	59	a1d 26	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
61	60	adantlr 728	. . . . . . 7 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
62		mnfltpnf 13177	. . . . . . . . . 10 ⊢ -∞ < +∞
63		breq12 5108	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐶 = +∞) → (𝐴 < 𝐶 ↔ -∞ < +∞))
64	62, 63	mpbiri 261	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
65	64	a1d 26	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐶 = +∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
66	65	adantlr 728	. . . . . . 7 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = +∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
67	43	adantll 727	. . . . . . 7 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = -∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
68	61, 66, 67	3jaodan 1458	. . . . . 6 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
69	68	anasss 472	. . . . 5 ⊢ ((𝐴 = -∞ ∧ (𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
70	46, 54, 69	3jaoian 1457	. . . 4 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ (𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
71	70	3impb 1132	. . 3 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
72	2, 71	syl3an3b 1432	. 2 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
73	1, 72	syl3an1b 1430	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ w3o 1102 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 class class class wbr 5103 ℝcr 11123 +∞cpnf 11264 -∞cmnf 11265 ℝ^*cxr 11266 < clt 11267

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7736 ax-cnex 11180 ax-resscn 11181 ax-pre-lttrn 11199

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5550 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-er 8696 df-en 8953 df-dom 8954 df-sdom 8955 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272

This theorem is used by: xrltso 13192 xrlelttr 13207 xrltletr 13208 xrlttrd 13210 xrub 13364 ioo0 13423 ioojoin 13536 hashgt23el 14489 leordtval2 23437 icopnfcld 24993 iocmnfcld 24994 ismbf3d 25882 tanord1 26774 tan2h 38366 asindmre 38452 iccpartlt 48324

W3C validator