Metamath Proof Explorer


Theorem 1mhdrd

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

Ref Expression
Assertion 1mhdrd 0 .99+0 .01=1

Proof

Step Hyp Ref Expression
1 0nn0 00
2 9nn0 90
3 1nn0 10
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
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 0 .99+0 .01=1 .00
17 1 dp20u 00=0
18 17 oveq2i 1 .00=1 .0
19 3 dp0u 1 .0=1
20 16 18 19 3eqtri 0 .99+0 .01=1