Theorem nn0ge0 9538

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 9515	. 2 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		nnre 9261	. . . 4 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
3		nngt0 9279	. . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
4		0re 8290	. . . . 5 ⊢ 0 ∈ ℝ
5		ltle 8377	. . . . 5 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 < 𝑁 → 0 ≤ 𝑁))
6	4, 5	mpan 424	. . . 4 ⊢ (𝑁 ∈ ℝ → (0 < 𝑁 → 0 ≤ 𝑁))
7	2, 3, 6	sylc 62	. . 3 ⊢ (𝑁 ∈ ℕ → 0 ≤ 𝑁)
8		0le0 9343	. . . 4 ⊢ 0 ≤ 0
9		breq2 4118	. . . 4 ⊢ (𝑁 = 0 → (0 ≤ 𝑁 ↔ 0 ≤ 0))
10	8, 9	mpbiri 168	. . 3 ⊢ (𝑁 = 0 → 0 ≤ 𝑁)
11	7, 10	jaoi 724	. 2 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → 0 ≤ 𝑁)
12	1, 11	sylbi 121	1 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)

Syntax hints:   → wi 4   ∨ wo 716   = wceq 1398   ∈ wcel 2205   class class class wbr 4114  ℝcr 8142  0cc0 8143   < clt 8324   ≤ cle 8325  ℕcn 9254  ℕ₀cn0 9513

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327  ax-un 4559  ax-setind 4664  ax-cnex 8234  ax-resscn 8235  ax-1cn 8236  ax-1re 8237  ax-icn 8238  ax-addcl 8239  ax-addrcl 8240  ax-mulcl 8241  ax-i2m1 8248  ax-0lt1 8249  ax-0id 8251  ax-rnegex 8252  ax-pre-ltirr 8255  ax-pre-ltwlin 8256  ax-pre-lttrn 8257  ax-pre-ltadd 8259

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-nel 2510  df-ral 2527  df-rex 2528  df-rab 2531  df-v 2817  df-dif 3216  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-int 3955  df-br 4115  df-opab 4177  df-xp 4760  df-cnv 4762  df-iota 5317  df-fv 5365  df-ov 6061  df-pnf 8326  df-mnf 8327  df-xr 8328  df-ltxr 8329  df-le 8330  df-inn 9255  df-n0 9514

This theorem is referenced by:  nn0nlt0  9539  nn0ge0i  9540  nn0le0eq0  9541  nn0p1gt0  9542  0mnnnnn0  9545  nn0addge1  9559  nn0addge2  9560  nn0ge0d  9573  elnn0z  9607  nn0negleid  9663  nn0lt10b  9676  nn0ge0div  9683  nn0pnfge0  10143  xnn0xadd0  10219  0elfz  10474  fz0fzelfz0  10483  fz0fzdiffz0  10486  fzctr  10489  difelfzle  10490  fzoun  10539  nn0p1elfzo  10543  elfzodifsumelfzo  10568  fvinim0ffz  10609  subfzo0  10610  adddivflid  10676  modqmuladdnn0  10754  modfzo0difsn  10781  uzennn  10822  bernneq  11047  bernneq3  11049  zzlesq  11095  faclbnd  11128  faclbnd6  11131  facubnd  11132  bcval5  11150  fihashneq0  11182  ccat0  11309  ccat2s1fvwd  11360  nn0maxcl  11935  dvdseq  12559  evennn02n  12593  nn0ehalf  12614  nn0oddm1d2  12620  bitsinv1  12673  gcdn0gt0  12699  nn0gcdid0  12702  absmulgcd  12738  algcvgblem  12771  algcvga  12773  lcmgcdnn  12804  hashgcdlem  12960  odzdvds  12968  pcfaclem  13072  znnen  13233  logbgcd1irr  15958  lgsdinn0  16047