| 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 11302 | . . . 4 ⊢ +∞ ∉ ℝ | |
| 2 | 1 | neli 3048 | . . 3 ⊢ ¬ +∞ ∈ ℝ |
| 3 | eleq1 2829 | . . 3 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ)) | |
| 4 | 2, 3 | mtbiri 327 | . 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ) |
| 5 | 4 | necon2ai 2970 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ℝcr 11154 +∞cpnf 11292 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-pr 5432 ax-un 7755 ax-resscn 11212 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-nel 3047 df-rab 3437 df-v 3482 df-un 3956 df-in 3958 df-ss 3968 df-pw 4602 df-sn 4627 df-pr 4629 df-uni 4908 df-pnf 11297 |
| This theorem is referenced by: renepnfd 11312 renfdisj 11321 xrnepnf 13160 rexneg 13253 rexadd 13274 xaddnepnf 13279 xaddcom 13282 xaddrid 13283 xnn0xadd0 13289 xnegdi 13290 xpncan 13293 xleadd1a 13295 rexmul 13313 xmulpnf1 13316 xadddilem 13336 rpsup 13906 hashneq0 14403 hash1snb 14458 xrsnsgrp 21420 xaddeq0 32757 icorempo 37352 ovoliunnfl 37669 voliunnfl 37671 volsupnfl 37672 supxrgelem 45348 supxrge 45349 infleinflem1 45381 infleinflem2 45382 xrre4 45422 supminfxr2 45480 climxrre 45765 sge0repnf 46401 voliunsge0lem 46487 |
| Copyright terms: Public domain | W3C validator |