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 13161

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 13137	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		elxr 13137	. . 3 ⊢ (𝐶 ∈ ℝ^* ↔ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))
3		elxr 13137	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
4		lttr 11282	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5	4	3expa 1134	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
6	5	an32s 664	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
7		rexr 11251	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℝ^*)
8		pnfnlt 13149	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ ℝ^* → ¬ +∞ < 𝐶)
9	7, 8	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ ℝ → ¬ +∞ < 𝐶)
10	9	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → ¬ +∞ < 𝐶)
11		breq1 5113	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = +∞ → (𝐵 < 𝐶 ↔ +∞ < 𝐶))
12	11	adantl 486	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 < 𝐶 ↔ +∞ < 𝐶))
13	10, 12	mtbird 328	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → ¬ 𝐵 < 𝐶)
14	13	pm2.21d 122	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 < 𝐶 → 𝐴 < 𝐶))
15	14	adantll 726	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = +∞) → (𝐵 < 𝐶 → 𝐴 < 𝐶))
16	15	adantld 495	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = +∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
17		rexr 11251	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
18		nltmnf 13150	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℝ^* → ¬ 𝐴 < -∞)
19	17, 18	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℝ → ¬ 𝐴 < -∞)
20	19	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
21		breq2 5114	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
22	21	adantl 486	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
23	20, 22	mtbird 328	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
24	23	pm2.21d 122	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → 𝐴 < 𝐶))
25	24	adantlr 727	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → 𝐴 < 𝐶))
26	25	adantrd 496	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = -∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
27	6, 16, 26	3jaodan 1456	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
28	3, 27	sylan2b 605	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
29	28	an32s 664	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
30		ltpnf 13141	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)
31	30	adantr 485	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → 𝐴 < +∞)
32		breq2 5114	. . . . . . . . . . 11 ⊢ (𝐶 = +∞ → (𝐴 < 𝐶 ↔ 𝐴 < +∞))
33	32	adantl 486	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → (𝐴 < 𝐶 ↔ 𝐴 < +∞))
34	31, 33	mpbird 260	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
35	34	adantlr 727	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
36	35	a1d 26	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = +∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
37		nltmnf 13150	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ^* → ¬ 𝐵 < -∞)
38	37	adantr 485	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → ¬ 𝐵 < -∞)
39		breq2 5114	. . . . . . . . . . . 12 ⊢ (𝐶 = -∞ → (𝐵 < 𝐶 ↔ 𝐵 < -∞))
40	39	adantl 486	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → (𝐵 < 𝐶 ↔ 𝐵 < -∞))
41	38, 40	mtbird 328	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → ¬ 𝐵 < 𝐶)
42	41	pm2.21d 122	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → (𝐵 < 𝐶 → 𝐴 < 𝐶))
43	42	adantld 495	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
44	43	adantll 726	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = -∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
45	29, 36, 44	3jaodan 1456	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
46	45	anasss 471	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
47		pnfnlt 13149	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ^* → ¬ +∞ < 𝐵)
48	47	adantl 486	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ¬ +∞ < 𝐵)
49		breq1 5113	. . . . . . . . . 10 ⊢ (𝐴 = +∞ → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
50	49	adantr 485	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
51	48, 50	mtbird 328	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ¬ 𝐴 < 𝐵)
52	51	pm2.21d 122	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → 𝐴 < 𝐶))
53	52	adantrd 496	. . . . . 6 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
54	53	adantrr 729	. . . . 5 ⊢ ((𝐴 = +∞ ∧ (𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
55		mnflt 13144	. . . . . . . . . . 11 ⊢ (𝐶 ∈ ℝ → -∞ < 𝐶)
56	55	adantl 486	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → -∞ < 𝐶)
57		breq1 5113	. . . . . . . . . . 11 ⊢ (𝐴 = -∞ → (𝐴 < 𝐶 ↔ -∞ < 𝐶))
58	57	adantr 485	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 ↔ -∞ < 𝐶))
59	56, 58	mpbird 260	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → 𝐴 < 𝐶)
60	59	a1d 26	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
61	60	adantlr 727	. . . . . . 7 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
62		mnfltpnf 13147	. . . . . . . . . 10 ⊢ -∞ < +∞
63		breq12 5115	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐶 = +∞) → (𝐴 < 𝐶 ↔ -∞ < +∞))
64	62, 63	mpbiri 261	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
65	64	a1d 26	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐶 = +∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
66	65	adantlr 727	. . . . . . 7 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = +∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
67	43	adantll 726	. . . . . . 7 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = -∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
68	61, 66, 67	3jaodan 1456	. . . . . 6 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
69	68	anasss 471	. . . . 5 ⊢ ((𝐴 = -∞ ∧ (𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
70	46, 54, 69	3jaoian 1455	. . . 4 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ (𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
71	70	3impb 1130	. . 3 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
72	2, 71	syl3an3b 1430	. 2 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
73	1, 72	syl3an1b 1428	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ w3o 1100 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 class class class wbr 5110 ℝcr 11095 +∞cpnf 11236 -∞cmnf 11237 ℝ^*cxr 11238 < clt 11239

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5258 ax-nul 5268 ax-pow 5334 ax-pr 5402 ax-un 7730 ax-cnex 11152 ax-resscn 11153 ax-pre-lttrn 11171

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4874 df-br 5111 df-opab 5175 df-mpt 5194 df-id 5554 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 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 8690 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11241 df-mnf 11242 df-xr 11243 df-ltxr 11244

This theorem is referenced by: xrltso 13162 xrlelttr 13177 xrltletr 13178 xrlttrd 13180 xrub 13334 ioo0 13393 ioojoin 13506 hashgt23el 14457 leordtval2 23334 icopnfcld 24889 iocmnfcld 24890 ismbf3d 25778 tanord1 26664 tan2h 38146 asindmre 38237 iccpartlt 48055

W3C validator