Metamath Proof Explorer

Theorem dpadd

Description: Addition with one decimal. (Contributed by Thierry Arnoux, 27-Dec-2021)

Ref Expression
Hypotheses dpmul.a 
|- A e. NN0
dpmul.b 
|- B e. NN0
dpmul.c 
|- C e. NN0
dpmul.d 
|- D e. NN0
dpmul.e 
|- E e. NN0
dpadd.f 
|- F e. NN0
dpadd.1 
|- ( ; A B + ; C D ) = ; E F
Assertion dpadd 
|- ( ( A . B ) + ( C . D ) ) = ( E . F )

Proof

Step Hyp Ref Expression
1 dpmul.a 
 |-  A e. NN0
2 dpmul.b 
 |-  B e. NN0
3 dpmul.c 
 |-  C e. NN0
4 dpmul.d 
 |-  D e. NN0
5 dpmul.e 
 |-  E e. NN0
6 dpadd.f 
 |-  F e. NN0
7 dpadd.1 
 |-  ( ; A B + ; C D ) = ; E F
8 1 2 deccl 
 |-  ; A B e. NN0
9 8 nn0cni 
 |-  ; A B e. CC
10 3 4 deccl 
 |-  ; C D e. NN0
11 10 nn0cni 
 |-  ; C D e. CC
12 10nn 
 |-  ; 1 0 e. NN
13 12 nncni 
 |-  ; 1 0 e. CC
14 12 nnne0i 
 |-  ; 1 0 =/= 0
15 9 11 13 14 divdiri 
 |-  ( ( ; A B + ; C D ) / ; 1 0 ) = ( ( ; A B / ; 1 0 ) + ( ; C D / ; 1 0 ) )
16 7 oveq1i 
 |-  ( ( ; A B + ; C D ) / ; 1 0 ) = ( ; E F / ; 1 0 )
17 15 16 eqtr3i 
 |-  ( ( ; A B / ; 1 0 ) + ( ; C D / ; 1 0 ) ) = ( ; E F / ; 1 0 )
18 2 nn0rei 
 |-  B e. RR
19 1 18 decdiv10 
 |-  ( ; A B / ; 1 0 ) = ( A . B )
20 4 nn0rei 
 |-  D e. RR
21 3 20 decdiv10 
 |-  ( ; C D / ; 1 0 ) = ( C . D )
22 19 21 oveq12i 
 |-  ( ( ; A B / ; 1 0 ) + ( ; C D / ; 1 0 ) ) = ( ( A . B ) + ( C . D ) )
23 6 nn0rei 
 |-  F e. RR
24 5 23 decdiv10 
 |-  ( ; E F / ; 1 0 ) = ( E . F )
25 17 22 24 3eqtr3i 
 |-  ( ( A . B ) + ( C . D ) ) = ( E . F )