Theorem nn0ge0 9355

Description: A nonnegative integer is greater than or equal to zero. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 16-May-2014.)

Assertion

Ref	Expression
nn0ge0	|- ( N e. NN0 -> 0 <_ N )

Proof of Theorem nn0ge0

Step	Hyp	Ref	Expression
1		elnn0 9332	. 2 |- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2		nnre 9078	. . . 4 |- ( N e. NN -> N e. RR )
3		nngt0 9096	. . . 4 |- ( N e. NN -> 0 < N )
4		0re 8107	. . . . 5 |- 0 e. RR
5		ltle 8195	. . . . 5 |- ( ( 0 e. RR /\ N e. RR ) -> ( 0 < N -> 0 <_ N ) )
6	4, 5	mpan 424	. . . 4 |- ( N e. RR -> ( 0 < N -> 0 <_ N ) )
7	2, 3, 6	sylc 62	. . 3 |- ( N e. NN -> 0 <_ N )
8		0le0 9160	. . . 4 |- 0 <_ 0
9		breq2 4063	. . . 4 |- ( N = 0 -> ( 0 <_ N <-> 0 <_ 0 ) )
10	8, 9	mpbiri 168	. . 3 |- ( N = 0 -> 0 <_ N )
11	7, 10	jaoi 718	. 2 |- ( ( N e. NN \/ N = 0 ) -> 0 <_ N )
12	1, 11	sylbi 121	1 |- ( N e. NN0 -> 0 <_ N )

Syntax hints:   -> wi 4   \/ wo 710   = wceq 1373   e. wcel 2178   class class class wbr 4059   RRcr 7959   0cc0 7960   < clt 8142   <_ cle 8143   NNcn 9071   NN0cn0 9330

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 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2180  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269  ax-un 4498  ax-setind 4603  ax-cnex 8051  ax-resscn 8052  ax-1cn 8053  ax-1re 8054  ax-icn 8055  ax-addcl 8056  ax-addrcl 8057  ax-mulcl 8058  ax-i2m1 8065  ax-0lt1 8066  ax-0id 8068  ax-rnegex 8069  ax-pre-ltirr 8072  ax-pre-ltwlin 8073  ax-pre-lttrn 8074  ax-pre-ltadd 8076

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ne 2379  df-nel 2474  df-ral 2491  df-rex 2492  df-rab 2495  df-v 2778  df-dif 3176  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-int 3900  df-br 4060  df-opab 4122  df-xp 4699  df-cnv 4701  df-iota 5251  df-fv 5298  df-ov 5970  df-pnf 8144  df-mnf 8145  df-xr 8146  df-ltxr 8147  df-le 8148  df-inn 9072  df-n0 9331

This theorem is referenced by:  nn0nlt0  9356  nn0ge0i  9357  nn0le0eq0  9358  nn0p1gt0  9359  0mnnnnn0  9362  nn0addge1  9376  nn0addge2  9377  nn0ge0d  9386  elnn0z  9420  nn0negleid  9476  nn0lt10b  9488  nn0ge0div  9495  nn0pnfge0  9948  xnn0xadd0  10024  0elfz  10275  fz0fzelfz0  10284  fz0fzdiffz0  10287  fzctr  10290  difelfzle  10291  fzoun  10340  elfzodifsumelfzo  10367  fvinim0ffz  10407  subfzo0  10408  adddivflid  10472  modqmuladdnn0  10550  modfzo0difsn  10577  uzennn  10618  bernneq  10842  bernneq3  10844  zzlesq  10890  faclbnd  10923  faclbnd6  10926  facubnd  10927  bcval5  10945  fihashneq0  10976  ccat0  11090  nn0maxcl  11651  dvdseq  12274  evennn02n  12308  nn0ehalf  12329  nn0oddm1d2  12335  bitsinv1  12388  gcdn0gt0  12414  nn0gcdid0  12417  absmulgcd  12453  algcvgblem  12486  algcvga  12488  lcmgcdnn  12519  hashgcdlem  12675  odzdvds  12683  pcfaclem  12787  znnen  12884  logbgcd1irr  15554  lgsdinn0  15640