Theorem 10re 12725

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 12707	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12337	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11233	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11248	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11249	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11235	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11248	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2830	1 ⊢ ;10 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7403  ℝcr 11126  0cc0 11127  1c1 11128   + caddc 11130   · cmul 11132  9c9 12300  ;cdc 12706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-2 12301  df-3 12302  df-4 12303  df-5 12304  df-6 12305  df-7 12306  df-8 12307  df-9 12308  df-dec 12707

This theorem is referenced by:  8lt10  12838  7lt10  12839  6lt10  12840  5lt10  12841  4lt10  12842  3lt10  12843  2lt10  12844  1lt10  12845  0.999...  15895  bpoly4  16073  plendxnocndx  17396  slotsdifdsndx  17406  slotsdifunifndx  17413  slotsdifplendx2  17428  bposlem4  27248  bposlem5  27249  dp2cl  32800  dp2lt10  32804  dp2lt  32805  dp2ltsuc  32806  dp2ltc  32807  dpfrac1  32812  dplti  32825  dpgti  32826  dpexpp1  32828  hgt750lem  34629  problem2  35634  lcmineqlem23  42010  aks4d1p1p7  42033  bgoldbtbndlem1  47767  tgblthelfgott  47777  tgoldbach  47779