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 10762 | . . . 4 ⊢ +∞ ∉ ℝ | |
2 | 1 | neli 3040 | . . 3 ⊢ ¬ +∞ ∈ ℝ |
3 | eleq1 2820 | . . 3 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ)) | |
4 | 2, 3 | mtbiri 330 | . 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ) |
5 | 4 | necon2ai 2963 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 ≠ wne 2934 ℝcr 10616 +∞cpnf 10752 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 ax-sep 5167 ax-nul 5174 ax-pr 5296 ax-un 7481 ax-resscn 10674 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-ne 2935 df-nel 3039 df-rab 3062 df-v 3400 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-nul 4212 df-pw 4490 df-sn 4517 df-pr 4519 df-uni 4797 df-pnf 10757 |
This theorem is referenced by: renepnfd 10772 renfdisj 10781 xrnepnf 12598 rexneg 12689 rexadd 12710 xaddnepnf 12715 xaddcom 12718 xaddid1 12719 xnn0xadd0 12725 xnegdi 12726 xpncan 12729 xleadd1a 12731 rexmul 12749 xmulpnf1 12752 xadddilem 12772 rpsup 13327 hashneq0 13819 hash1snb 13874 xrsnsgrp 20255 xaddeq0 30653 icorempo 35167 ovoliunnfl 35464 voliunnfl 35466 volsupnfl 35467 supxrgelem 42436 supxrge 42437 infleinflem1 42469 infleinflem2 42470 xrre4 42511 supminfxr2 42571 climxrre 42855 sge0repnf 43488 voliunsge0lem 43574 |
Copyright terms: Public domain | W3C validator |