Theorem 10re 12646

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

Step	Hyp	Ref	Expression
1		df-dec 12628	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12261	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11164	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11179	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11180	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11166	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11179	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2828	1 ⊢ ;10 ∈ ℝ

Syntax hints:   ∈ wcel 2106  (class class class)co 7362  ℝcr 11059  0cc0 11060  1c1 11061   + caddc 11063   · cmul 11065  9c9 12224  ;cdc 12627

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-i2m1 11128  ax-1ne0 11129  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231  df-9 12232  df-dec 12628

This theorem is referenced by:  8lt10  12759  7lt10  12760  6lt10  12761  5lt10  12762  4lt10  12763  3lt10  12764  2lt10  12765  1lt10  12766  0.999...  15777  bpoly4  15953  plendxnocndx  17279  slotsdifdsndx  17289  slotsdifunifndx  17296  slotsdifplendx2  17312  cnfldfunALTOLD  20847  thlleOLD  21140  bposlem4  26672  bposlem5  26673  dp2cl  31806  dp2lt10  31810  dp2lt  31811  dp2ltsuc  31812  dp2ltc  31813  dpfrac1  31818  dplti  31831  dpgti  31832  dpexpp1  31834  hgt750lem  33353  problem2  34341  lcmineqlem23  40581  aks4d1p1p7  40604  bgoldbtbndlem1  46117  tgblthelfgott  46127  tgoldbach  46129  prstclevalOLD  47209