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 11016 | . . . 4 ⊢ +∞ ∉ ℝ | |
2 | 1 | neli 3051 | . . 3 ⊢ ¬ +∞ ∈ ℝ |
3 | eleq1 2826 | . . 3 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ)) | |
4 | 2, 3 | mtbiri 327 | . 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ) |
5 | 4 | necon2ai 2973 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ℝcr 10870 +∞cpnf 11006 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 ax-un 7588 ax-resscn 10928 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ne 2944 df-nel 3050 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-pw 4535 df-sn 4562 df-pr 4564 df-uni 4840 df-pnf 11011 |
This theorem is referenced by: renepnfd 11026 renfdisj 11035 xrnepnf 12854 rexneg 12945 rexadd 12966 xaddnepnf 12971 xaddcom 12974 xaddid1 12975 xnn0xadd0 12981 xnegdi 12982 xpncan 12985 xleadd1a 12987 rexmul 13005 xmulpnf1 13008 xadddilem 13028 rpsup 13586 hashneq0 14079 hash1snb 14134 xrsnsgrp 20634 xaddeq0 31076 icorempo 35522 ovoliunnfl 35819 voliunnfl 35821 volsupnfl 35822 supxrgelem 42876 supxrge 42877 infleinflem1 42909 infleinflem2 42910 xrre4 42951 supminfxr2 43009 climxrre 43291 sge0repnf 43924 voliunsge0lem 44010 |
Copyright terms: Public domain | W3C validator |