![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xrlelttrd | 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 | ⊢ (𝜑 → 𝐶 ∈ ℝ*) |
xrlelttrd.4 | ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
xrlelttrd.5 | ⊢ (𝜑 → 𝐵 < 𝐶) |
Ref | Expression |
---|---|
xrlelttrd | ⊢ (𝜑 → 𝐴 < 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xrlelttrd.4 | . 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵) | |
2 | xrlelttrd.5 | . 2 ⊢ (𝜑 → 𝐵 < 𝐶) | |
3 | xrlttrd.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ*) | |
4 | xrlttrd.2 | . . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ*) | |
5 | xrlttrd.3 | . . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ*) | |
6 | xrlelttr 12172 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | |
7 | 3, 4, 5, 6 | syl3anc 1473 | . 2 ⊢ (𝜑 → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
8 | 1, 2, 7 | mp2and 717 | 1 ⊢ (𝜑 → 𝐴 < 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 2131 class class class wbr 4796 ℝ*cxr 10257 < clt 10258 ≤ cle 10259 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-8 2133 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-sep 4925 ax-nul 4933 ax-pow 4984 ax-pr 5047 ax-un 7106 ax-cnex 10176 ax-resscn 10177 ax-pre-lttri 10194 ax-pre-lttrn 10195 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ne 2925 df-nel 3028 df-ral 3047 df-rex 3048 df-rab 3051 df-v 3334 df-sbc 3569 df-csb 3667 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-nul 4051 df-if 4223 df-pw 4296 df-sn 4314 df-pr 4316 df-op 4320 df-uni 4581 df-br 4797 df-opab 4857 df-mpt 4874 df-id 5166 df-po 5179 df-so 5180 df-xp 5264 df-rel 5265 df-cnv 5266 df-co 5267 df-dm 5268 df-rn 5269 df-res 5270 df-ima 5271 df-iota 6004 df-fun 6043 df-fn 6044 df-f 6045 df-f1 6046 df-fo 6047 df-f1o 6048 df-fv 6049 df-er 7903 df-en 8114 df-dom 8115 df-sdom 8116 df-pnf 10260 df-mnf 10261 df-xr 10262 df-ltxr 10263 df-le 10264 |
This theorem is referenced by: xlt2add 12275 ixxub 12381 elioc2 12421 elicc2 12423 limsupgre 14403 xrsdsreclblem 19986 mnfnei 21219 blgt0 22397 xblss2ps 22399 xblss2 22400 metustexhalf 22554 tgioo 22792 blcvx 22794 xrge0tsms 22830 metdcnlem 22832 metdscnlem 22851 ioombl 23525 uniioombllem1 23541 dvferm2lem 23940 dvlip2 23949 ftc1a 23991 coe1mul3 24050 ply1remlem 24113 pserulm 24367 isblo3i 27957 xrge0infss 29826 iocinioc2 29842 xrge0tsmsd 30086 sibfinima 30702 heicant 33749 itg2gt0cn 33770 ftc1anclem7 33796 ftc1anc 33798 idomrootle 38267 supxrgelem 40043 supxrge 40044 xralrple2 40060 infxr 40073 infleinflem2 40077 xrralrecnnle 40092 unb2ltle 40132 eliocre 40229 iocopn 40241 ge0lere 40254 iccdificc 40261 limsupre 40368 limsuppnflem 40437 limsupre3lem 40459 xlimmnfv 40555 fourierdlem27 40846 sge0isum 41139 meassre 41189 meaiuninclem 41192 omessre 41222 omeiunltfirp 41231 sge0hsphoire 41301 hoidmv1lelem1 41303 hoidmv1lelem2 41304 hoidmv1lelem3 41305 hoidmvlelem1 41307 hoidmvlelem4 41310 pimiooltgt 41419 pimincfltioc 41424 preimaleiinlt 41429 |
Copyright terms: Public domain | W3C validator |