Theorem nn0ge0 12438

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	⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)

Proof of Theorem nn0ge0

Step	Hyp	Ref	Expression
1		elnn0 12415	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		nngt0 12188	. . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
3		id 22	. . . . 5 ⊢ (𝑁 = 0 → 𝑁 = 0)
4	3	eqcomd 2743	. . . 4 ⊢ (𝑁 = 0 → 0 = 𝑁)
5	2, 4	orim12i 909	. . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0 < 𝑁 ∨ 0 = 𝑁))
6	1, 5	sylbi 217	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 < 𝑁 ∨ 0 = 𝑁))
7		0re 11146	. . 3 ⊢ 0 ∈ ℝ
8		nn0re 12422	. . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
9		leloe 11231	. . 3 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
10	7, 8, 9	sylancr 588	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
11	6, 10	mpbird 257	1 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 848   = wceq 1542   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037  0cc0 11038   < clt 11178   ≤ cle 11179  ℕcn 12157  ℕ₀cn0 12413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-n0 12414

This theorem is referenced by:  nn0nlt0  12439  nn0ge0i  12440  nn0le0eq0  12441  nn0p1gt0  12442  0mnnnnn0  12445  nn0addge1  12459  nn0addge2  12460  nn0negleid  12465  nn0ge0d  12477  nn0ge0div  12573  xnn0ge0  13060  xnn0xadd0  13174  nn0rp0  13383  xnn0xrge0  13434  0elfz  13552  fz0fzelfz0  13562  fz0fzdiffz0  13565  fzctr  13568  difelfzle  13569  fzoun  13624  nn0p1elfzo  13630  elfzodifsumelfzo  13659  fvinim0ffz  13717  subfzo0  13720  adddivflid  13750  modmuladdnn0  13850  addmodid  13854  modifeq2int  13868  modfzo0difsn  13878  nn0sq11  14067  zzlesq  14141  bernneq  14164  bernneq3  14166  faclbnd  14225  faclbnd6  14234  facubnd  14235  bcval5  14253  hashneq0  14299  fi1uzind  14442  ccat0  14511  ccat2s1fvw  14574  repswswrd  14719  nn0sqeq1  15211  nn0absid  15365  rprisefaccl  15958  dvdseq  16253  evennn02n  16289  nn0ehalf  16317  nn0oddm1d2  16324  bitsinv1  16381  smuval2  16421  gcdn0gt0  16457  nn0gcdid0  16460  absmulgcd  16488  algcvgblem  16516  algcvga  16518  lcmgcdnn  16550  lcmfun  16584  lcmfass  16585  2mulprm  16632  nonsq  16698  hashgcdlem  16727  odzdvds  16735  pcfaclem  16838  prmirredlem  21439  prmirred  21441  coe1sclmul  22236  coe1sclmul2  22238  fvmptnn04ifb  22807  mdegle0  26050  plypf1  26185  dgrlt  26240  fta1  26284  taylfval  26334  logbgcd1irr  26772  eldmgm  27000  basellem3  27061  bcmono  27256  lgsdinn0  27324  2sq2  27412  2sqnn0  27417  2sqreulem1  27425  dchrisumlem1  27468  dchrisumlem2  27469  wwlksnextwrd  29982  wwlksnextfun  29983  wwlksnextinj  29984  wwlksnextproplem2  29995  wwlksnextproplem3  29996  wrdt2ind  33045  xrsmulgzz  33101  hashf2  34261  hasheuni  34262  reprinfz1  34799  0nn0m1nnn0  35326  faclimlem1  35956  rrntotbnd  38084  gcdnn0id  42696  pell14qrgt0  43213  pell1qrgaplem  43227  monotoddzzfi  43296  jm2.17a  43314  jm2.22  43349  rmxdiophlem  43369  rexanuz2nf  45847  wallispilem3  46422  stirlinglem7  46435  elfz2z  47672  fz0addge0  47676  elfzlble  47677  2ffzoeq  47684  addmodne  47701  iccpartigtl  47780  sqrtpwpw2p  47895  flsqrt  47950  nn0e  48054  nn0sumltlt  48707  nn0eo  48885  fllog2  48925  dignn0fr  48958  dignnld  48960  dig1  48965  itcovalt2lem2lem1  49030