Theorem nn0ge0 9415

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 9392	. 2 |- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2		nnre 9138	. . . 4 |- ( N e. NN -> N e. RR )
3		nngt0 9156	. . . 4 |- ( N e. NN -> 0 < N )
4		0re 8167	. . . . 5 |- 0 e. RR
5		ltle 8255	. . . . 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 9220	. . . 4 |- 0 <_ 0
9		breq2 4088	. . . 4 |- ( N = 0 -> ( 0 <_ N <-> 0 <_ 0 ) )
10	8, 9	mpbiri 168	. . 3 |- ( N = 0 -> 0 <_ N )
11	7, 10	jaoi 721	. 2 |- ( ( N e. NN \/ N = 0 ) -> 0 <_ N )
12	1, 11	sylbi 121	1 |- ( N e. NN0 -> 0 <_ N )

Syntax hints:   -> wi 4   \/ wo 713   = wceq 1395   e. wcel 2200   class class class wbr 4084   RRcr 8019   0cc0 8020   < clt 8202   <_ cle 8203   NNcn 9131   NN0cn0 9390

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4203  ax-pow 4260  ax-pr 4295  ax-un 4526  ax-setind 4631  ax-cnex 8111  ax-resscn 8112  ax-1cn 8113  ax-1re 8114  ax-icn 8115  ax-addcl 8116  ax-addrcl 8117  ax-mulcl 8118  ax-i2m1 8125  ax-0lt1 8126  ax-0id 8128  ax-rnegex 8129  ax-pre-ltirr 8132  ax-pre-ltwlin 8133  ax-pre-lttrn 8134  ax-pre-ltadd 8136

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2802  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3890  df-int 3925  df-br 4085  df-opab 4147  df-xp 4727  df-cnv 4729  df-iota 5282  df-fv 5330  df-ov 6014  df-pnf 8204  df-mnf 8205  df-xr 8206  df-ltxr 8207  df-le 8208  df-inn 9132  df-n0 9391

This theorem is referenced by:  nn0nlt0  9416  nn0ge0i  9417  nn0le0eq0  9418  nn0p1gt0  9419  0mnnnnn0  9422  nn0addge1  9436  nn0addge2  9437  nn0ge0d  9446  elnn0z  9480  nn0negleid  9536  nn0lt10b  9548  nn0ge0div  9555  nn0pnfge0  10014  xnn0xadd0  10090  0elfz  10341  fz0fzelfz0  10350  fz0fzdiffz0  10353  fzctr  10356  difelfzle  10357  fzoun  10406  elfzodifsumelfzo  10434  fvinim0ffz  10475  subfzo0  10476  adddivflid  10540  modqmuladdnn0  10618  modfzo0difsn  10645  uzennn  10686  bernneq  10910  bernneq3  10912  zzlesq  10958  faclbnd  10991  faclbnd6  10994  facubnd  10995  bcval5  11013  fihashneq0  11044  ccat0  11160  ccat2s1fvwd  11211  nn0maxcl  11773  dvdseq  12396  evennn02n  12430  nn0ehalf  12451  nn0oddm1d2  12457  bitsinv1  12510  gcdn0gt0  12536  nn0gcdid0  12539  absmulgcd  12575  algcvgblem  12608  algcvga  12610  lcmgcdnn  12641  hashgcdlem  12797  odzdvds  12805  pcfaclem  12909  znnen  13006  logbgcd1irr  15678  lgsdinn0  15764