Theorem nnm1nn0 9137

Description: A positive integer minus 1 is a nonnegative integer. (Contributed by Jason Orendorff, 24-Jan-2007.) (Revised by Mario Carneiro, 16-May-2014.)

Assertion

Ref	Expression
nnm1nn0	|- ( N e. NN -> ( N - 1 ) e. NN0 )

Proof of Theorem nnm1nn0

Step	Hyp	Ref	Expression
1		nn1m1nn 8857	. . . 4 |- ( N e. NN -> ( N = 1 \/ ( N - 1 ) e. NN ) )
2		oveq1 5834	. . . . . 6 |- ( N = 1 -> ( N - 1 ) = ( 1 - 1 ) )
3		1m1e0 8908	. . . . . 6 |- ( 1 - 1 ) = 0
4	2, 3	eqtrdi 2206	. . . . 5 |- ( N = 1 -> ( N - 1 ) = 0 )
5	4	orim1i 750	. . . 4 |- ( ( N = 1 \/ ( N - 1 ) e. NN ) -> ( ( N - 1 ) = 0 \/ ( N - 1 ) e. NN ) )
6	1, 5	syl 14	. . 3 |- ( N e. NN -> ( ( N - 1 ) = 0 \/ ( N - 1 ) e. NN ) )
7	6	orcomd 719	. 2 |- ( N e. NN -> ( ( N - 1 ) e. NN \/ ( N - 1 ) = 0 ) )
8		elnn0 9098	. 2 |- ( ( N - 1 ) e. NN0 <-> ( ( N - 1 ) e. NN \/ ( N - 1 ) = 0 ) )
9	7, 8	sylibr 133	1 |- ( N e. NN -> ( N - 1 ) e. NN0 )

Syntax hints:   -> wi 4   \/ wo 698   = wceq 1335   e. wcel 2128  (class class class)co 5827   0cc0 7735   1c1 7736   - cmin 8051   NNcn 8839   NN0cn0 9096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4085  ax-pow 4138  ax-pr 4172  ax-setind 4499  ax-cnex 7826  ax-resscn 7827  ax-1cn 7828  ax-1re 7829  ax-icn 7830  ax-addcl 7831  ax-addrcl 7832  ax-mulcl 7833  ax-addcom 7835  ax-addass 7837  ax-distr 7839  ax-i2m1 7840  ax-0id 7843  ax-rnegex 7844  ax-cnre 7846

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-pw 3546  df-sn 3567  df-pr 3568  df-op 3570  df-uni 3775  df-int 3810  df-br 3968  df-opab 4029  df-id 4256  df-xp 4595  df-rel 4596  df-cnv 4597  df-co 4598  df-dm 4599  df-iota 5138  df-fun 5175  df-fv 5181  df-riota 5783  df-ov 5830  df-oprab 5831  df-mpo 5832  df-sub 8053  df-inn 8840  df-n0 9097

This theorem is referenced by:  elnn0nn  9138  nnaddm1cl  9234  nn0n0n1ge2  9240  fseq1m1p1  10004  nn0ennn  10342  expm1t  10457  expgt1  10467  nn0ltexp2  10596  bcn1  10644  bcm1k  10646  bcn2m1  10655  resqrexlemnm  10930  resqrexlemcvg  10931  resqrexlemga  10935  binomlem  11392  arisum  11407  arisum2  11408  cvgratnnlemnexp  11433  cvgratnnlemfm  11438  mertenslem2  11445  iddvdsexp  11723  dvdsfac  11765  oexpneg  11781  phibnd  12108  phiprmpw  12113  prmdiv  12126  oddprm  12150  dvexp  13171