Theorem 10re 12628

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 12610	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12246	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11134	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11149	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11150	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11136	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11149	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2832	1 ⊢ ;10 ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℝcr 11027  0cc0 11028  1c1 11029   + caddc 11031   · cmul 11033  9c9 12209  ;cdc 12609

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-i2m1 11096  ax-1ne0 11097  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-2 12210  df-3 12211  df-4 12212  df-5 12213  df-6 12214  df-7 12215  df-8 12216  df-9 12217  df-dec 12610

This theorem is referenced by:  8lt10  12741  7lt10  12742  6lt10  12743  5lt10  12744  4lt10  12745  3lt10  12746  2lt10  12747  1lt10  12748  0.999...  15806  bpoly4  15984  plendxnocndx  17306  slotsdifdsndx  17316  slotsdifunifndx  17323  slotsdifplendx2  17338  bposlem4  27256  bposlem5  27257  dp2cl  32963  dp2lt10  32967  dp2lt  32968  dp2ltsuc  32969  dp2ltc  32970  dpfrac1  32975  dplti  32988  dpgti  32989  dpexpp1  32991  hgt750lem  34810  problem2  35862  lcmineqlem23  42327  aks4d1p1p7  42350  bgoldbtbndlem1  48072  tgblthelfgott  48082  tgoldbach  48084