Theorem 10re 12456

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 12438	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12072	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 10975	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10990	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 10991	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 10977	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 10990	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2835	1 ⊢ ;10 ∈ ℝ

Syntax hints:   ∈ wcel 2106  (class class class)co 7275  ℝcr 10870  0cc0 10871  1c1 10872   + caddc 10874   · cmul 10876  9c9 12035  ;cdc 12437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-i2m1 10939  ax-1ne0 10940  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-dec 12438

This theorem is referenced by:  8lt10  12569  7lt10  12570  6lt10  12571  5lt10  12572  4lt10  12573  3lt10  12574  2lt10  12575  1lt10  12576  0.999...  15593  bpoly4  15769  plendxnocndx  17094  slotsdifdsndx  17104  slotsdifunifndx  17111  slotsdifplendx2  17127  cnfldfunALTOLD  20611  thlleOLD  20904  bposlem4  26435  bposlem5  26436  dp2cl  31154  dp2lt10  31158  dp2lt  31159  dp2ltsuc  31160  dp2ltc  31161  dpfrac1  31166  dplti  31179  dpgti  31180  dpexpp1  31182  hgt750lem  32631  problem2  33624  lcmineqlem23  40059  aks4d1p1p7  40082  bgoldbtbndlem1  45257  tgblthelfgott  45267  tgoldbach  45269  prstclevalOLD  46350