Step |
Hyp |
Ref |
Expression |
1 |
|
df-dp2 |
|- _ A B = ( A + ( B / ; 1 0 ) ) |
2 |
|
dpval |
|- ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B ) |
3 |
|
nn0cn |
|- ( A e. NN0 -> A e. CC ) |
4 |
|
recn |
|- ( B e. RR -> B e. CC ) |
5 |
|
dfdec10 |
|- ; A B = ( ( ; 1 0 x. A ) + B ) |
6 |
5
|
oveq1i |
|- ( ; A B / ; 1 0 ) = ( ( ( ; 1 0 x. A ) + B ) / ; 1 0 ) |
7 |
|
10re |
|- ; 1 0 e. RR |
8 |
7
|
recni |
|- ; 1 0 e. CC |
9 |
8
|
a1i |
|- ( A e. CC -> ; 1 0 e. CC ) |
10 |
|
id |
|- ( A e. CC -> A e. CC ) |
11 |
9 10
|
mulcld |
|- ( A e. CC -> ( ; 1 0 x. A ) e. CC ) |
12 |
|
10pos |
|- 0 < ; 1 0 |
13 |
7 12
|
gt0ne0ii |
|- ; 1 0 =/= 0 |
14 |
8 13
|
pm3.2i |
|- ( ; 1 0 e. CC /\ ; 1 0 =/= 0 ) |
15 |
|
divdir |
|- ( ( ( ; 1 0 x. A ) e. CC /\ B e. CC /\ ( ; 1 0 e. CC /\ ; 1 0 =/= 0 ) ) -> ( ( ( ; 1 0 x. A ) + B ) / ; 1 0 ) = ( ( ( ; 1 0 x. A ) / ; 1 0 ) + ( B / ; 1 0 ) ) ) |
16 |
14 15
|
mp3an3 |
|- ( ( ( ; 1 0 x. A ) e. CC /\ B e. CC ) -> ( ( ( ; 1 0 x. A ) + B ) / ; 1 0 ) = ( ( ( ; 1 0 x. A ) / ; 1 0 ) + ( B / ; 1 0 ) ) ) |
17 |
11 16
|
sylan |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( ; 1 0 x. A ) + B ) / ; 1 0 ) = ( ( ( ; 1 0 x. A ) / ; 1 0 ) + ( B / ; 1 0 ) ) ) |
18 |
|
divcan3 |
|- ( ( A e. CC /\ ; 1 0 e. CC /\ ; 1 0 =/= 0 ) -> ( ( ; 1 0 x. A ) / ; 1 0 ) = A ) |
19 |
8 13 18
|
mp3an23 |
|- ( A e. CC -> ( ( ; 1 0 x. A ) / ; 1 0 ) = A ) |
20 |
19
|
oveq1d |
|- ( A e. CC -> ( ( ( ; 1 0 x. A ) / ; 1 0 ) + ( B / ; 1 0 ) ) = ( A + ( B / ; 1 0 ) ) ) |
21 |
20
|
adantr |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( ; 1 0 x. A ) / ; 1 0 ) + ( B / ; 1 0 ) ) = ( A + ( B / ; 1 0 ) ) ) |
22 |
17 21
|
eqtrd |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( ; 1 0 x. A ) + B ) / ; 1 0 ) = ( A + ( B / ; 1 0 ) ) ) |
23 |
6 22
|
syl5eq |
|- ( ( A e. CC /\ B e. CC ) -> ( ; A B / ; 1 0 ) = ( A + ( B / ; 1 0 ) ) ) |
24 |
3 4 23
|
syl2an |
|- ( ( A e. NN0 /\ B e. RR ) -> ( ; A B / ; 1 0 ) = ( A + ( B / ; 1 0 ) ) ) |
25 |
1 2 24
|
3eqtr4a |
|- ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = ( ; A B / ; 1 0 ) ) |