![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pnfnre | Structured version Visualization version GIF version |
Description: Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
Ref | Expression |
---|---|
pnfnre | ⊢ +∞ ∉ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwuninel 7666 | . . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ | |
2 | df-pnf 10393 | . . . . 5 ⊢ +∞ = 𝒫 ∪ ℂ | |
3 | 2 | eleq1i 2897 | . . . 4 ⊢ (+∞ ∈ ℂ ↔ 𝒫 ∪ ℂ ∈ ℂ) |
4 | 1, 3 | mtbir 315 | . . 3 ⊢ ¬ +∞ ∈ ℂ |
5 | recn 10342 | . . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ) | |
6 | 4, 5 | mto 189 | . 2 ⊢ ¬ +∞ ∈ ℝ |
7 | 6 | nelir 3105 | 1 ⊢ +∞ ∉ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2166 ∉ wnel 3102 𝒫 cpw 4378 ∪ cuni 4658 ℂcc 10250 ℝcr 10251 +∞cpnf 10388 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 ax-sep 5005 ax-nul 5013 ax-pr 5127 ax-un 7209 ax-resscn 10309 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-nel 3103 df-rex 3123 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-pw 4380 df-sn 4398 df-pr 4400 df-uni 4659 df-pnf 10393 |
This theorem is referenced by: renepnf 10404 ltxrlt 10427 nn0nepnf 11698 xrltnr 12239 pnfnlt 12248 xnn0lenn0nn0 12363 hashclb 13439 hasheq0 13444 pcgcd1 15952 pc2dvds 15954 ramtcl2 16086 odhash3 18342 xrsdsreclblem 20152 pnfnei 21395 iccpnfcnv 23113 i1f0rn 23848 pnfnre2 40423 |
Copyright terms: Public domain | W3C validator |