Theorem 10re 12749

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 12731	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12362	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11258	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11273	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11274	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11260	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11273	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2834	1 ⊢ ;10 ∈ ℝ

Syntax hints:   ∈ wcel 2105  (class class class)co 7430  ℝcr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157  9c9 12325  ;cdc 12730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-dec 12731

This theorem is referenced by:  8lt10  12862  7lt10  12863  6lt10  12864  5lt10  12865  4lt10  12866  3lt10  12867  2lt10  12868  1lt10  12869  0.999...  15913  bpoly4  16091  plendxnocndx  17429  slotsdifdsndx  17439  slotsdifunifndx  17446  slotsdifplendx2  17462  cnfldfunALTOLDOLD  21410  thlleOLD  21734  bposlem4  27345  bposlem5  27346  dp2cl  32846  dp2lt10  32850  dp2lt  32851  dp2ltsuc  32852  dp2ltc  32853  dpfrac1  32858  dplti  32871  dpgti  32872  dpexpp1  32874  hgt750lem  34644  problem2  35650  lcmineqlem23  42032  aks4d1p1p7  42055  bgoldbtbndlem1  47729  tgblthelfgott  47739  tgoldbach  47741  prstclevalOLD  48869