Theorem 10re 12663

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 12645	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12280	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11144	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11160	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11161	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11146	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11160	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2832	1 ⊢ ;10 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℝcr 11037  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043  9c9 12243  ;cdc 12644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250  df-9 12251  df-dec 12645

This theorem is referenced by:  8lt10  12776  7lt10  12777  6lt10  12778  5lt10  12779  4lt10  12780  3lt10  12781  2lt10  12782  1lt10  12783  0.999...  15846  bpoly4  16024  plendxnocndx  17347  slotsdifdsndx  17357  slotsdifunifndx  17364  slotsdifplendx2  17379  bposlem4  27250  bposlem5  27251  dp2cl  32939  dp2lt10  32943  dp2lt  32944  dp2ltsuc  32945  dp2ltc  32946  dpfrac1  32951  dplti  32964  dpgti  32965  dpexpp1  32967  hgt750lem  34795  problem2  35848  lcmineqlem23  42490  aks4d1p1p7  42513  goldrasin  47330  bgoldbtbndlem1  48281  tgblthelfgott  48291  tgoldbach  48293