Theorem 10re 12668

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 12650	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12285	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11174	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11189	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11190	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11176	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11189	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2824	1 ⊢ ;10 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067  0cc0 11068  1c1 11069   + caddc 11071   · cmul 11073  9c9 12248  ;cdc 12649

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253  df-7 12254  df-8 12255  df-9 12256  df-dec 12650

This theorem is referenced by:  8lt10  12781  7lt10  12782  6lt10  12783  5lt10  12784  4lt10  12785  3lt10  12786  2lt10  12787  1lt10  12788  0.999...  15847  bpoly4  16025  plendxnocndx  17347  slotsdifdsndx  17357  slotsdifunifndx  17364  slotsdifplendx2  17379  bposlem4  27198  bposlem5  27199  dp2cl  32800  dp2lt10  32804  dp2lt  32805  dp2ltsuc  32806  dp2ltc  32807  dpfrac1  32812  dplti  32825  dpgti  32826  dpexpp1  32828  hgt750lem  34642  problem2  35653  lcmineqlem23  42039  aks4d1p1p7  42062  bgoldbtbndlem1  47806  tgblthelfgott  47816  tgoldbach  47818