Theorem elnnz 12733

Description: Positive integer property expressed in terms of integers. (Contributed by NM, 8-Jan-2002.)

Assertion

Ref	Expression
elnnz	⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))

Proof of Theorem elnnz

Step	Hyp	Ref	Expression
1		nnre 12372	. . . 4 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2		orc 881	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℕ ∨ ( -𝑁 ∈ ℕ ∨ 𝑁 = 0)))
3		nngt0 12399	. . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
4	1, 2, 3	jca31 524	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ ( -𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁))
5		idd 25	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → (𝑁 ∈ ℕ → 𝑁 ∈ ℕ))
6		lt0neg2 11853	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℝ → (0 < 𝑁 ↔ -𝑁 < 0))
7		renegcl 11651	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℝ → -𝑁 ∈ ℝ)
8		0re 11340	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
9		ltnsym 11438	. . . . . . . . . . . . 13 ⊢ (( -𝑁 ∈ ℝ ∧ 0 ∈ ℝ) → ( -𝑁 < 0 → ¬ 0 < -𝑁))
10	7, 8, 9	sylancl 598	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℝ → ( -𝑁 < 0 → ¬ 0 < -𝑁))
11	6, 10	sylbid 243	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (0 < 𝑁 → ¬ 0 < -𝑁))
12	11	imp 412	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ 0 < -𝑁)
13		nngt0 12399	. . . . . . . . . 10 ⊢ ( -𝑁 ∈ ℕ → 0 < -𝑁)
14	12, 13	nsyl 141	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ -𝑁 ∈ ℕ)
15		gt0ne0 11811	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → 𝑁 ≠ 0)
16	15	neneqd 2964	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ 𝑁 = 0)
17		ioran 999	. . . . . . . . 9 ⊢ (¬ ( -𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ (¬ -𝑁 ∈ ℕ ∧ ¬ 𝑁 = 0))
18	14, 16, 17	sylanbrc 595	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ ( -𝑁 ∈ ℕ ∨ 𝑁 = 0))
19	18	pm2.21d 122	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → (( -𝑁 ∈ ℕ ∨ 𝑁 = 0) → 𝑁 ∈ ℕ))
20	5, 19	jaod 873	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ((𝑁 ∈ ℕ ∨ ( -𝑁 ∈ ℕ ∨ 𝑁 = 0)) → 𝑁 ∈ ℕ))
21	20	ex 418	. . . . 5 ⊢ (𝑁 ∈ ℝ → (0 < 𝑁 → ((𝑁 ∈ ℕ ∨ ( -𝑁 ∈ ℕ ∨ 𝑁 = 0)) → 𝑁 ∈ ℕ)))
22	21	com23 87	. . . 4 ⊢ (𝑁 ∈ ℝ → ((𝑁 ∈ ℕ ∨ ( -𝑁 ∈ ℕ ∨ 𝑁 = 0)) → (0 < 𝑁 → 𝑁 ∈ ℕ)))
23	22	imp31 423	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ ( -𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁) → 𝑁 ∈ ℕ)
24	4, 23	impbii 212	. 2 ⊢ (𝑁 ∈ ℕ ↔ ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ ( -𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁))
25		elz 12725	. . . 4 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
26		3orrot 1108	. . . . . 6 ⊢ ((𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ) ↔ (𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ ∨ 𝑁 = 0))
27		3orass 1106	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ (𝑁 ∈ ℕ ∨ ( -𝑁 ∈ ℕ ∨ 𝑁 = 0)))
28	26, 27	bitri 278	. . . . 5 ⊢ ((𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ) ↔ (𝑁 ∈ ℕ ∨ ( -𝑁 ∈ ℕ ∨ 𝑁 = 0)))
29	28	anbi2i 635	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)) ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ ( -𝑁 ∈ ℕ ∨ 𝑁 = 0))))
30	25, 29	bitri 278	. . 3 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ ( -𝑁 ∈ ℕ ∨ 𝑁 = 0))))
31	30	anbi1i 636	. 2 ⊢ ((𝑁 ∈ ℤ ∧ 0 < 𝑁) ↔ ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ ( -𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁))
32	24, 31	bitr4i 281	1 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   = wceq 1570   ∈ wcel 2147   class class class wbr 5106  ℝcr 11229  0cc0 11230   < clt 11373   -cneg 11572  ℕcn 12365  ℤcz 12723

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-resscn 11287  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-addrcl 11291  ax-mulcl 11292  ax-mulrcl 11293  ax-mulcom 11294  ax-addass 11295  ax-mulass 11296  ax-distr 11297  ax-i2m1 11298  ax-1ne0 11299  ax-1rid 11300  ax-rnegex 11301  ax-rrecex 11302  ax-cnre 11303  ax-pre-lttri 11304  ax-pre-lttrn 11305  ax-pre-ltadd 11306  ax-pre-mulgt0 11307

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6325  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7403  df-ov 7449  df-oprab 7450  df-mpo 7451  df-om 7905  df-2nd 8029  df-frecs 8330  df-wrecs 8361  df-recs 8410  df-rdg 8449  df-er 8748  df-en 9005  df-dom 9006  df-sdom 9007  df-pnf 11375  df-mnf 11376  df-xr 11377  df-ltxr 11378  df-le 11379  df-sub 11573  df-neg 11574  df-nn 12366  df-z 12724

This theorem is used by:  elnn0z  12736  elnnz1  12752  znnsub  12772  nn0ge0div  12798  msqznn  12811  elpq  13133  lbfzo0  13864  elfzo0z  13866  fzofzim  13874  fzo1fzo0n0  13880  elfzodifsumelfzo  13896  elfznelfzo  13938  nnesq  14401  swrdlsw  14848  pfxccatin12lem3  14912  repswswrd  14966  cshwcsh2id  15010  swrd2lsw  15137  2swrd2eqwrdeq  15138  nnabscl  15525  iseralt  15884  sqrt2irrlem  16448  p1modz1  16461  nndivdvds  16463  oddge22np1  16551  evennn2n  16553  nno  16584  nnoddm1d2  16588  ndvdsadd  16612  bitsfzolem  16636  sqgcd  16768  qredeu  16865  prmind2  16892  qgt0numnn  16959  posqsqznn  16968  oddprm  17020  pythagtriplem6  17031  pythagtriplem11  17035  pythagtriplem13  17037  pythagtriplem19  17043  pc2dvds  17089  pcadd  17099  prmreclem3  17128  4sqlem11  17165  4sqlem12  17166  prmgaplem7  17267  cshwshashlem2  17306  subgmulg  19383  znidomb  21900  rtprmirr  27121  sgmnncl  27507  muinv  27553  mersenne  27587  bposlem6  27649  gausslemma2dlem1a  27725  lgseisenlem1  27735  lgsquadlem1  27740  lgsquadlem2  27741  2sqlem8  27786  2sqnn0  27798  dchrisum0flblem2  27869  clwlkclwwlklem2a2  30617  clwlkclwwlklem2a4  30621  clwlkclwwlklem2a  30622  eucrct2eupth1  30878  nn0prpwlem  37301  poimirlem7  38750  poimirlem29  38772  mblfinlem2  38781  lcmineqlem15  43296  lcmineqlem23  43304  aks4d1lem1  43315  aks4d1p1p2  43323  aks4d1p1  43329  aks4d1p2  43330  aks4d1p3  43331  aks4d1p5  43333  aks4d1p6  43334  aks4d1p7d1  43335  aks4d1p8  43340  posbezout  43353  aks6d1c1  43369  hashscontpow1  43374  aks6d1c4  43377  aks6d1c2  43383  aks6d1c5lem2  43391  2ap1caineq  43398  aks6d1c7lem1  43433  aks6d1c7lem2  43434  aks6d1c7  43437  aks5lem6  43445  aks5lem8  43454  fimgmcyc  43802  dffltz  43874  irrapxlem4  44036  rmspecnonsq  44118  rmynn  44167  jm2.24  44174  jm2.23  44207  jm2.20nn  44208  jm2.27a  44216  jm2.27c  44218  rmydioph  44225  jm3.1lem3  44230  sumnnodd  46857  dvnxpaek  47167  dirkertrigeqlem3  47325  fourierdlem47  47378  fouriersw  47456  etransclem15  47474  etransclem24  47483  etransclem25  47484  etransclem35  47494  etransclem48  47507  zm1nn  48587  modm1p1ne  48661  muldvdsfacgt  48671  muldvdsfacm1  48672  iccpartigtl  48720  nnoALTV  49008  nneven  49011  ztprmneprm  49674  blennngt2o2  49919