Theorem 10re

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)

	Ref	Expression
Assertion	10re	$$⊢10\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		df-dec	$$⊢10=\left(9+1\right)\cdot 1+0$$
2		9re	$$⊢9\in ℝ$$
3		1re	$$⊢1\in ℝ$$
4	2 3	readdcli	$$⊢9+1\in ℝ$$
5	4 3	remulcli	$$⊢\left(9+1\right)\cdot 1\in ℝ$$
6		0re	$$⊢0\in ℝ$$
7	5 6	readdcli	$$⊢\left(9+1\right)\cdot 1+0\in ℝ$$
8	1 7	eqeltri	$$⊢10\in ℝ$$