Theorem mulsproplem9

Description: Lemma for surreal multiplication. Show that the cut involved in surreal multiplication makes sense. (Contributed by Scott Fenton, 5-Mar-2025)

	Ref	Expression
Hypotheses	mulsproplem.1	No typesetting found for |- ( ph -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
	mulsproplem9.1	$$⊢\phi \to A\in \mathrm{No}$$
	mulsproplem9.2	$$⊢\phi \to B\in \mathrm{No}$$
Assertion	mulsproplem9	Could not format assertion : No typesetting found for |- ( ph -> ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <

Proof

Step	Hyp	Ref	Expression
1		mulsproplem.1	Could not format ( ph -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
2		mulsproplem9.1	$$⊢\phi \to A\in \mathrm{No}$$
3		mulsproplem9.2	$$⊢\phi \to B\in \mathrm{No}$$
4		eqid	Could not format ( p e. ( _Left ` A ) , q e. ( _Left ` B ) |-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) = ( p e. ( _Left ` A ) , q e. ( _Left ` B ) |-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) : No typesetting found for |- ( p e. ( _Left ` A ) , q e. ( _Left ` B ) |-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) = ( p e. ( _Left ` A ) , q e. ( _Left ` B ) |-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) with typecode |-
5	4	rnmpo	Could not format ran ( p e. ( _Left ` A ) , q e. ( _Left ` B ) |-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) = { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } : No typesetting found for |- ran ( p e. ( _Left ` A ) , q e. ( _Left ` B ) |-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) = { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } with typecode |-
6		fvex	Could not format ( _Left ` A ) e. _V : No typesetting found for |- ( _Left ` A ) e. _V with typecode |-
7		fvex	Could not format ( _Left ` B ) e. _V : No typesetting found for |- ( _Left ` B ) e. _V with typecode |-
8	6 7	mpoex	Could not format ( p e. ( _Left ` A ) , q e. ( _Left ` B ) |-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) e. _V : No typesetting found for |- ( p e. ( _Left ` A ) , q e. ( _Left ` B ) |-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) e. _V with typecode |-
9	8	rnex	Could not format ran ( p e. ( _Left ` A ) , q e. ( _Left ` B ) |-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) e. _V : No typesetting found for |- ran ( p e. ( _Left ` A ) , q e. ( _Left ` B ) |-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) e. _V with typecode |-
10	5 9	eqeltrri	Could not format { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } e. _V : No typesetting found for |- { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } e. _V with typecode |-
11		eqid	Could not format ( r e. ( _Right ` A ) , s e. ( _Right ` B ) |-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) = ( r e. ( _Right ` A ) , s e. ( _Right ` B ) |-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) : No typesetting found for |- ( r e. ( _Right ` A ) , s e. ( _Right ` B ) |-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) = ( r e. ( _Right ` A ) , s e. ( _Right ` B ) |-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) with typecode |-
12	11	rnmpo	Could not format ran ( r e. ( _Right ` A ) , s e. ( _Right ` B ) |-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) = { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } : No typesetting found for |- ran ( r e. ( _Right ` A ) , s e. ( _Right ` B ) |-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) = { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } with typecode |-
13		fvex	Could not format ( _Right ` A ) e. _V : No typesetting found for |- ( _Right ` A ) e. _V with typecode |-
14		fvex	Could not format ( _Right ` B ) e. _V : No typesetting found for |- ( _Right ` B ) e. _V with typecode |-
15	13 14	mpoex	Could not format ( r e. ( _Right ` A ) , s e. ( _Right ` B ) |-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) e. _V : No typesetting found for |- ( r e. ( _Right ` A ) , s e. ( _Right ` B ) |-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) e. _V with typecode |-
16	15	rnex	Could not format ran ( r e. ( _Right ` A ) , s e. ( _Right ` B ) |-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) e. _V : No typesetting found for |- ran ( r e. ( _Right ` A ) , s e. ( _Right ` B ) |-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) e. _V with typecode |-
17	12 16	eqeltrri	Could not format { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } e. _V : No typesetting found for |- { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } e. _V with typecode |-
18	10 17	unex	Could not format ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) e. _V : No typesetting found for |- ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) e. _V with typecode |-
19	18	a1i	Could not format ( ph -> ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) e. _V ) : No typesetting found for |- ( ph -> ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) e. _V ) with typecode |-
20		eqid	Could not format ( t e. ( _Left ` A ) , u e. ( _Right ` B ) |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) = ( t e. ( _Left ` A ) , u e. ( _Right ` B ) |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) : No typesetting found for |- ( t e. ( _Left ` A ) , u e. ( _Right ` B ) |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) = ( t e. ( _Left ` A ) , u e. ( _Right ` B ) |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) with typecode |-
21	20	rnmpo	Could not format ran ( t e. ( _Left ` A ) , u e. ( _Right ` B ) |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) = { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } : No typesetting found for |- ran ( t e. ( _Left ` A ) , u e. ( _Right ` B ) |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) = { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } with typecode |-
22	6 14	mpoex	Could not format ( t e. ( _Left ` A ) , u e. ( _Right ` B ) |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) e. _V : No typesetting found for |- ( t e. ( _Left ` A ) , u e. ( _Right ` B ) |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) e. _V with typecode |-
23	22	rnex	Could not format ran ( t e. ( _Left ` A ) , u e. ( _Right ` B ) |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) e. _V : No typesetting found for |- ran ( t e. ( _Left ` A ) , u e. ( _Right ` B ) |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) e. _V with typecode |-
24	21 23	eqeltrri	Could not format { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } e. _V : No typesetting found for |- { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } e. _V with typecode |-
25		eqid	Could not format ( v e. ( _Right ` A ) , w e. ( _Left ` B ) |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) = ( v e. ( _Right ` A ) , w e. ( _Left ` B ) |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) : No typesetting found for |- ( v e. ( _Right ` A ) , w e. ( _Left ` B ) |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) = ( v e. ( _Right ` A ) , w e. ( _Left ` B ) |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) with typecode |-
26	25	rnmpo	Could not format ran ( v e. ( _Right ` A ) , w e. ( _Left ` B ) |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) = { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } : No typesetting found for |- ran ( v e. ( _Right ` A ) , w e. ( _Left ` B ) |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) = { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } with typecode |-
27	13 7	mpoex	Could not format ( v e. ( _Right ` A ) , w e. ( _Left ` B ) |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) e. _V : No typesetting found for |- ( v e. ( _Right ` A ) , w e. ( _Left ` B ) |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) e. _V with typecode |-
28	27	rnex	Could not format ran ( v e. ( _Right ` A ) , w e. ( _Left ` B ) |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) e. _V : No typesetting found for |- ran ( v e. ( _Right ` A ) , w e. ( _Left ` B ) |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) e. _V with typecode |-
29	26 28	eqeltrri	Could not format { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } e. _V : No typesetting found for |- { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } e. _V with typecode |-
30	24 29	unex	Could not format ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) e. _V : No typesetting found for |- ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) e. _V with typecode |-
31	30	a1i	Could not format ( ph -> ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) e. _V ) : No typesetting found for |- ( ph -> ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) e. _V ) with typecode |-
32	1	adantr	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
33		leftssold	Could not format ( _Left ` A ) C_ ( _Old ` ( bday ` A ) ) : No typesetting found for |- ( _Left ` A ) C_ ( _Old ` ( bday ` A ) ) with typecode |-
34		simprl	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> p e. ( _Left ` A ) ) : No typesetting found for |- ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> p e. ( _Left ` A ) ) with typecode |-
35	33 34	sselid	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> p e. ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> p e. ( _Old ` ( bday ` A ) ) ) with typecode |-
36	3	adantr	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> B e. No ) : No typesetting found for |- ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> B e. No ) with typecode |-
37	32 35 36	mulsproplem2	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( p x.s B ) e. No ) : No typesetting found for |- ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( p x.s B ) e. No ) with typecode |-
38	2	adantr	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> A e. No ) : No typesetting found for |- ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> A e. No ) with typecode |-
39		leftssold	Could not format ( _Left ` B ) C_ ( _Old ` ( bday ` B ) ) : No typesetting found for |- ( _Left ` B ) C_ ( _Old ` ( bday ` B ) ) with typecode |-
40		simprr	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> q e. ( _Left ` B ) ) : No typesetting found for |- ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> q e. ( _Left ` B ) ) with typecode |-
41	39 40	sselid	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> q e. ( _Old ` ( bday ` B ) ) ) : No typesetting found for |- ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> q e. ( _Old ` ( bday ` B ) ) ) with typecode |-
42	32 38 41	mulsproplem3	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( A x.s q ) e. No ) : No typesetting found for |- ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( A x.s q ) e. No ) with typecode |-
43	37 42	addscld	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( ( p x.s B ) +s ( A x.s q ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( ( p x.s B ) +s ( A x.s q ) ) e. No ) with typecode |-
44	32 35 41	mulsproplem4	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( p x.s q ) e. No ) : No typesetting found for |- ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( p x.s q ) e. No ) with typecode |-
45	43 44	subscld	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) e. No ) with typecode |-
46		eleq1	Could not format ( g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( g e. No <-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) e. No ) ) : No typesetting found for |- ( g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( g e. No <-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) e. No ) ) with typecode |-
47	45 46	syl5ibrcom	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> g e. No ) ) : No typesetting found for |- ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> g e. No ) ) with typecode |-
48	47	rexlimdvva	Could not format ( ph -> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> g e. No ) ) : No typesetting found for |- ( ph -> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> g e. No ) ) with typecode |-
49	48	abssdv	Could not format ( ph -> { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } C_ No ) : No typesetting found for |- ( ph -> { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } C_ No ) with typecode |-
50	1	adantr	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
51		rightssold	Could not format ( _Right ` A ) C_ ( _Old ` ( bday ` A ) ) : No typesetting found for |- ( _Right ` A ) C_ ( _Old ` ( bday ` A ) ) with typecode |-
52		simprl	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> r e. ( _Right ` A ) ) : No typesetting found for |- ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> r e. ( _Right ` A ) ) with typecode |-
53	51 52	sselid	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> r e. ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> r e. ( _Old ` ( bday ` A ) ) ) with typecode |-
54	3	adantr	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> B e. No ) : No typesetting found for |- ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> B e. No ) with typecode |-
55	50 53 54	mulsproplem2	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( r x.s B ) e. No ) : No typesetting found for |- ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( r x.s B ) e. No ) with typecode |-
56	2	adantr	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> A e. No ) : No typesetting found for |- ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> A e. No ) with typecode |-
57		rightssold	Could not format ( _Right ` B ) C_ ( _Old ` ( bday ` B ) ) : No typesetting found for |- ( _Right ` B ) C_ ( _Old ` ( bday ` B ) ) with typecode |-
58		simprr	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> s e. ( _Right ` B ) ) : No typesetting found for |- ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> s e. ( _Right ` B ) ) with typecode |-
59	57 58	sselid	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> s e. ( _Old ` ( bday ` B ) ) ) : No typesetting found for |- ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> s e. ( _Old ` ( bday ` B ) ) ) with typecode |-
60	50 56 59	mulsproplem3	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( A x.s s ) e. No ) : No typesetting found for |- ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( A x.s s ) e. No ) with typecode |-
61	55 60	addscld	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( ( r x.s B ) +s ( A x.s s ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( ( r x.s B ) +s ( A x.s s ) ) e. No ) with typecode |-
62	50 53 59	mulsproplem4	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( r x.s s ) e. No ) : No typesetting found for |- ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( r x.s s ) e. No ) with typecode |-
63	61 62	subscld	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) e. No ) with typecode |-
64		eleq1	Could not format ( h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( h e. No <-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) e. No ) ) : No typesetting found for |- ( h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( h e. No <-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) e. No ) ) with typecode |-
65	63 64	syl5ibrcom	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> h e. No ) ) : No typesetting found for |- ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> h e. No ) ) with typecode |-
66	65	rexlimdvva	Could not format ( ph -> ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> h e. No ) ) : No typesetting found for |- ( ph -> ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> h e. No ) ) with typecode |-
67	66	abssdv	Could not format ( ph -> { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } C_ No ) : No typesetting found for |- ( ph -> { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } C_ No ) with typecode |-
68	49 67	unssd	Could not format ( ph -> ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) C_ No ) : No typesetting found for |- ( ph -> ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) C_ No ) with typecode |-
69	1	adantr	Could not format ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
70		simprl	Could not format ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> t e. ( _Left ` A ) ) : No typesetting found for |- ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> t e. ( _Left ` A ) ) with typecode |-
71	33 70	sselid	Could not format ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> t e. ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> t e. ( _Old ` ( bday ` A ) ) ) with typecode |-
72	3	adantr	Could not format ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> B e. No ) : No typesetting found for |- ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> B e. No ) with typecode |-
73	69 71 72	mulsproplem2	Could not format ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( t x.s B ) e. No ) : No typesetting found for |- ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( t x.s B ) e. No ) with typecode |-
74	2	adantr	Could not format ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> A e. No ) : No typesetting found for |- ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> A e. No ) with typecode |-
75		simprr	Could not format ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> u e. ( _Right ` B ) ) : No typesetting found for |- ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> u e. ( _Right ` B ) ) with typecode |-
76	57 75	sselid	Could not format ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> u e. ( _Old ` ( bday ` B ) ) ) : No typesetting found for |- ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> u e. ( _Old ` ( bday ` B ) ) ) with typecode |-
77	69 74 76	mulsproplem3	Could not format ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( A x.s u ) e. No ) : No typesetting found for |- ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( A x.s u ) e. No ) with typecode |-
78	73 77	addscld	Could not format ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( ( t x.s B ) +s ( A x.s u ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( ( t x.s B ) +s ( A x.s u ) ) e. No ) with typecode |-
79	69 71 76	mulsproplem4	Could not format ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( t x.s u ) e. No ) : No typesetting found for |- ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( t x.s u ) e. No ) with typecode |-
80	78 79	subscld	Could not format ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) e. No ) with typecode |-
81		eleq1	Could not format ( i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( i e. No <-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) e. No ) ) : No typesetting found for |- ( i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( i e. No <-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) e. No ) ) with typecode |-
82	80 81	syl5ibrcom	Could not format ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> i e. No ) ) : No typesetting found for |- ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> i e. No ) ) with typecode |-
83	82	rexlimdvva	Could not format ( ph -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> i e. No ) ) : No typesetting found for |- ( ph -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> i e. No ) ) with typecode |-
84	83	abssdv	Could not format ( ph -> { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } C_ No ) : No typesetting found for |- ( ph -> { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } C_ No ) with typecode |-
85	1	adantr	Could not format ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
86		simprl	Could not format ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> v e. ( _Right ` A ) ) : No typesetting found for |- ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> v e. ( _Right ` A ) ) with typecode |-
87	51 86	sselid	Could not format ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> v e. ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> v e. ( _Old ` ( bday ` A ) ) ) with typecode |-
88	3	adantr	Could not format ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> B e. No ) : No typesetting found for |- ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> B e. No ) with typecode |-
89	85 87 88	mulsproplem2	Could not format ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( v x.s B ) e. No ) : No typesetting found for |- ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( v x.s B ) e. No ) with typecode |-
90	2	adantr	Could not format ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> A e. No ) : No typesetting found for |- ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> A e. No ) with typecode |-
91		simprr	Could not format ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> w e. ( _Left ` B ) ) : No typesetting found for |- ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> w e. ( _Left ` B ) ) with typecode |-
92	39 91	sselid	Could not format ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> w e. ( _Old ` ( bday ` B ) ) ) : No typesetting found for |- ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> w e. ( _Old ` ( bday ` B ) ) ) with typecode |-
93	85 90 92	mulsproplem3	Could not format ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( A x.s w ) e. No ) : No typesetting found for |- ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( A x.s w ) e. No ) with typecode |-
94	89 93	addscld	Could not format ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( ( v x.s B ) +s ( A x.s w ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( ( v x.s B ) +s ( A x.s w ) ) e. No ) with typecode |-
95	85 87 92	mulsproplem4	Could not format ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( v x.s w ) e. No ) : No typesetting found for |- ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( v x.s w ) e. No ) with typecode |-
96	94 95	subscld	Could not format ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) e. No ) with typecode |-
97		eleq1	Could not format ( j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( j e. No <-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) e. No ) ) : No typesetting found for |- ( j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( j e. No <-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) e. No ) ) with typecode |-
98	96 97	syl5ibrcom	Could not format ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> j e. No ) ) : No typesetting found for |- ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> j e. No ) ) with typecode |-
99	98	rexlimdvva	Could not format ( ph -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> j e. No ) ) : No typesetting found for |- ( ph -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> j e. No ) ) with typecode |-
100	99	abssdv	Could not format ( ph -> { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } C_ No ) : No typesetting found for |- ( ph -> { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } C_ No ) with typecode |-
101	84 100	unssd	Could not format ( ph -> ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) C_ No ) : No typesetting found for |- ( ph -> ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) C_ No ) with typecode |-
102		elun	Could not format ( x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <-> ( x e. { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } \/ x e. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ) : No typesetting found for |- ( x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <-> ( x e. { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } \/ x e. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ) with typecode |-
103		vex	$$⊢x\in \mathrm{V}$$
104		eqeq1	Could not format ( g = x -> ( g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) <-> x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) ) : No typesetting found for |- ( g = x -> ( g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) <-> x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) ) with typecode |-
105	104	2rexbidv	Could not format ( g = x -> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) <-> E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) ) : No typesetting found for |- ( g = x -> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) <-> E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) ) with typecode |-
106	103 105	elab	Could not format ( x e. { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } <-> E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) : No typesetting found for |- ( x e. { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } <-> E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) with typecode |-
107		eqeq1	Could not format ( h = x -> ( h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) <-> x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) ) : No typesetting found for |- ( h = x -> ( h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) <-> x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) ) with typecode |-
108	107	2rexbidv	Could not format ( h = x -> ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) <-> E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) ) : No typesetting found for |- ( h = x -> ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) <-> E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) ) with typecode |-
109	103 108	elab	Could not format ( x e. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } <-> E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) : No typesetting found for |- ( x e. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } <-> E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) with typecode |-
110	106 109	orbi12i	Could not format ( ( x e. { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } \/ x e. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <-> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) \/ E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) ) : No typesetting found for |- ( ( x e. { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } \/ x e. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <-> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) \/ E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) ) with typecode |-
111	102 110	bitri	Could not format ( x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <-> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) \/ E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) ) : No typesetting found for |- ( x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <-> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) \/ E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) ) with typecode |-
112		elun	Could not format ( y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) <-> ( y e. { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } \/ y e. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) : No typesetting found for |- ( y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) <-> ( y e. { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } \/ y e. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) with typecode |-
113		vex	$$⊢y\in \mathrm{V}$$
114		eqeq1	Could not format ( i = y -> ( i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <-> y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) ) : No typesetting found for |- ( i = y -> ( i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <-> y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) ) with typecode |-
115	114	2rexbidv	Could not format ( i = y -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <-> E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) ) : No typesetting found for |- ( i = y -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <-> E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) ) with typecode |-
116	113 115	elab	Could not format ( y e. { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } <-> E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) : No typesetting found for |- ( y e. { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } <-> E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) with typecode |-
117		eqeq1	Could not format ( j = y -> ( j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <-> y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) : No typesetting found for |- ( j = y -> ( j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <-> y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) with typecode |-
118	117	2rexbidv	Could not format ( j = y -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) : No typesetting found for |- ( j = y -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) with typecode |-
119	113 118	elab	Could not format ( y e. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } <-> E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) : No typesetting found for |- ( y e. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } <-> E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) with typecode |-
120	116 119	orbi12i	Could not format ( ( y e. { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } \/ y e. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) <-> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) \/ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) : No typesetting found for |- ( ( y e. { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } \/ y e. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) <-> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) \/ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) with typecode |-
121	112 120	bitri	Could not format ( y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) <-> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) \/ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) : No typesetting found for |- ( y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) <-> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) \/ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) with typecode |-
122	111 121	anbi12i	Could not format ( ( x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) /\ y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) <-> ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) \/ E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) /\ ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) \/ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) ) : No typesetting found for |- ( ( x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) /\ y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) <-> ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) \/ E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) /\ ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) \/ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) ) with typecode |-
123		anddi	Could not format ( ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) \/ E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) /\ ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) \/ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) <-> ( ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) \/ ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) ) ) : No typesetting found for |- ( ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) \/ E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) /\ ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) \/ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) <-> ( ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) \/ ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) ) ) with typecode |-
124	122 123	bitri	Could not format ( ( x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) /\ y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) <-> ( ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) \/ ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) ) ) : No typesetting found for |- ( ( x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) /\ y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) <-> ( ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) \/ ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) ) ) with typecode |-
125	1	adantr	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
126	2	adantr	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> A e. No ) : No typesetting found for |- ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> A e. No ) with typecode |-
127	3	adantr	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> B e. No ) : No typesetting found for |- ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> B e. No ) with typecode |-
128		simprll	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> p e. ( _Left ` A ) ) : No typesetting found for |- ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> p e. ( _Left ` A ) ) with typecode |-
129		simprlr	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> q e. ( _Left ` B ) ) : No typesetting found for |- ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> q e. ( _Left ` B ) ) with typecode |-
130		simprrl	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> t e. ( _Left ` A ) ) : No typesetting found for |- ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> t e. ( _Left ` A ) ) with typecode |-
131		simprrr	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> u e. ( _Right ` B ) ) : No typesetting found for |- ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> u e. ( _Right ` B ) ) with typecode |-
132	125 126 127 128 129 130 131	mulsproplem5	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
133		breq2	Could not format ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
134	132 133	syl5ibrcom	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
135	134	anassrs	Could not format ( ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
136	135	rexlimdvva	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
137		breq1	Could not format ( x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( x ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( x ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
138	137	imbi2d	Could not format ( x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
139	136 138	syl5ibrcom	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x ( x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x
140	139	rexlimdvva	Could not format ( ph -> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x
141	140	impd	Could not format ( ph -> ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) -> x ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) -> x
142	1	adantr	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
143	2	adantr	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> A e. No ) : No typesetting found for |- ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> A e. No ) with typecode |-
144	3	adantr	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> B e. No ) : No typesetting found for |- ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> B e. No ) with typecode |-
145		simprll	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> p e. ( _Left ` A ) ) : No typesetting found for |- ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> p e. ( _Left ` A ) ) with typecode |-
146		simprlr	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> q e. ( _Left ` B ) ) : No typesetting found for |- ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> q e. ( _Left ` B ) ) with typecode |-
147		simprrl	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> v e. ( _Right ` A ) ) : No typesetting found for |- ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> v e. ( _Right ` A ) ) with typecode |-
148		simprrr	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> w e. ( _Left ` B ) ) : No typesetting found for |- ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> w e. ( _Left ` B ) ) with typecode |-
149	142 143 144 145 146 147 148	mulsproplem6	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
150		breq2	Could not format ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
151	149 150	syl5ibrcom	Could not format ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
152	151	anassrs	Could not format ( ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
153	152	rexlimdvva	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
154	137	imbi2d	Could not format ( x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ( ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
155	153 154	syl5ibrcom	Could not format ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x ( x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x
156	155	rexlimdvva	Could not format ( ph -> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x
157	156	impd	Could not format ( ph -> ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) -> x ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) -> x
158	141 157	jaod	Could not format ( ph -> ( ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) -> x ( ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) -> x
159	1	adantr	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
160	2	adantr	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> A e. No ) : No typesetting found for |- ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> A e. No ) with typecode |-
161	3	adantr	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> B e. No ) : No typesetting found for |- ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> B e. No ) with typecode |-
162		simprll	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> r e. ( _Right ` A ) ) : No typesetting found for |- ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> r e. ( _Right ` A ) ) with typecode |-
163		simprlr	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> s e. ( _Right ` B ) ) : No typesetting found for |- ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> s e. ( _Right ` B ) ) with typecode |-
164		simprrl	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> t e. ( _Left ` A ) ) : No typesetting found for |- ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> t e. ( _Left ` A ) ) with typecode |-
165		simprrr	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> u e. ( _Right ` B ) ) : No typesetting found for |- ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> u e. ( _Right ` B ) ) with typecode |-
166	159 160 161 162 163 164 165	mulsproplem7	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
167		breq2	Could not format ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
168	166 167	syl5ibrcom	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
169	168	anassrs	Could not format ( ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
170	169	rexlimdvva	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
171		breq1	Could not format ( x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( x ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( x ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
172	171	imbi2d	Could not format ( x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
173	170 172	syl5ibrcom	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x ( x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x
174	173	rexlimdvva	Could not format ( ph -> ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x
175	174	impd	Could not format ( ph -> ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) -> x ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) -> x
176	1	adantr	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
177	2	adantr	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> A e. No ) : No typesetting found for |- ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> A e. No ) with typecode |-
178	3	adantr	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> B e. No ) : No typesetting found for |- ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> B e. No ) with typecode |-
179		simprll	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> r e. ( _Right ` A ) ) : No typesetting found for |- ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> r e. ( _Right ` A ) ) with typecode |-
180		simprlr	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> s e. ( _Right ` B ) ) : No typesetting found for |- ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> s e. ( _Right ` B ) ) with typecode |-
181		simprrl	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> v e. ( _Right ` A ) ) : No typesetting found for |- ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> v e. ( _Right ` A ) ) with typecode |-
182		simprrr	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> w e. ( _Left ` B ) ) : No typesetting found for |- ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> w e. ( _Left ` B ) ) with typecode |-
183	176 177 178 179 180 181 182	mulsproplem8	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
184		breq2	Could not format ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
185	183 184	syl5ibrcom	Could not format ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
186	185	anassrs	Could not format ( ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
187	186	rexlimdvva	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
188	171	imbi2d	Could not format ( x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ( ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
189	187 188	syl5ibrcom	Could not format ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x ( x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x
190	189	rexlimdvva	Could not format ( ph -> ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x
191	190	impd	Could not format ( ph -> ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) -> x ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) -> x
192	175 191	jaod	Could not format ( ph -> ( ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) -> x ( ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) -> x
193	158 192	jaod	Could not format ( ph -> ( ( ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) \/ ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) ) -> x ( ( ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) \/ ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) ) -> x
194	124 193	biimtrid	Could not format ( ph -> ( ( x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) /\ y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) -> x ( ( x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) /\ y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) -> x
195	194	3impib	Could not format ( ( ph /\ x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) /\ y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) -> x x
196	19 31 68 101 195	ssltd	Could not format ( ph -> ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <