![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > renemnf | GIF version |
Description: No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Ref | Expression |
---|---|
renemnf | ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mnfnre 7732 | . . . 4 ⊢ -∞ ∉ ℝ | |
2 | 1 | neli 2379 | . . 3 ⊢ ¬ -∞ ∈ ℝ |
3 | eleq1 2177 | . . 3 ⊢ (𝐴 = -∞ → (𝐴 ∈ ℝ ↔ -∞ ∈ ℝ)) | |
4 | 2, 3 | mtbiri 647 | . 2 ⊢ (𝐴 = -∞ → ¬ 𝐴 ∈ ℝ) |
5 | 4 | necon2ai 2336 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1314 ∈ wcel 1463 ≠ wne 2282 ℝcr 7546 -∞cmnf 7722 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-setind 4412 ax-cnex 7636 ax-resscn 7637 |
This theorem depends on definitions: df-bi 116 df-3an 947 df-tru 1317 df-nf 1420 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-ne 2283 df-nel 2378 df-ral 2395 df-v 2659 df-dif 3039 df-un 3041 df-in 3043 df-ss 3050 df-pw 3478 df-sn 3499 df-pr 3500 df-uni 3703 df-pnf 7726 df-mnf 7727 |
This theorem is referenced by: renemnfd 7741 renfdisj 7748 ltxrlt 7754 xrnemnf 9457 xrlttri3 9476 ngtmnft 9493 xrrebnd 9495 rexneg 9506 xrmnfdc 9519 rexadd 9528 xaddnemnf 9533 xaddcom 9537 xaddid1 9538 xnegdi 9544 xpncan 9547 xleadd1a 9549 xltadd1 9552 xposdif 9558 xrmaxrecl 10916 isxmet2d 12337 |
Copyright terms: Public domain | W3C validator |