Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xrltletrd | Structured version Visualization version GIF version |
Description: Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
Ref | Expression |
---|---|
xrlttrd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ*) |
xrlttrd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ*) |
xrlttrd.3 | ⊢ (𝜑 → 𝐶 ∈ ℝ*) |
xrltletrd.4 | ⊢ (𝜑 → 𝐴 < 𝐵) |
xrltletrd.5 | ⊢ (𝜑 → 𝐵 ≤ 𝐶) |
Ref | Expression |
---|---|
xrltletrd | ⊢ (𝜑 → 𝐴 < 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xrltletrd.4 | . 2 ⊢ (𝜑 → 𝐴 < 𝐵) | |
2 | xrltletrd.5 | . 2 ⊢ (𝜑 → 𝐵 ≤ 𝐶) | |
3 | xrlttrd.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ*) | |
4 | xrlttrd.2 | . . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ*) | |
5 | xrlttrd.3 | . . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ*) | |
6 | xrltletr 12730 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) | |
7 | 3, 4, 5, 6 | syl3anc 1373 | . 2 ⊢ (𝜑 → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) |
8 | 1, 2, 7 | mp2and 699 | 1 ⊢ (𝜑 → 𝐴 < 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2110 class class class wbr 5043 ℝ*cxr 10849 < clt 10850 ≤ cle 10851 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-sep 5181 ax-nul 5188 ax-pow 5247 ax-pr 5311 ax-un 7512 ax-cnex 10768 ax-resscn 10769 ax-pre-lttri 10786 ax-pre-lttrn 10787 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-rab 3063 df-v 3403 df-sbc 3688 df-csb 3803 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-nul 4228 df-if 4430 df-pw 4505 df-sn 4532 df-pr 4534 df-op 4538 df-uni 4810 df-br 5044 df-opab 5106 df-mpt 5125 df-id 5444 df-po 5457 df-so 5458 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-res 5552 df-ima 5553 df-iota 6327 df-fun 6371 df-fn 6372 df-f 6373 df-f1 6374 df-fo 6375 df-f1o 6376 df-fv 6377 df-er 8380 df-en 8616 df-dom 8617 df-sdom 8618 df-pnf 10852 df-mnf 10853 df-xr 10854 df-ltxr 10855 df-le 10856 |
This theorem is referenced by: xlt2add 12833 xadddi2 12870 supxrre 12900 infxrre 12909 ixxlb 12940 elicore 12970 elico2 12982 elicc2 12983 caucvgrlem 15219 isnzr2hash 20274 xrsdsreclblem 20381 xblss2ps 23271 xblss2 23272 tgioo 23665 xrge0tsms 23703 xrhmeo 23815 ovoliunlem1 24371 ovoliun 24374 ioombl1lem2 24428 vitalilem4 24480 itg2monolem2 24621 itg2gt0 24630 dvferm1lem 24853 dvferm2lem 24855 lhop1lem 24882 pserdvlem2 25292 abelthlem3 25297 logtayl 25520 xrge0tsmsd 31008 esum2d 31745 usgrcyclgt2v 32778 relowlssretop 35228 itg2gt0cn 35526 areacirclem5 35563 xrge0nemnfd 42496 supxrgere 42497 supxrgelem 42501 infrpge 42515 xrralrecnnge 42555 supxrunb3 42564 icoopn 42690 limsupre 42811 limsupre3lem 42902 xlimpnfv 43008 fourierdlem27 43304 fourierdlem87 43363 gsumge0cl 43538 sge0pr 43561 sge0ssre 43564 sge0xaddlem1 43600 meaiuninc3v 43651 pimiooltgt 43874 pimdecfgtioc 43878 preimageiingt 43883 |
Copyright terms: Public domain | W3C validator |