MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrlttr Structured version   Visualization version   GIF version

Theorem xrlttr 13122
Description: Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.)
Assertion
Ref Expression
xrlttr ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))

Proof of Theorem xrlttr
StepHypRef Expression
1 elxr 13099 . 2 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2 elxr 13099 . . 3 (𝐶 ∈ ℝ* ↔ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))
3 elxr 13099 . . . . . . . . 9 (𝐵 ∈ ℝ* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
4 lttr 11291 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
543expa 1115 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
65an32s 649 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
7 rexr 11261 . . . . . . . . . . . . . . . 16 (𝐶 ∈ ℝ → 𝐶 ∈ ℝ*)
8 pnfnlt 13111 . . . . . . . . . . . . . . . 16 (𝐶 ∈ ℝ* → ¬ +∞ < 𝐶)
97, 8syl 17 . . . . . . . . . . . . . . 15 (𝐶 ∈ ℝ → ¬ +∞ < 𝐶)
109adantr 480 . . . . . . . . . . . . . 14 ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → ¬ +∞ < 𝐶)
11 breq1 5144 . . . . . . . . . . . . . . 15 (𝐵 = +∞ → (𝐵 < 𝐶 ↔ +∞ < 𝐶))
1211adantl 481 . . . . . . . . . . . . . 14 ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 < 𝐶 ↔ +∞ < 𝐶))
1310, 12mtbird 325 . . . . . . . . . . . . 13 ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → ¬ 𝐵 < 𝐶)
1413pm2.21d 121 . . . . . . . . . . . 12 ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 < 𝐶𝐴 < 𝐶))
1514adantll 711 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = +∞) → (𝐵 < 𝐶𝐴 < 𝐶))
1615adantld 490 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = +∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
17 rexr 11261 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
18 nltmnf 13112 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℝ* → ¬ 𝐴 < -∞)
1917, 18syl 17 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℝ → ¬ 𝐴 < -∞)
2019adantr 480 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
21 breq2 5145 . . . . . . . . . . . . . . 15 (𝐵 = -∞ → (𝐴 < 𝐵𝐴 < -∞))
2221adantl 481 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵𝐴 < -∞))
2320, 22mtbird 325 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
2423pm2.21d 121 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵𝐴 < 𝐶))
2524adantlr 712 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = -∞) → (𝐴 < 𝐵𝐴 < 𝐶))
2625adantrd 491 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = -∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
276, 16, 263jaodan 1427 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
283, 27sylan2b 593 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ∈ ℝ*) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
2928an32s 649 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
30 ltpnf 13103 . . . . . . . . . . 11 (𝐴 ∈ ℝ → 𝐴 < +∞)
3130adantr 480 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → 𝐴 < +∞)
32 breq2 5145 . . . . . . . . . . 11 (𝐶 = +∞ → (𝐴 < 𝐶𝐴 < +∞))
3332adantl 481 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → (𝐴 < 𝐶𝐴 < +∞))
3431, 33mpbird 257 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
3534adantlr 712 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
3635a1d 25 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 = +∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
37 nltmnf 13112 . . . . . . . . . . . 12 (𝐵 ∈ ℝ* → ¬ 𝐵 < -∞)
3837adantr 480 . . . . . . . . . . 11 ((𝐵 ∈ ℝ*𝐶 = -∞) → ¬ 𝐵 < -∞)
39 breq2 5145 . . . . . . . . . . . 12 (𝐶 = -∞ → (𝐵 < 𝐶𝐵 < -∞))
4039adantl 481 . . . . . . . . . . 11 ((𝐵 ∈ ℝ*𝐶 = -∞) → (𝐵 < 𝐶𝐵 < -∞))
4138, 40mtbird 325 . . . . . . . . . 10 ((𝐵 ∈ ℝ*𝐶 = -∞) → ¬ 𝐵 < 𝐶)
4241pm2.21d 121 . . . . . . . . 9 ((𝐵 ∈ ℝ*𝐶 = -∞) → (𝐵 < 𝐶𝐴 < 𝐶))
4342adantld 490 . . . . . . . 8 ((𝐵 ∈ ℝ*𝐶 = -∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
4443adantll 711 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 = -∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
4529, 36, 443jaodan 1427 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
4645anasss 466 . . . . 5 ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
47 pnfnlt 13111 . . . . . . . . . 10 (𝐵 ∈ ℝ* → ¬ +∞ < 𝐵)
4847adantl 481 . . . . . . . . 9 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → ¬ +∞ < 𝐵)
49 breq1 5144 . . . . . . . . . 10 (𝐴 = +∞ → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
5049adantr 480 . . . . . . . . 9 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
5148, 50mtbird 325 . . . . . . . 8 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → ¬ 𝐴 < 𝐵)
5251pm2.21d 121 . . . . . . 7 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵𝐴 < 𝐶))
5352adantrd 491 . . . . . 6 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
5453adantrr 714 . . . . 5 ((𝐴 = +∞ ∧ (𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
55 mnflt 13106 . . . . . . . . . . 11 (𝐶 ∈ ℝ → -∞ < 𝐶)
5655adantl 481 . . . . . . . . . 10 ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → -∞ < 𝐶)
57 breq1 5144 . . . . . . . . . . 11 (𝐴 = -∞ → (𝐴 < 𝐶 ↔ -∞ < 𝐶))
5857adantr 480 . . . . . . . . . 10 ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 ↔ -∞ < 𝐶))
5956, 58mpbird 257 . . . . . . . . 9 ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → 𝐴 < 𝐶)
6059a1d 25 . . . . . . . 8 ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
6160adantlr 712 . . . . . . 7 (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
62 mnfltpnf 13109 . . . . . . . . . 10 -∞ < +∞
63 breq12 5146 . . . . . . . . . 10 ((𝐴 = -∞ ∧ 𝐶 = +∞) → (𝐴 < 𝐶 ↔ -∞ < +∞))
6462, 63mpbiri 258 . . . . . . . . 9 ((𝐴 = -∞ ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
6564a1d 25 . . . . . . . 8 ((𝐴 = -∞ ∧ 𝐶 = +∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
6665adantlr 712 . . . . . . 7 (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 = +∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
6743adantll 711 . . . . . . 7 (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 = -∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
6861, 66, 673jaodan 1427 . . . . . 6 (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
6968anasss 466 . . . . 5 ((𝐴 = -∞ ∧ (𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
7046, 54, 693jaoian 1426 . . . 4 (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ (𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
71703impb 1112 . . 3 (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
722, 71syl3an3b 1402 . 2 (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
731, 72syl3an1b 1400 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3o 1083  w3a 1084   = wceq 1533  wcel 2098   class class class wbr 5141  cr 11108  +∞cpnf 11246  -∞cmnf 11247  *cxr 11248   < clt 11249
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  ax-cnex 11165  ax-resscn 11166  ax-pre-lttrn 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254
This theorem is referenced by:  xrltso  13123  xrlelttr  13138  xrltletr  13139  xrlttrd  13141  xrub  13294  ioo0  13352  ioojoin  13463  hashgt23el  14387  leordtval2  23067  icopnfcld  24635  iocmnfcld  24636  ismbf3d  25534  tanord1  26422  tan2h  36991  asindmre  37082  iccpartlt  46645
  Copyright terms: Public domain W3C validator