Step |
Hyp |
Ref |
Expression |
1 |
|
dp3mul10.a |
|
2 |
|
dp3mul10.b |
|
3 |
|
dp3mul10.c |
|
4 |
2
|
nn0rei |
|
5 |
|
dp2cl |
Could not format ( ( B e. RR /\ C e. RR ) -> _ B C e. RR ) : No typesetting found for |- ( ( B e. RR /\ C e. RR ) -> _ B C e. RR ) with typecode |- |
6 |
4 3 5
|
mp2an |
Could not format _ B C e. RR : No typesetting found for |- _ B C e. RR with typecode |- |
7 |
1 6
|
dpmul10 |
Could not format ( ( A . _ B C ) x. ; 1 0 ) = ; A _ B C : No typesetting found for |- ( ( A . _ B C ) x. ; 1 0 ) = ; A _ B C with typecode |- |
8 |
|
dfdec10 |
Could not format ; A _ B C = ( ( ; 1 0 x. A ) + _ B C ) : No typesetting found for |- ; A _ B C = ( ( ; 1 0 x. A ) + _ B C ) with typecode |- |
9 |
|
10nn |
|
10 |
9
|
nncni |
|
11 |
1
|
nn0cni |
|
12 |
10 11
|
mulcli |
|
13 |
4
|
recni |
|
14 |
3
|
recni |
|
15 |
9
|
nnne0i |
|
16 |
14 10 15
|
divcli |
|
17 |
12 13 16
|
addassi |
|
18 |
|
dfdec10 |
Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |- |
19 |
18
|
oveq1i |
Could not format ( ; A B + ( C / ; 1 0 ) ) = ( ( ( ; 1 0 x. A ) + B ) + ( C / ; 1 0 ) ) : No typesetting found for |- ( ; A B + ( C / ; 1 0 ) ) = ( ( ( ; 1 0 x. A ) + B ) + ( C / ; 1 0 ) ) with typecode |- |
20 |
|
df-dp2 |
Could not format _ B C = ( B + ( C / ; 1 0 ) ) : No typesetting found for |- _ B C = ( B + ( C / ; 1 0 ) ) with typecode |- |
21 |
20
|
oveq2i |
Could not format ( ( ; 1 0 x. A ) + _ B C ) = ( ( ; 1 0 x. A ) + ( B + ( C / ; 1 0 ) ) ) : No typesetting found for |- ( ( ; 1 0 x. A ) + _ B C ) = ( ( ; 1 0 x. A ) + ( B + ( C / ; 1 0 ) ) ) with typecode |- |
22 |
17 19 21
|
3eqtr4ri |
Could not format ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B + ( C / ; 1 0 ) ) : No typesetting found for |- ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B + ( C / ; 1 0 ) ) with typecode |- |
23 |
1 2
|
deccl |
Could not format ; A B e. NN0 : No typesetting found for |- ; A B e. NN0 with typecode |- |
24 |
23 3
|
dpval2 |
Could not format ( ; A B . C ) = ( ; A B + ( C / ; 1 0 ) ) : No typesetting found for |- ( ; A B . C ) = ( ; A B + ( C / ; 1 0 ) ) with typecode |- |
25 |
22 24
|
eqtr4i |
Could not format ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B . C ) : No typesetting found for |- ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B . C ) with typecode |- |
26 |
7 8 25
|
3eqtri |
Could not format ( ( A . _ B C ) x. ; 1 0 ) = ( ; A B . C ) : No typesetting found for |- ( ( A . _ B C ) x. ; 1 0 ) = ( ; A B . C ) with typecode |- |