![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > renepnf | Structured version Visualization version GIF version |
Description: No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Ref | Expression |
---|---|
renepnf | ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pnfnre 10418 | . . . 4 ⊢ +∞ ∉ ℝ | |
2 | 1 | neli 3077 | . . 3 ⊢ ¬ +∞ ∈ ℝ |
3 | eleq1 2847 | . . 3 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ)) | |
4 | 2, 3 | mtbiri 319 | . 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ) |
5 | 4 | necon2ai 2998 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 ∈ wcel 2107 ≠ wne 2969 ℝcr 10271 +∞cpnf 10408 |
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 5017 ax-nul 5025 ax-pr 5138 ax-un 7226 ax-resscn 10329 |
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-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-nel 3076 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-pw 4381 df-sn 4399 df-pr 4401 df-uni 4672 df-pnf 10413 |
This theorem is referenced by: renepnfd 10427 renfdisj 10437 xrnepnf 12263 rexneg 12354 rexadd 12375 xaddnepnf 12380 xaddcom 12383 xaddid1 12384 xnn0xadd0 12389 xnegdi 12390 xpncan 12393 xleadd1a 12395 rexmul 12413 xmulpnf1 12416 xadddilem 12436 rpsup 12984 hashneq0 13470 hash1snb 13521 xrsnsgrp 20178 xaddeq0 30083 icorempt2 33794 ovoliunnfl 34077 voliunnfl 34079 volsupnfl 34080 supxrgelem 40461 supxrge 40462 infleinflem1 40494 infleinflem2 40495 xrre4 40544 supminfxr2 40604 climxrre 40890 sge0repnf 41527 voliunsge0lem 41613 |
Copyright terms: Public domain | W3C validator |