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 ∈ ℕ0
2		9nn0	⊢ 9 ∈ ℕ0
3		1nn0	⊢ 1 ∈ ℕ0
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 ∈ ℂ
11	10	addridi	⊢ ( 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