Description: Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | 1mhdrd | |- ( ( 0 . _ 9 9 ) + ( 0 . _ 0 1 ) ) = 1 |
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 |