1mhdrd

Description: Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021)

		Ref	Expression
	Assertion	1mhdrd	$⊢ 0.99 + 0.01 = 1$

Step	Hyp	Ref	Expression
1		0nn0	$⊢ 0 \in ℕ_{0}$
2		9nn0	$⊢ 9 \in ℕ_{0}$
3		1nn0	$⊢ 1 \in ℕ_{0}$
4	2	dec0h	$⊢ 9 = 09$
5	4	eqcomi	$⊢ 09 = 9$
6	5	deceq1i	$⊢ 099 = 99$
7	1	dec0h	$⊢ 0 = 00$
8	7	eqcomi	$⊢ 00 = 0$
9	8	deceq1i	$⊢ 001 = 01$
10		9cn	$⊢ 9 \in ℂ$
11	10	addid1i	$⊢ 9 + 0 = 9$
12	11	oveq1i	$⊢ 9 + 0 + 1 = 9 + 1$
13		9p1e10	$⊢ 9 + 1 = 10$
14	12 13	eqtri	$⊢ 9 + 0 + 1 = 10$
15	2 2 1 3 6 9 14 1 13	decaddc	$⊢ 099 + 001 = 100$
16	1 2 2 1 1 3 3 1 1 15	dpadd3	$⊢ 0.99 + 0.01 = 1.00$
17	1	dp20u	$⊢ 00 = 0$
18	17	oveq2i	$⊢ 1.00 = 1.0$
19	3	dp0u	$⊢ 1.0 = 1$
20	16 18 19	3eqtri	$⊢ 0.99 + 0.01 = 1$

Metamath Proof Explorer