![]() |
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 10700 | . . . 4 ⊢ +∞ = 𝒫 ∪ ℂ | |
2 | pwuninel 7944 | . . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ | |
3 | 1, 2 | eqneltri 2844 | . . 3 ⊢ ¬ +∞ ∈ ℂ |
4 | recn 10650 | . . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ) | |
5 | 3, 4 | mto 200 | . 2 ⊢ ¬ +∞ ∈ ℝ |
6 | 5 | nelir 3056 | 1 ⊢ +∞ ∉ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2112 ∉ wnel 3053 𝒫 cpw 4487 ∪ cuni 4791 ℂcc 10558 ℝcr 10559 +∞cpnf 10695 |
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 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-ext 2730 ax-sep 5162 ax-nul 5169 ax-pr 5291 ax-un 7452 ax-resscn 10617 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-tru 1542 df-ex 1783 df-sb 2071 df-clab 2737 df-cleq 2751 df-clel 2831 df-nel 3054 df-rab 3077 df-v 3409 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-nul 4222 df-pw 4489 df-sn 4516 df-pr 4518 df-uni 4792 df-pnf 10700 |
This theorem is referenced by: pnfnre2 10706 renepnf 10712 ltxrlt 10734 nn0nepnf 11999 xrltnr 12540 pnfnlt 12549 xnn0lenn0nn0 12664 hashclb 13754 hasheq0 13759 pcgcd1 16253 pc2dvds 16255 ramtcl2 16387 odhash3 18753 xrsdsreclblem 20197 pnfnei 21905 iccpnfcnv 23630 i1f0rn 24367 |
Copyright terms: Public domain | W3C validator |