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 12803

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 12781	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		elxr 12781	. . 3 ⊢ (𝐶 ∈ ℝ^* ↔ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))
3		elxr 12781	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
4		lttr 10982	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5	4	3expa 1116	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
6	5	an32s 648	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
7		rexr 10952	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℝ^*)
8		pnfnlt 12793	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ ℝ^* → ¬ +∞ < 𝐶)
9	7, 8	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ ℝ → ¬ +∞ < 𝐶)
10	9	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → ¬ +∞ < 𝐶)
11		breq1 5073	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = +∞ → (𝐵 < 𝐶 ↔ +∞ < 𝐶))
12	11	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 < 𝐶 ↔ +∞ < 𝐶))
13	10, 12	mtbird 324	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → ¬ 𝐵 < 𝐶)
14	13	pm2.21d 121	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 < 𝐶 → 𝐴 < 𝐶))
15	14	adantll 710	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = +∞) → (𝐵 < 𝐶 → 𝐴 < 𝐶))
16	15	adantld 490	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = +∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
17		rexr 10952	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
18		nltmnf 12794	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℝ^* → ¬ 𝐴 < -∞)
19	17, 18	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℝ → ¬ 𝐴 < -∞)
20	19	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
21		breq2 5074	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
22	21	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
23	20, 22	mtbird 324	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
24	23	pm2.21d 121	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → 𝐴 < 𝐶))
25	24	adantlr 711	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → 𝐴 < 𝐶))
26	25	adantrd 491	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = -∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
27	6, 16, 26	3jaodan 1428	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
28	3, 27	sylan2b 593	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
29	28	an32s 648	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
30		ltpnf 12785	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)
31	30	adantr 480	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → 𝐴 < +∞)
32		breq2 5074	. . . . . . . . . . 11 ⊢ (𝐶 = +∞ → (𝐴 < 𝐶 ↔ 𝐴 < +∞))
33	32	adantl 481	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → (𝐴 < 𝐶 ↔ 𝐴 < +∞))
34	31, 33	mpbird 256	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
35	34	adantlr 711	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
36	35	a1d 25	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = +∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
37		nltmnf 12794	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ^* → ¬ 𝐵 < -∞)
38	37	adantr 480	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → ¬ 𝐵 < -∞)
39		breq2 5074	. . . . . . . . . . . 12 ⊢ (𝐶 = -∞ → (𝐵 < 𝐶 ↔ 𝐵 < -∞))
40	39	adantl 481	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → (𝐵 < 𝐶 ↔ 𝐵 < -∞))
41	38, 40	mtbird 324	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → ¬ 𝐵 < 𝐶)
42	41	pm2.21d 121	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → (𝐵 < 𝐶 → 𝐴 < 𝐶))
43	42	adantld 490	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 = -∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
44	43	adantll 710	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = -∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
45	29, 36, 44	3jaodan 1428	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
46	45	anasss 466	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
47		pnfnlt 12793	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ^* → ¬ +∞ < 𝐵)
48	47	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ¬ +∞ < 𝐵)
49		breq1 5073	. . . . . . . . . 10 ⊢ (𝐴 = +∞ → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
50	49	adantr 480	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
51	48, 50	mtbird 324	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ¬ 𝐴 < 𝐵)
52	51	pm2.21d 121	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → 𝐴 < 𝐶))
53	52	adantrd 491	. . . . . 6 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
54	53	adantrr 713	. . . . 5 ⊢ ((𝐴 = +∞ ∧ (𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
55		mnflt 12788	. . . . . . . . . . 11 ⊢ (𝐶 ∈ ℝ → -∞ < 𝐶)
56	55	adantl 481	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → -∞ < 𝐶)
57		breq1 5073	. . . . . . . . . . 11 ⊢ (𝐴 = -∞ → (𝐴 < 𝐶 ↔ -∞ < 𝐶))
58	57	adantr 480	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 ↔ -∞ < 𝐶))
59	56, 58	mpbird 256	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → 𝐴 < 𝐶)
60	59	a1d 25	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
61	60	adantlr 711	. . . . . . 7 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
62		mnfltpnf 12791	. . . . . . . . . 10 ⊢ -∞ < +∞
63		breq12 5075	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐶 = +∞) → (𝐴 < 𝐶 ↔ -∞ < +∞))
64	62, 63	mpbiri 257	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
65	64	a1d 25	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐶 = +∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
66	65	adantlr 711	. . . . . . 7 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = +∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
67	43	adantll 710	. . . . . . 7 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 = -∞) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
68	61, 66, 67	3jaodan 1428	. . . . . 6 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
69	68	anasss 466	. . . . 5 ⊢ ((𝐴 = -∞ ∧ (𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
70	46, 54, 69	3jaoian 1427	. . . 4 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ (𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
71	70	3impb 1113	. . 3 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
72	2, 71	syl3an3b 1403	. 2 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
73	1, 72	syl3an1b 1401	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ w3o 1084 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 class class class wbr 5070 ℝcr 10801 +∞cpnf 10937 -∞cmnf 10938 ℝ^*cxr 10939 < clt 10940

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-pre-lttrn 10877

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945

This theorem is referenced by: xrltso 12804 xrlelttr 12819 xrltletr 12820 xrlttrd 12822 xrub 12975 ioo0 13033 ioojoin 13144 hashgt23el 14067 leordtval2 22271 icopnfcld 23837 iocmnfcld 23838 ismbf3d 24723 tanord1 25598 tan2h 35696 asindmre 35787 iccpartlt 44764

W3C validator