xrlttrt - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem xrlttrt 5565

Description: Ordering on the extended reals is transitive.

**Assertion**
Ref	Expression
xrlttrt	⊢ ((A ∈ ℝ^* ⋀ B ∈ ℝ^* ⋀ C ∈ ℝ^*) → ((A < B ⋀ B < C) → A < C))

**Proof of Theorem xrlttrt**
Step	Hyp	Ref	Expression
1		axlttrn 5516	. . . . . . . . . . . 12 ⊢ ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ C ∈ ℝ) → ((A < B ⋀ B < C) → A < C))
2	1	3expa 835	. . . . . . . . . . 11 ⊢ (((A ∈ ℝ ⋀ B ∈ ℝ) ⋀ C ∈ ℝ) → ((A < B ⋀ B < C) → A < C))
3	2	an1rs 491	. . . . . . . . . 10 ⊢ (((A ∈ ℝ ⋀ C ∈ ℝ) ⋀ B ∈ ℝ) → ((A < B ⋀ B < C) → A < C))
4		rexrt 5511	. . . . . . . . . . . . . . . 16 ⊢ (C ∈ ℝ → C ∈ ℝ^*)
5		pnfnltt 5558	. . . . . . . . . . . . . . . 16 ⊢ (C ∈ ℝ^* → ¬ +∞ < C)
6	4, 5	syl 10	. . . . . . . . . . . . . . 15 ⊢ (C ∈ ℝ → ¬ +∞ < C)
7	6	adantr 391	. . . . . . . . . . . . . 14 ⊢ ((C ∈ ℝ ⋀ B = +∞) → ¬ +∞ < C)
8		breq1 2627	. . . . . . . . . . . . . . 15 ⊢ (B = +∞ → (B < C ↔ +∞ < C))
9	8	adantl 390	. . . . . . . . . . . . . 14 ⊢ ((C ∈ ℝ ⋀ B = +∞) → (B < C ↔ +∞ < C))
10	7, 9	mtbird 717	. . . . . . . . . . . . 13 ⊢ ((C ∈ ℝ ⋀ B = +∞) → ¬ B < C)
11	10	pm2.21d 78	. . . . . . . . . . . 12 ⊢ ((C ∈ ℝ ⋀ B = +∞) → (B < C → A < C))
12	11	adantll 394	. . . . . . . . . . 11 ⊢ (((A ∈ ℝ ⋀ C ∈ ℝ) ⋀ B = +∞) → (B < C → A < C))
13	12	adantld 392	. . . . . . . . . 10 ⊢ (((A ∈ ℝ ⋀ C ∈ ℝ) ⋀ B = +∞) → ((A < B ⋀ B < C) → A < C))
14		rexrt 5511	. . . . . . . . . . . . . . . 16 ⊢ (A ∈ ℝ → A ∈ ℝ^*)
15		nltmnft 5559	. . . . . . . . . . . . . . . 16 ⊢ (A ∈ ℝ^* → ¬ A < -∞)
16	14, 15	syl 10	. . . . . . . . . . . . . . 15 ⊢ (A ∈ ℝ → ¬ A < -∞)
17	16	adantr 391	. . . . . . . . . . . . . 14 ⊢ ((A ∈ ℝ ⋀ B = -∞) → ¬ A < -∞)
18		breq2 2628	. . . . . . . . . . . . . . 15 ⊢ (B = -∞ → (A < B ↔ A < -∞))
19	18	adantl 390	. . . . . . . . . . . . . 14 ⊢ ((A ∈ ℝ ⋀ B = -∞) → (A < B ↔ A < -∞))
20	17, 19	mtbird 717	. . . . . . . . . . . . 13 ⊢ ((A ∈ ℝ ⋀ B = -∞) → ¬ A < B)
21	20	pm2.21d 78	. . . . . . . . . . . 12 ⊢ ((A ∈ ℝ ⋀ B = -∞) → (A < B → A < C))
22	21	adantlr 395	. . . . . . . . . . 11 ⊢ (((A ∈ ℝ ⋀ C ∈ ℝ) ⋀ B = -∞) → (A < B → A < C))
23	22	adantrd 393	. . . . . . . . . 10 ⊢ (((A ∈ ℝ ⋀ C ∈ ℝ) ⋀ B = -∞) → ((A < B ⋀ B < C) → A < C))
24	3, 13, 23	3jaodan 892	. . . . . . . . 9 ⊢ (((A ∈ ℝ ⋀ C ∈ ℝ) ⋀ (B ∈ ℝ ⋁ B = +∞ ⋁ B = -∞)) → ((A < B ⋀ B < C) → A < C))
25		elxr 5547	. . . . . . . . 9 ⊢ (B ∈ ℝ^* ↔ (B ∈ ℝ ⋁ B = +∞ ⋁ B = -∞))
26	24, 25	sylan2b 454	. . . . . . . 8 ⊢ (((A ∈ ℝ ⋀ C ∈ ℝ) ⋀ B ∈ ℝ^*) → ((A < B ⋀ B < C) → A < C))
27	26	an1rs 491	. . . . . . 7 ⊢ (((A ∈ ℝ ⋀ B ∈ ℝ^*) ⋀ C ∈ ℝ) → ((A < B ⋀ B < C) → A < C))
28		ltpnft 5554	. . . . . . . . . . 11 ⊢ (A ∈ ℝ → A < +∞)
29	28	adantr 391	. . . . . . . . . 10 ⊢ ((A ∈ ℝ ⋀ C = +∞) → A < +∞)
30		breq2 2628	. . . . . . . . . . 11 ⊢ (C = +∞ → (A < C ↔ A < +∞))
31	30	adantl 390	. . . . . . . . . 10 ⊢ ((A ∈ ℝ ⋀ C = +∞) → (A < C ↔ A < +∞))
32	29, 31	mpbird 196	. . . . . . . . 9 ⊢ ((A ∈ ℝ ⋀ C = +∞) → A < C)
33	32	adantlr 395	. . . . . . . 8 ⊢ (((A ∈ ℝ ⋀ B ∈ ℝ^*) ⋀ C = +∞) → A < C)
34	33	a1d 12	. . . . . . 7 ⊢ (((A ∈ ℝ ⋀ B ∈ ℝ^*) ⋀ C = +∞) → ((A < B ⋀ B < C) → A < C))
35		nltmnft 5559	. . . . . . . . . . . 12 ⊢ (B ∈ ℝ^* → ¬ B < -∞)
36	35	adantr 391	. . . . . . . . . . 11 ⊢ ((B ∈ ℝ^* ⋀ C = -∞) → ¬ B < -∞)
37		breq2 2628	. . . . . . . . . . . 12 ⊢ (C = -∞ → (B < C ↔ B < -∞))
38	37	adantl 390	. . . . . . . . . . 11 ⊢ ((B ∈ ℝ^* ⋀ C = -∞) → (B < C ↔ B < -∞))
39	36, 38	mtbird 717	. . . . . . . . . 10 ⊢ ((B ∈ ℝ^* ⋀ C = -∞) → ¬ B < C)
40	39	pm2.21d 78	. . . . . . . . 9 ⊢ ((B ∈ ℝ^* ⋀ C = -∞) → (B < C → A < C))
41	40	adantld 392	. . . . . . . 8 ⊢ ((B ∈ ℝ^* ⋀ C = -∞) → ((A < B ⋀ B < C) → A < C))
42	41	adantll 394	. . . . . . 7 ⊢ (((A ∈ ℝ ⋀ B ∈ ℝ^*) ⋀ C = -∞) → ((A < B ⋀ B < C) → A < C))
43	27, 34, 42	3jaodan 892	. . . . . 6 ⊢ (((A ∈ ℝ ⋀ B ∈ ℝ^*) ⋀ (C ∈ ℝ ⋁ C = +∞ ⋁ C = -∞)) → ((A < B ⋀ B < C) → A < C))
44	43	anasss 442	. . . . 5 ⊢ ((A ∈ ℝ ⋀ (B ∈ ℝ^* ⋀ (C ∈ ℝ ⋁ C = +∞ ⋁ C = -∞))) → ((A < B ⋀ B < C) → A < C))
45		pnfnltt 5558	. . . . . . . . . 10 ⊢ (B ∈ ℝ^* → ¬ +∞ < B)
46	45	adantl 390	. . . . . . . . 9 ⊢ ((A = +∞ ⋀ B ∈ ℝ^*) → ¬ +∞ < B)
47		breq1 2627	. . . . . . . . . 10 ⊢ (A = +∞ → (A < B ↔ +∞ < B))
48	47	adantr 391	. . . . . . . . 9 ⊢ ((A = +∞ ⋀ B ∈ ℝ^*) → (A < B ↔ +∞ < B))
49	46, 48	mtbird 717	. . . . . . . 8 ⊢ ((A = +∞ ⋀ B ∈ ℝ^*) → ¬ A < B)
50	49	pm2.21d 78	. . . . . . 7 ⊢ ((A = +∞ ⋀ B ∈ ℝ^*) → (A < B → A < C))
51	50	adantrd 393	. . . . . 6 ⊢ ((A = +∞ ⋀ B ∈ ℝ^*) → ((A < B ⋀ B < C) → A < C))
52	51	adantrr 397	. . . . 5 ⊢ ((A = +∞ ⋀ (B ∈ ℝ^* ⋀ (C ∈ ℝ ⋁ C = +∞ ⋁ C = -∞))) → ((A < B ⋀ B < C) → A < C))
53		mnfltt 5555	. . . . . . . . . . 11 ⊢ (C ∈ ℝ → -∞ < C)
54	53	adantl 390	. . . . . . . . . 10 ⊢ ((A = -∞ ⋀ C ∈ ℝ) → -∞ < C)
55		breq1 2627	. . . . . . . . . . 11 ⊢ (A = -∞ → (A < C ↔ -∞ < C))
56	55	adantr 391	. . . . . . . . . 10 ⊢ ((A = -∞ ⋀ C ∈ ℝ) → (A < C ↔ -∞ < C))
57	54, 56	mpbird 196	. . . . . . . . 9 ⊢ ((A = -∞ ⋀ C ∈ ℝ) → A < C)
58	57	a1d 12	. . . . . . . 8 ⊢ ((A = -∞ ⋀ C ∈ ℝ) → ((A < B ⋀ B < C) → A < C))
59	58	adantlr 395	. . . . . . 7 ⊢ (((A = -∞ ⋀ B ∈ ℝ^*) ⋀ C ∈ ℝ) → ((A < B ⋀ B < C) → A < C))
60		mnfltpnf 5556	. . . . . . . . . 10 ⊢ -∞ < +∞
61		breq12 2629	. . . . . . . . . 10 ⊢ ((A = -∞ ⋀ C = +∞) → (A < C ↔ -∞ < +∞))
62	60, 61	mpbiri 194	. . . . . . . . 9 ⊢ ((A = -∞ ⋀ C = +∞) → A < C)
63	62	a1d 12	. . . . . . . 8 ⊢ ((A = -∞ ⋀ C = +∞) → ((A < B ⋀ B < C) → A < C))
64	63	adantlr 395	. . . . . . 7 ⊢ (((A = -∞ ⋀ B ∈ ℝ^*) ⋀ C = +∞) → ((A < B ⋀ B < C) → A < C))
65	41	adantll 394	. . . . . . 7 ⊢ (((A = -∞ ⋀ B ∈ ℝ^*) ⋀ C = -∞) → ((A < B ⋀ B < C) → A < C))
66	59, 64, 65	3jaodan 892	. . . . . 6 ⊢ (((A = -∞ ⋀ B ∈ ℝ^*) ⋀ (C ∈ ℝ ⋁ C = +∞ ⋁ C = -∞)) → ((A < B ⋀ B < C) → A < C))
67	66	anasss 442	. . . . 5 ⊢ ((A = -∞ ⋀ (B ∈ ℝ^* ⋀ (C ∈ ℝ ⋁ C = +∞ ⋁ C = -∞))) → ((A < B ⋀ B < C) → A < C))
68	44, 52, 67	3jaoian 891	. . . 4 ⊢ (((A ∈ ℝ ⋁ A = +∞ ⋁ A = -∞) ⋀ (B ∈ ℝ^* ⋀ (C ∈ ℝ ⋁ C = +∞ ⋁ C = -∞))) → ((A < B ⋀ B < C) → A < C))
69	68	3impb 831	. . 3 ⊢ (((A ∈ ℝ ⋁ A = +∞ ⋁ A = -∞) ⋀ B ∈ ℝ^* ⋀ (C ∈ ℝ ⋁ C = +∞ ⋁ C = -∞)) → ((A < B ⋀ B < C) → A < C))
70		elxr 5547	. . 3 ⊢ (C ∈ ℝ^* ↔ (C ∈ ℝ ⋁ C = +∞ ⋁ C = -∞))
71	69, 70	syl3an3b 866	. 2 ⊢ (((A ∈ ℝ ⋁ A = +∞ ⋁ A = -∞) ⋀ B ∈ ℝ^* ⋀ C ∈ ℝ^*) → ((A < B ⋀ B < C) → A < C))
72		elxr 5547	. 2 ⊢ (A ∈ ℝ^* ↔ (A ∈ ℝ ⋁ A = +∞ ⋁ A = -∞))
73	71, 72	syl3an1b 864	1 ⊢ ((A ∈ ℝ^* ⋀ B ∈ ℝ^* ⋀ C ∈ ℝ^*) → ((A < B ⋀ B < C) → A < C))

Colors of variables: wff set class

Syntax hints: ¬ wn 2 → wi 3 ↔ wb 146 ⋀ wa 223 ⋁ w3o 776 ⋀ w3a 777 = wceq 958 ∈ wcel 960 class class class wbr 2624 ℝcr 5245 +∞cpnf 5495 -∞cmnf 5496 ℝ^*cxr 5497 < clt 5498

This theorem is referenced by: xrltso 5566 xrlelttrt 5574 xrltletrt 5575 xrub 6082 qbtwnxr 6280 ioo0t 6369 elioc2t 6391 elico2t 6392 elioo1t3 10482 truni1 10485

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 964 ax-gen 965 ax-8 966 ax-9 967 ax-10 968 ax-11 969 ax-12 970 ax-13 971 ax-14 972 ax-17 973 ax-4 975 ax-5o 977 ax-6o 980 ax-9o 1125 ax-10o 1142 ax-16 1212 ax-11o 1220 ax-ext 1462 ax-rep 2698 ax-sep 2708 ax-nul 2715 ax-pow 2748 ax-pr 2785 ax-un 2872 ax-inf2 4634

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 778 df-3an 779 df-ex 983 df-sb 1174 df-eu 1384 df-mo 1385 df-clab 1467 df-cleq 1472 df-clel 1475 df-ne 1590 df-nel 1591 df-ral 1652 df-rex 1653 df-reu 1654 df-rab 1655 df-v 1815 df-sbc 1945 df-csb 2005 df-dif 2052 df-un 2053 df-in 2054 df-ss 2056 df-pss 2058 df-nul 2284 df-if 2366 df-pw 2406 df-sn 2416 df-pr 2417 df-tp 2419 df-op 2420 df-uni 2508 df-int 2538 df-iun 2572 df-br 2625 df-opab 2672 df-tr 2686 df-eprel 2838 df-id 2841 df-po 2846 df-so 2856 df-fr 2923 df-we 2940 df-ord 2957 df-on 2958 df-lim 2959 df-suc 2960 df-om 3138 df-xp 3190 df-rel 3191 df-cnv 3192 df-co 3193 df-dm 3194 df-rn 3195 df-res 3196 df-ima 3197 df-fun 3198 df-fn 3199 df-f 3200 df-f1 3201 df-fo 3202 df-f1o 3203 df-fv 3204 df-rdg 3938 df-opr 3971 df-oprab 3972 df-1st 4085 df-2nd 4086 df-1o 4139 df-oadd 4141 df-omul 4142 df-er 4267 df-ec 4269 df-qs 4272 df-en 4374 df-dom 4375 df-sdom 4376 df-ni 5012 df-pli 5013 df-mi 5014 df-lti 5015 df-plpq 5047 df-mpq 5048 df-enq 5049 df-nq 5050 df-plq 5051 df-mq 5052 df-rq 5053 df-ltq 5054 df-1q 5055 df-np 5098 df-1p 5099 df-plp 5100 df-ltp 5102 df-enr 5178 df-nr 5179 df-ltr 5182 df-0r 5183 df-c 5252 df-r 5256 df-lt 5259 df-pnf 5499 df-mnf 5500 df-xr 5501 df-ltxr 5502