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 ) |