![]() |
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 12272 | . 2 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → -∞ < 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 class class class wbr 4888 ℝcr 10273 -∞cmnf 10411 < clt 10413 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5019 ax-nul 5027 ax-pow 5079 ax-pr 5140 ax-un 7228 ax-cnex 10330 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4674 df-br 4889 df-opab 4951 df-xp 5363 df-pnf 10415 df-mnf 10416 df-xr 10417 df-ltxr 10418 |
This theorem is referenced by: qbtwnxr 12347 xltnegi 12363 supxrre 12473 infxrre 12482 caucvgrlem 14815 ovoliunlem1 23710 areacirclem5 34134 infleinflem2 40505 xrralrecnnge 40529 icoopn 40670 icomnfinre 40697 ressiocsup 40699 ressioosup 40700 preimaiocmnf 40706 limciccioolb 40771 limsupre 40791 limcresioolb 40793 limcleqr 40794 xlimmnfvlem1 40982 fourierdlem32 41293 fourierdlem46 41306 fourierdlem48 41308 fourierdlem49 41309 fourierdlem74 41334 fourierdlem88 41348 fourierdlem95 41355 fourierdlem103 41363 fourierdlem104 41364 fouriersw 41385 ioorrnopnxrlem 41460 hspdifhsp 41767 hspmbllem2 41778 pimltmnf2 41848 pimgtmnf2 41861 smfsuplem1 41954 |
Copyright terms: Public domain | W3C validator |