![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mnfltd | Structured version Visualization version GIF version |
Description: Minus infinity is less than any (finite) real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
mnfltd.a | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
Ref | Expression |
---|---|
mnfltd | ⊢ (𝜑 → -∞ < 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mnfltd.a | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
2 | mnflt 12506 | . 2 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → -∞ < 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2111 class class class wbr 5030 ℝcr 10525 -∞cmnf 10662 < clt 10664 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-cnex 10582 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-xp 5525 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 |
This theorem is referenced by: qbtwnxr 12581 xltnegi 12597 supxrre 12708 infxrre 12717 caucvgrlem 15021 tgioo 23401 reconnlem1 23431 reconnlem2 23432 ovoliunlem1 24106 ovoliun 24109 ioombl1lem2 24163 ismbf3d 24258 dvferm1lem 24587 dvferm2lem 24589 degltlem1 24673 ply1divex 24737 dvdsq1p 24761 logdmnrp 25232 atans2 25517 areacirclem5 35149 infleinflem2 42003 xrralrecnnge 42026 icoopn 42162 icomnfinre 42189 ressiocsup 42191 ressioosup 42192 preimaiocmnf 42198 limciccioolb 42263 limsupre 42283 limcresioolb 42285 limcleqr 42286 xlimmnfvlem1 42474 fourierdlem32 42781 fourierdlem46 42794 fourierdlem48 42796 fourierdlem49 42797 fourierdlem74 42822 fourierdlem88 42836 fourierdlem95 42843 fourierdlem103 42851 fourierdlem104 42852 fouriersw 42873 ioorrnopnxrlem 42948 hspdifhsp 43255 hspmbllem2 43266 pimltmnf2 43336 pimgtmnf2 43349 smfsuplem1 43442 |
Copyright terms: Public domain | W3C validator |