This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dpadd2

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

Ref Expression
Hypotheses dpadd2.a 
|- A e. NN0
dpadd2.b 
|- B e. RR+
dpadd2.c 
|- C e. NN0
dpadd2.d 
|- D e. RR+
dpadd2.e 
|- E e. NN0
dpadd2.f 
|- F e. RR+
dpadd2.g 
|- G e. NN0
dpadd2.h 
|- H e. NN0
dpadd2.i 
|- ( G + H ) = I
dpadd2.1 
|- ( ( A . B ) + ( C . D ) ) = ( E . F )
Assertion dpadd2 
|- ( ( G . _ A B ) + ( H . _ C D ) ) = ( I . _ E F )

Proof

Step Hyp Ref Expression
1 dpadd2.a 
 |-  A e. NN0
2 dpadd2.b 
 |-  B e. RR+
3 dpadd2.c 
 |-  C e. NN0
4 dpadd2.d 
 |-  D e. RR+
5 dpadd2.e 
 |-  E e. NN0
6 dpadd2.f 
 |-  F e. RR+
7 dpadd2.g 
 |-  G e. NN0
8 dpadd2.h 
 |-  H e. NN0
9 dpadd2.i 
 |-  ( G + H ) = I
10 dpadd2.1 
 |-  ( ( A . B ) + ( C . D ) ) = ( E . F )
11 1 nn0rei 
 |-  A e. RR
12 rpre 
 |-  ( B e. RR+ -> B e. RR )
13 2 12 ax-mp 
 |-  B e. RR
14 dp2cl 
 |-  ( ( A e. RR /\ B e. RR ) -> _ A B e. RR )
15 11 13 14 mp2an 
 |-  _ A B e. RR
16 7 15 dpval2 
 |-  ( G . _ A B ) = ( G + ( _ A B / ; 1 0 ) )
17 3 nn0rei 
 |-  C e. RR
18 rpre 
 |-  ( D e. RR+ -> D e. RR )
19 4 18 ax-mp 
 |-  D e. RR
20 dp2cl 
 |-  ( ( C e. RR /\ D e. RR ) -> _ C D e. RR )
21 17 19 20 mp2an 
 |-  _ C D e. RR
22 8 21 dpval2 
 |-  ( H . _ C D ) = ( H + ( _ C D / ; 1 0 ) )
23 16 22 oveq12i 
 |-  ( ( G . _ A B ) + ( H . _ C D ) ) = ( ( G + ( _ A B / ; 1 0 ) ) + ( H + ( _ C D / ; 1 0 ) ) )
24 7 nn0cni 
 |-  G e. CC
25 15 recni 
 |-  _ A B e. CC
26 10nn 
 |-  ; 1 0 e. NN
27 26 nncni 
 |-  ; 1 0 e. CC
28 26 nnne0i 
 |-  ; 1 0 =/= 0
29 25 27 28 divcli 
 |-  ( _ A B / ; 1 0 ) e. CC
30 8 nn0cni 
 |-  H e. CC
31 21 recni 
 |-  _ C D e. CC
32 31 27 28 divcli 
 |-  ( _ C D / ; 1 0 ) e. CC
33 24 29 30 32 add4i 
 |-  ( ( G + ( _ A B / ; 1 0 ) ) + ( H + ( _ C D / ; 1 0 ) ) ) = ( ( G + H ) + ( ( _ A B / ; 1 0 ) + ( _ C D / ; 1 0 ) ) )
34 25 31 27 28 divdiri 
 |-  ( ( _ A B + _ C D ) / ; 1 0 ) = ( ( _ A B / ; 1 0 ) + ( _ C D / ; 1 0 ) )
35 dpval 
 |-  ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B )
36 1 13 35 mp2an 
 |-  ( A . B ) = _ A B
37 dpval 
 |-  ( ( C e. NN0 /\ D e. RR ) -> ( C . D ) = _ C D )
38 3 19 37 mp2an 
 |-  ( C . D ) = _ C D
39 36 38 oveq12i 
 |-  ( ( A . B ) + ( C . D ) ) = ( _ A B + _ C D )
40 rpre 
 |-  ( F e. RR+ -> F e. RR )
41 6 40 ax-mp 
 |-  F e. RR
42 dpval 
 |-  ( ( E e. NN0 /\ F e. RR ) -> ( E . F ) = _ E F )
43 5 41 42 mp2an 
 |-  ( E . F ) = _ E F
44 10 39 43 3eqtr3i 
 |-  ( _ A B + _ C D ) = _ E F
45 44 oveq1i 
 |-  ( ( _ A B + _ C D ) / ; 1 0 ) = ( _ E F / ; 1 0 )
46 34 45 eqtr3i 
 |-  ( ( _ A B / ; 1 0 ) + ( _ C D / ; 1 0 ) ) = ( _ E F / ; 1 0 )
47 9 46 oveq12i 
 |-  ( ( G + H ) + ( ( _ A B / ; 1 0 ) + ( _ C D / ; 1 0 ) ) ) = ( I + ( _ E F / ; 1 0 ) )
48 7 8 nn0addcli 
 |-  ( G + H ) e. NN0
49 9 48 eqeltrri 
 |-  I e. NN0
50 5 nn0rei 
 |-  E e. RR
51 dp2cl 
 |-  ( ( E e. RR /\ F e. RR ) -> _ E F e. RR )
52 50 41 51 mp2an 
 |-  _ E F e. RR
53 49 52 dpval2 
 |-  ( I . _ E F ) = ( I + ( _ E F / ; 1 0 ) )
54 47 53 eqtr4i 
 |-  ( ( G + H ) + ( ( _ A B / ; 1 0 ) + ( _ C D / ; 1 0 ) ) ) = ( I . _ E F )
55 23 33 54 3eqtri 
 |-  ( ( G . _ A B ) + ( H . _ C D ) ) = ( I . _ E F )