Theorem 1mhdrd

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

	Ref	Expression
Assertion	1mhdrd	|- ( ( 0 . _ 9 9 ) + ( 0 . _ 0 1 ) ) = 1

Proof

Step	Hyp	Ref	Expression
1		0nn0	|- 0 e. NN0
2		9nn0	|- 9 e. NN0
3		1nn0	|- 1 e. NN0
4	2	dec0h	|- 9 = ; 0 9
5	4	eqcomi	|- ; 0 9 = 9
6	5	deceq1i	|- ; ; 0 9 9 = ; 9 9
7	1	dec0h	|- 0 = ; 0 0
8	7	eqcomi	|- ; 0 0 = 0
9	8	deceq1i	|- ; ; 0 0 1 = ; 0 1
10		9cn	|- 9 e. CC
11	10	addid1i	|- ( 9 + 0 ) = 9
12	11	oveq1i	|- ( ( 9 + 0 ) + 1 ) = ( 9 + 1 )
13		9p1e10	|- ( 9 + 1 ) = ; 1 0
14	12 13	eqtri	|- ( ( 9 + 0 ) + 1 ) = ; 1 0
15	2 2 1 3 6 9 14 1 13	decaddc	|- ( ; ; 0 9 9 + ; ; 0 0 1 ) = ; ; 1 0 0
16	1 2 2 1 1 3 3 1 1 15	dpadd3	|- ( ( 0 . _ 9 9 ) + ( 0 . _ 0 1 ) ) = ( 1 . _ 0 0 )
17	1	dp20u	|- _ 0 0 = 0
18	17	oveq2i	|- ( 1 . _ 0 0 ) = ( 1 . 0 )
19	3	dp0u	|- ( 1 . 0 ) = 1
20	16 18 19	3eqtri	|- ( ( 0 . _ 9 9 ) + ( 0 . _ 0 1 ) ) = 1