Theorem 10re 12629

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 12611	. 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 2824	1 ⊢ ;10 ∈ ℝ

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  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 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  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 12611

This theorem is referenced by:  8lt10  12742  7lt10  12743  6lt10  12744  5lt10  12745  4lt10  12746  3lt10  12747  2lt10  12748  1lt10  12749  0.999...  15807  bpoly4  15985  plendxnocndx  17307  slotsdifdsndx  17317  slotsdifunifndx  17324  slotsdifplendx2  17339  bposlem4  27215  bposlem5  27216  dp2cl  32839  dp2lt10  32843  dp2lt  32844  dp2ltsuc  32845  dp2ltc  32846  dpfrac1  32851  dplti  32864  dpgti  32865  dpexpp1  32867  hgt750lem  34638  problem2  35658  lcmineqlem23  42044  aks4d1p1p7  42067  bgoldbtbndlem1  47809  tgblthelfgott  47819  tgoldbach  47821