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