Theorem mulsproplem12

Description: Lemma for surreal multiplication. Demonstrate the second half of the inductive statement assuming C and D are not the same age and E and F are not the same age. (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 ) )
	mulsproplem.2	$$⊢\phi \to C\in \mathrm{No}$$
	mulsproplem.3	$$⊢\phi \to D\in \mathrm{No}$$
	mulsproplem.4	$$⊢\phi \to E\in \mathrm{No}$$
	mulsproplem.5	$$⊢\phi \to F\in \mathrm{No}$$
	mulsproplem.6	$$⊢\phi \to C{<}_{s}D$$
	mulsproplem.7	$$⊢\phi \to E{<}_{s}F$$
	mulsproplem12.1	$$⊢\phi \to \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)$$
	mulsproplem12.2	$$⊢\phi \to \left(\mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)$$
Assertion	mulsproplem12	Could not format assertion : No typesetting found for |- ( ph -> ( ( C x.s F ) -s ( C x.s E ) )

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		mulsproplem.2	$$⊢\phi \to C\in \mathrm{No}$$
3		mulsproplem.3	$$⊢\phi \to D\in \mathrm{No}$$
4		mulsproplem.4	$$⊢\phi \to E\in \mathrm{No}$$
5		mulsproplem.5	$$⊢\phi \to F\in \mathrm{No}$$
6		mulsproplem.6	$$⊢\phi \to C{<}_{s}D$$
7		mulsproplem.7	$$⊢\phi \to E{<}_{s}F$$
8		mulsproplem12.1	$$⊢\phi \to \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)$$
9		mulsproplem12.2	$$⊢\phi \to \left(\mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)$$
10		unidm	Could not format ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) : No typesetting found for |- ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) with typecode |-
11		unidm	Could not format ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = ( ( bday ` 0s ) +no ( bday ` 0s ) ) : No typesetting found for |- ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = ( ( bday ` 0s ) +no ( bday ` 0s ) ) with typecode |-
12		bday0s	Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-
13	12 12	oveq12i	Could not format ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) ) : No typesetting found for |- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) ) with typecode |-
14		0elon	$$⊢\varnothing \in \mathrm{On}$$
15		naddrid	Could not format ( (/) e. On -> ( (/) +no (/) ) = (/) ) : No typesetting found for |- ( (/) e. On -> ( (/) +no (/) ) = (/) ) with typecode |-
16	14 15	ax-mp	Could not format ( (/) +no (/) ) = (/) : No typesetting found for |- ( (/) +no (/) ) = (/) with typecode |-
17	13 16	eqtri	Could not format ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/) : No typesetting found for |- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/) with typecode |-
18	11 17	eqtri	Could not format ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = (/) : No typesetting found for |- ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = (/) with typecode |-
19	10 18	eqtri	Could not format ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = (/) : No typesetting found for |- ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = (/) with typecode |-
20	19	uneq2i	Could not format ( ( ( bday ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` D ) +no ( bday ` F ) ) u. (/) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` D ) +no ( bday ` F ) ) u. (/) ) with typecode |-
21		un0	Could not format ( ( ( bday ` D ) +no ( bday ` F ) ) u. (/) ) = ( ( bday ` D ) +no ( bday ` F ) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` F ) ) u. (/) ) = ( ( bday ` D ) +no ( bday ` F ) ) with typecode |-
22	20 21	eqtri	Could not format ( ( ( bday ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` D ) +no ( bday ` F ) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` D ) +no ( bday ` F ) ) with typecode |-
23		ssun2	Could not format ( ( bday ` D ) +no ( bday ` F ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) : No typesetting found for |- ( ( bday ` D ) +no ( bday ` F ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) with typecode |-
24		ssun1	Could not format ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
25	23 24	sstri	Could not format ( ( bday ` D ) +no ( bday ` F ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( bday ` D ) +no ( bday ` F ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
26		ssun2	Could not format ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) C_ ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) C_ ( ( ( 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 ) ) ) ) ) with typecode |-
27	25 26	sstri	Could not format ( ( bday ` D ) +no ( bday ` F ) ) C_ ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( bday ` D ) +no ( bday ` F ) ) C_ ( ( ( 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 ) ) ) ) ) with typecode |-
28	22 27	eqsstri	Could not format ( ( ( bday ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ) ) ) ) ) with typecode |-
29	28	sseli	Could not format ( ( ( ( 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) : No typesetting found for |- ( ( ( ( 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) with typecode |-
30	29	imim1i	Could not format ( ( ( ( ( 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 ) ) ( ( ( ( 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s 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 ) ) ) ) ) e. ( ( ( bday ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
31	30	6ralimi	Could not format ( 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
32	1 31	syl	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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
33	32 3 5	mulsproplem10	Could not format ( ph -> ( ( D x.s F ) e. No /\ ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) < ( ( D x.s F ) e. No /\ ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) <
34	33	simp2d	Could not format ( ph -> ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) < ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) <
35	34	adantr	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) < ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) <
36		simprl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to \mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)$$
37		bdayelon	$$⊢\mathrm{bday}\left(D\right)\in \mathrm{On}$$
38	2	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to C\in \mathrm{No}$$
39		oldbday	$$⊢\left(\mathrm{bday}\left(D\right)\in \mathrm{On}\wedge C\in \mathrm{No}\right)\to \left(C\in \mathrm{Old}\left(\mathrm{bday}\left(D\right)\right)\leftrightarrow \mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\right)$$
40	37 38 39	sylancr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to \left(C\in \mathrm{Old}\left(\mathrm{bday}\left(D\right)\right)\leftrightarrow \mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\right)$$
41	36 40	mpbird	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to C\in \mathrm{Old}\left(\mathrm{bday}\left(D\right)\right)$$
42	6	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to C{<}_{s}D$$
43		breq1	$$⊢x=C\to \left(x{<}_{s}D\leftrightarrow C{<}_{s}D\right)$$
44		leftval	Could not format ( _Left ` D ) = { x e. ( _Old ` ( bday ` D ) ) | x
45	43 44	elrab2	Could not format ( C e. ( _Left ` D ) <-> ( C e. ( _Old ` ( bday ` D ) ) /\ C ( C e. ( _Old ` ( bday ` D ) ) /\ C
46	41 42 45	sylanbrc	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> C e. ( _Left ` D ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> C e. ( _Left ` D ) ) with typecode |-
47		simprr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)$$
48		bdayelon	$$⊢\mathrm{bday}\left(F\right)\in \mathrm{On}$$
49	4	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to E\in \mathrm{No}$$
50		oldbday	$$⊢\left(\mathrm{bday}\left(F\right)\in \mathrm{On}\wedge E\in \mathrm{No}\right)\to \left(E\in \mathrm{Old}\left(\mathrm{bday}\left(F\right)\right)\leftrightarrow \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)$$
51	48 49 50	sylancr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to \left(E\in \mathrm{Old}\left(\mathrm{bday}\left(F\right)\right)\leftrightarrow \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)$$
52	47 51	mpbird	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to E\in \mathrm{Old}\left(\mathrm{bday}\left(F\right)\right)$$
53	7	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to E{<}_{s}F$$
54		breq1	$$⊢x=E\to \left(x{<}_{s}F\leftrightarrow E{<}_{s}F\right)$$
55		leftval	Could not format ( _Left ` F ) = { x e. ( _Old ` ( bday ` F ) ) | x
56	54 55	elrab2	Could not format ( E e. ( _Left ` F ) <-> ( E e. ( _Old ` ( bday ` F ) ) /\ E ( E e. ( _Old ` ( bday ` F ) ) /\ E
57	52 53 56	sylanbrc	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. ( _Left ` F ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. ( _Left ` F ) ) with typecode |-
58		eqid	Could not format ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) : No typesetting found for |- ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) with typecode |-
59		oveq1	Could not format ( p = C -> ( p x.s F ) = ( C x.s F ) ) : No typesetting found for |- ( p = C -> ( p x.s F ) = ( C x.s F ) ) with typecode |-
60	59	oveq1d	Could not format ( p = C -> ( ( p x.s F ) +s ( D x.s q ) ) = ( ( C x.s F ) +s ( D x.s q ) ) ) : No typesetting found for |- ( p = C -> ( ( p x.s F ) +s ( D x.s q ) ) = ( ( C x.s F ) +s ( D x.s q ) ) ) with typecode |-
61		oveq1	Could not format ( p = C -> ( p x.s q ) = ( C x.s q ) ) : No typesetting found for |- ( p = C -> ( p x.s q ) = ( C x.s q ) ) with typecode |-
62	60 61	oveq12d	Could not format ( p = C -> ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) = ( ( ( C x.s F ) +s ( D x.s q ) ) -s ( C x.s q ) ) ) : No typesetting found for |- ( p = C -> ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) = ( ( ( C x.s F ) +s ( D x.s q ) ) -s ( C x.s q ) ) ) with typecode |-
63	62	eqeq2d	Could not format ( p = C -> ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) <-> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( C x.s F ) +s ( D x.s q ) ) -s ( C x.s q ) ) ) ) : No typesetting found for |- ( p = C -> ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) <-> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( C x.s F ) +s ( D x.s q ) ) -s ( C x.s q ) ) ) ) with typecode |-
64		oveq2	Could not format ( q = E -> ( D x.s q ) = ( D x.s E ) ) : No typesetting found for |- ( q = E -> ( D x.s q ) = ( D x.s E ) ) with typecode |-
65	64	oveq2d	Could not format ( q = E -> ( ( C x.s F ) +s ( D x.s q ) ) = ( ( C x.s F ) +s ( D x.s E ) ) ) : No typesetting found for |- ( q = E -> ( ( C x.s F ) +s ( D x.s q ) ) = ( ( C x.s F ) +s ( D x.s E ) ) ) with typecode |-
66		oveq2	Could not format ( q = E -> ( C x.s q ) = ( C x.s E ) ) : No typesetting found for |- ( q = E -> ( C x.s q ) = ( C x.s E ) ) with typecode |-
67	65 66	oveq12d	Could not format ( q = E -> ( ( ( C x.s F ) +s ( D x.s q ) ) -s ( C x.s q ) ) = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) ) : No typesetting found for |- ( q = E -> ( ( ( C x.s F ) +s ( D x.s q ) ) -s ( C x.s q ) ) = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) ) with typecode |-
68	67	eqeq2d	Could not format ( q = E -> ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( C x.s F ) +s ( D x.s q ) ) -s ( C x.s q ) ) <-> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) ) ) : No typesetting found for |- ( q = E -> ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( C x.s F ) +s ( D x.s q ) ) -s ( C x.s q ) ) <-> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) ) ) with typecode |-
69	63 68	rspc2ev	Could not format ( ( C e. ( _Left ` D ) /\ E e. ( _Left ` F ) /\ ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) ) -> E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) ) : No typesetting found for |- ( ( C e. ( _Left ` D ) /\ E e. ( _Left ` F ) /\ ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) ) -> E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) ) with typecode |-
70	58 69	mp3an3	Could not format ( ( C e. ( _Left ` D ) /\ E e. ( _Left ` F ) ) -> E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) ) : No typesetting found for |- ( ( C e. ( _Left ` D ) /\ E e. ( _Left ` F ) ) -> E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) ) with typecode |-
71	46 57 70	syl2anc	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) ) with typecode |-
72		ovex	Could not format ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. _V : No typesetting found for |- ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. _V with typecode |-
73		eqeq1	Could not format ( g = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) -> ( g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) <-> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) ) ) : No typesetting found for |- ( g = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) -> ( g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) <-> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) ) ) with typecode |-
74	73	2rexbidv	Could not format ( g = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) -> ( E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) <-> E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) ) ) : No typesetting found for |- ( g = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) -> ( E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) <-> E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) ) ) with typecode |-
75	72 74	elab	Could not format ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } <-> E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) ) : No typesetting found for |- ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } <-> E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) ) with typecode |-
76	71 75	sylibr	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } ) with typecode |-
77		elun1	Could not format ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) ) : No typesetting found for |- ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) ) with typecode |-
78	76 77	syl	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) ) with typecode |-
79		ovex	Could not format ( D x.s F ) e. _V : No typesetting found for |- ( D x.s F ) e. _V with typecode |-
80	79	snid	Could not format ( D x.s F ) e. { ( D x.s F ) } : No typesetting found for |- ( D x.s F ) e. { ( D x.s F ) } with typecode |-
81	80	a1i	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( D x.s F ) e. { ( D x.s F ) } ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( D x.s F ) e. { ( D x.s F ) } ) with typecode |-
82	35 78 81	ssltsepcd	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) )
83	19	uneq2i	Could not format ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` C ) +no ( bday ` F ) ) u. (/) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` C ) +no ( bday ` F ) ) u. (/) ) with typecode |-
84		un0	Could not format ( ( ( bday ` C ) +no ( bday ` F ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` F ) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` F ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` F ) ) with typecode |-
85	83 84	eqtri	Could not format ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` C ) +no ( bday ` F ) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` C ) +no ( bday ` F ) ) with typecode |-
86		ssun1	Could not format ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) : No typesetting found for |- ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) with typecode |-
87		ssun2	Could not format ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
88	86 87	sstri	Could not format ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
89	88 26	sstri	Could not format ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( 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 ) ) ) ) ) with typecode |-
90	85 89	eqsstri	Could not format ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ) ) ) ) ) with typecode |-
91	90	sseli	Could not format ( ( ( ( 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) : No typesetting found for |- ( ( ( ( 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) with typecode |-
92	91	imim1i	Could not format ( ( ( ( ( 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 ) ) ( ( ( ( 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s 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 ) ) ) ) ) e. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
93	92	6ralimi	Could not format ( 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
94	1 93	syl	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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
95	94 2 5	mulsproplem10	Could not format ( ph -> ( ( C x.s F ) e. No /\ ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) < ( ( C x.s F ) e. No /\ ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) <
96	95	simp1d	Could not format ( ph -> ( C x.s F ) e. No ) : No typesetting found for |- ( ph -> ( C x.s F ) e. No ) with typecode |-
97	19	uneq2i	Could not format ( ( ( bday ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` D ) +no ( bday ` E ) ) u. (/) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` D ) +no ( bday ` E ) ) u. (/) ) with typecode |-
98		un0	Could not format ( ( ( bday ` D ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` D ) +no ( bday ` E ) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` D ) +no ( bday ` E ) ) with typecode |-
99	97 98	eqtri	Could not format ( ( ( bday ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` D ) +no ( bday ` E ) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` D ) +no ( bday ` E ) ) with typecode |-
100		ssun2	Could not format ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) : No typesetting found for |- ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) with typecode |-
101	100 87	sstri	Could not format ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
102	101 26	sstri	Could not format ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( 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 ) ) ) ) ) with typecode |-
103	99 102	eqsstri	Could not format ( ( ( bday ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ) ) ) ) ) with typecode |-
104	103	sseli	Could not format ( ( ( ( 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) : No typesetting found for |- ( ( ( ( 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) with typecode |-
105	104	imim1i	Could not format ( ( ( ( ( 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 ) ) ( ( ( ( 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s 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 ) ) ) ) ) e. ( ( ( bday ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
106	105	6ralimi	Could not format ( 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
107	1 106	syl	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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
108	107 3 4	mulsproplem10	Could not format ( ph -> ( ( D x.s E ) e. No /\ ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) < ( ( D x.s E ) e. No /\ ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) <
109	108	simp1d	Could not format ( ph -> ( D x.s E ) e. No ) : No typesetting found for |- ( ph -> ( D x.s E ) e. No ) with typecode |-
110	96 109	addscomd	Could not format ( ph -> ( ( C x.s F ) +s ( D x.s E ) ) = ( ( D x.s E ) +s ( C x.s F ) ) ) : No typesetting found for |- ( ph -> ( ( C x.s F ) +s ( D x.s E ) ) = ( ( D x.s E ) +s ( C x.s F ) ) ) with typecode |-
111	110	oveq1d	Could not format ( ph -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( C x.s E ) ) ) : No typesetting found for |- ( ph -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( C x.s E ) ) ) with typecode |-
112	19	uneq2i	Could not format ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` C ) +no ( bday ` E ) ) u. (/) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` C ) +no ( bday ` E ) ) u. (/) ) with typecode |-
113		un0	Could not format ( ( ( bday ` C ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` E ) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` E ) ) with typecode |-
114	112 113	eqtri	Could not format ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` C ) +no ( bday ` E ) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` C ) +no ( bday ` E ) ) with typecode |-
115		ssun1	Could not format ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) : No typesetting found for |- ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) with typecode |-
116	115 24	sstri	Could not format ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
117	116 26	sstri	Could not format ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( 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 ) ) ) ) ) with typecode |-
118	114 117	eqsstri	Could not format ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ) ) ) ) ) with typecode |-
119	118	sseli	Could not format ( ( ( ( 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) : No typesetting found for |- ( ( ( ( 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) with typecode |-
120	119	imim1i	Could not format ( ( ( ( ( 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 ) ) ( ( ( ( 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s 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 ) ) ) ) ) e. ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
121	120	6ralimi	Could not format ( 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
122	1 121	syl	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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
123	122 2 4	mulsproplem10	Could not format ( ph -> ( ( C x.s E ) e. No /\ ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) < ( ( C x.s E ) e. No /\ ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) <
124	123	simp1d	Could not format ( ph -> ( C x.s E ) e. No ) : No typesetting found for |- ( ph -> ( C x.s E ) e. No ) with typecode |-
125	109 96 124	addsubsassd	Could not format ( ph -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( C x.s E ) ) = ( ( D x.s E ) +s ( ( C x.s F ) -s ( C x.s E ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( C x.s E ) ) = ( ( D x.s E ) +s ( ( C x.s F ) -s ( C x.s E ) ) ) ) with typecode |-
126	111 125	eqtrd	Could not format ( ph -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( D x.s E ) +s ( ( C x.s F ) -s ( C x.s E ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( D x.s E ) +s ( ( C x.s F ) -s ( C x.s E ) ) ) ) with typecode |-
127	126	breq1d	Could not format ( ph -> ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) ( ( D x.s E ) +s ( ( C x.s F ) -s ( C x.s E ) ) ) ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) ( ( D x.s E ) +s ( ( C x.s F ) -s ( C x.s E ) ) )
128	96 124	subscld	Could not format ( ph -> ( ( C x.s F ) -s ( C x.s E ) ) e. No ) : No typesetting found for |- ( ph -> ( ( C x.s F ) -s ( C x.s E ) ) e. No ) with typecode |-
129	33	simp1d	Could not format ( ph -> ( D x.s F ) e. No ) : No typesetting found for |- ( ph -> ( D x.s F ) e. No ) with typecode |-
130	109 128 129	sltaddsub2d	Could not format ( ph -> ( ( ( D x.s E ) +s ( ( C x.s F ) -s ( C x.s E ) ) ) ( ( C x.s F ) -s ( C x.s E ) ) ( ( ( D x.s E ) +s ( ( C x.s F ) -s ( C x.s E ) ) ) ( ( C x.s F ) -s ( C x.s E ) )
131	127 130	bitrd	Could not format ( ph -> ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) ) ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
132	131	adantr	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) ) ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
133	82 132	mpbid	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
134	133	anassrs	Could not format ( ( ( ph /\ ( bday ` C ) e. ( bday ` D ) ) /\ ( bday ` E ) e. ( bday ` F ) ) -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
135	108	simp3d	Could not format ( ph -> { ( D x.s E ) } < { ( D x.s E ) } <
136	135	adantr	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> { ( D x.s E ) } < { ( D x.s E ) } <
137		ovex	Could not format ( D x.s E ) e. _V : No typesetting found for |- ( D x.s E ) e. _V with typecode |-
138	137	snid	Could not format ( D x.s E ) e. { ( D x.s E ) } : No typesetting found for |- ( D x.s E ) e. { ( D x.s E ) } with typecode |-
139	138	a1i	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( D x.s E ) e. { ( D x.s E ) } ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( D x.s E ) e. { ( D x.s E ) } ) with typecode |-
140		simprl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to \mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)$$
141	2	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to C\in \mathrm{No}$$
142	37 141 39	sylancr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to \left(C\in \mathrm{Old}\left(\mathrm{bday}\left(D\right)\right)\leftrightarrow \mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\right)$$
143	140 142	mpbird	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to C\in \mathrm{Old}\left(\mathrm{bday}\left(D\right)\right)$$
144	6	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to C{<}_{s}D$$
145	143 144 45	sylanbrc	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> C e. ( _Left ` D ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> C e. ( _Left ` D ) ) with typecode |-
146		simprr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)$$
147		bdayelon	$$⊢\mathrm{bday}\left(E\right)\in \mathrm{On}$$
148	5	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to F\in \mathrm{No}$$
149		oldbday	$$⊢\left(\mathrm{bday}\left(E\right)\in \mathrm{On}\wedge F\in \mathrm{No}\right)\to \left(F\in \mathrm{Old}\left(\mathrm{bday}\left(E\right)\right)\leftrightarrow \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)$$
150	147 148 149	sylancr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to \left(F\in \mathrm{Old}\left(\mathrm{bday}\left(E\right)\right)\leftrightarrow \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)$$
151	146 150	mpbird	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to F\in \mathrm{Old}\left(\mathrm{bday}\left(E\right)\right)$$
152	7	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to E{<}_{s}F$$
153		breq2	$$⊢x=F\to \left(E{<}_{s}x\leftrightarrow E{<}_{s}F\right)$$
154		rightval	Could not format ( _Right ` E ) = { x e. ( _Old ` ( bday ` E ) ) | E
155	153 154	elrab2	Could not format ( F e. ( _Right ` E ) <-> ( F e. ( _Old ` ( bday ` E ) ) /\ E ( F e. ( _Old ` ( bday ` E ) ) /\ E
156	151 152 155	sylanbrc	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. ( _Right ` E ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. ( _Right ` E ) ) with typecode |-
157		eqid	Could not format ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) : No typesetting found for |- ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) with typecode |-
158		oveq1	Could not format ( t = C -> ( t x.s E ) = ( C x.s E ) ) : No typesetting found for |- ( t = C -> ( t x.s E ) = ( C x.s E ) ) with typecode |-
159	158	oveq1d	Could not format ( t = C -> ( ( t x.s E ) +s ( D x.s u ) ) = ( ( C x.s E ) +s ( D x.s u ) ) ) : No typesetting found for |- ( t = C -> ( ( t x.s E ) +s ( D x.s u ) ) = ( ( C x.s E ) +s ( D x.s u ) ) ) with typecode |-
160		oveq1	Could not format ( t = C -> ( t x.s u ) = ( C x.s u ) ) : No typesetting found for |- ( t = C -> ( t x.s u ) = ( C x.s u ) ) with typecode |-
161	159 160	oveq12d	Could not format ( t = C -> ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) = ( ( ( C x.s E ) +s ( D x.s u ) ) -s ( C x.s u ) ) ) : No typesetting found for |- ( t = C -> ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) = ( ( ( C x.s E ) +s ( D x.s u ) ) -s ( C x.s u ) ) ) with typecode |-
162	161	eqeq2d	Could not format ( t = C -> ( ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) <-> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( C x.s E ) +s ( D x.s u ) ) -s ( C x.s u ) ) ) ) : No typesetting found for |- ( t = C -> ( ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) <-> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( C x.s E ) +s ( D x.s u ) ) -s ( C x.s u ) ) ) ) with typecode |-
163		oveq2	Could not format ( u = F -> ( D x.s u ) = ( D x.s F ) ) : No typesetting found for |- ( u = F -> ( D x.s u ) = ( D x.s F ) ) with typecode |-
164	163	oveq2d	Could not format ( u = F -> ( ( C x.s E ) +s ( D x.s u ) ) = ( ( C x.s E ) +s ( D x.s F ) ) ) : No typesetting found for |- ( u = F -> ( ( C x.s E ) +s ( D x.s u ) ) = ( ( C x.s E ) +s ( D x.s F ) ) ) with typecode |-
165		oveq2	Could not format ( u = F -> ( C x.s u ) = ( C x.s F ) ) : No typesetting found for |- ( u = F -> ( C x.s u ) = ( C x.s F ) ) with typecode |-
166	164 165	oveq12d	Could not format ( u = F -> ( ( ( C x.s E ) +s ( D x.s u ) ) -s ( C x.s u ) ) = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) ) : No typesetting found for |- ( u = F -> ( ( ( C x.s E ) +s ( D x.s u ) ) -s ( C x.s u ) ) = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) ) with typecode |-
167	166	eqeq2d	Could not format ( u = F -> ( ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( C x.s E ) +s ( D x.s u ) ) -s ( C x.s u ) ) <-> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) ) ) : No typesetting found for |- ( u = F -> ( ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( C x.s E ) +s ( D x.s u ) ) -s ( C x.s u ) ) <-> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) ) ) with typecode |-
168	162 167	rspc2ev	Could not format ( ( C e. ( _Left ` D ) /\ F e. ( _Right ` E ) /\ ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) ) -> E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) ) : No typesetting found for |- ( ( C e. ( _Left ` D ) /\ F e. ( _Right ` E ) /\ ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) ) -> E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) ) with typecode |-
169	157 168	mp3an3	Could not format ( ( C e. ( _Left ` D ) /\ F e. ( _Right ` E ) ) -> E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) ) : No typesetting found for |- ( ( C e. ( _Left ` D ) /\ F e. ( _Right ` E ) ) -> E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) ) with typecode |-
170	145 156 169	syl2anc	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) ) with typecode |-
171		ovex	Could not format ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. _V : No typesetting found for |- ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. _V with typecode |-
172		eqeq1	Could not format ( i = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) -> ( i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) <-> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) ) ) : No typesetting found for |- ( i = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) -> ( i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) <-> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) ) ) with typecode |-
173	172	2rexbidv	Could not format ( i = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) -> ( E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) <-> E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) ) ) : No typesetting found for |- ( i = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) -> ( E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) <-> E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) ) ) with typecode |-
174	171 173	elab	Could not format ( ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. { i | E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) } <-> E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) ) : No typesetting found for |- ( ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. { i | E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) } <-> E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) ) with typecode |-
175	170 174	sylibr	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. { i | E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) } ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. { i | E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) } ) with typecode |-
176		elun1	Could not format ( ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. { i | E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) } -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. ( { i | E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` D ) E. w e. ( _Left ` E ) j = ( ( ( v x.s E ) +s ( D x.s w ) ) -s ( v x.s w ) ) } ) ) : No typesetting found for |- ( ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. { i | E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) } -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. ( { i | E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` D ) E. w e. ( _Left ` E ) j = ( ( ( v x.s E ) +s ( D x.s w ) ) -s ( v x.s w ) ) } ) ) with typecode |-
177	175 176	syl	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. ( { i | E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` D ) E. w e. ( _Left ` E ) j = ( ( ( v x.s E ) +s ( D x.s w ) ) -s ( v x.s w ) ) } ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. ( { i | E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` D ) E. w e. ( _Left ` E ) j = ( ( ( v x.s E ) +s ( D x.s w ) ) -s ( v x.s w ) ) } ) ) with typecode |-
178	136 139 177	ssltsepcd	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( D x.s E ) ( D x.s E )
179	124 129	addscomd	Could not format ( ph -> ( ( C x.s E ) +s ( D x.s F ) ) = ( ( D x.s F ) +s ( C x.s E ) ) ) : No typesetting found for |- ( ph -> ( ( C x.s E ) +s ( D x.s F ) ) = ( ( D x.s F ) +s ( C x.s E ) ) ) with typecode |-
180	179	oveq1d	Could not format ( ph -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( C x.s F ) ) ) : No typesetting found for |- ( ph -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( C x.s F ) ) ) with typecode |-
181	129 124 96	addsubsassd	Could not format ( ph -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( C x.s F ) ) = ( ( D x.s F ) +s ( ( C x.s E ) -s ( C x.s F ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( C x.s F ) ) = ( ( D x.s F ) +s ( ( C x.s E ) -s ( C x.s F ) ) ) ) with typecode |-
182	180 181	eqtrd	Could not format ( ph -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( D x.s F ) +s ( ( C x.s E ) -s ( C x.s F ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( D x.s F ) +s ( ( C x.s E ) -s ( C x.s F ) ) ) ) with typecode |-
183	182	breq2d	Could not format ( ph -> ( ( D x.s E ) ( D x.s E ) ( ( D x.s E ) ( D x.s E )
184	124 96	subscld	Could not format ( ph -> ( ( C x.s E ) -s ( C x.s F ) ) e. No ) : No typesetting found for |- ( ph -> ( ( C x.s E ) -s ( C x.s F ) ) e. No ) with typecode |-
185	109 129 184	sltsubadd2d	Could not format ( ph -> ( ( ( D x.s E ) -s ( D x.s F ) ) ( D x.s E ) ( ( ( D x.s E ) -s ( D x.s F ) ) ( D x.s E )
186	183 185	bitr4d	Could not format ( ph -> ( ( D x.s E ) ( ( D x.s E ) -s ( D x.s F ) ) ( ( D x.s E ) ( ( D x.s E ) -s ( D x.s F ) )
187	109 129 124 96	sltsubsub2bd	Could not format ( ph -> ( ( ( D x.s E ) -s ( D x.s F ) ) ( ( C x.s F ) -s ( C x.s E ) ) ( ( ( D x.s E ) -s ( D x.s F ) ) ( ( C x.s F ) -s ( C x.s E ) )
188	186 187	bitrd	Could not format ( ph -> ( ( D x.s E ) ( ( C x.s F ) -s ( C x.s E ) ) ( ( D x.s E ) ( ( C x.s F ) -s ( C x.s E ) )
189	188	adantr	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( D x.s E ) ( ( C x.s F ) -s ( C x.s E ) ) ( ( D x.s E ) ( ( C x.s F ) -s ( C x.s E ) )
190	178 189	mpbid	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
191	190	anassrs	Could not format ( ( ( ph /\ ( bday ` C ) e. ( bday ` D ) ) /\ ( bday ` F ) e. ( bday ` E ) ) -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
192	9	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\right)\to \left(\mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)$$
193	134 191 192	mpjaodan	Could not format ( ( ph /\ ( bday ` C ) e. ( bday ` D ) ) -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
194	95	simp3d	Could not format ( ph -> { ( C x.s F ) } < { ( C x.s F ) } <
195	194	adantr	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> { ( C x.s F ) } < { ( C x.s F ) } <
196		ovex	Could not format ( C x.s F ) e. _V : No typesetting found for |- ( C x.s F ) e. _V with typecode |-
197	196	snid	Could not format ( C x.s F ) e. { ( C x.s F ) } : No typesetting found for |- ( C x.s F ) e. { ( C x.s F ) } with typecode |-
198	197	a1i	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( C x.s F ) e. { ( C x.s F ) } ) : No typesetting found for |- ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( C x.s F ) e. { ( C x.s F ) } ) with typecode |-
199		simprl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)$$
200		bdayelon	$$⊢\mathrm{bday}\left(C\right)\in \mathrm{On}$$
201	3	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to D\in \mathrm{No}$$
202		oldbday	$$⊢\left(\mathrm{bday}\left(C\right)\in \mathrm{On}\wedge D\in \mathrm{No}\right)\to \left(D\in \mathrm{Old}\left(\mathrm{bday}\left(C\right)\right)\leftrightarrow \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)$$
203	200 201 202	sylancr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to \left(D\in \mathrm{Old}\left(\mathrm{bday}\left(C\right)\right)\leftrightarrow \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)$$
204	199 203	mpbird	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to D\in \mathrm{Old}\left(\mathrm{bday}\left(C\right)\right)$$
205	6	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to C{<}_{s}D$$
206		breq2	$$⊢x=D\to \left(C{<}_{s}x\leftrightarrow C{<}_{s}D\right)$$
207		rightval	Could not format ( _Right ` C ) = { x e. ( _Old ` ( bday ` C ) ) | C
208	206 207	elrab2	Could not format ( D e. ( _Right ` C ) <-> ( D e. ( _Old ` ( bday ` C ) ) /\ C ( D e. ( _Old ` ( bday ` C ) ) /\ C
209	204 205 208	sylanbrc	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> D e. ( _Right ` C ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> D e. ( _Right ` C ) ) with typecode |-
210		simprr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)$$
211	4	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to E\in \mathrm{No}$$
212	48 211 50	sylancr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to \left(E\in \mathrm{Old}\left(\mathrm{bday}\left(F\right)\right)\leftrightarrow \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)$$
213	210 212	mpbird	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to E\in \mathrm{Old}\left(\mathrm{bday}\left(F\right)\right)$$
214	7	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\right)\right)\to E{<}_{s}F$$
215	213 214 56	sylanbrc	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. ( _Left ` F ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. ( _Left ` F ) ) with typecode |-
216		eqid	Could not format ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) : No typesetting found for |- ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) with typecode |-
217		oveq1	Could not format ( v = D -> ( v x.s F ) = ( D x.s F ) ) : No typesetting found for |- ( v = D -> ( v x.s F ) = ( D x.s F ) ) with typecode |-
218	217	oveq1d	Could not format ( v = D -> ( ( v x.s F ) +s ( C x.s w ) ) = ( ( D x.s F ) +s ( C x.s w ) ) ) : No typesetting found for |- ( v = D -> ( ( v x.s F ) +s ( C x.s w ) ) = ( ( D x.s F ) +s ( C x.s w ) ) ) with typecode |-
219		oveq1	Could not format ( v = D -> ( v x.s w ) = ( D x.s w ) ) : No typesetting found for |- ( v = D -> ( v x.s w ) = ( D x.s w ) ) with typecode |-
220	218 219	oveq12d	Could not format ( v = D -> ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) = ( ( ( D x.s F ) +s ( C x.s w ) ) -s ( D x.s w ) ) ) : No typesetting found for |- ( v = D -> ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) = ( ( ( D x.s F ) +s ( C x.s w ) ) -s ( D x.s w ) ) ) with typecode |-
221	220	eqeq2d	Could not format ( v = D -> ( ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) <-> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( D x.s F ) +s ( C x.s w ) ) -s ( D x.s w ) ) ) ) : No typesetting found for |- ( v = D -> ( ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) <-> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( D x.s F ) +s ( C x.s w ) ) -s ( D x.s w ) ) ) ) with typecode |-
222		oveq2	Could not format ( w = E -> ( C x.s w ) = ( C x.s E ) ) : No typesetting found for |- ( w = E -> ( C x.s w ) = ( C x.s E ) ) with typecode |-
223	222	oveq2d	Could not format ( w = E -> ( ( D x.s F ) +s ( C x.s w ) ) = ( ( D x.s F ) +s ( C x.s E ) ) ) : No typesetting found for |- ( w = E -> ( ( D x.s F ) +s ( C x.s w ) ) = ( ( D x.s F ) +s ( C x.s E ) ) ) with typecode |-
224		oveq2	Could not format ( w = E -> ( D x.s w ) = ( D x.s E ) ) : No typesetting found for |- ( w = E -> ( D x.s w ) = ( D x.s E ) ) with typecode |-
225	223 224	oveq12d	Could not format ( w = E -> ( ( ( D x.s F ) +s ( C x.s w ) ) -s ( D x.s w ) ) = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) ) : No typesetting found for |- ( w = E -> ( ( ( D x.s F ) +s ( C x.s w ) ) -s ( D x.s w ) ) = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) ) with typecode |-
226	225	eqeq2d	Could not format ( w = E -> ( ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( D x.s F ) +s ( C x.s w ) ) -s ( D x.s w ) ) <-> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) ) ) : No typesetting found for |- ( w = E -> ( ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( D x.s F ) +s ( C x.s w ) ) -s ( D x.s w ) ) <-> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) ) ) with typecode |-
227	221 226	rspc2ev	Could not format ( ( D e. ( _Right ` C ) /\ E e. ( _Left ` F ) /\ ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) ) -> E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) ) : No typesetting found for |- ( ( D e. ( _Right ` C ) /\ E e. ( _Left ` F ) /\ ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) ) -> E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) ) with typecode |-
228	216 227	mp3an3	Could not format ( ( D e. ( _Right ` C ) /\ E e. ( _Left ` F ) ) -> E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) ) : No typesetting found for |- ( ( D e. ( _Right ` C ) /\ E e. ( _Left ` F ) ) -> E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) ) with typecode |-
229	209 215 228	syl2anc	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) ) with typecode |-
230		ovex	Could not format ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. _V : No typesetting found for |- ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. _V with typecode |-
231		eqeq1	Could not format ( j = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) -> ( j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) <-> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) ) ) : No typesetting found for |- ( j = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) -> ( j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) <-> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) ) ) with typecode |-
232	231	2rexbidv	Could not format ( j = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) -> ( E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) ) ) : No typesetting found for |- ( j = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) -> ( E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) ) ) with typecode |-
233	230 232	elab	Could not format ( ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. { j | E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) } <-> E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) ) : No typesetting found for |- ( ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. { j | E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) } <-> E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) ) with typecode |-
234	229 233	sylibr	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. { j | E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) } ) : No typesetting found for |- ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. { j | E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) } ) with typecode |-
235		elun2	Could not format ( ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. { j | E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) } -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. ( { i | E. t e. ( _Left ` C ) E. u e. ( _Right ` F ) i = ( ( ( t x.s F ) +s ( C x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) } ) ) : No typesetting found for |- ( ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. { j | E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) } -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. ( { i | E. t e. ( _Left ` C ) E. u e. ( _Right ` F ) i = ( ( ( t x.s F ) +s ( C x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) } ) ) with typecode |-
236	234 235	syl	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. ( { i | E. t e. ( _Left ` C ) E. u e. ( _Right ` F ) i = ( ( ( t x.s F ) +s ( C x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) } ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. ( { i | E. t e. ( _Left ` C ) E. u e. ( _Right ` F ) i = ( ( ( t x.s F ) +s ( C x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) } ) ) with typecode |-
237	195 198 236	ssltsepcd	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( C x.s F ) ( C x.s F )
238	129 124	addscomd	Could not format ( ph -> ( ( D x.s F ) +s ( C x.s E ) ) = ( ( C x.s E ) +s ( D x.s F ) ) ) : No typesetting found for |- ( ph -> ( ( D x.s F ) +s ( C x.s E ) ) = ( ( C x.s E ) +s ( D x.s F ) ) ) with typecode |-
239	238	oveq1d	Could not format ( ph -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( D x.s E ) ) ) : No typesetting found for |- ( ph -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( D x.s E ) ) ) with typecode |-
240	124 129 109	addsubsassd	Could not format ( ph -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( D x.s E ) ) = ( ( C x.s E ) +s ( ( D x.s F ) -s ( D x.s E ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( D x.s E ) ) = ( ( C x.s E ) +s ( ( D x.s F ) -s ( D x.s E ) ) ) ) with typecode |-
241	239 240	eqtrd	Could not format ( ph -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( C x.s E ) +s ( ( D x.s F ) -s ( D x.s E ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( C x.s E ) +s ( ( D x.s F ) -s ( D x.s E ) ) ) ) with typecode |-
242	241	breq2d	Could not format ( ph -> ( ( C x.s F ) ( C x.s F ) ( ( C x.s F ) ( C x.s F )
243	129 109	subscld	Could not format ( ph -> ( ( D x.s F ) -s ( D x.s E ) ) e. No ) : No typesetting found for |- ( ph -> ( ( D x.s F ) -s ( D x.s E ) ) e. No ) with typecode |-
244	96 124 243	sltsubadd2d	Could not format ( ph -> ( ( ( C x.s F ) -s ( C x.s E ) ) ( C x.s F ) ( ( ( C x.s F ) -s ( C x.s E ) ) ( C x.s F )
245	242 244	bitr4d	Could not format ( ph -> ( ( C x.s F ) ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) ( ( C x.s F ) -s ( C x.s E ) )
246	245	adantr	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( C x.s F ) ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) ( ( C x.s F ) -s ( C x.s E ) )
247	237 246	mpbid	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
248	247	anassrs	Could not format ( ( ( ph /\ ( bday ` D ) e. ( bday ` C ) ) /\ ( bday ` E ) e. ( bday ` F ) ) -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
249	123	simp2d	Could not format ( ph -> ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) < ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) <
250	249	adantr	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) < ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) <
251		simprl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)$$
252	3	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to D\in \mathrm{No}$$
253	200 252 202	sylancr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to \left(D\in \mathrm{Old}\left(\mathrm{bday}\left(C\right)\right)\leftrightarrow \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)$$
254	251 253	mpbird	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to D\in \mathrm{Old}\left(\mathrm{bday}\left(C\right)\right)$$
255	6	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to C{<}_{s}D$$
256	254 255 208	sylanbrc	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> D e. ( _Right ` C ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> D e. ( _Right ` C ) ) with typecode |-
257		simprr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)$$
258	5	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to F\in \mathrm{No}$$
259	147 258 149	sylancr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to \left(F\in \mathrm{Old}\left(\mathrm{bday}\left(E\right)\right)\leftrightarrow \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)$$
260	257 259	mpbird	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to F\in \mathrm{Old}\left(\mathrm{bday}\left(E\right)\right)$$
261	7	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\wedge \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\right)\to E{<}_{s}F$$
262	260 261 155	sylanbrc	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. ( _Right ` E ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. ( _Right ` E ) ) with typecode |-
263		eqid	Could not format ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) : No typesetting found for |- ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) with typecode |-
264		oveq1	Could not format ( r = D -> ( r x.s E ) = ( D x.s E ) ) : No typesetting found for |- ( r = D -> ( r x.s E ) = ( D x.s E ) ) with typecode |-
265	264	oveq1d	Could not format ( r = D -> ( ( r x.s E ) +s ( C x.s s ) ) = ( ( D x.s E ) +s ( C x.s s ) ) ) : No typesetting found for |- ( r = D -> ( ( r x.s E ) +s ( C x.s s ) ) = ( ( D x.s E ) +s ( C x.s s ) ) ) with typecode |-
266		oveq1	Could not format ( r = D -> ( r x.s s ) = ( D x.s s ) ) : No typesetting found for |- ( r = D -> ( r x.s s ) = ( D x.s s ) ) with typecode |-
267	265 266	oveq12d	Could not format ( r = D -> ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) = ( ( ( D x.s E ) +s ( C x.s s ) ) -s ( D x.s s ) ) ) : No typesetting found for |- ( r = D -> ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) = ( ( ( D x.s E ) +s ( C x.s s ) ) -s ( D x.s s ) ) ) with typecode |-
268	267	eqeq2d	Could not format ( r = D -> ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) <-> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( D x.s E ) +s ( C x.s s ) ) -s ( D x.s s ) ) ) ) : No typesetting found for |- ( r = D -> ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) <-> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( D x.s E ) +s ( C x.s s ) ) -s ( D x.s s ) ) ) ) with typecode |-
269		oveq2	Could not format ( s = F -> ( C x.s s ) = ( C x.s F ) ) : No typesetting found for |- ( s = F -> ( C x.s s ) = ( C x.s F ) ) with typecode |-
270	269	oveq2d	Could not format ( s = F -> ( ( D x.s E ) +s ( C x.s s ) ) = ( ( D x.s E ) +s ( C x.s F ) ) ) : No typesetting found for |- ( s = F -> ( ( D x.s E ) +s ( C x.s s ) ) = ( ( D x.s E ) +s ( C x.s F ) ) ) with typecode |-
271		oveq2	Could not format ( s = F -> ( D x.s s ) = ( D x.s F ) ) : No typesetting found for |- ( s = F -> ( D x.s s ) = ( D x.s F ) ) with typecode |-
272	270 271	oveq12d	Could not format ( s = F -> ( ( ( D x.s E ) +s ( C x.s s ) ) -s ( D x.s s ) ) = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ) : No typesetting found for |- ( s = F -> ( ( ( D x.s E ) +s ( C x.s s ) ) -s ( D x.s s ) ) = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ) with typecode |-
273	272	eqeq2d	Could not format ( s = F -> ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( D x.s E ) +s ( C x.s s ) ) -s ( D x.s s ) ) <-> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ) ) : No typesetting found for |- ( s = F -> ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( D x.s E ) +s ( C x.s s ) ) -s ( D x.s s ) ) <-> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ) ) with typecode |-
274	268 273	rspc2ev	Could not format ( ( D e. ( _Right ` C ) /\ F e. ( _Right ` E ) /\ ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ) -> E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) ) : No typesetting found for |- ( ( D e. ( _Right ` C ) /\ F e. ( _Right ` E ) /\ ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ) -> E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) ) with typecode |-
275	263 274	mp3an3	Could not format ( ( D e. ( _Right ` C ) /\ F e. ( _Right ` E ) ) -> E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) ) : No typesetting found for |- ( ( D e. ( _Right ` C ) /\ F e. ( _Right ` E ) ) -> E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) ) with typecode |-
276	256 262 275	syl2anc	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) ) with typecode |-
277		ovex	Could not format ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. _V : No typesetting found for |- ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. _V with typecode |-
278		eqeq1	Could not format ( h = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) -> ( h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) <-> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) ) ) : No typesetting found for |- ( h = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) -> ( h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) <-> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) ) ) with typecode |-
279	278	2rexbidv	Could not format ( h = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) -> ( E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) <-> E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) ) ) : No typesetting found for |- ( h = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) -> ( E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) <-> E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) ) ) with typecode |-
280	277 279	elab	Could not format ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } <-> E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) ) : No typesetting found for |- ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } <-> E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) ) with typecode |-
281	276 280	sylibr	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) : No typesetting found for |- ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) with typecode |-
282		elun2	Could not format ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) ) : No typesetting found for |- ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) ) with typecode |-
283	281 282	syl	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) ) with typecode |-
284		ovex	Could not format ( C x.s E ) e. _V : No typesetting found for |- ( C x.s E ) e. _V with typecode |-
285	284	snid	Could not format ( C x.s E ) e. { ( C x.s E ) } : No typesetting found for |- ( C x.s E ) e. { ( C x.s E ) } with typecode |-
286	285	a1i	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( C x.s E ) e. { ( C x.s E ) } ) : No typesetting found for |- ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( C x.s E ) e. { ( C x.s E ) } ) with typecode |-
287	250 283 286	ssltsepcd	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) )
288	109 96	addscomd	Could not format ( ph -> ( ( D x.s E ) +s ( C x.s F ) ) = ( ( C x.s F ) +s ( D x.s E ) ) ) : No typesetting found for |- ( ph -> ( ( D x.s E ) +s ( C x.s F ) ) = ( ( C x.s F ) +s ( D x.s E ) ) ) with typecode |-
289	288	oveq1d	Could not format ( ph -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( D x.s F ) ) ) : No typesetting found for |- ( ph -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( D x.s F ) ) ) with typecode |-
290	96 109 129	addsubsassd	Could not format ( ph -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( D x.s F ) ) = ( ( C x.s F ) +s ( ( D x.s E ) -s ( D x.s F ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( D x.s F ) ) = ( ( C x.s F ) +s ( ( D x.s E ) -s ( D x.s F ) ) ) ) with typecode |-
291	289 290	eqtrd	Could not format ( ph -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( C x.s F ) +s ( ( D x.s E ) -s ( D x.s F ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( C x.s F ) +s ( ( D x.s E ) -s ( D x.s F ) ) ) ) with typecode |-
292	291	breq1d	Could not format ( ph -> ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ( ( C x.s F ) +s ( ( D x.s E ) -s ( D x.s F ) ) ) ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ( ( C x.s F ) +s ( ( D x.s E ) -s ( D x.s F ) ) )
293	109 129	subscld	Could not format ( ph -> ( ( D x.s E ) -s ( D x.s F ) ) e. No ) : No typesetting found for |- ( ph -> ( ( D x.s E ) -s ( D x.s F ) ) e. No ) with typecode |-
294	96 293 124	sltaddsub2d	Could not format ( ph -> ( ( ( C x.s F ) +s ( ( D x.s E ) -s ( D x.s F ) ) ) ( ( D x.s E ) -s ( D x.s F ) ) ( ( ( C x.s F ) +s ( ( D x.s E ) -s ( D x.s F ) ) ) ( ( D x.s E ) -s ( D x.s F ) )
295	292 294	bitrd	Could not format ( ph -> ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ( ( D x.s E ) -s ( D x.s F ) ) ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ( ( D x.s E ) -s ( D x.s F ) )
296	295 187	bitrd	Could not format ( ph -> ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ( ( C x.s F ) -s ( C x.s E ) ) ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ( ( C x.s F ) -s ( C x.s E ) )
297	296	adantr	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ( ( C x.s F ) -s ( C x.s E ) ) ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ( ( C x.s F ) -s ( C x.s E ) )
298	287 297	mpbid	Could not format ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
299	298	anassrs	Could not format ( ( ( ph /\ ( bday ` D ) e. ( bday ` C ) ) /\ ( bday ` F ) e. ( bday ` E ) ) -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
300	9	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\to \left(\mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)$$
301	248 299 300	mpjaodan	Could not format ( ( ph /\ ( bday ` D ) e. ( bday ` C ) ) -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
302	193 301 8	mpjaodan	Could not format ( ph -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )