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 )