Theorem nn0ge0 8631

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 8608	. 2 |- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2		nnre 8364	. . . 4 |- ( N e. NN -> N e. RR )
3		nngt0 8382	. . . 4 |- ( N e. NN -> 0 < N )
4		0re 7432	. . . . 5 |- 0 e. RR
5		ltle 7516	. . . . 5 |- ( ( 0 e. RR /\ N e. RR ) -> ( 0 < N -> 0 <_ N ) )
6	4, 5	mpan 415	. . . 4 |- ( N e. RR -> ( 0 < N -> 0 <_ N ) )
7	2, 3, 6	sylc 61	. . 3 |- ( N e. NN -> 0 <_ N )
8		0le0 8446	. . . 4 |- 0 <_ 0
9		breq2 3824	. . . 4 |- ( N = 0 -> ( 0 <_ N <-> 0 <_ 0 ) )
10	8, 9	mpbiri 166	. . 3 |- ( N = 0 -> 0 <_ N )
11	7, 10	jaoi 669	. 2 |- ( ( N e. NN \/ N = 0 ) -> 0 <_ N )
12	1, 11	sylbi 119	1 |- ( N e. NN0 -> 0 <_ N )

Syntax hints:   -> wi 4   \/ wo 662   = wceq 1287   e. wcel 1436   class class class wbr 3820   RRcr 7293   0cc0 7294   < clt 7466   <_ cle 7467   NNcn 8357   NN0cn0 8606

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3932  ax-pow 3984  ax-pr 4010  ax-un 4234  ax-setind 4326  ax-cnex 7380  ax-resscn 7381  ax-1cn 7382  ax-1re 7383  ax-icn 7384  ax-addcl 7385  ax-addrcl 7386  ax-mulcl 7387  ax-i2m1 7394  ax-0lt1 7395  ax-0id 7397  ax-rnegex 7398  ax-pre-ltirr 7401  ax-pre-ltwlin 7402  ax-pre-lttrn 7403  ax-pre-ltadd 7405

This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-nel 2347  df-ral 2360  df-rex 2361  df-rab 2364  df-v 2617  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3637  df-int 3672  df-br 3821  df-opab 3875  df-xp 4417  df-cnv 4419  df-iota 4946  df-fv 4989  df-ov 5616  df-pnf 7468  df-mnf 7469  df-xr 7470  df-ltxr 7471  df-le 7472  df-inn 8358  df-n0 8607

This theorem is referenced by:  nn0nlt0  8632  nn0ge0i  8633  nn0le0eq0  8634  nn0p1gt0  8635  0mnnnnn0  8638  nn0addge1  8652  nn0addge2  8653  nn0ge0d  8662  elnn0z  8696  nn0lt10b  8760  nn0ge0div  8766  nn0pnfge0  9193  0elfz  9460  fz0fzelfz0  9466  fz0fzdiffz0  9469  fzctr  9472  difelfzle  9473  elfzodifsumelfzo  9540  fvinim0ffz  9580  subfzo0  9581  adddivflid  9627  modqmuladdnn0  9703  modfzo0difsn  9730  bernneq  9970  bernneq3  9972  faclbnd  10045  faclbnd6  10048  facubnd  10049  ibcval5  10067  fihashneq0  10099  dvdseq  10724  evennn02n  10757  nn0ehalf  10778  nn0oddm1d2  10784  gcdn0gt0  10844  nn0gcdid0  10847  absmulgcd  10881  algcvgblem  10906  ialgcvga  10908  lcmgcdnn  10939  hashgcdlem  11078  znnen  11086