Theorem 10re 12638

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

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

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 2709  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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224  df-7 12225  df-8 12226  df-9 12227  df-dec 12620

This theorem is referenced by:  8lt10  12751  7lt10  12752  6lt10  12753  5lt10  12754  4lt10  12755  3lt10  12756  2lt10  12757  1lt10  12758  0.999...  15816  bpoly4  15994  plendxnocndx  17316  slotsdifdsndx  17326  slotsdifunifndx  17333  slotsdifplendx2  17348  bposlem4  27269  bposlem5  27270  dp2cl  32976  dp2lt10  32980  dp2lt  32981  dp2ltsuc  32982  dp2ltc  32983  dpfrac1  32988  dplti  33001  dpgti  33002  dpexpp1  33004  hgt750lem  34833  problem2  35886  lcmineqlem23  42425  aks4d1p1p7  42448  bgoldbtbndlem1  48169  tgblthelfgott  48179  tgoldbach  48181