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 10665 | . . . 4 ⊢ +∞ = 𝒫 ∪ ℂ | |
2 | pwuninel 7930 | . . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ | |
3 | 1, 2 | eqneltri 2903 | . . 3 ⊢ ¬ +∞ ∈ ℂ |
4 | recn 10615 | . . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ) | |
5 | 3, 4 | mto 198 | . 2 ⊢ ¬ +∞ ∈ ℝ |
6 | 5 | nelir 3123 | 1 ⊢ +∞ ∉ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 ∉ wnel 3120 𝒫 cpw 4535 ∪ cuni 4830 ℂcc 10523 ℝcr 10524 +∞cpnf 10660 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 ax-un 7450 ax-resscn 10582 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-nel 3121 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-pw 4537 df-sn 4558 df-pr 4560 df-uni 4831 df-pnf 10665 |
This theorem is referenced by: pnfnre2 10671 renepnf 10677 ltxrlt 10699 nn0nepnf 11963 xrltnr 12502 pnfnlt 12511 xnn0lenn0nn0 12626 hashclb 13707 hasheq0 13712 pcgcd1 16201 pc2dvds 16203 ramtcl2 16335 odhash3 18630 xrsdsreclblem 20519 pnfnei 21756 iccpnfcnv 23475 i1f0rn 24210 |
Copyright terms: Public domain | W3C validator |