![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0mnnnnn0 | GIF version |
Description: The result of subtracting a positive integer from 0 is not a nonnegative integer. (Contributed by Alexander van der Vekens, 19-Mar-2018.) |
Ref | Expression |
---|---|
0mnnnnn0 | ⊢ (𝑁 ∈ ℕ → (0 − 𝑁) ∉ ℕ0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re 7233 | . . 3 ⊢ 0 ∈ ℝ | |
2 | df-neg 7401 | . . . . . 6 ⊢ -𝑁 = (0 − 𝑁) | |
3 | 2 | eqcomi 2087 | . . . . 5 ⊢ (0 − 𝑁) = -𝑁 |
4 | 3 | eleq1i 2148 | . . . 4 ⊢ ((0 − 𝑁) ∈ ℕ0 ↔ -𝑁 ∈ ℕ0) |
5 | nn0ge0 8432 | . . . . 5 ⊢ (-𝑁 ∈ ℕ0 → 0 ≤ -𝑁) | |
6 | nnre 8165 | . . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ) | |
7 | 6 | le0neg1d 7737 | . . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝑁 ≤ 0 ↔ 0 ≤ -𝑁)) |
8 | nngt0 8183 | . . . . . . 7 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁) | |
9 | 0red 7234 | . . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 0 ∈ ℝ) | |
10 | 6, 9 | lenltd 7346 | . . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (𝑁 ≤ 0 ↔ ¬ 0 < 𝑁)) |
11 | pm2.21 580 | . . . . . . . 8 ⊢ (¬ 0 < 𝑁 → (0 < 𝑁 → ¬ 0 ∈ ℝ)) | |
12 | 10, 11 | syl6bi 161 | . . . . . . 7 ⊢ (𝑁 ∈ ℕ → (𝑁 ≤ 0 → (0 < 𝑁 → ¬ 0 ∈ ℝ))) |
13 | 8, 12 | mpid 41 | . . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝑁 ≤ 0 → ¬ 0 ∈ ℝ)) |
14 | 7, 13 | sylbird 168 | . . . . 5 ⊢ (𝑁 ∈ ℕ → (0 ≤ -𝑁 → ¬ 0 ∈ ℝ)) |
15 | 5, 14 | syl5 32 | . . . 4 ⊢ (𝑁 ∈ ℕ → (-𝑁 ∈ ℕ0 → ¬ 0 ∈ ℝ)) |
16 | 4, 15 | syl5bi 150 | . . 3 ⊢ (𝑁 ∈ ℕ → ((0 − 𝑁) ∈ ℕ0 → ¬ 0 ∈ ℝ)) |
17 | 1, 16 | mt2i 606 | . 2 ⊢ (𝑁 ∈ ℕ → ¬ (0 − 𝑁) ∈ ℕ0) |
18 | df-nel 2345 | . 2 ⊢ ((0 − 𝑁) ∉ ℕ0 ↔ ¬ (0 − 𝑁) ∈ ℕ0) | |
19 | 17, 18 | sylibr 132 | 1 ⊢ (𝑁 ∈ ℕ → (0 − 𝑁) ∉ ℕ0) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 1434 ∉ wnel 2344 class class class wbr 3805 (class class class)co 5563 ℝcr 7094 0cc0 7095 < clt 7267 ≤ cle 7268 − cmin 7398 -cneg 7399 ℕcn 8158 ℕ0cn0 8407 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-sep 3916 ax-pow 3968 ax-pr 3992 ax-un 4216 ax-setind 4308 ax-cnex 7181 ax-resscn 7182 ax-1cn 7183 ax-1re 7184 ax-icn 7185 ax-addcl 7186 ax-addrcl 7187 ax-mulcl 7188 ax-addcom 7190 ax-addass 7192 ax-distr 7194 ax-i2m1 7195 ax-0lt1 7196 ax-0id 7198 ax-rnegex 7199 ax-cnre 7201 ax-pre-ltirr 7202 ax-pre-ltwlin 7203 ax-pre-lttrn 7204 ax-pre-ltadd 7206 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1688 df-eu 1946 df-mo 1947 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ne 2250 df-nel 2345 df-ral 2358 df-rex 2359 df-reu 2360 df-rab 2362 df-v 2612 df-sbc 2825 df-dif 2984 df-un 2986 df-in 2988 df-ss 2995 df-pw 3402 df-sn 3422 df-pr 3423 df-op 3425 df-uni 3622 df-int 3657 df-br 3806 df-opab 3860 df-id 4076 df-xp 4397 df-rel 4398 df-cnv 4399 df-co 4400 df-dm 4401 df-iota 4917 df-fun 4954 df-fv 4960 df-riota 5519 df-ov 5566 df-oprab 5567 df-mpt2 5568 df-pnf 7269 df-mnf 7270 df-xr 7271 df-ltxr 7272 df-le 7273 df-sub 7400 df-neg 7401 df-inn 8159 df-n0 8408 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |