Metamath Proof Explorer


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