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 |
|
dpmul.j |
|- J e. NN0 |
8 |
|
dpmul.k |
|- K e. NN0 |
9 |
|
dpmul.1 |
|- ( A x. C ) = F |
10 |
|
dpmul.2 |
|- ( A x. D ) = M |
11 |
|
dpmul.3 |
|- ( B x. C ) = L |
12 |
|
dpmul.4 |
|- ( B x. D ) = ; E K |
13 |
|
dpmul.5 |
|- ( ( L + M ) + E ) = ; G J |
14 |
|
dpmul.6 |
|- ( F + G ) = I |
15 |
1 2
|
deccl |
|- ; A B e. NN0 |
16 |
|
eqid |
|- ; C D = ; C D |
17 |
1 4
|
nn0mulcli |
|- ( A x. D ) e. NN0 |
18 |
10 17
|
eqeltrri |
|- M e. NN0 |
19 |
18 5
|
nn0addcli |
|- ( M + E ) e. NN0 |
20 |
|
eqid |
|- ; A B = ; A B |
21 |
3 1 2 20 9 11
|
decmul1 |
|- ( ; A B x. C ) = ; F L |
22 |
21
|
oveq1i |
|- ( ( ; A B x. C ) + ( M + E ) ) = ( ; F L + ( M + E ) ) |
23 |
|
dfdec10 |
|- ; F L = ( ( ; 1 0 x. F ) + L ) |
24 |
23
|
oveq1i |
|- ( ; F L + ( M + E ) ) = ( ( ( ; 1 0 x. F ) + L ) + ( M + E ) ) |
25 |
|
10nn0 |
|- ; 1 0 e. NN0 |
26 |
25
|
nn0cni |
|- ; 1 0 e. CC |
27 |
1 3
|
nn0mulcli |
|- ( A x. C ) e. NN0 |
28 |
9 27
|
eqeltrri |
|- F e. NN0 |
29 |
28
|
nn0cni |
|- F e. CC |
30 |
26 29
|
mulcli |
|- ( ; 1 0 x. F ) e. CC |
31 |
2 3
|
nn0mulcli |
|- ( B x. C ) e. NN0 |
32 |
11 31
|
eqeltrri |
|- L e. NN0 |
33 |
32
|
nn0cni |
|- L e. CC |
34 |
19
|
nn0cni |
|- ( M + E ) e. CC |
35 |
30 33 34
|
addassi |
|- ( ( ( ; 1 0 x. F ) + L ) + ( M + E ) ) = ( ( ; 1 0 x. F ) + ( L + ( M + E ) ) ) |
36 |
18
|
nn0cni |
|- M e. CC |
37 |
5
|
nn0cni |
|- E e. CC |
38 |
33 36 37
|
addassi |
|- ( ( L + M ) + E ) = ( L + ( M + E ) ) |
39 |
|
dfdec10 |
|- ; G J = ( ( ; 1 0 x. G ) + J ) |
40 |
13 38 39
|
3eqtr3ri |
|- ( ( ; 1 0 x. G ) + J ) = ( L + ( M + E ) ) |
41 |
40
|
oveq2i |
|- ( ( ; 1 0 x. F ) + ( ( ; 1 0 x. G ) + J ) ) = ( ( ; 1 0 x. F ) + ( L + ( M + E ) ) ) |
42 |
|
dfdec10 |
|- ; I J = ( ( ; 1 0 x. I ) + J ) |
43 |
6
|
nn0cni |
|- G e. CC |
44 |
26 29 43
|
adddii |
|- ( ; 1 0 x. ( F + G ) ) = ( ( ; 1 0 x. F ) + ( ; 1 0 x. G ) ) |
45 |
14
|
oveq2i |
|- ( ; 1 0 x. ( F + G ) ) = ( ; 1 0 x. I ) |
46 |
44 45
|
eqtr3i |
|- ( ( ; 1 0 x. F ) + ( ; 1 0 x. G ) ) = ( ; 1 0 x. I ) |
47 |
46
|
oveq1i |
|- ( ( ( ; 1 0 x. F ) + ( ; 1 0 x. G ) ) + J ) = ( ( ; 1 0 x. I ) + J ) |
48 |
26 43
|
mulcli |
|- ( ; 1 0 x. G ) e. CC |
49 |
7
|
nn0cni |
|- J e. CC |
50 |
30 48 49
|
addassi |
|- ( ( ( ; 1 0 x. F ) + ( ; 1 0 x. G ) ) + J ) = ( ( ; 1 0 x. F ) + ( ( ; 1 0 x. G ) + J ) ) |
51 |
42 47 50
|
3eqtr2ri |
|- ( ( ; 1 0 x. F ) + ( ( ; 1 0 x. G ) + J ) ) = ; I J |
52 |
35 41 51
|
3eqtr2i |
|- ( ( ( ; 1 0 x. F ) + L ) + ( M + E ) ) = ; I J |
53 |
22 24 52
|
3eqtri |
|- ( ( ; A B x. C ) + ( M + E ) ) = ; I J |
54 |
10
|
oveq1i |
|- ( ( A x. D ) + E ) = ( M + E ) |
55 |
4 1 2 20 8 5 54 12
|
decmul1c |
|- ( ; A B x. D ) = ; ( M + E ) K |
56 |
15 3 4 16 8 19 53 55
|
decmul2c |
|- ( ; A B x. ; C D ) = ; ; I J K |
57 |
2
|
nn0rei |
|- B e. RR |
58 |
|
dpcl |
|- ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) e. RR ) |
59 |
1 57 58
|
mp2an |
|- ( A . B ) e. RR |
60 |
59
|
recni |
|- ( A . B ) e. CC |
61 |
4
|
nn0rei |
|- D e. RR |
62 |
|
dpcl |
|- ( ( C e. NN0 /\ D e. RR ) -> ( C . D ) e. RR ) |
63 |
3 61 62
|
mp2an |
|- ( C . D ) e. RR |
64 |
63
|
recni |
|- ( C . D ) e. CC |
65 |
60 64 26 26
|
mul4i |
|- ( ( ( A . B ) x. ( C . D ) ) x. ( ; 1 0 x. ; 1 0 ) ) = ( ( ( A . B ) x. ; 1 0 ) x. ( ( C . D ) x. ; 1 0 ) ) |
66 |
25
|
dec0u |
|- ( ; 1 0 x. ; 1 0 ) = ; ; 1 0 0 |
67 |
66
|
oveq2i |
|- ( ( ( A . B ) x. ( C . D ) ) x. ( ; 1 0 x. ; 1 0 ) ) = ( ( ( A . B ) x. ( C . D ) ) x. ; ; 1 0 0 ) |
68 |
1 57
|
dpmul10 |
|- ( ( A . B ) x. ; 1 0 ) = ; A B |
69 |
3 61
|
dpmul10 |
|- ( ( C . D ) x. ; 1 0 ) = ; C D |
70 |
68 69
|
oveq12i |
|- ( ( ( A . B ) x. ; 1 0 ) x. ( ( C . D ) x. ; 1 0 ) ) = ( ; A B x. ; C D ) |
71 |
65 67 70
|
3eqtr3i |
|- ( ( ( A . B ) x. ( C . D ) ) x. ; ; 1 0 0 ) = ( ; A B x. ; C D ) |
72 |
28 6
|
nn0addcli |
|- ( F + G ) e. NN0 |
73 |
14 72
|
eqeltrri |
|- I e. NN0 |
74 |
8
|
nn0rei |
|- K e. RR |
75 |
73 7 74
|
dpmul100 |
|- ( ( I . _ J K ) x. ; ; 1 0 0 ) = ; ; I J K |
76 |
56 71 75
|
3eqtr4i |
|- ( ( ( A . B ) x. ( C . D ) ) x. ; ; 1 0 0 ) = ( ( I . _ J K ) x. ; ; 1 0 0 ) |
77 |
60 64
|
mulcli |
|- ( ( A . B ) x. ( C . D ) ) e. CC |
78 |
7
|
nn0rei |
|- J e. RR |
79 |
|
dp2cl |
|- ( ( J e. RR /\ K e. RR ) -> _ J K e. RR ) |
80 |
78 74 79
|
mp2an |
|- _ J K e. RR |
81 |
|
dpcl |
|- ( ( I e. NN0 /\ _ J K e. RR ) -> ( I . _ J K ) e. RR ) |
82 |
73 80 81
|
mp2an |
|- ( I . _ J K ) e. RR |
83 |
82
|
recni |
|- ( I . _ J K ) e. CC |
84 |
|
10nn |
|- ; 1 0 e. NN |
85 |
84
|
decnncl2 |
|- ; ; 1 0 0 e. NN |
86 |
85
|
nncni |
|- ; ; 1 0 0 e. CC |
87 |
85
|
nnne0i |
|- ; ; 1 0 0 =/= 0 |
88 |
86 87
|
pm3.2i |
|- ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 ) |
89 |
|
mulcan2 |
|- ( ( ( ( A . B ) x. ( C . D ) ) e. CC /\ ( I . _ J K ) e. CC /\ ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 ) ) -> ( ( ( ( A . B ) x. ( C . D ) ) x. ; ; 1 0 0 ) = ( ( I . _ J K ) x. ; ; 1 0 0 ) <-> ( ( A . B ) x. ( C . D ) ) = ( I . _ J K ) ) ) |
90 |
77 83 88 89
|
mp3an |
|- ( ( ( ( A . B ) x. ( C . D ) ) x. ; ; 1 0 0 ) = ( ( I . _ J K ) x. ; ; 1 0 0 ) <-> ( ( A . B ) x. ( C . D ) ) = ( I . _ J K ) ) |
91 |
76 90
|
mpbi |
|- ( ( A . B ) x. ( C . D ) ) = ( I . _ J K ) |