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\in {\mathbb{N}}_0$$
	dpmul.b	$$⊢B\in {\mathbb{N}}_0$$
	dpmul.c	$$⊢C\in {\mathbb{N}}_0$$
	dpmul.d	$$⊢D\in {\mathbb{N}}_0$$
	dpmul.e	$$⊢E\in {\mathbb{N}}_0$$
	dpmul.g	$$⊢G\in {\mathbb{N}}_0$$
	dpmul.j	$$⊢J\in {\mathbb{N}}_0$$
	dpmul.k	$$⊢K\in {\mathbb{N}}_0$$
	dpmul4.f	$$⊢F\in {\mathbb{N}}_0$$
	dpmul4.h	$$⊢H\in {\mathbb{N}}_0$$
	dpmul4.i	$$⊢I\in {\mathbb{N}}_0$$
	dpmul4.l	$$⊢L\in {\mathbb{N}}_0$$
	dpmul4.m	$$⊢M\in {\mathbb{N}}_0$$
	dpmul4.n	$$⊢N\in {\mathbb{N}}_0$$
	dpmul4.o	$$⊢O\in {\mathbb{N}}_0$$
	dpmul4.p	$$⊢P\in {\mathbb{N}}_0$$
	dpmul4.q	$$⊢Q\in {\mathbb{N}}_0$$
	dpmul4.r	$$⊢R\in {\mathbb{N}}_0$$
	dpmul4.s	$$⊢S\in {\mathbb{N}}_0$$
	dpmul4.t	$$⊢T\in {\mathbb{N}}_0$$
	dpmul4.u	$$⊢U\in {\mathbb{N}}_0$$
	dpmul4.w	$$⊢W\in {\mathbb{N}}_0$$
	dpmul4.x	$$⊢X\in {\mathbb{N}}_0$$
	dpmul4.y	$$⊢Y\in {\mathbb{N}}_0$$
	dpmul4.z	$$⊢Z\in {\mathbb{N}}_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\in {\mathbb{N}}_0$$
2		dpmul.b	$$⊢B\in {\mathbb{N}}_0$$
3		dpmul.c	$$⊢C\in {\mathbb{N}}_0$$
4		dpmul.d	$$⊢D\in {\mathbb{N}}_0$$
5		dpmul.e	$$⊢E\in {\mathbb{N}}_0$$
6		dpmul.g	$$⊢G\in {\mathbb{N}}_0$$
7		dpmul.j	$$⊢J\in {\mathbb{N}}_0$$
8		dpmul.k	$$⊢K\in {\mathbb{N}}_0$$
9		dpmul4.f	$$⊢F\in {\mathbb{N}}_0$$
10		dpmul4.h	$$⊢H\in {\mathbb{N}}_0$$
11		dpmul4.i	$$⊢I\in {\mathbb{N}}_0$$
12		dpmul4.l	$$⊢L\in {\mathbb{N}}_0$$
13		dpmul4.m	$$⊢M\in {\mathbb{N}}_0$$
14		dpmul4.n	$$⊢N\in {\mathbb{N}}_0$$
15		dpmul4.o	$$⊢O\in {\mathbb{N}}_0$$
16		dpmul4.p	$$⊢P\in {\mathbb{N}}_0$$
17		dpmul4.q	$$⊢Q\in {\mathbb{N}}_0$$
18		dpmul4.r	$$⊢R\in {\mathbb{N}}_0$$
19		dpmul4.s	$$⊢S\in {\mathbb{N}}_0$$
20		dpmul4.t	$$⊢T\in {\mathbb{N}}_0$$
21		dpmul4.u	$$⊢U\in {\mathbb{N}}_0$$
22		dpmul4.w	$$⊢W\in {\mathbb{N}}_0$$
23		dpmul4.x	$$⊢X\in {\mathbb{N}}_0$$
24		dpmul4.y	$$⊢Y\in {\mathbb{N}}_0$$
25		dpmul4.z	$$⊢Z\in {\mathbb{N}}_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\in {\mathbb{N}}_0$$
41	2	nn0rei	$$⊢B\in ℝ$$
42		dpcl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in ℝ\right)\to A.B\in ℝ$$
43	1 41 42	mp2an	$$⊢A.B\in ℝ$$
44	43	recni	$$⊢A.B\in ℂ$$
45		10nn	$$⊢10\in \mathbb{N}$$
46	45	nncni	$$⊢10\in ℂ$$
47	9	nn0rei	$$⊢F\in ℝ$$
48		dpcl	$$⊢\left(E\in {\mathbb{N}}_0\wedge F\in ℝ\right)\to E.F\in ℝ$$
49	5 47 48	mp2an	$$⊢E.F\in ℝ$$
50	49	recni	$$⊢E.F\in ℂ$$
51	44 46 50 46	mul4i	$$⊢\left(A.B\right)\cdot 10\left(E.F\right)\cdot 10=\left(A.B\right)\left(E.F\right)10\cdot 10$$
52	44 50	mulcli	$$⊢\left(A.B\right)\left(E.F\right)\in ℂ$$
53	52 46 46	mulassi	$$⊢\left(A.B\right)\left(E.F\right)\cdot 10\cdot 10=\left(A.B\right)\left(E.F\right)10\cdot 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\in ℝ$$
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	$$⊢\left(A.B\right)\left(E.F\right)\cdot 10=\mathrm{<mi\; mathcolor="\#808">I</mi>\; <mi\; mathcolor="\#808">J</mi>}.K$$
58	57	oveq1i	$$⊢\left(A.B\right)\left(E.F\right)\cdot 10\cdot 10=\left(\mathrm{<mi\; mathcolor="\#808">I</mi>\; <mi\; mathcolor="\#808">J</mi>}.K\right)\cdot 10$$
59	51 53 58	3eqtr2ri	$$⊢\left(\mathrm{<mi\; mathcolor="\#808">I</mi>\; <mi\; mathcolor="\#808">J</mi>}.K\right)\cdot 10=\left(A.B\right)\cdot 10\left(E.F\right)\cdot 10$$
60	11 7	deccl	$$⊢\mathrm{<mi\; mathcolor="\#808">I</mi>\; <mi\; mathcolor="\#808">J</mi>}\in {\mathbb{N}}_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\in ℝ$$
67		dpcl	$$⊢\left(C\in {\mathbb{N}}_0\wedge D\in ℝ\right)\to C.D\in ℝ$$
68	3 66 67	mp2an	$$⊢C.D\in ℝ$$
69	68	recni	$$⊢C.D\in ℂ$$
70	10	nn0rei	$$⊢H\in ℝ$$
71		dpcl	$$⊢\left(G\in {\mathbb{N}}_0\wedge H\in ℝ\right)\to G.H\in ℝ$$
72	6 70 71	mp2an	$$⊢G.H\in ℝ$$
73	72	recni	$$⊢G.H\in ℂ$$
74	69 46 73 46	mul4i	$$⊢\left(C.D\right)\cdot 10\left(G.H\right)\cdot 10=\left(C.D\right)\left(G.H\right)10\cdot 10$$
75	69 73	mulcli	$$⊢\left(C.D\right)\left(G.H\right)\in ℂ$$
76	75 46 46	mulassi	$$⊢\left(C.D\right)\left(G.H\right)\cdot 10\cdot 10=\left(C.D\right)\left(G.H\right)10\cdot 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\in ℝ$$
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	$$⊢\left(\left(A.B\right)+\left(C.D\right)\right)\cdot 10=\left(A.B\right)\cdot 10+\left(C.D\right)\cdot 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	$$⊢\left(\left(E.F\right)+\left(G.H\right)\right)\cdot 10=\left(E.F\right)\cdot 10+\left(G.H\right)\cdot 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	$$⊢\left(A.B\right)+\left(C.D\right)\in ℂ$$
97	50 73	addcli	$$⊢\left(E.F\right)+\left(G.H\right)\in ℂ$$
98	96 46 97 46	mul4i	$$⊢\left(\left(A.B\right)+\left(C.D\right)\right)\cdot 10\left(\left(E.F\right)+\left(G.H\right)\right)\cdot 10=\left(\left(A.B\right)+\left(C.D\right)\right)\left(\left(E.F\right)+\left(G.H\right)\right)10\cdot 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\in {\mathbb{N}}_0$$
102	101	dec0u	$$⊢10\cdot 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\in ℝ$$
106	14	nn0rei	$$⊢N\in ℝ$$
107		dp2cl	$$⊢\left(M\in ℝ\wedge N\in ℝ\right)\to \mathrm{<mi\; mathcolor="\#808">M</mi>\; <mi\; mathcolor="\#808">N</mi>}\in ℝ$$
108	105 106 107	mp2an	$$⊢\mathrm{<mi\; mathcolor="\#808">M</mi>\; <mi\; mathcolor="\#808">N</mi>}\in ℝ$$
109		dpcl	$$⊢\left(L\in {\mathbb{N}}_0\wedge \mathrm{<mi\; mathcolor="\#808">M</mi>\; <mi\; mathcolor="\#808">N</mi>}\in ℝ\right)\to L.\mathrm{<mi\; mathcolor="\#808">M</mi>\; <mi\; mathcolor="\#808">N</mi>}\in ℝ$$
110	12 108 109	mp2an	$$⊢L.\mathrm{<mi\; mathcolor="\#808">M</mi>\; <mi\; mathcolor="\#808">N</mi>}\in ℝ$$
111	110	recni	$$⊢L.\mathrm{<mi\; mathcolor="\#808">M</mi>\; <mi\; mathcolor="\#808">N</mi>}\in ℂ$$
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\in {\mathbb{N}}_0$$
115	101 114	deccl	$$⊢100\in {\mathbb{N}}_0$$
116	115	nn0cni	$$⊢100\in ℂ$$
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\cdot 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\in ℂ$$
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	addlidi	$$⊢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\in {\mathbb{N}}_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\in {\mathbb{N}}_0$$
182	181	nn0cni	$$⊢1000\in ℂ$$
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\in ℂ$$
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\cdot 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\in ℝ$$
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\in ℝ$$
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\in ℝ$$
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\in ℝ$$
224	220 223	remulcli	$$⊢100O\in ℝ$$
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	$$⊢100O\in ℂ$$
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\in ℂ$$
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\in ℂ$$
248	116 247	mulcli	$$⊢100U\in ℂ$$
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\cdot 100=100\cdot 10$$
256	255 200	eqtr3i	$$⊢100\cdot 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	mullidi	$$⊢1\cdot 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\in \mathbb{N}$$
287	286	decnncl2	$$⊢1000\in \mathbb{N}$$
288	287	nngt0i	$$⊢0<1000$$
289	214 288	pm3.2i	$$⊢\left(1000\in ℝ\wedge 0<1000\right)$$
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\ne 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\in ℝ$$
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\in ℝ$$
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\in ℝ$$
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\in ℝ$$
336	24	nn0rei	$$⊢Y\in ℝ$$
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 |-