ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elnn0z GIF version

Theorem elnn0z 8696
Description: Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
elnn0z (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))

Proof of Theorem elnn0z
StepHypRef Expression
1 nn0re 8615 . . . 4 (𝑁 ∈ ℕ0𝑁 ∈ ℝ)
2 elnn0 8608 . . . . . . 7 (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
32biimpi 118 . . . . . 6 (𝑁 ∈ ℕ0 → (𝑁 ∈ ℕ ∨ 𝑁 = 0))
43orcomd 681 . . . . 5 (𝑁 ∈ ℕ0 → (𝑁 = 0 ∨ 𝑁 ∈ ℕ))
5 3mix1 1110 . . . . . 6 (𝑁 = 0 → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
6 3mix2 1111 . . . . . 6 (𝑁 ∈ ℕ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
75, 6jaoi 669 . . . . 5 ((𝑁 = 0 ∨ 𝑁 ∈ ℕ) → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
84, 7syl 14 . . . 4 (𝑁 ∈ ℕ0 → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
9 elz 8685 . . . 4 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
101, 8, 9sylanbrc 408 . . 3 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
11 nn0ge0 8631 . . 3 (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)
1210, 11jca 300 . 2 (𝑁 ∈ ℕ0 → (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))
139simprbi 269 . . . 4 (𝑁 ∈ ℤ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
1413adantr 270 . . 3 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
15 0nn0 8621 . . . . . 6 0 ∈ ℕ0
16 eleq1 2147 . . . . . 6 (𝑁 = 0 → (𝑁 ∈ ℕ0 ↔ 0 ∈ ℕ0))
1715, 16mpbiri 166 . . . . 5 (𝑁 = 0 → 𝑁 ∈ ℕ0)
1817a1i 9 . . . 4 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (𝑁 = 0 → 𝑁 ∈ ℕ0))
19 nnnn0 8613 . . . . 5 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
2019a1i 9 . . . 4 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0))
21 simpr 108 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → 0 ≤ 𝑁)
22 0red 7433 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → 0 ∈ ℝ)
23 zre 8687 . . . . . . . . 9 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2423adantr 270 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → 𝑁 ∈ ℝ)
2522, 24lenltd 7545 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (0 ≤ 𝑁 ↔ ¬ 𝑁 < 0))
2621, 25mpbid 145 . . . . . 6 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → ¬ 𝑁 < 0)
27 nngt0 8382 . . . . . . 7 (-𝑁 ∈ ℕ → 0 < -𝑁)
2824lt0neg1d 7934 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (𝑁 < 0 ↔ 0 < -𝑁))
2927, 28syl5ibr 154 . . . . . 6 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (-𝑁 ∈ ℕ → 𝑁 < 0))
3026, 29mtod 622 . . . . 5 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → ¬ -𝑁 ∈ ℕ)
3130pm2.21d 582 . . . 4 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (-𝑁 ∈ ℕ → 𝑁 ∈ ℕ0))
3218, 20, 313jaod 1238 . . 3 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → ((𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ) → 𝑁 ∈ ℕ0))
3314, 32mpd 13 . 2 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → 𝑁 ∈ ℕ0)
3412, 33impbii 124 1 (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wo 662  w3o 921   = wceq 1287  wcel 1436   class class class wbr 3820  cr 7293  0cc0 7294   < clt 7466  cle 7467  -cneg 7598  cn 8357  0cn0 8606  cz 8683
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3932  ax-pow 3984  ax-pr 4010  ax-un 4234  ax-setind 4326  ax-cnex 7380  ax-resscn 7381  ax-1cn 7382  ax-1re 7383  ax-icn 7384  ax-addcl 7385  ax-addrcl 7386  ax-mulcl 7387  ax-addcom 7389  ax-addass 7391  ax-distr 7393  ax-i2m1 7394  ax-0lt1 7395  ax-0id 7397  ax-rnegex 7398  ax-cnre 7400  ax-pre-ltirr 7401  ax-pre-ltwlin 7402  ax-pre-lttrn 7403  ax-pre-ltadd 7405
This theorem depends on definitions:  df-bi 115  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-nel 2347  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2617  df-sbc 2830  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3637  df-int 3672  df-br 3821  df-opab 3875  df-id 4094  df-xp 4417  df-rel 4418  df-cnv 4419  df-co 4420  df-dm 4421  df-iota 4946  df-fun 4983  df-fv 4989  df-riota 5569  df-ov 5616  df-oprab 5617  df-mpt2 5618  df-pnf 7468  df-mnf 7469  df-xr 7470  df-ltxr 7471  df-le 7472  df-sub 7599  df-neg 7600  df-inn 8358  df-n0 8607  df-z 8684
This theorem is referenced by:  nn0zrab  8708  znn0sub  8748  nn0ind  8793  fnn0ind  8795  fznn0  9457  elfz0ubfz0  9464  elfz0fzfz0  9465  fz0fzelfz0  9466  elfzmlbp  9471  difelfzle  9473  difelfznle  9474  elfzo0z  9523  fzofzim  9527  ubmelm1fzo  9565  flqge0nn0  9628  zmodcl  9679  modqmuladdnn0  9703  modsumfzodifsn  9731  zsqcl2  9930  nn0abscl  10413  oexpneg  10752  oddnn02np1  10755  evennn02n  10757  nn0ehalf  10778  nn0oddm1d2  10784  divalgb  10800  dfgcd2  10878  ialgcvga  10908  hashgcdlem  11078
  Copyright terms: Public domain W3C validator