![]() |
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 | df-pnf 11291 | . . . 4 ⊢ +∞ = 𝒫 ∪ ℂ | |
2 | pwuninel 8282 | . . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ | |
3 | 1, 2 | eqneltri 2845 | . . 3 ⊢ ¬ +∞ ∈ ℂ |
4 | recn 11239 | . . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ) | |
5 | 3, 4 | mto 196 | . 2 ⊢ ¬ +∞ ∈ ℝ |
6 | 5 | nelir 3039 | 1 ⊢ +∞ ∉ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 ∉ wnel 3036 𝒫 cpw 4597 ∪ cuni 4905 ℂcc 11147 ℝcr 11148 +∞cpnf 11286 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-sep 5296 ax-pr 5425 ax-un 7738 ax-resscn 11206 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-nel 3037 df-rab 3420 df-v 3464 df-un 3951 df-in 3953 df-ss 3963 df-pw 4599 df-sn 4624 df-pr 4626 df-uni 4906 df-pnf 11291 |
This theorem is referenced by: pnfnre2 11297 renepnf 11303 ltxrlt 11325 nn0nepnf 12598 xrltnr 13147 pnfnlt 13156 xnn0lenn0nn0 13272 hashclb 14370 hasheq0 14375 pcgcd1 16874 pc2dvds 16876 ramtcl2 17008 odhash3 19570 xrsdsreclblem 21405 pnfnei 23212 iccpnfcnv 24957 i1f0rn 25699 |
Copyright terms: Public domain | W3C validator |