Metamath Proof Explorer


Theorem dpmul4

Description: An upper bound to multiplication of decimal numbers with 4 digits. (Contributed by Thierry Arnoux, 25-Dec-2021)

Ref Expression
Hypotheses dpmul.a A 0
dpmul.b B 0
dpmul.c C 0
dpmul.d D 0
dpmul.e E 0
dpmul.g G 0
dpmul.j J 0
dpmul.k K 0
dpmul4.f F 0
dpmul4.h H 0
dpmul4.i I 0
dpmul4.l L 0
dpmul4.m M 0
dpmul4.n N 0
dpmul4.o O 0
dpmul4.p P 0
dpmul4.q Q 0
dpmul4.r R 0
dpmul4.s S 0
dpmul4.t T 0
dpmul4.u U 0
dpmul4.w W 0
dpmul4.x X 0
dpmul4.y Y 0
dpmul4.z Z 0
dpmul4.a U < 10
dpmul4.b P < 10
dpmul4.c Q < 10
dpmul4.1 No typesetting found for |- ( ; ; L M N + O ) = ; ; ; R S T U with typecode |-
dpmul4.2 No typesetting found for |- ( ( A . B ) x. ( E . F ) ) = ( I . _ J K ) with typecode |-
dpmul4.3 No typesetting found for |- ( ( C . D ) x. ( G . H ) ) = ( O . _ P Q ) with typecode |-
dpmul4.4 No typesetting found for |- ( ; ; ; I J K 1 + ; ; R S T ) = ; ; ; W X Y Z with typecode |-
dpmul4.5 No typesetting found for |- ( ( ( A . B ) + ( C . D ) ) x. ( ( E . F ) + ( G . H ) ) ) = ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) with typecode |-
Assertion dpmul4 Could not format assertion : No typesetting found for |- ( ( A . _ B _ C D ) x. ( E . _ F _ G H ) ) < ( W . _ X _ Y Z ) with typecode |-

Proof

Step Hyp Ref Expression
1 dpmul.a A 0
2 dpmul.b B 0
3 dpmul.c C 0
4 dpmul.d D 0
5 dpmul.e E 0
6 dpmul.g G 0
7 dpmul.j J 0
8 dpmul.k K 0
9 dpmul4.f F 0
10 dpmul4.h H 0
11 dpmul4.i I 0
12 dpmul4.l L 0
13 dpmul4.m M 0
14 dpmul4.n N 0
15 dpmul4.o O 0
16 dpmul4.p P 0
17 dpmul4.q Q 0
18 dpmul4.r R 0
19 dpmul4.s S 0
20 dpmul4.t T 0
21 dpmul4.u U 0
22 dpmul4.w W 0
23 dpmul4.x X 0
24 dpmul4.y Y 0
25 dpmul4.z Z 0
26 dpmul4.a U < 10
27 dpmul4.b P < 10
28 dpmul4.c Q < 10
29 dpmul4.1 Could not format ( ; ; L M N + O ) = ; ; ; R S T U : No typesetting found for |- ( ; ; L M N + O ) = ; ; ; R S T U with typecode |-
30 dpmul4.2 Could not format ( ( A . B ) x. ( E . F ) ) = ( I . _ J K ) : No typesetting found for |- ( ( A . B ) x. ( E . F ) ) = ( I . _ J K ) with typecode |-
31 dpmul4.3 Could not format ( ( C . D ) x. ( G . H ) ) = ( O . _ P Q ) : No typesetting found for |- ( ( C . D ) x. ( G . H ) ) = ( O . _ P Q ) with typecode |-
32 dpmul4.4 Could not format ( ; ; ; I J K 1 + ; ; R S T ) = ; ; ; W X Y Z : No typesetting found for |- ( ; ; ; I J K 1 + ; ; R S T ) = ; ; ; W X Y Z with typecode |-
33 dpmul4.5 Could not format ( ( ( A . B ) + ( C . D ) ) x. ( ( E . F ) + ( G . H ) ) ) = ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) : No typesetting found for |- ( ( ( A . B ) + ( C . D ) ) x. ( ( E . F ) + ( G . H ) ) ) = ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) with typecode |-
34 1 2 deccl Could not format ; A B e. NN0 : No typesetting found for |- ; A B e. NN0 with typecode |-
35 3 4 deccl Could not format ; C D e. NN0 : No typesetting found for |- ; C D e. NN0 with typecode |-
36 5 9 deccl Could not format ; E F e. NN0 : No typesetting found for |- ; E F e. NN0 with typecode |-
37 6 10 deccl Could not format ; G H e. NN0 : No typesetting found for |- ; G H e. NN0 with typecode |-
38 12 13 deccl Could not format ; L M e. NN0 : No typesetting found for |- ; L M e. NN0 with typecode |-
39 38 14 deccl Could not format ; ; L M N e. NN0 : No typesetting found for |- ; ; L M N e. NN0 with typecode |-
40 2nn0 2 0
41 2 nn0rei B
42 dpcl A 0 B A . B
43 1 41 42 mp2an A . B
44 43 recni A . B
45 10nn 10
46 45 nncni 10
47 9 nn0rei F
48 dpcl E 0 F E . F
49 5 47 48 mp2an E . F
50 49 recni E . F
51 44 46 50 46 mul4i A . B 10 E . F 10 = A . B E . F 10 10
52 44 50 mulcli A . B E . F
53 52 46 46 mulassi A . B E . F 10 10 = A . B E . F 10 10
54 30 oveq1i Could not format ( ( ( A . B ) x. ( E . F ) ) x. ; 1 0 ) = ( ( I . _ J K ) x. ; 1 0 ) : No typesetting found for |- ( ( ( A . B ) x. ( E . F ) ) x. ; 1 0 ) = ( ( I . _ J K ) x. ; 1 0 ) with typecode |-
55 8 nn0rei K
56 11 7 55 dp3mul10 Could not format ( ( I . _ J K ) x. ; 1 0 ) = ( ; I J . K ) : No typesetting found for |- ( ( I . _ J K ) x. ; 1 0 ) = ( ; I J . K ) with typecode |-
57 54 56 eqtri A . B E . F 10 = IJ . K
58 57 oveq1i A . B E . F 10 10 = IJ . K 10
59 51 53 58 3eqtr2ri IJ . K 10 = A . B 10 E . F 10
60 11 7 deccl IJ 0
61 60 55 dpmul10 Could not format ( ( ; I J . K ) x. ; 1 0 ) = ; ; I J K : No typesetting found for |- ( ( ; I J . K ) x. ; 1 0 ) = ; ; I J K with typecode |-
62 1 41 dpmul10 Could not format ( ( A . B ) x. ; 1 0 ) = ; A B : No typesetting found for |- ( ( A . B ) x. ; 1 0 ) = ; A B with typecode |-
63 5 47 dpmul10 Could not format ( ( E . F ) x. ; 1 0 ) = ; E F : No typesetting found for |- ( ( E . F ) x. ; 1 0 ) = ; E F with typecode |-
64 62 63 oveq12i Could not format ( ( ( A . B ) x. ; 1 0 ) x. ( ( E . F ) x. ; 1 0 ) ) = ( ; A B x. ; E F ) : No typesetting found for |- ( ( ( A . B ) x. ; 1 0 ) x. ( ( E . F ) x. ; 1 0 ) ) = ( ; A B x. ; E F ) with typecode |-
65 59 61 64 3eqtr3ri Could not format ( ; A B x. ; E F ) = ; ; I J K : No typesetting found for |- ( ; A B x. ; E F ) = ; ; I J K with typecode |-
66 4 nn0rei D
67 dpcl C 0 D C . D
68 3 66 67 mp2an C . D
69 68 recni C . D
70 10 nn0rei H
71 dpcl G 0 H G . H
72 6 70 71 mp2an G . H
73 72 recni G . H
74 69 46 73 46 mul4i C . D 10 G . H 10 = C . D G . H 10 10
75 69 73 mulcli C . D G . H
76 75 46 46 mulassi C . D G . H 10 10 = C . D G . H 10 10
77 31 oveq1i Could not format ( ( ( C . D ) x. ( G . H ) ) x. ; 1 0 ) = ( ( O . _ P Q ) x. ; 1 0 ) : No typesetting found for |- ( ( ( C . D ) x. ( G . H ) ) x. ; 1 0 ) = ( ( O . _ P Q ) x. ; 1 0 ) with typecode |-
78 17 nn0rei Q
79 15 16 78 dp3mul10 Could not format ( ( O . _ P Q ) x. ; 1 0 ) = ( ; O P . Q ) : No typesetting found for |- ( ( O . _ P Q ) x. ; 1 0 ) = ( ; O P . Q ) with typecode |-
80 77 79 eqtri Could not format ( ( ( C . D ) x. ( G . H ) ) x. ; 1 0 ) = ( ; O P . Q ) : No typesetting found for |- ( ( ( C . D ) x. ( G . H ) ) x. ; 1 0 ) = ( ; O P . Q ) with typecode |-
81 80 oveq1i Could not format ( ( ( ( C . D ) x. ( G . H ) ) x. ; 1 0 ) x. ; 1 0 ) = ( ( ; O P . Q ) x. ; 1 0 ) : No typesetting found for |- ( ( ( ( C . D ) x. ( G . H ) ) x. ; 1 0 ) x. ; 1 0 ) = ( ( ; O P . Q ) x. ; 1 0 ) with typecode |-
82 74 76 81 3eqtr2ri Could not format ( ( ; O P . Q ) x. ; 1 0 ) = ( ( ( C . D ) x. ; 1 0 ) x. ( ( G . H ) x. ; 1 0 ) ) : No typesetting found for |- ( ( ; O P . Q ) x. ; 1 0 ) = ( ( ( C . D ) x. ; 1 0 ) x. ( ( G . H ) x. ; 1 0 ) ) with typecode |-
83 15 16 deccl Could not format ; O P e. NN0 : No typesetting found for |- ; O P e. NN0 with typecode |-
84 83 78 dpmul10 Could not format ( ( ; O P . Q ) x. ; 1 0 ) = ; ; O P Q : No typesetting found for |- ( ( ; O P . Q ) x. ; 1 0 ) = ; ; O P Q with typecode |-
85 3 66 dpmul10 Could not format ( ( C . D ) x. ; 1 0 ) = ; C D : No typesetting found for |- ( ( C . D ) x. ; 1 0 ) = ; C D with typecode |-
86 6 70 dpmul10 Could not format ( ( G . H ) x. ; 1 0 ) = ; G H : No typesetting found for |- ( ( G . H ) x. ; 1 0 ) = ; G H with typecode |-
87 85 86 oveq12i Could not format ( ( ( C . D ) x. ; 1 0 ) x. ( ( G . H ) x. ; 1 0 ) ) = ( ; C D x. ; G H ) : No typesetting found for |- ( ( ( C . D ) x. ; 1 0 ) x. ( ( G . H ) x. ; 1 0 ) ) = ( ; C D x. ; G H ) with typecode |-
88 82 84 87 3eqtr3ri Could not format ( ; C D x. ; G H ) = ; ; O P Q : No typesetting found for |- ( ; C D x. ; G H ) = ; ; O P Q with typecode |-
89 44 69 46 adddiri A . B + C . D 10 = A . B 10 + C . D 10
90 62 85 oveq12i Could not format ( ( ( A . B ) x. ; 1 0 ) + ( ( C . D ) x. ; 1 0 ) ) = ( ; A B + ; C D ) : No typesetting found for |- ( ( ( A . B ) x. ; 1 0 ) + ( ( C . D ) x. ; 1 0 ) ) = ( ; A B + ; C D ) with typecode |-
91 89 90 eqtr2i Could not format ( ; A B + ; C D ) = ( ( ( A . B ) + ( C . D ) ) x. ; 1 0 ) : No typesetting found for |- ( ; A B + ; C D ) = ( ( ( A . B ) + ( C . D ) ) x. ; 1 0 ) with typecode |-
92 50 73 46 adddiri E . F + G . H 10 = E . F 10 + G . H 10
93 63 86 oveq12i Could not format ( ( ( E . F ) x. ; 1 0 ) + ( ( G . H ) x. ; 1 0 ) ) = ( ; E F + ; G H ) : No typesetting found for |- ( ( ( E . F ) x. ; 1 0 ) + ( ( G . H ) x. ; 1 0 ) ) = ( ; E F + ; G H ) with typecode |-
94 92 93 eqtr2i Could not format ( ; E F + ; G H ) = ( ( ( E . F ) + ( G . H ) ) x. ; 1 0 ) : No typesetting found for |- ( ; E F + ; G H ) = ( ( ( E . F ) + ( G . H ) ) x. ; 1 0 ) with typecode |-
95 91 94 oveq12i Could not format ( ( ; A B + ; C D ) x. ( ; E F + ; G H ) ) = ( ( ( ( A . B ) + ( C . D ) ) x. ; 1 0 ) x. ( ( ( E . F ) + ( G . H ) ) x. ; 1 0 ) ) : No typesetting found for |- ( ( ; A B + ; C D ) x. ( ; E F + ; G H ) ) = ( ( ( ( A . B ) + ( C . D ) ) x. ; 1 0 ) x. ( ( ( E . F ) + ( G . H ) ) x. ; 1 0 ) ) with typecode |-
96 44 69 addcli A . B + C . D
97 50 73 addcli E . F + G . H
98 96 46 97 46 mul4i A . B + C . D 10 E . F + G . H 10 = A . B + C . D E . F + G . H 10 10
99 33 oveq1i Could not format ( ( ( ( A . B ) + ( C . D ) ) x. ( ( E . F ) + ( G . H ) ) ) x. ( ; 1 0 x. ; 1 0 ) ) = ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ( ; 1 0 x. ; 1 0 ) ) : No typesetting found for |- ( ( ( ( A . B ) + ( C . D ) ) x. ( ( E . F ) + ( G . H ) ) ) x. ( ; 1 0 x. ; 1 0 ) ) = ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ( ; 1 0 x. ; 1 0 ) ) with typecode |-
100 95 98 99 3eqtri Could not format ( ( ; A B + ; C D ) x. ( ; E F + ; G H ) ) = ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ( ; 1 0 x. ; 1 0 ) ) : No typesetting found for |- ( ( ; A B + ; C D ) x. ( ; E F + ; G H ) ) = ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ( ; 1 0 x. ; 1 0 ) ) with typecode |-
101 10nn0 10 0
102 101 dec0u 10 10 = 100
103 102 oveq2i Could not format ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ( ; 1 0 x. ; 1 0 ) ) = ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ; ; 1 0 0 ) : No typesetting found for |- ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ( ; 1 0 x. ; 1 0 ) ) = ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ; ; 1 0 0 ) with typecode |-
104 30 52 eqeltrri Could not format ( I . _ J K ) e. CC : No typesetting found for |- ( I . _ J K ) e. CC with typecode |-
105 13 nn0rei M
106 14 nn0rei N
107 dp2cl M N MN
108 105 106 107 mp2an MN
109 dpcl L 0 MN L . MN
110 12 108 109 mp2an L . MN
111 110 recni L . MN
112 104 111 addcli Could not format ( ( I . _ J K ) + ( L . _ M N ) ) e. CC : No typesetting found for |- ( ( I . _ J K ) + ( L . _ M N ) ) e. CC with typecode |-
113 31 75 eqeltrri Could not format ( O . _ P Q ) e. CC : No typesetting found for |- ( O . _ P Q ) e. CC with typecode |-
114 0nn0 0 0
115 101 114 deccl 100 0
116 115 nn0cni 100
117 112 113 116 adddiri Could not format ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ; ; 1 0 0 ) = ( ( ( ( I . _ J K ) + ( L . _ M N ) ) x. ; ; 1 0 0 ) + ( ( O . _ P Q ) x. ; ; 1 0 0 ) ) : No typesetting found for |- ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ; ; 1 0 0 ) = ( ( ( ( I . _ J K ) + ( L . _ M N ) ) x. ; ; 1 0 0 ) + ( ( O . _ P Q ) x. ; ; 1 0 0 ) ) with typecode |-
118 104 111 116 adddiri Could not format ( ( ( I . _ J K ) + ( L . _ M N ) ) x. ; ; 1 0 0 ) = ( ( ( I . _ J K ) x. ; ; 1 0 0 ) + ( ( L . _ M N ) x. ; ; 1 0 0 ) ) : No typesetting found for |- ( ( ( I . _ J K ) + ( L . _ M N ) ) x. ; ; 1 0 0 ) = ( ( ( I . _ J K ) x. ; ; 1 0 0 ) + ( ( L . _ M N ) x. ; ; 1 0 0 ) ) with typecode |-
119 118 oveq1i Could not format ( ( ( ( I . _ J K ) + ( L . _ M N ) ) x. ; ; 1 0 0 ) + ( ( O . _ P Q ) x. ; ; 1 0 0 ) ) = ( ( ( ( I . _ J K ) x. ; ; 1 0 0 ) + ( ( L . _ M N ) x. ; ; 1 0 0 ) ) + ( ( O . _ P Q ) x. ; ; 1 0 0 ) ) : No typesetting found for |- ( ( ( ( I . _ J K ) + ( L . _ M N ) ) x. ; ; 1 0 0 ) + ( ( O . _ P Q ) x. ; ; 1 0 0 ) ) = ( ( ( ( I . _ J K ) x. ; ; 1 0 0 ) + ( ( L . _ M N ) x. ; ; 1 0 0 ) ) + ( ( O . _ P Q ) x. ; ; 1 0 0 ) ) with typecode |-
120 11 7 55 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 |-
121 12 13 106 dpmul100 Could not format ( ( L . _ M N ) x. ; ; 1 0 0 ) = ; ; L M N : No typesetting found for |- ( ( L . _ M N ) x. ; ; 1 0 0 ) = ; ; L M N with typecode |-
122 120 121 oveq12i Could not format ( ( ( I . _ J K ) x. ; ; 1 0 0 ) + ( ( L . _ M N ) x. ; ; 1 0 0 ) ) = ( ; ; I J K + ; ; L M N ) : No typesetting found for |- ( ( ( I . _ J K ) x. ; ; 1 0 0 ) + ( ( L . _ M N ) x. ; ; 1 0 0 ) ) = ( ; ; I J K + ; ; L M N ) with typecode |-
123 15 16 78 dpmul100 Could not format ( ( O . _ P Q ) x. ; ; 1 0 0 ) = ; ; O P Q : No typesetting found for |- ( ( O . _ P Q ) x. ; ; 1 0 0 ) = ; ; O P Q with typecode |-
124 122 123 oveq12i Could not format ( ( ( ( I . _ J K ) x. ; ; 1 0 0 ) + ( ( L . _ M N ) x. ; ; 1 0 0 ) ) + ( ( O . _ P Q ) x. ; ; 1 0 0 ) ) = ( ( ; ; I J K + ; ; L M N ) + ; ; O P Q ) : No typesetting found for |- ( ( ( ( I . _ J K ) x. ; ; 1 0 0 ) + ( ( L . _ M N ) x. ; ; 1 0 0 ) ) + ( ( O . _ P Q ) x. ; ; 1 0 0 ) ) = ( ( ; ; I J K + ; ; L M N ) + ; ; O P Q ) with typecode |-
125 117 119 124 3eqtri Could not format ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ; ; 1 0 0 ) = ( ( ; ; I J K + ; ; L M N ) + ; ; O P Q ) : No typesetting found for |- ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ; ; 1 0 0 ) = ( ( ; ; I J K + ; ; L M N ) + ; ; O P Q ) with typecode |-
126 100 103 125 3eqtri Could not format ( ( ; A B + ; C D ) x. ( ; E F + ; G H ) ) = ( ( ; ; I J K + ; ; L M N ) + ; ; O P Q ) : No typesetting found for |- ( ( ; A B + ; C D ) x. ( ; E F + ; G H ) ) = ( ( ; ; I J K + ; ; L M N ) + ; ; O P Q ) with typecode |-
127 sq10 10 2 = 100
128 127 oveq2i Could not format ( ; A B x. ( ; 1 0 ^ 2 ) ) = ( ; A B x. ; ; 1 0 0 ) : No typesetting found for |- ( ; A B x. ( ; 1 0 ^ 2 ) ) = ( ; A B x. ; ; 1 0 0 ) with typecode |-
129 34 nn0cni Could not format ; A B e. CC : No typesetting found for |- ; A B e. CC with typecode |-
130 116 129 mulcomi Could not format ( ; ; 1 0 0 x. ; A B ) = ( ; A B x. ; ; 1 0 0 ) : No typesetting found for |- ( ; ; 1 0 0 x. ; A B ) = ( ; A B x. ; ; 1 0 0 ) with typecode |-
131 128 130 eqtr4i Could not format ( ; A B x. ( ; 1 0 ^ 2 ) ) = ( ; ; 1 0 0 x. ; A B ) : No typesetting found for |- ( ; A B x. ( ; 1 0 ^ 2 ) ) = ( ; ; 1 0 0 x. ; A B ) with typecode |-
132 131 oveq1i Could not format ( ( ; A B x. ( ; 1 0 ^ 2 ) ) + ; C D ) = ( ( ; ; 1 0 0 x. ; A B ) + ; C D ) : No typesetting found for |- ( ( ; A B x. ( ; 1 0 ^ 2 ) ) + ; C D ) = ( ( ; ; 1 0 0 x. ; A B ) + ; C D ) with typecode |-
133 34 3 66 dfdec100 Could not format ; ; ; A B C D = ( ( ; ; 1 0 0 x. ; A B ) + ; C D ) : No typesetting found for |- ; ; ; A B C D = ( ( ; ; 1 0 0 x. ; A B ) + ; C D ) with typecode |-
134 132 133 eqtr4i Could not format ( ( ; A B x. ( ; 1 0 ^ 2 ) ) + ; C D ) = ; ; ; A B C D : No typesetting found for |- ( ( ; A B x. ( ; 1 0 ^ 2 ) ) + ; C D ) = ; ; ; A B C D with typecode |-
135 127 oveq2i Could not format ( ; E F x. ( ; 1 0 ^ 2 ) ) = ( ; E F x. ; ; 1 0 0 ) : No typesetting found for |- ( ; E F x. ( ; 1 0 ^ 2 ) ) = ( ; E F x. ; ; 1 0 0 ) with typecode |-
136 36 nn0cni Could not format ; E F e. CC : No typesetting found for |- ; E F e. CC with typecode |-
137 116 136 mulcomi Could not format ( ; ; 1 0 0 x. ; E F ) = ( ; E F x. ; ; 1 0 0 ) : No typesetting found for |- ( ; ; 1 0 0 x. ; E F ) = ( ; E F x. ; ; 1 0 0 ) with typecode |-
138 135 137 eqtr4i Could not format ( ; E F x. ( ; 1 0 ^ 2 ) ) = ( ; ; 1 0 0 x. ; E F ) : No typesetting found for |- ( ; E F x. ( ; 1 0 ^ 2 ) ) = ( ; ; 1 0 0 x. ; E F ) with typecode |-
139 138 oveq1i Could not format ( ( ; E F x. ( ; 1 0 ^ 2 ) ) + ; G H ) = ( ( ; ; 1 0 0 x. ; E F ) + ; G H ) : No typesetting found for |- ( ( ; E F x. ( ; 1 0 ^ 2 ) ) + ; G H ) = ( ( ; ; 1 0 0 x. ; E F ) + ; G H ) with typecode |-
140 36 6 70 dfdec100 Could not format ; ; ; E F G H = ( ( ; ; 1 0 0 x. ; E F ) + ; G H ) : No typesetting found for |- ; ; ; E F G H = ( ( ; ; 1 0 0 x. ; E F ) + ; G H ) with typecode |-
141 139 140 eqtr4i Could not format ( ( ; E F x. ( ; 1 0 ^ 2 ) ) + ; G H ) = ; ; ; E F G H : No typesetting found for |- ( ( ; E F x. ( ; 1 0 ^ 2 ) ) + ; G H ) = ; ; ; E F G H with typecode |-
142 46 sqvali 10 2 = 10 10
143 142 oveq2i Could not format ( ; ; I J K x. ( ; 1 0 ^ 2 ) ) = ( ; ; I J K x. ( ; 1 0 x. ; 1 0 ) ) : No typesetting found for |- ( ; ; I J K x. ( ; 1 0 ^ 2 ) ) = ( ; ; I J K x. ( ; 1 0 x. ; 1 0 ) ) with typecode |-
144 60 8 deccl Could not format ; ; I J K e. NN0 : No typesetting found for |- ; ; I J K e. NN0 with typecode |-
145 144 nn0cni Could not format ; ; I J K e. CC : No typesetting found for |- ; ; I J K e. CC with typecode |-
146 145 46 46 mulassi Could not format ( ( ; ; I J K x. ; 1 0 ) x. ; 1 0 ) = ( ; ; I J K x. ( ; 1 0 x. ; 1 0 ) ) : No typesetting found for |- ( ( ; ; I J K x. ; 1 0 ) x. ; 1 0 ) = ( ; ; I J K x. ( ; 1 0 x. ; 1 0 ) ) with typecode |-
147 143 146 eqtr4i Could not format ( ; ; I J K x. ( ; 1 0 ^ 2 ) ) = ( ( ; ; I J K x. ; 1 0 ) x. ; 1 0 ) : No typesetting found for |- ( ; ; I J K x. ( ; 1 0 ^ 2 ) ) = ( ( ; ; I J K x. ; 1 0 ) x. ; 1 0 ) with typecode |-
148 18 19 deccl Could not format ; R S e. NN0 : No typesetting found for |- ; R S e. NN0 with typecode |-
149 148 20 deccl Could not format ; ; R S T e. NN0 : No typesetting found for |- ; ; R S T e. NN0 with typecode |-
150 149 nn0cni Could not format ; ; R S T e. CC : No typesetting found for |- ; ; R S T e. CC with typecode |-
151 ax-1cn 1
152 150 151 addcli Could not format ( ; ; R S T + 1 ) e. CC : No typesetting found for |- ( ; ; R S T + 1 ) e. CC with typecode |-
153 145 46 mulcli Could not format ( ; ; I J K x. ; 1 0 ) e. CC : No typesetting found for |- ( ; ; I J K x. ; 1 0 ) e. CC with typecode |-
154 151 153 addcomi Could not format ( 1 + ( ; ; I J K x. ; 1 0 ) ) = ( ( ; ; I J K x. ; 1 0 ) + 1 ) : No typesetting found for |- ( 1 + ( ; ; I J K x. ; 1 0 ) ) = ( ( ; ; I J K x. ; 1 0 ) + 1 ) with typecode |-
155 46 145 mulcomi Could not format ( ; 1 0 x. ; ; I J K ) = ( ; ; I J K x. ; 1 0 ) : No typesetting found for |- ( ; 1 0 x. ; ; I J K ) = ( ; ; I J K x. ; 1 0 ) with typecode |-
156 144 dec0u Could not format ( ; 1 0 x. ; ; I J K ) = ; ; ; I J K 0 : No typesetting found for |- ( ; 1 0 x. ; ; I J K ) = ; ; ; I J K 0 with typecode |-
157 155 156 eqtr3i Could not format ( ; ; I J K x. ; 1 0 ) = ; ; ; I J K 0 : No typesetting found for |- ( ; ; I J K x. ; 1 0 ) = ; ; ; I J K 0 with typecode |-
158 157 oveq1i Could not format ( ( ; ; I J K x. ; 1 0 ) + 1 ) = ( ; ; ; I J K 0 + 1 ) : No typesetting found for |- ( ( ; ; I J K x. ; 1 0 ) + 1 ) = ( ; ; ; I J K 0 + 1 ) with typecode |-
159 151 addid2i 0 + 1 = 1
160 eqid Could not format ; ; ; I J K 0 = ; ; ; I J K 0 : No typesetting found for |- ; ; ; I J K 0 = ; ; ; I J K 0 with typecode |-
161 144 114 159 160 decsuc Could not format ( ; ; ; I J K 0 + 1 ) = ; ; ; I J K 1 : No typesetting found for |- ( ; ; ; I J K 0 + 1 ) = ; ; ; I J K 1 with typecode |-
162 154 158 161 3eqtri Could not format ( 1 + ( ; ; I J K x. ; 1 0 ) ) = ; ; ; I J K 1 : No typesetting found for |- ( 1 + ( ; ; I J K x. ; 1 0 ) ) = ; ; ; I J K 1 with typecode |-
163 162 oveq2i Could not format ( ; ; R S T + ( 1 + ( ; ; I J K x. ; 1 0 ) ) ) = ( ; ; R S T + ; ; ; I J K 1 ) : No typesetting found for |- ( ; ; R S T + ( 1 + ( ; ; I J K x. ; 1 0 ) ) ) = ( ; ; R S T + ; ; ; I J K 1 ) with typecode |-
164 150 151 153 addassi Could not format ( ( ; ; R S T + 1 ) + ( ; ; I J K x. ; 1 0 ) ) = ( ; ; R S T + ( 1 + ( ; ; I J K x. ; 1 0 ) ) ) : No typesetting found for |- ( ( ; ; R S T + 1 ) + ( ; ; I J K x. ; 1 0 ) ) = ( ; ; R S T + ( 1 + ( ; ; I J K x. ; 1 0 ) ) ) with typecode |-
165 1nn0 1 0
166 144 165 deccl Could not format ; ; ; I J K 1 e. NN0 : No typesetting found for |- ; ; ; I J K 1 e. NN0 with typecode |-
167 166 nn0cni Could not format ; ; ; I J K 1 e. CC : No typesetting found for |- ; ; ; I J K 1 e. CC with typecode |-
168 167 150 addcomi Could not format ( ; ; ; I J K 1 + ; ; R S T ) = ( ; ; R S T + ; ; ; I J K 1 ) : No typesetting found for |- ( ; ; ; I J K 1 + ; ; R S T ) = ( ; ; R S T + ; ; ; I J K 1 ) with typecode |-
169 163 164 168 3eqtr4i Could not format ( ( ; ; R S T + 1 ) + ( ; ; I J K x. ; 1 0 ) ) = ( ; ; ; I J K 1 + ; ; R S T ) : No typesetting found for |- ( ( ; ; R S T + 1 ) + ( ; ; I J K x. ; 1 0 ) ) = ( ; ; ; I J K 1 + ; ; R S T ) with typecode |-
170 169 32 eqtri Could not format ( ( ; ; R S T + 1 ) + ( ; ; I J K x. ; 1 0 ) ) = ; ; ; W X Y Z : No typesetting found for |- ( ( ; ; R S T + 1 ) + ( ; ; I J K x. ; 1 0 ) ) = ; ; ; W X Y Z with typecode |-
171 152 153 170 mvlladdi Could not format ( ; ; I J K x. ; 1 0 ) = ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) : No typesetting found for |- ( ; ; I J K x. ; 1 0 ) = ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) with typecode |-
172 171 oveq1i Could not format ( ( ; ; I J K x. ; 1 0 ) x. ; 1 0 ) = ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) : No typesetting found for |- ( ( ; ; I J K x. ; 1 0 ) x. ; 1 0 ) = ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) with typecode |-
173 147 172 eqtri Could not format ( ; ; I J K x. ( ; 1 0 ^ 2 ) ) = ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) : No typesetting found for |- ( ; ; I J K x. ( ; 1 0 ^ 2 ) ) = ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) with typecode |-
174 173 oveq1i Could not format ( ( ; ; I J K x. ( ; 1 0 ^ 2 ) ) + ; ; L M N ) = ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) : No typesetting found for |- ( ( ; ; I J K x. ( ; 1 0 ^ 2 ) ) + ; ; L M N ) = ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) with typecode |-
175 eqid Could not format ( ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) + ; ; O P Q ) = ( ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) + ; ; O P Q ) : No typesetting found for |- ( ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) + ; ; O P Q ) = ( ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) + ; ; O P Q ) with typecode |-
176 34 35 36 37 39 40 65 88 126 134 141 174 175 karatsuba Could not format ( ; ; ; A B C D x. ; ; ; E F G H ) = ( ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) + ; ; O P Q ) : No typesetting found for |- ( ; ; ; A B C D x. ; ; ; E F G H ) = ( ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) + ; ; O P Q ) with typecode |-
177 22 23 deccl Could not format ; W X e. NN0 : No typesetting found for |- ; W X e. NN0 with typecode |-
178 177 24 deccl Could not format ; ; W X Y e. NN0 : No typesetting found for |- ; ; W X Y e. NN0 with typecode |-
179 178 25 deccl Could not format ; ; ; W X Y Z e. NN0 : No typesetting found for |- ; ; ; W X Y Z e. NN0 with typecode |-
180 179 nn0cni Could not format ; ; ; W X Y Z e. CC : No typesetting found for |- ; ; ; W X Y Z e. CC with typecode |-
181 115 114 deccl 1000 0
182 181 nn0cni 1000
183 180 182 mulcli Could not format ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) e. CC : No typesetting found for |- ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) e. CC with typecode |-
184 152 182 mulcli Could not format ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) e. CC : No typesetting found for |- ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) e. CC with typecode |-
185 183 184 subcli Could not format ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) e. CC : No typesetting found for |- ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) e. CC with typecode |-
186 39 nn0cni Could not format ; ; L M N e. CC : No typesetting found for |- ; ; L M N e. CC with typecode |-
187 116 186 mulcli Could not format ( ; ; 1 0 0 x. ; ; L M N ) e. CC : No typesetting found for |- ( ; ; 1 0 0 x. ; ; L M N ) e. CC with typecode |-
188 15 16 78 dfdec100 Could not format ; ; O P Q = ( ( ; ; 1 0 0 x. O ) + ; P Q ) : No typesetting found for |- ; ; O P Q = ( ( ; ; 1 0 0 x. O ) + ; P Q ) with typecode |-
189 83 17 deccl Could not format ; ; O P Q e. NN0 : No typesetting found for |- ; ; O P Q e. NN0 with typecode |-
190 189 nn0cni Could not format ; ; O P Q e. CC : No typesetting found for |- ; ; O P Q e. CC with typecode |-
191 188 190 eqeltrri Could not format ( ( ; ; 1 0 0 x. O ) + ; P Q ) e. CC : No typesetting found for |- ( ( ; ; 1 0 0 x. O ) + ; P Q ) e. CC with typecode |-
192 185 187 191 addassi Could not format ( ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 x. ; ; L M N ) ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) = ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) : No typesetting found for |- ( ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 x. ; ; L M N ) ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) = ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) with typecode |-
193 46 sqcli 10 2
194 145 193 mulcli Could not format ( ; ; I J K x. ( ; 1 0 ^ 2 ) ) e. CC : No typesetting found for |- ( ; ; I J K x. ( ; 1 0 ^ 2 ) ) e. CC with typecode |-
195 173 194 eqeltrri Could not format ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) e. CC : No typesetting found for |- ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) e. CC with typecode |-
196 195 186 116 adddiri Could not format ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ; ; 1 0 0 ) = ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) x. ; ; 1 0 0 ) + ( ; ; L M N x. ; ; 1 0 0 ) ) : No typesetting found for |- ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ; ; 1 0 0 ) = ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) x. ; ; 1 0 0 ) + ( ; ; L M N x. ; ; 1 0 0 ) ) with typecode |-
197 127 oveq2i Could not format ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) = ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ; ; 1 0 0 ) : No typesetting found for |- ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) = ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ; ; 1 0 0 ) with typecode |-
198 180 152 subcli Could not format ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) e. CC : No typesetting found for |- ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) e. CC with typecode |-
199 198 46 116 mulassi Could not format ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) x. ; ; 1 0 0 ) = ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ( ; 1 0 x. ; ; 1 0 0 ) ) : No typesetting found for |- ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) x. ; ; 1 0 0 ) = ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ( ; 1 0 x. ; ; 1 0 0 ) ) with typecode |-
200 115 dec0u 10 100 = 1000
201 200 oveq2i Could not format ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ( ; 1 0 x. ; ; 1 0 0 ) ) = ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ( ; 1 0 x. ; ; 1 0 0 ) ) = ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; ; ; 1 0 0 0 ) with typecode |-
202 180 152 182 subdiri Could not format ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; ; ; 1 0 0 0 ) = ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) : No typesetting found for |- ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; ; ; 1 0 0 0 ) = ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) with typecode |-
203 199 201 202 3eqtrri Could not format ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) = ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) x. ; ; 1 0 0 ) : No typesetting found for |- ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) = ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) x. ; ; 1 0 0 ) with typecode |-
204 116 186 mulcomi Could not format ( ; ; 1 0 0 x. ; ; L M N ) = ( ; ; L M N x. ; ; 1 0 0 ) : No typesetting found for |- ( ; ; 1 0 0 x. ; ; L M N ) = ( ; ; L M N x. ; ; 1 0 0 ) with typecode |-
205 203 204 oveq12i Could not format ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 x. ; ; L M N ) ) = ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) x. ; ; 1 0 0 ) + ( ; ; L M N x. ; ; 1 0 0 ) ) : No typesetting found for |- ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 x. ; ; L M N ) ) = ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) x. ; ; 1 0 0 ) + ( ; ; L M N x. ; ; 1 0 0 ) ) with typecode |-
206 196 197 205 3eqtr4i Could not format ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) = ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 x. ; ; L M N ) ) : No typesetting found for |- ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) = ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 x. ; ; L M N ) ) with typecode |-
207 206 188 oveq12i Could not format ( ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) + ; ; O P Q ) = ( ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 x. ; ; L M N ) ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) : No typesetting found for |- ( ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) + ; ; O P Q ) = ( ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 x. ; ; L M N ) ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) with typecode |-
208 187 191 addcli Could not format ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) e. CC : No typesetting found for |- ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) e. CC with typecode |-
209 subsub Could not format ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) e. CC /\ ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) e. CC /\ ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) e. CC ) -> ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) = ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) : No typesetting found for |- ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) e. CC /\ ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) e. CC /\ ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) e. CC ) -> ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) = ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) with typecode |-
210 183 184 208 209 mp3an Could not format ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) = ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) : No typesetting found for |- ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) = ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) with typecode |-
211 192 207 210 3eqtr4ri Could not format ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) = ( ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) + ; ; O P Q ) : No typesetting found for |- ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) = ( ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) + ; ; O P Q ) with typecode |-
212 176 211 eqtr4i Could not format ( ; ; ; A B C D x. ; ; ; E F G H ) = ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) : No typesetting found for |- ( ; ; ; A B C D x. ; ; ; E F G H ) = ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) with typecode |-
213 179 nn0rei Could not format ; ; ; W X Y Z e. RR : No typesetting found for |- ; ; ; W X Y Z e. RR with typecode |-
214 181 nn0rei 1000
215 213 214 remulcli Could not format ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) e. RR : No typesetting found for |- ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) e. RR with typecode |-
216 149 nn0rei Could not format ; ; R S T e. RR : No typesetting found for |- ; ; R S T e. RR with typecode |-
217 1re 1
218 216 217 readdcli Could not format ( ; ; R S T + 1 ) e. RR : No typesetting found for |- ( ; ; R S T + 1 ) e. RR with typecode |-
219 218 214 remulcli Could not format ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) e. RR : No typesetting found for |- ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) e. RR with typecode |-
220 115 nn0rei 100
221 39 nn0rei Could not format ; ; L M N e. RR : No typesetting found for |- ; ; L M N e. RR with typecode |-
222 220 221 remulcli Could not format ( ; ; 1 0 0 x. ; ; L M N ) e. RR : No typesetting found for |- ( ; ; 1 0 0 x. ; ; L M N ) e. RR with typecode |-
223 15 nn0rei O
224 220 223 remulcli 100 O
225 16 17 deccl Could not format ; P Q e. NN0 : No typesetting found for |- ; P Q e. NN0 with typecode |-
226 225 nn0rei Could not format ; P Q e. RR : No typesetting found for |- ; P Q e. RR with typecode |-
227 224 226 readdcli Could not format ( ( ; ; 1 0 0 x. O ) + ; P Q ) e. RR : No typesetting found for |- ( ( ; ; 1 0 0 x. O ) + ; P Q ) e. RR with typecode |-
228 222 227 readdcli Could not format ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) e. RR : No typesetting found for |- ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) e. RR with typecode |-
229 219 228 resubcli Could not format ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) e. RR : No typesetting found for |- ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) e. RR with typecode |-
230 224 recni 100 O
231 226 recni Could not format ; P Q e. CC : No typesetting found for |- ; P Q e. CC with typecode |-
232 187 230 231 addassi Could not format ( ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ; ; 1 0 0 x. O ) ) + ; P Q ) = ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) : No typesetting found for |- ( ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ; ; 1 0 0 x. O ) ) + ; P Q ) = ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) with typecode |-
233 223 recni O
234 116 186 233 adddii Could not format ( ; ; 1 0 0 x. ( ; ; L M N + O ) ) = ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ; ; 1 0 0 x. O ) ) : No typesetting found for |- ( ; ; 1 0 0 x. ( ; ; L M N + O ) ) = ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ; ; 1 0 0 x. O ) ) with typecode |-
235 29 oveq2i Could not format ( ; ; 1 0 0 x. ( ; ; L M N + O ) ) = ( ; ; 1 0 0 x. ; ; ; R S T U ) : No typesetting found for |- ( ; ; 1 0 0 x. ( ; ; L M N + O ) ) = ( ; ; 1 0 0 x. ; ; ; R S T U ) with typecode |-
236 234 235 eqtr3i Could not format ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ; ; 1 0 0 x. O ) ) = ( ; ; 1 0 0 x. ; ; ; R S T U ) : No typesetting found for |- ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ; ; 1 0 0 x. O ) ) = ( ; ; 1 0 0 x. ; ; ; R S T U ) with typecode |-
237 236 oveq1i Could not format ( ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ; ; 1 0 0 x. O ) ) + ; P Q ) = ( ( ; ; 1 0 0 x. ; ; ; R S T U ) + ; P Q ) : No typesetting found for |- ( ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ; ; 1 0 0 x. O ) ) + ; P Q ) = ( ( ; ; 1 0 0 x. ; ; ; R S T U ) + ; P Q ) with typecode |-
238 232 237 eqtr3i Could not format ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) = ( ( ; ; 1 0 0 x. ; ; ; R S T U ) + ; P Q ) : No typesetting found for |- ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) = ( ( ; ; 1 0 0 x. ; ; ; R S T U ) + ; P Q ) with typecode |-
239 21 101 16 114 17 114 26 27 28 3decltc Could not format ; ; U P Q < ; ; ; 1 0 0 0 : No typesetting found for |- ; ; U P Q < ; ; ; 1 0 0 0 with typecode |-
240 21 16 deccl Could not format ; U P e. NN0 : No typesetting found for |- ; U P e. NN0 with typecode |-
241 240 17 deccl Could not format ; ; U P Q e. NN0 : No typesetting found for |- ; ; U P Q e. NN0 with typecode |-
242 241 nn0rei Could not format ; ; U P Q e. RR : No typesetting found for |- ; ; U P Q e. RR with typecode |-
243 216 214 remulcli Could not format ( ; ; R S T x. ; ; ; 1 0 0 0 ) e. RR : No typesetting found for |- ( ; ; R S T x. ; ; ; 1 0 0 0 ) e. RR with typecode |-
244 242 214 243 ltadd2i Could not format ( ; ; U P Q < ; ; ; 1 0 0 0 <-> ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; U P Q ) < ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 ) ) : No typesetting found for |- ( ; ; U P Q < ; ; ; 1 0 0 0 <-> ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; U P Q ) < ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 ) ) with typecode |-
245 239 244 mpbi Could not format ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; U P Q ) < ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; U P Q ) < ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 ) with typecode |-
246 150 182 mulcli Could not format ( ; ; R S T x. ; ; ; 1 0 0 0 ) e. CC : No typesetting found for |- ( ; ; R S T x. ; ; ; 1 0 0 0 ) e. CC with typecode |-
247 21 nn0cni U
248 116 247 mulcli 100 U
249 246 248 231 addassi Could not format ( ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 x. U ) ) + ; P Q ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ( ; ; 1 0 0 x. U ) + ; P Q ) ) : No typesetting found for |- ( ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 x. U ) ) + ; P Q ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ( ; ; 1 0 0 x. U ) + ; P Q ) ) with typecode |-
250 dfdec10 Could not format ; ; ; R S T U = ( ( ; 1 0 x. ; ; R S T ) + U ) : No typesetting found for |- ; ; ; R S T U = ( ( ; 1 0 x. ; ; R S T ) + U ) with typecode |-
251 250 oveq2i Could not format ( ; ; 1 0 0 x. ; ; ; R S T U ) = ( ; ; 1 0 0 x. ( ( ; 1 0 x. ; ; R S T ) + U ) ) : No typesetting found for |- ( ; ; 1 0 0 x. ; ; ; R S T U ) = ( ; ; 1 0 0 x. ( ( ; 1 0 x. ; ; R S T ) + U ) ) with typecode |-
252 46 150 mulcli Could not format ( ; 1 0 x. ; ; R S T ) e. CC : No typesetting found for |- ( ; 1 0 x. ; ; R S T ) e. CC with typecode |-
253 116 252 247 adddii Could not format ( ; ; 1 0 0 x. ( ( ; 1 0 x. ; ; R S T ) + U ) ) = ( ( ; ; 1 0 0 x. ( ; 1 0 x. ; ; R S T ) ) + ( ; ; 1 0 0 x. U ) ) : No typesetting found for |- ( ; ; 1 0 0 x. ( ( ; 1 0 x. ; ; R S T ) + U ) ) = ( ( ; ; 1 0 0 x. ( ; 1 0 x. ; ; R S T ) ) + ( ; ; 1 0 0 x. U ) ) with typecode |-
254 150 182 mulcomi Could not format ( ; ; R S T x. ; ; ; 1 0 0 0 ) = ( ; ; ; 1 0 0 0 x. ; ; R S T ) : No typesetting found for |- ( ; ; R S T x. ; ; ; 1 0 0 0 ) = ( ; ; ; 1 0 0 0 x. ; ; R S T ) with typecode |-
255 46 116 mulcomi 10 100 = 100 10
256 255 200 eqtr3i 100 10 = 1000
257 256 oveq1i Could not format ( ( ; ; 1 0 0 x. ; 1 0 ) x. ; ; R S T ) = ( ; ; ; 1 0 0 0 x. ; ; R S T ) : No typesetting found for |- ( ( ; ; 1 0 0 x. ; 1 0 ) x. ; ; R S T ) = ( ; ; ; 1 0 0 0 x. ; ; R S T ) with typecode |-
258 116 46 150 mulassi Could not format ( ( ; ; 1 0 0 x. ; 1 0 ) x. ; ; R S T ) = ( ; ; 1 0 0 x. ( ; 1 0 x. ; ; R S T ) ) : No typesetting found for |- ( ( ; ; 1 0 0 x. ; 1 0 ) x. ; ; R S T ) = ( ; ; 1 0 0 x. ( ; 1 0 x. ; ; R S T ) ) with typecode |-
259 254 257 258 3eqtr2ri Could not format ( ; ; 1 0 0 x. ( ; 1 0 x. ; ; R S T ) ) = ( ; ; R S T x. ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ; ; 1 0 0 x. ( ; 1 0 x. ; ; R S T ) ) = ( ; ; R S T x. ; ; ; 1 0 0 0 ) with typecode |-
260 259 oveq1i Could not format ( ( ; ; 1 0 0 x. ( ; 1 0 x. ; ; R S T ) ) + ( ; ; 1 0 0 x. U ) ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 x. U ) ) : No typesetting found for |- ( ( ; ; 1 0 0 x. ( ; 1 0 x. ; ; R S T ) ) + ( ; ; 1 0 0 x. U ) ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 x. U ) ) with typecode |-
261 251 253 260 3eqtri Could not format ( ; ; 1 0 0 x. ; ; ; R S T U ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 x. U ) ) : No typesetting found for |- ( ; ; 1 0 0 x. ; ; ; R S T U ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 x. U ) ) with typecode |-
262 261 oveq1i Could not format ( ( ; ; 1 0 0 x. ; ; ; R S T U ) + ; P Q ) = ( ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 x. U ) ) + ; P Q ) : No typesetting found for |- ( ( ; ; 1 0 0 x. ; ; ; R S T U ) + ; P Q ) = ( ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 x. U ) ) + ; P Q ) with typecode |-
263 21 16 78 dfdec100 Could not format ; ; U P Q = ( ( ; ; 1 0 0 x. U ) + ; P Q ) : No typesetting found for |- ; ; U P Q = ( ( ; ; 1 0 0 x. U ) + ; P Q ) with typecode |-
264 263 oveq2i Could not format ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; U P Q ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ( ; ; 1 0 0 x. U ) + ; P Q ) ) : No typesetting found for |- ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; U P Q ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ( ; ; 1 0 0 x. U ) + ; P Q ) ) with typecode |-
265 249 262 264 3eqtr4i Could not format ( ( ; ; 1 0 0 x. ; ; ; R S T U ) + ; P Q ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; U P Q ) : No typesetting found for |- ( ( ; ; 1 0 0 x. ; ; ; R S T U ) + ; P Q ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; U P Q ) with typecode |-
266 150 151 182 adddiri Could not format ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( 1 x. ; ; ; 1 0 0 0 ) ) : No typesetting found for |- ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( 1 x. ; ; ; 1 0 0 0 ) ) with typecode |-
267 182 mulid2i 1 1000 = 1000
268 267 oveq2i Could not format ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( 1 x. ; ; ; 1 0 0 0 ) ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( 1 x. ; ; ; 1 0 0 0 ) ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 ) with typecode |-
269 266 268 eqtri Could not format ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 ) with typecode |-
270 245 265 269 3brtr4i Could not format ( ( ; ; 1 0 0 x. ; ; ; R S T U ) + ; P Q ) < ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ( ; ; 1 0 0 x. ; ; ; R S T U ) + ; P Q ) < ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) with typecode |-
271 238 270 eqbrtri Could not format ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) < ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) < ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) with typecode |-
272 228 219 posdifi Could not format ( ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) < ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) <-> 0 < ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) : No typesetting found for |- ( ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) < ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) <-> 0 < ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) with typecode |-
273 271 272 mpbi Could not format 0 < ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) : No typesetting found for |- 0 < ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) with typecode |-
274 elrp Could not format ( ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) e. RR+ <-> ( ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) e. RR /\ 0 < ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) ) : No typesetting found for |- ( ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) e. RR+ <-> ( ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) e. RR /\ 0 < ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) ) with typecode |-
275 229 273 274 mpbir2an Could not format ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) e. RR+ : No typesetting found for |- ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) e. RR+ with typecode |-
276 ltsubrp Could not format ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) e. RR /\ ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) e. RR+ ) -> ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) < ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) ) : No typesetting found for |- ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) e. RR /\ ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) e. RR+ ) -> ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) < ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) ) with typecode |-
277 215 275 276 mp2an Could not format ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) < ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) < ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) with typecode |-
278 212 277 eqbrtri Could not format ( ; ; ; A B C D x. ; ; ; E F G H ) < ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ; ; ; A B C D x. ; ; ; E F G H ) < ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) with typecode |-
279 34 3 deccl Could not format ; ; A B C e. NN0 : No typesetting found for |- ; ; A B C e. NN0 with typecode |-
280 279 4 deccl Could not format ; ; ; A B C D e. NN0 : No typesetting found for |- ; ; ; A B C D e. NN0 with typecode |-
281 280 nn0rei Could not format ; ; ; A B C D e. RR : No typesetting found for |- ; ; ; A B C D e. RR with typecode |-
282 36 6 deccl Could not format ; ; E F G e. NN0 : No typesetting found for |- ; ; E F G e. NN0 with typecode |-
283 282 10 deccl Could not format ; ; ; E F G H e. NN0 : No typesetting found for |- ; ; ; E F G H e. NN0 with typecode |-
284 283 nn0rei Could not format ; ; ; E F G H e. RR : No typesetting found for |- ; ; ; E F G H e. RR with typecode |-
285 281 284 remulcli Could not format ( ; ; ; A B C D x. ; ; ; E F G H ) e. RR : No typesetting found for |- ( ; ; ; A B C D x. ; ; ; E F G H ) e. RR with typecode |-
286 45 decnncl2 100
287 286 decnncl2 1000
288 287 nngt0i 0 < 1000
289 214 288 pm3.2i 1000 0 < 1000
290 ltdiv1 Could not format ( ( ( ; ; ; A B C D x. ; ; ; E F G H ) e. RR /\ ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) e. RR /\ ( ; ; ; 1 0 0 0 e. RR /\ 0 < ; ; ; 1 0 0 0 ) ) -> ( ( ; ; ; A B C D x. ; ; ; E F G H ) < ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) <-> ( ( ; ; ; A B C D x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) ) ) : No typesetting found for |- ( ( ( ; ; ; A B C D x. ; ; ; E F G H ) e. RR /\ ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) e. RR /\ ( ; ; ; 1 0 0 0 e. RR /\ 0 < ; ; ; 1 0 0 0 ) ) -> ( ( ; ; ; A B C D x. ; ; ; E F G H ) < ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) <-> ( ( ; ; ; A B C D x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) ) ) with typecode |-
291 285 215 289 290 mp3an Could not format ( ( ; ; ; A B C D x. ; ; ; E F G H ) < ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) <-> ( ( ; ; ; A B C D x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) ) : No typesetting found for |- ( ( ; ; ; A B C D x. ; ; ; E F G H ) < ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) <-> ( ( ; ; ; A B C D x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) ) with typecode |-
292 278 291 mpbi Could not format ( ( ; ; ; A B C D x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ( ; ; ; A B C D x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) with typecode |-
293 280 nn0cni Could not format ; ; ; A B C D e. CC : No typesetting found for |- ; ; ; A B C D e. CC with typecode |-
294 283 nn0cni Could not format ; ; ; E F G H e. CC : No typesetting found for |- ; ; ; E F G H e. CC with typecode |-
295 214 288 gt0ne0ii 1000 0
296 293 294 182 295 div23i Could not format ( ( ; ; ; A B C D x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) = ( ( ; ; ; A B C D / ; ; ; 1 0 0 0 ) x. ; ; ; E F G H ) : No typesetting found for |- ( ( ; ; ; A B C D x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) = ( ( ; ; ; A B C D / ; ; ; 1 0 0 0 ) x. ; ; ; E F G H ) with typecode |-
297 1 2 3 66 dpmul1000 Could not format ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) = ; ; ; A B C D : No typesetting found for |- ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) = ; ; ; A B C D with typecode |-
298 297 oveq1i Could not format ( ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( ; ; ; A B C D / ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( ; ; ; A B C D / ; ; ; 1 0 0 0 ) with typecode |-
299 3 nn0rei C
300 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 |-
301 299 66 300 mp2an Could not format _ C D e. RR : No typesetting found for |- _ C D e. RR with typecode |-
302 dp2cl Could not format ( ( B e. RR /\ _ C D e. RR ) -> _ B _ C D e. RR ) : No typesetting found for |- ( ( B e. RR /\ _ C D e. RR ) -> _ B _ C D e. RR ) with typecode |-
303 41 301 302 mp2an Could not format _ B _ C D e. RR : No typesetting found for |- _ B _ C D e. RR with typecode |-
304 dpcl Could not format ( ( A e. NN0 /\ _ B _ C D e. RR ) -> ( A . _ B _ C D ) e. RR ) : No typesetting found for |- ( ( A e. NN0 /\ _ B _ C D e. RR ) -> ( A . _ B _ C D ) e. RR ) with typecode |-
305 1 303 304 mp2an Could not format ( A . _ B _ C D ) e. RR : No typesetting found for |- ( A . _ B _ C D ) e. RR with typecode |-
306 305 recni Could not format ( A . _ B _ C D ) e. CC : No typesetting found for |- ( A . _ B _ C D ) e. CC with typecode |-
307 306 182 295 divcan4i Could not format ( ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( A . _ B _ C D ) : No typesetting found for |- ( ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( A . _ B _ C D ) with typecode |-
308 298 307 eqtr3i Could not format ( ; ; ; A B C D / ; ; ; 1 0 0 0 ) = ( A . _ B _ C D ) : No typesetting found for |- ( ; ; ; A B C D / ; ; ; 1 0 0 0 ) = ( A . _ B _ C D ) with typecode |-
309 308 oveq1i Could not format ( ( ; ; ; A B C D / ; ; ; 1 0 0 0 ) x. ; ; ; E F G H ) = ( ( A . _ B _ C D ) x. ; ; ; E F G H ) : No typesetting found for |- ( ( ; ; ; A B C D / ; ; ; 1 0 0 0 ) x. ; ; ; E F G H ) = ( ( A . _ B _ C D ) x. ; ; ; E F G H ) with typecode |-
310 296 309 eqtri Could not format ( ( ; ; ; A B C D x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) = ( ( A . _ B _ C D ) x. ; ; ; E F G H ) : No typesetting found for |- ( ( ; ; ; A B C D x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) = ( ( A . _ B _ C D ) x. ; ; ; E F G H ) with typecode |-
311 180 182 295 divcan4i Could not format ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ; ; ; W X Y Z : No typesetting found for |- ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ; ; ; W X Y Z with typecode |-
312 292 310 311 3brtr3i Could not format ( ( A . _ B _ C D ) x. ; ; ; E F G H ) < ; ; ; W X Y Z : No typesetting found for |- ( ( A . _ B _ C D ) x. ; ; ; E F G H ) < ; ; ; W X Y Z with typecode |-
313 305 284 remulcli Could not format ( ( A . _ B _ C D ) x. ; ; ; E F G H ) e. RR : No typesetting found for |- ( ( A . _ B _ C D ) x. ; ; ; E F G H ) e. RR with typecode |-
314 ltdiv1 Could not format ( ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) e. RR /\ ; ; ; W X Y Z e. RR /\ ( ; ; ; 1 0 0 0 e. RR /\ 0 < ; ; ; 1 0 0 0 ) ) -> ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) < ; ; ; W X Y Z <-> ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ; ; ; W X Y Z / ; ; ; 1 0 0 0 ) ) ) : No typesetting found for |- ( ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) e. RR /\ ; ; ; W X Y Z e. RR /\ ( ; ; ; 1 0 0 0 e. RR /\ 0 < ; ; ; 1 0 0 0 ) ) -> ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) < ; ; ; W X Y Z <-> ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ; ; ; W X Y Z / ; ; ; 1 0 0 0 ) ) ) with typecode |-
315 313 213 289 314 mp3an Could not format ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) < ; ; ; W X Y Z <-> ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ; ; ; W X Y Z / ; ; ; 1 0 0 0 ) ) : No typesetting found for |- ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) < ; ; ; W X Y Z <-> ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ; ; ; W X Y Z / ; ; ; 1 0 0 0 ) ) with typecode |-
316 312 315 mpbi Could not format ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ; ; ; W X Y Z / ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ; ; ; W X Y Z / ; ; ; 1 0 0 0 ) with typecode |-
317 306 294 182 295 divassi Could not format ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) = ( ( A . _ B _ C D ) x. ( ; ; ; E F G H / ; ; ; 1 0 0 0 ) ) : No typesetting found for |- ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) = ( ( A . _ B _ C D ) x. ( ; ; ; E F G H / ; ; ; 1 0 0 0 ) ) with typecode |-
318 5 9 6 70 dpmul1000 Could not format ( ( E . _ F _ G H ) x. ; ; ; 1 0 0 0 ) = ; ; ; E F G H : No typesetting found for |- ( ( E . _ F _ G H ) x. ; ; ; 1 0 0 0 ) = ; ; ; E F G H with typecode |-
319 318 oveq1i Could not format ( ( ( E . _ F _ G H ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( ; ; ; E F G H / ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ( ( E . _ F _ G H ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( ; ; ; E F G H / ; ; ; 1 0 0 0 ) with typecode |-
320 6 nn0rei G
321 dp2cl Could not format ( ( G e. RR /\ H e. RR ) -> _ G H e. RR ) : No typesetting found for |- ( ( G e. RR /\ H e. RR ) -> _ G H e. RR ) with typecode |-
322 320 70 321 mp2an Could not format _ G H e. RR : No typesetting found for |- _ G H e. RR with typecode |-
323 dp2cl Could not format ( ( F e. RR /\ _ G H e. RR ) -> _ F _ G H e. RR ) : No typesetting found for |- ( ( F e. RR /\ _ G H e. RR ) -> _ F _ G H e. RR ) with typecode |-
324 47 322 323 mp2an Could not format _ F _ G H e. RR : No typesetting found for |- _ F _ G H e. RR with typecode |-
325 dpcl Could not format ( ( E e. NN0 /\ _ F _ G H e. RR ) -> ( E . _ F _ G H ) e. RR ) : No typesetting found for |- ( ( E e. NN0 /\ _ F _ G H e. RR ) -> ( E . _ F _ G H ) e. RR ) with typecode |-
326 5 324 325 mp2an Could not format ( E . _ F _ G H ) e. RR : No typesetting found for |- ( E . _ F _ G H ) e. RR with typecode |-
327 326 recni Could not format ( E . _ F _ G H ) e. CC : No typesetting found for |- ( E . _ F _ G H ) e. CC with typecode |-
328 327 182 295 divcan4i Could not format ( ( ( E . _ F _ G H ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( E . _ F _ G H ) : No typesetting found for |- ( ( ( E . _ F _ G H ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( E . _ F _ G H ) with typecode |-
329 319 328 eqtr3i Could not format ( ; ; ; E F G H / ; ; ; 1 0 0 0 ) = ( E . _ F _ G H ) : No typesetting found for |- ( ; ; ; E F G H / ; ; ; 1 0 0 0 ) = ( E . _ F _ G H ) with typecode |-
330 329 oveq2i Could not format ( ( A . _ B _ C D ) x. ( ; ; ; E F G H / ; ; ; 1 0 0 0 ) ) = ( ( A . _ B _ C D ) x. ( E . _ F _ G H ) ) : No typesetting found for |- ( ( A . _ B _ C D ) x. ( ; ; ; E F G H / ; ; ; 1 0 0 0 ) ) = ( ( A . _ B _ C D ) x. ( E . _ F _ G H ) ) with typecode |-
331 317 330 eqtri Could not format ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) = ( ( A . _ B _ C D ) x. ( E . _ F _ G H ) ) : No typesetting found for |- ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) = ( ( A . _ B _ C D ) x. ( E . _ F _ G H ) ) with typecode |-
332 25 nn0rei Z
333 22 23 24 332 dpmul1000 Could not format ( ( W . _ X _ Y Z ) x. ; ; ; 1 0 0 0 ) = ; ; ; W X Y Z : No typesetting found for |- ( ( W . _ X _ Y Z ) x. ; ; ; 1 0 0 0 ) = ; ; ; W X Y Z with typecode |-
334 333 oveq1i Could not format ( ( ( W . _ X _ Y Z ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( ; ; ; W X Y Z / ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ( ( W . _ X _ Y Z ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( ; ; ; W X Y Z / ; ; ; 1 0 0 0 ) with typecode |-
335 23 nn0rei X
336 24 nn0rei Y
337 dp2cl Could not format ( ( Y e. RR /\ Z e. RR ) -> _ Y Z e. RR ) : No typesetting found for |- ( ( Y e. RR /\ Z e. RR ) -> _ Y Z e. RR ) with typecode |-
338 336 332 337 mp2an Could not format _ Y Z e. RR : No typesetting found for |- _ Y Z e. RR with typecode |-
339 dp2cl Could not format ( ( X e. RR /\ _ Y Z e. RR ) -> _ X _ Y Z e. RR ) : No typesetting found for |- ( ( X e. RR /\ _ Y Z e. RR ) -> _ X _ Y Z e. RR ) with typecode |-
340 335 338 339 mp2an Could not format _ X _ Y Z e. RR : No typesetting found for |- _ X _ Y Z e. RR with typecode |-
341 dpcl Could not format ( ( W e. NN0 /\ _ X _ Y Z e. RR ) -> ( W . _ X _ Y Z ) e. RR ) : No typesetting found for |- ( ( W e. NN0 /\ _ X _ Y Z e. RR ) -> ( W . _ X _ Y Z ) e. RR ) with typecode |-
342 22 340 341 mp2an Could not format ( W . _ X _ Y Z ) e. RR : No typesetting found for |- ( W . _ X _ Y Z ) e. RR with typecode |-
343 342 recni Could not format ( W . _ X _ Y Z ) e. CC : No typesetting found for |- ( W . _ X _ Y Z ) e. CC with typecode |-
344 343 182 295 divcan4i Could not format ( ( ( W . _ X _ Y Z ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( W . _ X _ Y Z ) : No typesetting found for |- ( ( ( W . _ X _ Y Z ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( W . _ X _ Y Z ) with typecode |-
345 334 344 eqtr3i Could not format ( ; ; ; W X Y Z / ; ; ; 1 0 0 0 ) = ( W . _ X _ Y Z ) : No typesetting found for |- ( ; ; ; W X Y Z / ; ; ; 1 0 0 0 ) = ( W . _ X _ Y Z ) with typecode |-
346 316 331 345 3brtr3i Could not format ( ( A . _ B _ C D ) x. ( E . _ F _ G H ) ) < ( W . _ X _ Y Z ) : No typesetting found for |- ( ( A . _ B _ C D ) x. ( E . _ F _ G H ) ) < ( W . _ X _ Y Z ) with typecode |-