Theorem 10re 11936

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 11918	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 11551	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 10445	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10461	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 10462	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 10447	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 10461	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2864	1 ⊢ ;10 ∈ ℝ

Syntax hints:   ∈ wcel 2051  (class class class)co 6982  ℝcr 10340  0cc0 10341  1c1 10342   + caddc 10344   · cmul 10346  9c9 11508  ;cdc 11917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752  ax-1cn 10399  ax-icn 10400  ax-addcl 10401  ax-addrcl 10402  ax-mulcl 10403  ax-mulrcl 10404  ax-i2m1 10409  ax-1ne0 10410  ax-rnegex 10412  ax-rrecex 10413  ax-cnre 10414

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3419  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4182  df-if 4354  df-sn 4445  df-pr 4447  df-op 4451  df-uni 4718  df-br 4935  df-iota 6157  df-fv 6201  df-ov 6985  df-2 11509  df-3 11510  df-4 11511  df-5 11512  df-6 11513  df-7 11514  df-8 11515  df-9 11516  df-dec 11918

This theorem is referenced by:  8lt10  12051  7lt10  12052  6lt10  12053  5lt10  12054  4lt10  12055  3lt10  12056  2lt10  12057  1lt10  12058  0.999...  15103  bpoly4  15279  cnfldfun  20274  thlle  20558  bposlem4  25580  bposlem5  25581  dp2cl  30326  dp2lt10  30330  dp2lt  30331  dp2ltsuc  30332  dp2ltc  30333  dpfrac1  30338  dplti  30351  dpgti  30352  dpexpp1  30354  hgt750lem  31602  problem2  32469  bgoldbtbndlem1  43373  tgblthelfgott  43383  tgoldbach  43385