MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  10re Structured version   Visualization version   GIF version

Theorem 10re 12706
Description: The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 8-Oct-2022.)
Assertion
Ref Expression
10re 10 ∈ ℝ

Proof of Theorem 10re
StepHypRef Expression
1 df-dec 12684 . 2 10 = (((9 + 1) · 1) + 0)
2 9re 12312 . . . . 5 9 ∈ ℝ
3 1re 11176 . . . . 5 1 ∈ ℝ
42, 3readdcli 11192 . . . 4 (9 + 1) ∈ ℝ
54, 3remulcli 11193 . . 3 ((9 + 1) · 1) ∈ ℝ
6 0re 11178 . . 3 0 ∈ ℝ
75, 6readdcli 11192 . 2 (((9 + 1) · 1) + 0) ∈ ℝ
81, 7eqeltri 2857 1 10 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2141  (class class class)co 7390  cr 11067  0cc0 11068  1c1 11069   + caddc 11071   · cmul 11073  9c9 12274  cdc 12683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141
This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6471  df-fv 6523  df-ov 7393  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-dec 12684
This theorem is referenced by:  1lt10OLD  12829  0.999...  15892  bpoly4  16070  plendxnocndx  17394  slotsdifdsndx  17404  slotsdifunifndx  17411  slotsdifplendx2  17426  bposlem4  27326  bposlem5  27327  dp2cl  33016  dp2lt10  33020  dp2lt  33021  dp2ltsuc  33022  dp2ltc  33023  dpfrac1  33028  dplti  33041  dpgti  33042  dpexpp1  33044  hgt750lem  34907  problem2  35969  lcmineqlem23  42621  aks4d1p1p7  42644  goldrasin  47429  bgoldbtbndlem1  48380  tgblthelfgott  48390  tgoldbach  48392
  Copyright terms: Public domain W3C validator