Theorem 10re 12752

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 12734	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12365	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11261	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11276	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11277	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11263	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11276	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2837	1 ⊢ ;10 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7431  ℝcr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  9c9 12328  ;cdc 12733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-dec 12734

This theorem is referenced by:  8lt10  12865  7lt10  12866  6lt10  12867  5lt10  12868  4lt10  12869  3lt10  12870  2lt10  12871  1lt10  12872  0.999...  15917  bpoly4  16095  plendxnocndx  17428  slotsdifdsndx  17438  slotsdifunifndx  17445  slotsdifplendx2  17461  cnfldfunALTOLDOLD  21393  thlleOLD  21717  bposlem4  27331  bposlem5  27332  dp2cl  32862  dp2lt10  32866  dp2lt  32867  dp2ltsuc  32868  dp2ltc  32869  dpfrac1  32874  dplti  32887  dpgti  32888  dpexpp1  32890  hgt750lem  34666  problem2  35671  lcmineqlem23  42052  aks4d1p1p7  42075  bgoldbtbndlem1  47792  tgblthelfgott  47802  tgoldbach  47804  prstclevalOLD  49158