Theorem 1mhdrd

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

	Ref	Expression
Assertion	1mhdrd	$$⊢\mathrm{0\; <mi\; href="df-dp.html">.</mi>99}+\mathrm{0\; <mi\; href="df-dp.html">.</mi>01}=1$$

Proof

Step	Hyp	Ref	Expression
1		0nn0	$$⊢0\in {\mathbb{N}}_0$$
2		9nn0	$$⊢9\in {\mathbb{N}}_0$$
3		1nn0	$$⊢1\in {\mathbb{N}}_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	$$⊢\mathrm{0\; <mi\; href="df-dp.html">.</mi>99}+\mathrm{0\; <mi\; href="df-dp.html">.</mi>01}=\mathrm{1\; <mi\; href="df-dp.html">.</mi>00}$$
17	1	dp20u	$$⊢00=0$$
18	17	oveq2i	$$⊢\mathrm{1\; <mi\; href="df-dp.html">.</mi>00}=\mathrm{1\; <mi\; href="df-dp.html">.</mi>0}$$
19	3	dp0u	$$⊢\mathrm{1\; <mi\; href="df-dp.html">.</mi>0}=1$$
20	16 18 19	3eqtri	$$⊢\mathrm{0\; <mi\; href="df-dp.html">.</mi>99}+\mathrm{0\; <mi\; href="df-dp.html">.</mi>01}=1$$