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 7401 | . . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ | |
2 | df-pnf 10076 | . . . . 5 ⊢ +∞ = 𝒫 ∪ ℂ | |
3 | 2 | eleq1i 2692 | . . . 4 ⊢ (+∞ ∈ ℂ ↔ 𝒫 ∪ ℂ ∈ ℂ) |
4 | 1, 3 | mtbir 313 | . . 3 ⊢ ¬ +∞ ∈ ℂ |
5 | recn 10026 | . . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ) | |
6 | 4, 5 | mto 188 | . 2 ⊢ ¬ +∞ ∈ ℝ |
7 | 6 | nelir 2900 | 1 ⊢ +∞ ∉ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1990 ∉ wnel 2897 𝒫 cpw 4158 ∪ cuni 4436 ℂcc 9934 ℝcr 9935 +∞cpnf 10071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 ax-un 6949 ax-resscn 9993 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-nel 2898 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-pw 4160 df-sn 4178 df-pr 4180 df-uni 4437 df-pnf 10076 |
This theorem is referenced by: renepnf 10087 ltxrlt 10108 nn0nepnf 11371 xrltnr 11953 pnfnlt 11962 xnn0lenn0nn0 12075 hashclb 13149 hasheq0 13154 pcgcd1 15581 pc2dvds 15583 ramtcl2 15715 odhash3 17991 xrsdsreclblem 19792 pnfnei 21024 iccpnfcnv 22743 i1f0rn 23449 pnfnre2 39628 |
Copyright terms: Public domain | W3C validator |