| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > nltpnft | GIF version | ||
| Description: An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.) |
| Ref | Expression |
|---|---|
| nltpnft | ⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elxr 10011 | . 2 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) | |
| 2 | renepnf 8227 | . . . . 5 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞) | |
| 3 | 2 | neneqd 2423 | . . . 4 ⊢ (𝐴 ∈ ℝ → ¬ 𝐴 = +∞) |
| 4 | ltpnf 10015 | . . . . 5 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞) | |
| 5 | notnot 634 | . . . . 5 ⊢ (𝐴 < +∞ → ¬ ¬ 𝐴 < +∞) | |
| 6 | 4, 5 | syl 14 | . . . 4 ⊢ (𝐴 ∈ ℝ → ¬ ¬ 𝐴 < +∞) |
| 7 | 3, 6 | 2falsed 709 | . . 3 ⊢ (𝐴 ∈ ℝ → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞)) |
| 8 | id 19 | . . . 4 ⊢ (𝐴 = +∞ → 𝐴 = +∞) | |
| 9 | pnfxr 8232 | . . . . . 6 ⊢ +∞ ∈ ℝ* | |
| 10 | xrltnr 10014 | . . . . . 6 ⊢ (+∞ ∈ ℝ* → ¬ +∞ < +∞) | |
| 11 | 9, 10 | ax-mp 5 | . . . . 5 ⊢ ¬ +∞ < +∞ |
| 12 | breq1 4091 | . . . . 5 ⊢ (𝐴 = +∞ → (𝐴 < +∞ ↔ +∞ < +∞)) | |
| 13 | 11, 12 | mtbiri 681 | . . . 4 ⊢ (𝐴 = +∞ → ¬ 𝐴 < +∞) |
| 14 | 8, 13 | 2thd 175 | . . 3 ⊢ (𝐴 = +∞ → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞)) |
| 15 | mnfnepnf 8235 | . . . . . 6 ⊢ -∞ ≠ +∞ | |
| 16 | 15 | neii 2404 | . . . . 5 ⊢ ¬ -∞ = +∞ |
| 17 | eqeq1 2238 | . . . . 5 ⊢ (𝐴 = -∞ → (𝐴 = +∞ ↔ -∞ = +∞)) | |
| 18 | 16, 17 | mtbiri 681 | . . . 4 ⊢ (𝐴 = -∞ → ¬ 𝐴 = +∞) |
| 19 | mnfltpnf 10020 | . . . . . . 7 ⊢ -∞ < +∞ | |
| 20 | breq1 4091 | . . . . . . 7 ⊢ (𝐴 = -∞ → (𝐴 < +∞ ↔ -∞ < +∞)) | |
| 21 | 19, 20 | mpbiri 168 | . . . . . 6 ⊢ (𝐴 = -∞ → 𝐴 < +∞) |
| 22 | 21 | necon3bi 2452 | . . . . 5 ⊢ (¬ 𝐴 < +∞ → 𝐴 ≠ -∞) |
| 23 | 22 | necon2bi 2457 | . . . 4 ⊢ (𝐴 = -∞ → ¬ ¬ 𝐴 < +∞) |
| 24 | 18, 23 | 2falsed 709 | . . 3 ⊢ (𝐴 = -∞ → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞)) |
| 25 | 7, 14, 24 | 3jaoi 1339 | . 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞)) |
| 26 | 1, 25 | sylbi 121 | 1 ⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞)) |
| Colors of variables: wff set class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 105 ∨ w3o 1003 = wceq 1397 ∈ wcel 2202 class class class wbr 4088 ℝcr 8031 +∞cpnf 8211 -∞cmnf 8212 ℝ*cxr 8213 < clt 8214 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-sep 4207 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-cnex 8123 ax-resscn 8124 ax-pre-ltirr 8144 |
| This theorem depends on definitions: df-bi 117 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-rab 2519 df-v 2804 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-br 4089 df-opab 4151 df-xp 4731 df-pnf 8216 df-mnf 8217 df-xr 8218 df-ltxr 8219 |
| This theorem is referenced by: npnflt 10050 xgepnf 10051 xrmaxiflemlub 11810 |
| Copyright terms: Public domain | W3C validator |