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

Theorem xrlttr 12349
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 12327 . 2 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2 elxr 12327 . . 3 (𝐶 ∈ ℝ* ↔ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))
3 elxr 12327 . . . . . . . . 9 (𝐵 ∈ ℝ* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
4 lttr 10516 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
543expa 1099 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
65an32s 640 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
7 rexr 10485 . . . . . . . . . . . . . . . 16 (𝐶 ∈ ℝ → 𝐶 ∈ ℝ*)
8 pnfnlt 12339 . . . . . . . . . . . . . . . 16 (𝐶 ∈ ℝ* → ¬ +∞ < 𝐶)
97, 8syl 17 . . . . . . . . . . . . . . 15 (𝐶 ∈ ℝ → ¬ +∞ < 𝐶)
109adantr 473 . . . . . . . . . . . . . 14 ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → ¬ +∞ < 𝐶)
11 breq1 4929 . . . . . . . . . . . . . . 15 (𝐵 = +∞ → (𝐵 < 𝐶 ↔ +∞ < 𝐶))
1211adantl 474 . . . . . . . . . . . . . 14 ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 < 𝐶 ↔ +∞ < 𝐶))
1310, 12mtbird 317 . . . . . . . . . . . . 13 ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → ¬ 𝐵 < 𝐶)
1413pm2.21d 119 . . . . . . . . . . . 12 ((𝐶 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 < 𝐶𝐴 < 𝐶))
1514adantll 702 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = +∞) → (𝐵 < 𝐶𝐴 < 𝐶))
1615adantld 483 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = +∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
17 rexr 10485 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
18 nltmnf 12340 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℝ* → ¬ 𝐴 < -∞)
1917, 18syl 17 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℝ → ¬ 𝐴 < -∞)
2019adantr 473 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
21 breq2 4930 . . . . . . . . . . . . . . 15 (𝐵 = -∞ → (𝐴 < 𝐵𝐴 < -∞))
2221adantl 474 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵𝐴 < -∞))
2320, 22mtbird 317 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
2423pm2.21d 119 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵𝐴 < 𝐶))
2524adantlr 703 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = -∞) → (𝐴 < 𝐵𝐴 < 𝐶))
2625adantrd 484 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 = -∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
276, 16, 263jaodan 1411 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
283, 27sylan2b 585 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ∈ ℝ*) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
2928an32s 640 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
30 ltpnf 12331 . . . . . . . . . . 11 (𝐴 ∈ ℝ → 𝐴 < +∞)
3130adantr 473 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → 𝐴 < +∞)
32 breq2 4930 . . . . . . . . . . 11 (𝐶 = +∞ → (𝐴 < 𝐶𝐴 < +∞))
3332adantl 474 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → (𝐴 < 𝐶𝐴 < +∞))
3431, 33mpbird 249 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
3534adantlr 703 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
3635a1d 25 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 = +∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
37 nltmnf 12340 . . . . . . . . . . . 12 (𝐵 ∈ ℝ* → ¬ 𝐵 < -∞)
3837adantr 473 . . . . . . . . . . 11 ((𝐵 ∈ ℝ*𝐶 = -∞) → ¬ 𝐵 < -∞)
39 breq2 4930 . . . . . . . . . . . 12 (𝐶 = -∞ → (𝐵 < 𝐶𝐵 < -∞))
4039adantl 474 . . . . . . . . . . 11 ((𝐵 ∈ ℝ*𝐶 = -∞) → (𝐵 < 𝐶𝐵 < -∞))
4138, 40mtbird 317 . . . . . . . . . 10 ((𝐵 ∈ ℝ*𝐶 = -∞) → ¬ 𝐵 < 𝐶)
4241pm2.21d 119 . . . . . . . . 9 ((𝐵 ∈ ℝ*𝐶 = -∞) → (𝐵 < 𝐶𝐴 < 𝐶))
4342adantld 483 . . . . . . . 8 ((𝐵 ∈ ℝ*𝐶 = -∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
4443adantll 702 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 = -∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
4529, 36, 443jaodan 1411 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
4645anasss 459 . . . . 5 ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
47 pnfnlt 12339 . . . . . . . . . 10 (𝐵 ∈ ℝ* → ¬ +∞ < 𝐵)
4847adantl 474 . . . . . . . . 9 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → ¬ +∞ < 𝐵)
49 breq1 4929 . . . . . . . . . 10 (𝐴 = +∞ → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
5049adantr 473 . . . . . . . . 9 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
5148, 50mtbird 317 . . . . . . . 8 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → ¬ 𝐴 < 𝐵)
5251pm2.21d 119 . . . . . . 7 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵𝐴 < 𝐶))
5352adantrd 484 . . . . . 6 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
5453adantrr 705 . . . . 5 ((𝐴 = +∞ ∧ (𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
55 mnflt 12334 . . . . . . . . . . 11 (𝐶 ∈ ℝ → -∞ < 𝐶)
5655adantl 474 . . . . . . . . . 10 ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → -∞ < 𝐶)
57 breq1 4929 . . . . . . . . . . 11 (𝐴 = -∞ → (𝐴 < 𝐶 ↔ -∞ < 𝐶))
5857adantr 473 . . . . . . . . . 10 ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 ↔ -∞ < 𝐶))
5956, 58mpbird 249 . . . . . . . . 9 ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → 𝐴 < 𝐶)
6059a1d 25 . . . . . . . 8 ((𝐴 = -∞ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
6160adantlr 703 . . . . . . 7 (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
62 mnfltpnf 12337 . . . . . . . . . 10 -∞ < +∞
63 breq12 4931 . . . . . . . . . 10 ((𝐴 = -∞ ∧ 𝐶 = +∞) → (𝐴 < 𝐶 ↔ -∞ < +∞))
6462, 63mpbiri 250 . . . . . . . . 9 ((𝐴 = -∞ ∧ 𝐶 = +∞) → 𝐴 < 𝐶)
6564a1d 25 . . . . . . . 8 ((𝐴 = -∞ ∧ 𝐶 = +∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
6665adantlr 703 . . . . . . 7 (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 = +∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
6743adantll 702 . . . . . . 7 (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 = -∞) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
6861, 66, 673jaodan 1411 . . . . . 6 (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
6968anasss 459 . . . . 5 ((𝐴 = -∞ ∧ (𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
7046, 54, 693jaoian 1410 . . . 4 (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ (𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
71703impb 1096 . . 3 (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
722, 71syl3an3b 1386 . 2 (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
731, 72syl3an1b 1384 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  w3o 1068  w3a 1069   = wceq 1508  wcel 2051   class class class wbr 4926  cr 10333  +∞cpnf 10470  -∞cmnf 10471  *cxr 10472   < clt 10473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-cnex 10390  ax-resscn 10391  ax-pre-lttrn 10409
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-nel 3069  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-opab 4989  df-mpt 5006  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-er 8088  df-en 8306  df-dom 8307  df-sdom 8308  df-pnf 10475  df-mnf 10476  df-xr 10477  df-ltxr 10478
This theorem is referenced by:  xrltso  12350  xrlelttr  12365  xrltletr  12366  xrlttrd  12368  xrub  12520  ioo0  12578  ioojoin  12684  hashgt23el  13597  leordtval2  21540  icopnfcld  23095  iocmnfcld  23096  ismbf3d  23974  tanord1  24838  tan2h  34358  asindmre  34451  iccpartlt  42986
  Copyright terms: Public domain W3C validator