Theorem 10re 12644

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 12626	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12261	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11150	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11165	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11166	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11152	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11165	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2824	1 ⊢ ;10 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℝcr 11043  0cc0 11044  1c1 11045   + caddc 11047   · cmul 11049  9c9 12224  ;cdc 12625

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 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-i2m1 11112  ax-1ne0 11113  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231  df-9 12232  df-dec 12626

This theorem is referenced by:  8lt10  12757  7lt10  12758  6lt10  12759  5lt10  12760  4lt10  12761  3lt10  12762  2lt10  12763  1lt10  12764  0.999...  15823  bpoly4  16001  plendxnocndx  17323  slotsdifdsndx  17333  slotsdifunifndx  17340  slotsdifplendx2  17355  bposlem4  27231  bposlem5  27232  dp2cl  32850  dp2lt10  32854  dp2lt  32855  dp2ltsuc  32856  dp2ltc  32857  dpfrac1  32862  dplti  32875  dpgti  32876  dpexpp1  32878  hgt750lem  34635  problem2  35646  lcmineqlem23  42032  aks4d1p1p7  42055  bgoldbtbndlem1  47799  tgblthelfgott  47809  tgoldbach  47811