![]() |
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 11287 | . . . 4 ⊢ +∞ ∉ ℝ | |
2 | 1 | neli 3037 | . . 3 ⊢ ¬ +∞ ∈ ℝ |
3 | eleq1 2813 | . . 3 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ)) | |
4 | 2, 3 | mtbiri 326 | . 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ) |
5 | 4 | necon2ai 2959 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 ≠ wne 2929 ℝcr 11139 +∞cpnf 11277 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-pr 5429 ax-un 7741 ax-resscn 11197 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ne 2930 df-nel 3036 df-rab 3419 df-v 3463 df-un 3949 df-in 3951 df-ss 3961 df-pw 4606 df-sn 4631 df-pr 4633 df-uni 4910 df-pnf 11282 |
This theorem is referenced by: renepnfd 11297 renfdisj 11306 xrnepnf 13133 rexneg 13225 rexadd 13246 xaddnepnf 13251 xaddcom 13254 xaddrid 13255 xnn0xadd0 13261 xnegdi 13262 xpncan 13265 xleadd1a 13267 rexmul 13285 xmulpnf1 13288 xadddilem 13308 rpsup 13867 hashneq0 14359 hash1snb 14414 xrsnsgrp 21352 xaddeq0 32605 icorempo 36961 ovoliunnfl 37266 voliunnfl 37268 volsupnfl 37269 supxrgelem 44857 supxrge 44858 infleinflem1 44890 infleinflem2 44891 xrre4 44931 supminfxr2 44989 climxrre 45276 sge0repnf 45912 voliunsge0lem 45998 |
Copyright terms: Public domain | W3C validator |