Theorem elnnz 12525

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 12172	. . . 4 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2		orc 868	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)))
3		nngt0 12199	. . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
4	1, 2, 3	jca31 514	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁))
5		idd 24	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → (𝑁 ∈ ℕ → 𝑁 ∈ ℕ))
6		lt0neg2 11648	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℝ → (0 < 𝑁 ↔ -𝑁 < 0))
7		renegcl 11448	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℝ → -𝑁 ∈ ℝ)
8		0re 11137	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
9		ltnsym 11235	. . . . . . . . . . . . 13 ⊢ ((-𝑁 ∈ ℝ ∧ 0 ∈ ℝ) → (-𝑁 < 0 → ¬ 0 < -𝑁))
10	7, 8, 9	sylancl 587	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℝ → (-𝑁 < 0 → ¬ 0 < -𝑁))
11	6, 10	sylbid 240	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (0 < 𝑁 → ¬ 0 < -𝑁))
12	11	imp 406	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ 0 < -𝑁)
13		nngt0 12199	. . . . . . . . . 10 ⊢ (-𝑁 ∈ ℕ → 0 < -𝑁)
14	12, 13	nsyl 140	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ -𝑁 ∈ ℕ)
15		gt0ne0 11606	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → 𝑁 ≠ 0)
16	15	neneqd 2938	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ 𝑁 = 0)
17		ioran 986	. . . . . . . . 9 ⊢ (¬ (-𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ (¬ -𝑁 ∈ ℕ ∧ ¬ 𝑁 = 0))
18	14, 16, 17	sylanbrc 584	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))
19	18	pm2.21d 121	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ((-𝑁 ∈ ℕ ∨ 𝑁 = 0) → 𝑁 ∈ ℕ))
20	5, 19	jaod 860	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ((𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)) → 𝑁 ∈ ℕ))
21	20	ex 412	. . . . 5 ⊢ (𝑁 ∈ ℝ → (0 < 𝑁 → ((𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)) → 𝑁 ∈ ℕ)))
22	21	com23 86	. . . 4 ⊢ (𝑁 ∈ ℝ → ((𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)) → (0 < 𝑁 → 𝑁 ∈ ℕ)))
23	22	imp31 417	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁) → 𝑁 ∈ ℕ)
24	4, 23	impbii 209	. 2 ⊢ (𝑁 ∈ ℕ ↔ ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁))
25		elz 12517	. . . 4 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
26		3orrot 1092	. . . . . 6 ⊢ ((𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ) ↔ (𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ ∨ 𝑁 = 0))
27		3orass 1090	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)))
28	26, 27	bitri 275	. . . . 5 ⊢ ((𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ) ↔ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)))
29	28	anbi2i 624	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)) ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))))
30	25, 29	bitri 275	. . 3 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))))
31	30	anbi1i 625	. 2 ⊢ ((𝑁 ∈ ℤ ∧ 0 < 𝑁) ↔ ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁))
32	24, 31	bitr4i 278	1 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114   class class class wbr 5086  ℝcr 11028  0cc0 11029   < clt 11170  -cneg 11369  ℕcn 12165  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-z 12516

This theorem is referenced by:  elnn0z  12528  elnnz1  12544  znnsub  12564  nn0ge0div  12589  msqznn  12602  elpq  12916  lbfzo0  13645  elfzo0z  13647  fzofzim  13655  fzo1fzo0n0  13661  elfzodifsumelfzo  13677  elfznelfzo  13719  nnesq  14180  swrdlsw  14621  pfxccatin12lem3  14685  repswswrd  14737  cshwcsh2id  14781  swrd2lsw  14905  2swrd2eqwrdeq  14906  nnabscl  15279  iseralt  15638  sqrt2irrlem  16206  p1modz1  16219  nndivdvds  16221  oddge22np1  16309  evennn2n  16311  nno  16342  nnoddm1d2  16346  ndvdsadd  16370  bitsfzolem  16394  sqgcd  16522  qredeu  16618  prmind2  16645  qgt0numnn  16712  oddprm  16772  pythagtriplem6  16783  pythagtriplem11  16787  pythagtriplem13  16789  pythagtriplem19  16795  pc2dvds  16841  pcadd  16851  prmreclem3  16880  4sqlem11  16917  4sqlem12  16918  prmgaplem7  17019  cshwshashlem2  17058  subgmulg  19107  znidomb  21551  rtprmirr  26737  sgmnncl  27124  muinv  27170  mersenne  27204  bposlem6  27266  gausslemma2dlem1a  27342  lgseisenlem1  27352  lgsquadlem1  27357  lgsquadlem2  27358  2sqlem8  27403  2sqnn0  27415  dchrisum0flblem2  27486  clwlkclwwlklem2a2  30078  clwlkclwwlklem2a4  30082  clwlkclwwlklem2a  30083  eucrct2eupth1  30329  nn0prpwlem  36520  poimirlem7  37962  poimirlem29  37984  mblfinlem2  37993  lcmineqlem15  42496  lcmineqlem23  42504  aks4d1lem1  42515  aks4d1p1p2  42523  aks4d1p1  42529  aks4d1p2  42530  aks4d1p3  42531  aks4d1p5  42533  aks4d1p6  42534  aks4d1p7d1  42535  aks4d1p8  42540  posbezout  42553  aks6d1c1  42569  hashscontpow1  42574  aks6d1c4  42577  aks6d1c2  42583  aks6d1c5lem2  42591  2ap1caineq  42598  aks6d1c7lem1  42633  aks6d1c7lem2  42634  aks6d1c7  42637  aks5lem6  42645  aks5lem8  42654  posqsqznn  42782  fimgmcyc  42993  dffltz  43081  irrapxlem4  43271  rmspecnonsq  43353  rmynn  43402  jm2.24  43409  jm2.23  43442  jm2.20nn  43443  jm2.27a  43451  jm2.27c  43453  rmydioph  43460  jm3.1lem3  43465  sumnnodd  46078  dvnxpaek  46388  dirkertrigeqlem3  46546  fourierdlem47  46599  fouriersw  46677  etransclem15  46695  etransclem24  46704  etransclem25  46705  etransclem35  46715  etransclem48  46728  zm1nn  47762  modm1p1ne  47836  muldvdsfacgt  47846  muldvdsfacm1  47847  iccpartigtl  47895  nnoALTV  48183  nneven  48186  ztprmneprm  48835  blennngt2o2  49080