Theorem elznn0nn 12535

Description: Integer property expressed in terms nonnegative integers and positive integers. (Contributed by NM, 10-May-2004.)

Assertion

Ref	Expression
elznn0nn	⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)))

Proof of Theorem elznn0nn

Step	Hyp	Ref	Expression
1		elz 12523	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
2		andi 1010	. . 3 ⊢ ((𝑁 ∈ ℝ ∧ ((𝑁 = 0 ∨ 𝑁 ∈ ℕ) ∨ -𝑁 ∈ ℕ)) ↔ ((𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ)) ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)))
3		df-3or 1088	. . . 4 ⊢ ((𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ) ↔ ((𝑁 = 0 ∨ 𝑁 ∈ ℕ) ∨ -𝑁 ∈ ℕ))
4	3	anbi2i 624	. . 3 ⊢ ((𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)) ↔ (𝑁 ∈ ℝ ∧ ((𝑁 = 0 ∨ 𝑁 ∈ ℕ) ∨ -𝑁 ∈ ℕ)))
5		nn0re 12443	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
6	5	pm4.71ri 560	. . . . 5 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0))
7		elnn0 12436	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
8		orcom 871	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ (𝑁 = 0 ∨ 𝑁 ∈ ℕ))
9	7, 8	bitri 275	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 = 0 ∨ 𝑁 ∈ ℕ))
10	9	anbi2i 624	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0) ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ)))
11	6, 10	bitri 275	. . . 4 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ)))
12	11	orbi1i 914	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) ↔ ((𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ)) ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)))
13	2, 4, 12	3bitr4i 303	. 2 ⊢ ((𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)) ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)))
14	1, 13	bitri 275	1 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  ℝcr 11034  0cc0 11035  -cneg 11375  ℕcn 12171  ℕ₀cn0 12434  ℤcz 12521

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 5232  ax-nul 5242  ax-pr 5374  ax-un 7686  ax-1cn 11093  ax-icn 11094  ax-addcl 11095  ax-addrcl 11096  ax-mulcl 11097  ax-mulrcl 11098  ax-i2m1 11103  ax-1ne0 11104  ax-rnegex 11106  ax-rrecex 11107  ax-cnre 11108

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-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 5523  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5581  df-we 5583  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-pred 6263  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7367  df-om 7815  df-2nd 7940  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-neg 11377  df-nn 12172  df-n0 12435  df-z 12522

This theorem is referenced by:  zindd  12627  expcl2lem  14032  mulexpz  14061  expaddz  14065  expmulz  14067  absexpz  15264  bitsfzo  16401  pcid  16841  mulgsubcl  19061  mulgneg  19065  ghmmulg  19200  prmirred  21451  tgpmulg  24055  dvexp3  25942  2sqnn0  27398  ipasslem3  30901  reelznn0nn  42903  ztprmneprm  48814