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

Theorem 10re 12638
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 12620 . 2 10 = (((9 + 1) · 1) + 0)
2 9re 12253 . . . . 5 9 ∈ ℝ
3 1re 11156 . . . . 5 1 ∈ ℝ
42, 3readdcli 11171 . . . 4 (9 + 1) ∈ ℝ
54, 3remulcli 11172 . . 3 ((9 + 1) · 1) ∈ ℝ
6 0re 11158 . . 3 0 ∈ ℝ
75, 6readdcli 11171 . 2 (((9 + 1) · 1) + 0) ∈ ℝ
81, 7eqeltri 2834 1 10 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  (class class class)co 7358  cr 11051  0cc0 11052  1c1 11053   + caddc 11055   · cmul 11057  9c9 12216  cdc 12619
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-i2m1 11120  ax-1ne0 11121  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361  df-2 12217  df-3 12218  df-4 12219  df-5 12220  df-6 12221  df-7 12222  df-8 12223  df-9 12224  df-dec 12620
This theorem is referenced by:  8lt10  12751  7lt10  12752  6lt10  12753  5lt10  12754  4lt10  12755  3lt10  12756  2lt10  12757  1lt10  12758  0.999...  15767  bpoly4  15943  plendxnocndx  17266  slotsdifdsndx  17276  slotsdifunifndx  17283  slotsdifplendx2  17299  cnfldfunALTOLD  20813  thlleOLD  21106  bposlem4  26638  bposlem5  26639  dp2cl  31739  dp2lt10  31743  dp2lt  31744  dp2ltsuc  31745  dp2ltc  31746  dpfrac1  31751  dplti  31764  dpgti  31765  dpexpp1  31767  hgt750lem  33267  problem2  34257  lcmineqlem23  40511  aks4d1p1p7  40534  bgoldbtbndlem1  46004  tgblthelfgott  46014  tgoldbach  46016  prstclevalOLD  47096
  Copyright terms: Public domain W3C validator