This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrlttr

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

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

Proof

Step Hyp Ref Expression
1 elxr ⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
2 elxr ⊢ ( 𝐶 ∈ ℝ* ↔ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) )
3 elxr ⊢ ( 𝐵 ∈ ℝ* ↔ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) )
4 lttr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
5 4 3expa ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
6 5 an32s ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
7 rexr ⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℝ* )
8 pnfnlt ⊢ ( 𝐶 ∈ ℝ* → ¬ +∞ < 𝐶 )
9 7 8 syl ⊢ ( 𝐶 ∈ ℝ → ¬ +∞ < 𝐶 )
10 9 adantr ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 = +∞ ) → ¬ +∞ < 𝐶 )
11 breq1 ⊢ ( 𝐵 = +∞ → ( 𝐵 < 𝐶 ↔ +∞ < 𝐶 ) )
12 11 adantl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 = +∞ ) → ( 𝐵 < 𝐶 ↔ +∞ < 𝐶 ) )
13 10 12 mtbird ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 = +∞ ) → ¬ 𝐵 < 𝐶 )
14 13 pm2.21d ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 = +∞ ) → ( 𝐵 < 𝐶 → 𝐴 < 𝐶 ) )
15 14 adantll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 = +∞ ) → ( 𝐵 < 𝐶 → 𝐴 < 𝐶 ) )
16 15 adantld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 = +∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
17 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
18 nltmnf ⊢ ( 𝐴 ∈ ℝ* → ¬ 𝐴 < -∞ )
19 17 18 syl ⊢ ( 𝐴 ∈ ℝ → ¬ 𝐴 < -∞ )
20 19 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → ¬ 𝐴 < -∞ )
21 breq2 ⊢ ( 𝐵 = -∞ → ( 𝐴 < 𝐵 ↔ 𝐴 < -∞ ) )
22 21 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → ( 𝐴 < 𝐵 ↔ 𝐴 < -∞ ) )
23 20 22 mtbird ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → ¬ 𝐴 < 𝐵 )
24 23 pm2.21d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → ( 𝐴 < 𝐵 → 𝐴 < 𝐶 ) )
25 24 adantlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 = -∞ ) → ( 𝐴 < 𝐵 → 𝐴 < 𝐶 ) )
26 25 adantrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 = -∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
27 6 16 26 3jaodan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
28 3 27 sylan2b ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
29 28 an32s ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
30 ltpnf ⊢ ( 𝐴 ∈ ℝ → 𝐴 < +∞ )
31 30 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 = +∞ ) → 𝐴 < +∞ )
32 breq2 ⊢ ( 𝐶 = +∞ → ( 𝐴 < 𝐶 ↔ 𝐴 < +∞ ) )
33 32 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 = +∞ ) → ( 𝐴 < 𝐶 ↔ 𝐴 < +∞ ) )
34 31 33 mpbird ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 = +∞ ) → 𝐴 < 𝐶 )
35 34 adantlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 = +∞ ) → 𝐴 < 𝐶 )
36 35 a1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 = +∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
37 nltmnf ⊢ ( 𝐵 ∈ ℝ* → ¬ 𝐵 < -∞ )
38 37 adantr ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 = -∞ ) → ¬ 𝐵 < -∞ )
39 breq2 ⊢ ( 𝐶 = -∞ → ( 𝐵 < 𝐶 ↔ 𝐵 < -∞ ) )
40 39 adantl ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 = -∞ ) → ( 𝐵 < 𝐶 ↔ 𝐵 < -∞ ) )
41 38 40 mtbird ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 = -∞ ) → ¬ 𝐵 < 𝐶 )
42 41 pm2.21d ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 = -∞ ) → ( 𝐵 < 𝐶 → 𝐴 < 𝐶 ) )
43 42 adantld ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 = -∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
44 43 adantll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 = -∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
45 29 36 44 3jaodan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
46 45 anasss ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
47 pnfnlt ⊢ ( 𝐵 ∈ ℝ* → ¬ +∞ < 𝐵 )
48 47 adantl ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ¬ +∞ < 𝐵 )
49 breq1 ⊢ ( 𝐴 = +∞ → ( 𝐴 < 𝐵 ↔ +∞ < 𝐵 ) )
50 49 adantr ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ +∞ < 𝐵 ) )
51 48 50 mtbird ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ¬ 𝐴 < 𝐵 )
52 51 pm2.21d ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → 𝐴 < 𝐶 ) )
53 52 adantrd ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
54 53 adantrr ⊢ ( ( 𝐴 = +∞ ∧ ( 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
55 mnflt ⊢ ( 𝐶 ∈ ℝ → -∞ < 𝐶 )
56 55 adantl ⊢ ( ( 𝐴 = -∞ ∧ 𝐶 ∈ ℝ ) → -∞ < 𝐶 )
57 breq1 ⊢ ( 𝐴 = -∞ → ( 𝐴 < 𝐶 ↔ -∞ < 𝐶 ) )
58 57 adantr ⊢ ( ( 𝐴 = -∞ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐶 ↔ -∞ < 𝐶 ) )
59 56 58 mpbird ⊢ ( ( 𝐴 = -∞ ∧ 𝐶 ∈ ℝ ) → 𝐴 < 𝐶 )
60 59 a1d ⊢ ( ( 𝐴 = -∞ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
61 60 adantlr ⊢ ( ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
62 mnfltpnf ⊢ -∞ < +∞
63 breq12 ⊢ ( ( 𝐴 = -∞ ∧ 𝐶 = +∞ ) → ( 𝐴 < 𝐶 ↔ -∞ < +∞ ) )
64 62 63 mpbiri ⊢ ( ( 𝐴 = -∞ ∧ 𝐶 = +∞ ) → 𝐴 < 𝐶 )
65 64 a1d ⊢ ( ( 𝐴 = -∞ ∧ 𝐶 = +∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
66 65 adantlr ⊢ ( ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 = +∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
67 43 adantll ⊢ ( ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 = -∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
68 61 66 67 3jaodan ⊢ ( ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
69 68 anasss ⊢ ( ( 𝐴 = -∞ ∧ ( 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
70 46 54 69 3jaoian ⊢ ( ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
71 70 3impb ⊢ ( ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) ∧ 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
72 2 71 syl3an3b ⊢ ( ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
73 1 72 syl3an1b ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )