Metamath Proof Explorer

Theorem dpadd3

Description: Addition with two decimals. (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
dpmul.g 
|- G e. NN0
dpadd3.f 
|- F e. NN0
dpadd3.h 
|- H e. NN0
dpadd3.i 
|- I e. NN0
dpadd3.1 
|- ( ; ; A B C + ; ; D E F ) = ; ; G H I
Assertion dpadd3 
|- ( ( A . _ B C ) + ( D . _ E F ) ) = ( G . _ H I )

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 dpmul.g 
 |-  G e. NN0
7 dpadd3.f 
 |-  F e. NN0
8 dpadd3.h 
 |-  H e. NN0
9 dpadd3.i 
 |-  I e. NN0
10 dpadd3.1 
 |-  ( ; ; A B C + ; ; D E F ) = ; ; G H I
11 2 nn0rei 
 |-  B e. RR
12 3 nn0rei 
 |-  C e. RR
13 dp2cl 
 |-  ( ( B e. RR /\ C e. RR ) -> _ B C e. RR )
14 11 12 13 mp2an 
 |-  _ B C e. RR
15 dpcl 
 |-  ( ( A e. NN0 /\ _ B C e. RR ) -> ( A . _ B C ) e. RR )
16 1 14 15 mp2an 
 |-  ( A . _ B C ) e. RR
17 16 recni 
 |-  ( A . _ B C ) e. CC
18 5 nn0rei 
 |-  E e. RR
19 7 nn0rei 
 |-  F e. RR
20 dp2cl 
 |-  ( ( E e. RR /\ F e. RR ) -> _ E F e. RR )
21 18 19 20 mp2an 
 |-  _ E F e. RR
22 dpcl 
 |-  ( ( D e. NN0 /\ _ E F e. RR ) -> ( D . _ E F ) e. RR )
23 4 21 22 mp2an 
 |-  ( D . _ E F ) e. RR
24 23 recni 
 |-  ( D . _ E F ) e. CC
25 17 24 addcli 
 |-  ( ( A . _ B C ) + ( D . _ E F ) ) e. CC
26 8 nn0rei 
 |-  H e. RR
27 9 nn0rei 
 |-  I e. RR
28 dp2cl 
 |-  ( ( H e. RR /\ I e. RR ) -> _ H I e. RR )
29 26 27 28 mp2an 
 |-  _ H I e. RR
30 dpcl 
 |-  ( ( G e. NN0 /\ _ H I e. RR ) -> ( G . _ H I ) e. RR )
31 6 29 30 mp2an 
 |-  ( G . _ H I ) e. RR
32 31 recni 
 |-  ( G . _ H I ) e. CC
33 10nn 
 |-  ; 1 0 e. NN
34 33 decnncl2 
 |-  ; ; 1 0 0 e. NN
35 34 nncni 
 |-  ; ; 1 0 0 e. CC
36 34 nnne0i 
 |-  ; ; 1 0 0 =/= 0
37 35 36 pm3.2i 
 |-  ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 )
38 25 32 37 3pm3.2i 
 |-  ( ( ( A . _ B C ) + ( D . _ E F ) ) e. CC /\ ( G . _ H I ) e. CC /\ ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 ) )
39 17 24 35 adddiri 
 |-  ( ( ( A . _ B C ) + ( D . _ E F ) ) x. ; ; 1 0 0 ) = ( ( ( A . _ B C ) x. ; ; 1 0 0 ) + ( ( D . _ E F ) x. ; ; 1 0 0 ) )
40 1 2 12 dpmul100 
 |-  ( ( A . _ B C ) x. ; ; 1 0 0 ) = ; ; A B C
41 4 5 19 dpmul100 
 |-  ( ( D . _ E F ) x. ; ; 1 0 0 ) = ; ; D E F
42 40 41 oveq12i 
 |-  ( ( ( A . _ B C ) x. ; ; 1 0 0 ) + ( ( D . _ E F ) x. ; ; 1 0 0 ) ) = ( ; ; A B C + ; ; D E F )
43 6 8 27 dpmul100 
 |-  ( ( G . _ H I ) x. ; ; 1 0 0 ) = ; ; G H I
44 10 42 43 3eqtr4i 
 |-  ( ( ( A . _ B C ) x. ; ; 1 0 0 ) + ( ( D . _ E F ) x. ; ; 1 0 0 ) ) = ( ( G . _ H I ) x. ; ; 1 0 0 )
45 39 44 eqtri 
 |-  ( ( ( A . _ B C ) + ( D . _ E F ) ) x. ; ; 1 0 0 ) = ( ( G . _ H I ) x. ; ; 1 0 0 )
46 mulcan2 
 |-  ( ( ( ( A . _ B C ) + ( D . _ E F ) ) e. CC /\ ( G . _ H I ) e. CC /\ ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 ) ) -> ( ( ( ( A . _ B C ) + ( D . _ E F ) ) x. ; ; 1 0 0 ) = ( ( G . _ H I ) x. ; ; 1 0 0 ) <-> ( ( A . _ B C ) + ( D . _ E F ) ) = ( G . _ H I ) ) )
47 46 biimpa 
 |-  ( ( ( ( ( A . _ B C ) + ( D . _ E F ) ) e. CC /\ ( G . _ H I ) e. CC /\ ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 ) ) /\ ( ( ( A . _ B C ) + ( D . _ E F ) ) x. ; ; 1 0 0 ) = ( ( G . _ H I ) x. ; ; 1 0 0 ) ) -> ( ( A . _ B C ) + ( D . _ E F ) ) = ( G . _ H I ) )
48 38 45 47 mp2an 
 |-  ( ( A . _ B C ) + ( D . _ E F ) ) = ( G . _ H I )