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

Theorem peano2z 9288
Description: Second Peano postulate generalized to integers. (Contributed by NM, 13-Feb-2005.)
Assertion
Ref Expression
peano2z  |-  ( N  e.  ZZ  ->  ( N  +  1 )  e.  ZZ )

Proof of Theorem peano2z
StepHypRef Expression
1 zre 9256 . . 3  |-  ( N  e.  ZZ  ->  N  e.  RR )
2 1red 7971 . . 3  |-  ( N  e.  ZZ  ->  1  e.  RR )
31, 2readdcld 7986 . 2  |-  ( N  e.  ZZ  ->  ( N  +  1 )  e.  RR )
4 elznn0nn 9266 . . . . 5  |-  ( N  e.  ZZ  <->  ( N  e.  NN0  \/  ( N  e.  RR  /\  -u N  e.  NN ) ) )
54biimpi 120 . . . 4  |-  ( N  e.  ZZ  ->  ( N  e.  NN0  \/  ( N  e.  RR  /\  -u N  e.  NN ) ) )
61biantrurd 305 . . . . 5  |-  ( N  e.  ZZ  ->  ( -u N  e.  NN  <->  ( N  e.  RR  /\  -u N  e.  NN ) ) )
76orbi2d 790 . . . 4  |-  ( N  e.  ZZ  ->  (
( N  e.  NN0  \/  -u N  e.  NN ) 
<->  ( N  e.  NN0  \/  ( N  e.  RR  /\  -u N  e.  NN ) ) ) )
85, 7mpbird 167 . . 3  |-  ( N  e.  ZZ  ->  ( N  e.  NN0  \/  -u N  e.  NN ) )
9 peano2nn0 9215 . . . . 5  |-  ( N  e.  NN0  ->  ( N  +  1 )  e. 
NN0 )
109a1i 9 . . . 4  |-  ( N  e.  ZZ  ->  ( N  e.  NN0  ->  ( N  +  1 )  e.  NN0 ) )
111adantr 276 . . . . . . . . 9  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  N  e.  RR )
12 1red 7971 . . . . . . . . 9  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  1  e.  RR )
1311, 12readdcld 7986 . . . . . . . 8  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  ( N  + 
1 )  e.  RR )
1413renegcld 8336 . . . . . . 7  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  -u ( N  + 
1 )  e.  RR )
1514recnd 7985 . . . . . 6  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  -u ( N  + 
1 )  e.  CC )
1611recnd 7985 . . . . . . . . . . . 12  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  N  e.  CC )
17 1cnd 7972 . . . . . . . . . . . 12  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  1  e.  CC )
1816, 17negdid 8280 . . . . . . . . . . 11  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  -u ( N  + 
1 )  =  (
-u N  +  -u
1 ) )
1918oveq1d 5889 . . . . . . . . . 10  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  ( -u ( N  +  1 )  +  1 )  =  ( ( -u N  +  -u 1 )  +  1 ) )
2016negcld 8254 . . . . . . . . . . 11  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  -u N  e.  CC )
21 neg1cn 9023 . . . . . . . . . . . 12  |-  -u 1  e.  CC
2221a1i 9 . . . . . . . . . . 11  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  -u 1  e.  CC )
2320, 22, 17addassd 7979 . . . . . . . . . 10  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  ( ( -u N  +  -u 1 )  +  1 )  =  ( -u N  +  ( -u 1  +  1 ) ) )
2419, 23eqtrd 2210 . . . . . . . . 9  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  ( -u ( N  +  1 )  +  1 )  =  ( -u N  +  ( -u 1  +  1 ) ) )
25 ax-1cn 7903 . . . . . . . . . . 11  |-  1  e.  CC
26 1pneg1e0 9029 . . . . . . . . . . 11  |-  ( 1  +  -u 1 )  =  0
2725, 21, 26addcomli 8101 . . . . . . . . . 10  |-  ( -u
1  +  1 )  =  0
2827oveq2i 5885 . . . . . . . . 9  |-  ( -u N  +  ( -u 1  +  1 ) )  =  ( -u N  +  0 )
2924, 28eqtrdi 2226 . . . . . . . 8  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  ( -u ( N  +  1 )  +  1 )  =  ( -u N  + 
0 ) )
3020addid1d 8105 . . . . . . . 8  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  ( -u N  +  0 )  = 
-u N )
3129, 30eqtrd 2210 . . . . . . 7  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  ( -u ( N  +  1 )  +  1 )  = 
-u N )
32 simpr 110 . . . . . . 7  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  -u N  e.  NN )
3331, 32eqeltrd 2254 . . . . . 6  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  ( -u ( N  +  1 )  +  1 )  e.  NN )
34 elnn0nn 9217 . . . . . 6  |-  ( -u ( N  +  1
)  e.  NN0  <->  ( -u ( N  +  1 )  e.  CC  /\  ( -u ( N  +  1 )  +  1 )  e.  NN ) )
3515, 33, 34sylanbrc 417 . . . . 5  |-  ( ( N  e.  ZZ  /\  -u N  e.  NN )  ->  -u ( N  + 
1 )  e.  NN0 )
3635ex 115 . . . 4  |-  ( N  e.  ZZ  ->  ( -u N  e.  NN  ->  -u ( N  +  1
)  e.  NN0 )
)
3710, 36orim12d 786 . . 3  |-  ( N  e.  ZZ  ->  (
( N  e.  NN0  \/  -u N  e.  NN )  ->  ( ( N  +  1 )  e. 
NN0  \/  -u ( N  +  1 )  e. 
NN0 ) ) )
388, 37mpd 13 . 2  |-  ( N  e.  ZZ  ->  (
( N  +  1 )  e.  NN0  \/  -u ( N  +  1 )  e.  NN0 )
)
39 elznn0 9267 . 2  |-  ( ( N  +  1 )  e.  ZZ  <->  ( ( N  +  1 )  e.  RR  /\  (
( N  +  1 )  e.  NN0  \/  -u ( N  +  1 )  e.  NN0 )
) )
403, 38, 39sylanbrc 417 1  |-  ( N  e.  ZZ  ->  ( N  +  1 )  e.  ZZ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    \/ wo 708    e. wcel 2148  (class class class)co 5874   CCcc 7808   RRcr 7809   0cc0 7810   1c1 7811    + caddc 7813   -ucneg 8128   NNcn 8918   NN0cn0 9175   ZZcz 9252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209  ax-setind 4536  ax-cnex 7901  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-addcom 7910  ax-addass 7912  ax-distr 7914  ax-i2m1 7915  ax-0id 7918  ax-rnegex 7919  ax-cnre 7921
This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-br 4004  df-opab 4065  df-id 4293  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-iota 5178  df-fun 5218  df-fv 5224  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-sub 8129  df-neg 8130  df-inn 8919  df-n0 9176  df-z 9253
This theorem is referenced by:  zaddcllempos  9289  peano2zm  9290  zleltp1  9307  btwnnz  9346  peano2uz2  9359  uzind  9363  uzind2  9364  peano2zd  9377  eluzp1m1  9550  eluzp1p1  9552  peano2uz  9582  zltaddlt1le  10006  fzp1disj  10079  elfzp1b  10096  fzneuz  10100  fzp1nel  10103  fzval3  10203  fzossfzop1  10211  rebtwn2zlemstep  10252  flhalf  10301  frec2uzsucd  10400  zesq  10638  hashfzp1  10803  odd2np1lem  11876  odd2np1  11877  mulsucdiv2z  11889  oddp1d2  11894  zob  11895  ltoddhalfle  11897  fldivp1  12345  lgsdir2lem2  14400
  Copyright terms: Public domain W3C validator