Theorem nn0red 8929

Description: A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nn0red.1	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Assertion

Ref	Expression
nn0red	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem nn0red

Step	Hyp	Ref	Expression
1		nn0ssre 8879	. 2 ⊢ ℕ0 ⊆ ℝ
2		nn0red.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sseldi 3059	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1461  ℝcr 7540  ℕ₀cn0 8875

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-cnex 7630  ax-resscn 7631  ax-1re 7633  ax-addrcl 7636  ax-rnegex 7648

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-sn 3497  df-int 3736  df-inn 8625  df-n0 8876

This theorem is referenced by:  nn0cnd  8930  nn0readdcl  8934  nn01to3  9305  flqmulnn0  9959  modifeq2int  10046  modaddmodup  10047  modaddmodlo  10048  modsumfzodifsn  10056  expnegap0  10188  nn0le2msqd  10352  nn0opthlem2d  10354  nn0opthd  10355  faclbnd6  10377  bcval5  10396  filtinf  10425  zfz1isolemiso  10469  mertenslemi1  11190  efcllemp  11209  eftlub  11241  oddge22np1  11420  nn0oddm1d2  11448  gcdaddm  11514  bezoutlemsup  11537  gcdzeq  11550  dvdssqlem  11558  nn0seqcvgd  11562  lcmneg  11595  mulgcddvds  11615  qredeu  11618  pw2dvdseulemle  11684  pw2dvdseu  11685  nn0sqrtelqelz  11723  nonsq  11724  ennnfoneleminc  11763  ennnfonelemkh  11764  ennnfonelemex  11766  ennnfonelemim  11776