Theorem 10re 12105

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 12087	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 11724	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 10630	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10645	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 10646	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 10632	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 10645	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2886	1 ⊢ ;10 ∈ ℝ

Syntax hints:   ∈ wcel 2111  (class class class)co 7135  ℝcr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  9c9 11687  ;cdc 12086

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-dec 12087

This theorem is referenced by:  8lt10  12218  7lt10  12219  6lt10  12220  5lt10  12221  4lt10  12222  3lt10  12223  2lt10  12224  1lt10  12225  0.999...  15229  bpoly4  15405  cnfldfun  20103  thlle  20386  bposlem4  25871  bposlem5  25872  dp2cl  30582  dp2lt10  30586  dp2lt  30587  dp2ltsuc  30588  dp2ltc  30589  dpfrac1  30594  dplti  30607  dpgti  30608  dpexpp1  30610  hgt750lem  32032  problem2  33022  lcmineqlem23  39339  bgoldbtbndlem1  44323  tgblthelfgott  44333  tgoldbach  44335