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 0
dpadd2.b B +
dpadd2.c C 0
dpadd2.d D +
dpadd2.e E 0
dpadd2.f F +
dpadd2.g G 0
dpadd2.h H 0
dpadd2.i G + H = I
dpadd2.1 A . B + C . D = E . F
Assertion dpadd2 Could not format assertion : No typesetting found for |- ( ( G . _ A B ) + ( H . _ C D ) ) = ( I . _ E F ) with typecode |-

Proof

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