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

Theorem 10re 12114
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 12096 . 2 10 = (((9 + 1) · 1) + 0)
2 9re 11733 . . . . 5 9 ∈ ℝ
3 1re 10639 . . . . 5 1 ∈ ℝ
42, 3readdcli 10654 . . . 4 (9 + 1) ∈ ℝ
54, 3remulcli 10655 . . 3 ((9 + 1) · 1) ∈ ℝ
6 0re 10641 . . 3 0 ∈ ℝ
75, 6readdcli 10654 . 2 (((9 + 1) · 1) + 0) ∈ ℝ
81, 7eqeltri 2912 1 10 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2115  (class class class)co 7149  cr 10534  0cc0 10535  1c1 10536   + caddc 10538   · cmul 10540  9c9 11696  cdc 12095
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-i2m1 10603  ax-1ne0 10604  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-ne 3015  df-ral 3138  df-rex 3139  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-iota 6302  df-fv 6351  df-ov 7152  df-2 11697  df-3 11698  df-4 11699  df-5 11700  df-6 11701  df-7 11702  df-8 11703  df-9 11704  df-dec 12096
This theorem is referenced by:  8lt10  12227  7lt10  12228  6lt10  12229  5lt10  12230  4lt10  12231  3lt10  12232  2lt10  12233  1lt10  12234  0.999...  15237  bpoly4  15413  cnfldfun  20557  thlle  20841  bposlem4  25874  bposlem5  25875  dp2cl  30567  dp2lt10  30571  dp2lt  30572  dp2ltsuc  30573  dp2ltc  30574  dpfrac1  30579  dplti  30592  dpgti  30593  dpexpp1  30595  hgt750lem  31979  problem2  32966  lcmineqlem23  39287  bgoldbtbndlem1  44249  tgblthelfgott  44259  tgoldbach  44261
  Copyright terms: Public domain W3C validator