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

Theorem peano2z 8337
Description: Second Peano postulate generalized to integers. (Contributed by NM, 13-Feb-2005.)
Assertion
Ref Expression
peano2z (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)

Proof of Theorem peano2z
StepHypRef Expression
1 zre 8305 . . 3 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2 1red 7099 . . 3 (𝑁 ∈ ℤ → 1 ∈ ℝ)
31, 2readdcld 7113 . 2 (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℝ)
4 elznn0nn 8315 . . . . 5 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)))
54biimpi 117 . . . 4 (𝑁 ∈ ℤ → (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)))
61biantrurd 293 . . . . 5 (𝑁 ∈ ℤ → (-𝑁 ∈ ℕ ↔ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)))
76orbi2d 714 . . . 4 (𝑁 ∈ ℤ → ((𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ) ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ))))
85, 7mpbird 160 . . 3 (𝑁 ∈ ℤ → (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ))
9 peano2nn0 8278 . . . . 5 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
109a1i 9 . . . 4 (𝑁 ∈ ℤ → (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0))
111adantr 265 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → 𝑁 ∈ ℝ)
12 1red 7099 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → 1 ∈ ℝ)
1311, 12readdcld 7113 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → (𝑁 + 1) ∈ ℝ)
1413renegcld 7449 . . . . . . 7 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → -(𝑁 + 1) ∈ ℝ)
1514recnd 7112 . . . . . 6 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → -(𝑁 + 1) ∈ ℂ)
1611recnd 7112 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → 𝑁 ∈ ℂ)
17 1cnd 7100 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → 1 ∈ ℂ)
1816, 17negdid 7397 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → -(𝑁 + 1) = (-𝑁 + -1))
1918oveq1d 5554 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → (-(𝑁 + 1) + 1) = ((-𝑁 + -1) + 1))
2016negcld 7371 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → -𝑁 ∈ ℂ)
21 neg1cn 8094 . . . . . . . . . . . 12 -1 ∈ ℂ
2221a1i 9 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → -1 ∈ ℂ)
2320, 22, 17addassd 7106 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → ((-𝑁 + -1) + 1) = (-𝑁 + (-1 + 1)))
2419, 23eqtrd 2088 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → (-(𝑁 + 1) + 1) = (-𝑁 + (-1 + 1)))
25 ax-1cn 7034 . . . . . . . . . . 11 1 ∈ ℂ
26 1pneg1e0 8100 . . . . . . . . . . 11 (1 + -1) = 0
2725, 21, 26addcomli 7218 . . . . . . . . . 10 (-1 + 1) = 0
2827oveq2i 5550 . . . . . . . . 9 (-𝑁 + (-1 + 1)) = (-𝑁 + 0)
2924, 28syl6eq 2104 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → (-(𝑁 + 1) + 1) = (-𝑁 + 0))
3020addid1d 7222 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → (-𝑁 + 0) = -𝑁)
3129, 30eqtrd 2088 . . . . . . 7 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → (-(𝑁 + 1) + 1) = -𝑁)
32 simpr 107 . . . . . . 7 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → -𝑁 ∈ ℕ)
3331, 32eqeltrd 2130 . . . . . 6 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → (-(𝑁 + 1) + 1) ∈ ℕ)
34 elnn0nn 8280 . . . . . 6 (-(𝑁 + 1) ∈ ℕ0 ↔ (-(𝑁 + 1) ∈ ℂ ∧ (-(𝑁 + 1) + 1) ∈ ℕ))
3515, 33, 34sylanbrc 402 . . . . 5 ((𝑁 ∈ ℤ ∧ -𝑁 ∈ ℕ) → -(𝑁 + 1) ∈ ℕ0)
3635ex 112 . . . 4 (𝑁 ∈ ℤ → (-𝑁 ∈ ℕ → -(𝑁 + 1) ∈ ℕ0))
3710, 36orim12d 710 . . 3 (𝑁 ∈ ℤ → ((𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ) → ((𝑁 + 1) ∈ ℕ0 ∨ -(𝑁 + 1) ∈ ℕ0)))
388, 37mpd 13 . 2 (𝑁 ∈ ℤ → ((𝑁 + 1) ∈ ℕ0 ∨ -(𝑁 + 1) ∈ ℕ0))
39 elznn0 8316 . 2 ((𝑁 + 1) ∈ ℤ ↔ ((𝑁 + 1) ∈ ℝ ∧ ((𝑁 + 1) ∈ ℕ0 ∨ -(𝑁 + 1) ∈ ℕ0)))
403, 38, 39sylanbrc 402 1 (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wo 639  wcel 1409  (class class class)co 5539  cc 6944  cr 6945  0cc0 6946  1c1 6947   + caddc 6949  -cneg 7245  cn 7989  0cn0 8238  cz 8301
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-pow 3954  ax-pr 3971  ax-setind 4289  ax-cnex 7032  ax-resscn 7033  ax-1cn 7034  ax-1re 7035  ax-icn 7036  ax-addcl 7037  ax-addrcl 7038  ax-mulcl 7039  ax-addcom 7041  ax-addass 7043  ax-distr 7045  ax-i2m1 7046  ax-0id 7049  ax-rnegex 7050  ax-cnre 7052
This theorem depends on definitions:  df-bi 114  df-3or 897  df-3an 898  df-tru 1262  df-fal 1265  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ne 2221  df-ral 2328  df-rex 2329  df-reu 2330  df-rab 2332  df-v 2576  df-sbc 2787  df-dif 2947  df-un 2949  df-in 2951  df-ss 2958  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-int 3643  df-br 3792  df-opab 3846  df-id 4057  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-iota 4894  df-fun 4931  df-fv 4937  df-riota 5495  df-ov 5542  df-oprab 5543  df-mpt2 5544  df-sub 7246  df-neg 7247  df-inn 7990  df-n0 8239  df-z 8302
This theorem is referenced by:  zaddcllempos  8338  peano2zm  8339  zleltp1  8356  btwnnz  8391  peano2uz2  8403  uzind  8407  uzind2  8408  peano2zd  8421  eluzp1m1  8591  eluzp1p1  8593  peano2uz  8621  zltaddlt1le  8974  fzp1disj  9043  elfzp1b  9060  fzneuz  9064  fzp1nel  9067  fzval3  9161  fzossfzop1  9169  rebtwn2zlemstep  9208  flhalf  9246  frec2uzzd  9344  frec2uzsucd  9345  zesq  9528  odd2np1lem  10175  odd2np1  10176  mulsucdiv2z  10189  oddp1d2  10194  zob  10195  ltoddhalfle  10197
  Copyright terms: Public domain W3C validator