Step |
Hyp |
Ref |
Expression |
1 |
|
dpadd2.a |
|
2 |
|
dpadd2.b |
|
3 |
|
dpadd2.c |
|
4 |
|
dpadd2.d |
|
5 |
|
dpadd2.e |
|
6 |
|
dpadd2.f |
|
7 |
|
dpadd2.g |
|
8 |
|
dpadd2.h |
|
9 |
|
dpadd2.i |
|
10 |
|
dpadd2.1 |
|
11 |
1
|
nn0rei |
|
12 |
|
rpre |
|
13 |
2 12
|
ax-mp |
|
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 |
|
18 |
|
rpre |
|
19 |
4 18
|
ax-mp |
|
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 |
|
25 |
15
|
recni |
Could not format _ A B e. CC : No typesetting found for |- _ A B e. CC with typecode |- |
26 |
|
10nn |
|
27 |
26
|
nncni |
|
28 |
26
|
nnne0i |
|
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 |
|
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 |
|
41 |
6 40
|
ax-mp |
|
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 |
|
49 |
9 48
|
eqeltrri |
|
50 |
5
|
nn0rei |
|
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 |- |