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 13309

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 13285	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		elxr 13285	. . 3 ⊢ (𝐶 ∈ ℝ^* ↔ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))
3		elxr 13285	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
4		lttr 11425	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5	4	3expa 1136	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
6	5	an32s 665	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
7		rexr 11394	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℝ^*)
8		pnfnlt 13297	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ ℝ^* → ¬ +∞ < 𝐶)
9	7, 8	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ ℝ → ¬ +∞ < 𝐶)
10	9	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → ¬ +∞ < 𝐶)
11		breq1 5111	. . . . . . . . . . . . . . 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 11394	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
18		nltmnf 13298	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℝ^* → ¬ 𝐴 < -∞)
19	17, 18	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℝ → ¬ 𝐴 < -∞)
20	19	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
21		breq2 5112	. . . . . . . . . . . . . . 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 1459	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
28	3, 27	sylan2b 606	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
29	28	an32s 665	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
30		ltpnf 13289	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)
31	30	adantr 486	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → 𝐴 < +∞)
32		breq2 5112	. . . . . . . . . . 11 ⊢ (𝐶 = +∞ → (𝐴 < 𝐶 ↔ 𝐴 < +∞))
33	32	adantl 487	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → (𝐴 < 𝐶 ↔ 𝐴 < +∞))
34	31, 33	mpbird 260	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
35	34	adantlr 728	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
36	35	a1d 26	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = +∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
37		nltmnf 13298	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ^* → ¬ 𝐵 < -∞)
38	37	adantr 486	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → ¬ 𝐵 < -∞)
39		breq2 5112	. . . . . . . . . . . 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 1459	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
46	45	anasss 472	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
47		pnfnlt 13297	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ^* → ¬ +∞ < 𝐵)
48	47	adantl 487	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ¬ +∞ < 𝐵)
49		breq1 5111	. . . . . . . . . 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 13292	. . . . . . . . . . 11 ⊢ (𝐶 ∈ ℝ → -∞ < 𝐶)
56	55	adantl 487	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → -∞ < 𝐶)
57		breq1 5111	. . . . . . . . . . 11 ⊢ (𝐴 = -∞ → (𝐴 < 𝐶 ↔ -∞ < 𝐶))
58	57	adantr 486	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 ↔ -∞ < 𝐶))
59	56, 58	mpbird 260	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → 𝐴 < 𝐶)
60	59	a1d 26	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
61	60	adantlr 728	. . . . . . 7 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
62		mnfltpnf 13295	. . . . . . . . . 10 ⊢ -∞ < +∞
63		breq12 5113	. . . . . . . . . 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 1459	. . . . . 6 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
69	68	anasss 472	. . . . 5 ⊢ ((𝐴 = -∞ ∧ (𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
70	46, 54, 69	3jaoian 1458	. . . 4 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ (𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
71	70	3impb 1132	. . 3 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
72	2, 71	syl3an3b 1433	. 2 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
73	1, 72	syl3an1b 1431	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 2147 class class class wbr 5108 ℝcr 11238 +∞cpnf 11379 -∞cmnf 11380 ℝ^*cxr 11381 < clt 11382

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-pre-lttrn 11314

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-br 5109 df-opab 5174 df-mpt 5193 df-id 5553 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-er 8755 df-en 9012 df-dom 9013 df-sdom 9014 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387

This theorem is used by: xrltso 13310 xrlelttr 13325 xrltletr 13326 xrlttrd 13328 xrub 13482 ioo0 13541 ioojoin 13654 hashgt23el 14610 leordtval2 23585 icopnfcld 25141 iocmnfcld 25142 ismbf3d 26030 tanord1 26922 tan2h 38803 asindmre 38889 iccpartlt 48779

W3C validator