Theorem 10re 12561

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 12543	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12177	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11080	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11095	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11096	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11082	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11095	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2834	1 ⊢ ;10 ∈ ℝ

Syntax hints:   ∈ wcel 2106  (class class class)co 7341  ℝcr 10975  0cc0 10976  1c1 10977   + caddc 10979   · cmul 10981  9c9 12140  ;cdc 12542

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 2708  ax-1cn 11034  ax-icn 11035  ax-addcl 11036  ax-addrcl 11037  ax-mulcl 11038  ax-mulrcl 11039  ax-i2m1 11044  ax-1ne0 11045  ax-rnegex 11047  ax-rrecex 11048  ax-cnre 11049

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-br 5097  df-iota 6435  df-fv 6491  df-ov 7344  df-2 12141  df-3 12142  df-4 12143  df-5 12144  df-6 12145  df-7 12146  df-8 12147  df-9 12148  df-dec 12543

This theorem is referenced by:  8lt10  12674  7lt10  12675  6lt10  12676  5lt10  12677  4lt10  12678  3lt10  12679  2lt10  12680  1lt10  12681  0.999...  15692  bpoly4  15868  plendxnocndx  17191  slotsdifdsndx  17201  slotsdifunifndx  17208  slotsdifplendx2  17224  cnfldfunALTOLD  20716  thlleOLD  21009  bposlem4  26540  bposlem5  26541  dp2cl  31439  dp2lt10  31443  dp2lt  31444  dp2ltsuc  31445  dp2ltc  31446  dpfrac1  31451  dplti  31464  dpgti  31465  dpexpp1  31467  hgt750lem  32929  problem2  33921  lcmineqlem23  40364  aks4d1p1p7  40387  bgoldbtbndlem1  45675  tgblthelfgott  45685  tgoldbach  45687  prstclevalOLD  46768