Theorem mulsproplem14

Description: Lemma for surreal multiplication. Finally, we remove the restriction on E and F from mulsproplem12 and mulsproplem13 . This completes the induction on surreal multiplication. mulsprop brings all this together technically. (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$$
Assertion	mulsproplem14	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	1	adantr	Could not format ( ( ph /\ ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` 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 ) ) 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 ) )
9	2	adantr	$$⊢\left(\phi \wedge \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)\right)\to C\in \mathrm{No}$$
10	3	adantr	$$⊢\left(\phi \wedge \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)\right)\to D\in \mathrm{No}$$
11	4	adantr	$$⊢\left(\phi \wedge \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)\right)\to E\in \mathrm{No}$$
12	5	adantr	$$⊢\left(\phi \wedge \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)\right)\to F\in \mathrm{No}$$
13	6	adantr	$$⊢\left(\phi \wedge \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)\right)\to C{<}_{s}D$$
14	7	adantr	$$⊢\left(\phi \wedge \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)\right)\to E{<}_{s}F$$
15		simpr	$$⊢\left(\phi \wedge \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)\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)$$
16	8 9 10 11 12 13 14 15	mulsproplem13	Could not format ( ( ph /\ ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
17	4	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\right)\to E\in \mathrm{No}$$
18	5	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\right)\to F\in \mathrm{No}$$
19		simpr	$$⊢\left(\phi \wedge \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\right)\to \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)$$
20	7	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\right)\to E{<}_{s}F$$
21		nodense	$$⊢\left(\left(E\in \mathrm{No}\wedge F\in \mathrm{No}\right)\wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge E{<}_{s}F\right)\right)\to \exists x\in \mathrm{No}\left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)$$
22	17 18 19 20 21	syl22anc	$$⊢\left(\phi \wedge \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\right)\to \exists x\in \mathrm{No}\left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)$$
23		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 |-
24		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 |-
25		bday0s	Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-
26	25 25	oveq12i	Could not format ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) ) : No typesetting found for |- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) ) with typecode |-
27		0elon	$$⊢\varnothing \in \mathrm{On}$$
28		naddrid	Could not format ( (/) e. On -> ( (/) +no (/) ) = (/) ) : No typesetting found for |- ( (/) e. On -> ( (/) +no (/) ) = (/) ) with typecode |-
29	27 28	ax-mp	Could not format ( (/) +no (/) ) = (/) : No typesetting found for |- ( (/) +no (/) ) = (/) with typecode |-
30	26 29	eqtri	Could not format ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/) : No typesetting found for |- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/) with typecode |-
31	23 24 30	3eqtri	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 |-
32	31	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 |-
33		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 |-
34	32 33	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 |-
35		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 |-
36		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 |-
37	35 36	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 |-
38		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 |-
39	37 38	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 |-
40	34 39	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 |-
41	40	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 |-
42	41	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 ) )
43	42	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 ) )
44	1 43	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 ) )
45	44 3 4	mulsproplem11	Could not format ( ph -> ( D x.s E ) e. No ) : No typesetting found for |- ( ph -> ( D x.s E ) e. No ) with typecode |-
46	31	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 |-
47		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 |-
48	46 47	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 |-
49		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 |-
50		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 |-
51	49 50	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 |-
52	51 38	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 |-
53	48 52	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 |-
54	53	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 |-
55	54	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 ) )
56	55	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 ) )
57	1 56	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 ) )
58	57 2 4	mulsproplem11	Could not format ( ph -> ( C x.s E ) e. No ) : No typesetting found for |- ( ph -> ( C x.s E ) e. No ) with typecode |-
59	45 58	subscld	Could not format ( ph -> ( ( D x.s E ) -s ( C x.s E ) ) e. No ) : No typesetting found for |- ( ph -> ( ( D x.s E ) -s ( C x.s E ) ) e. No ) with typecode |-
60	59	adantr	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( D x.s E ) -s ( C x.s E ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( D x.s E ) -s ( C x.s E ) ) e. No ) with typecode |-
61	44	adantr	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ 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. 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 ) )
62	3	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to D\in \mathrm{No}$$
63		simprr1	$$⊢\left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\to \mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)$$
64	63	adantl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to \mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)$$
65		bdayelon	$$⊢\mathrm{bday}\left(E\right)\in \mathrm{On}$$
66		simprrl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to x\in \mathrm{No}$$
67		oldbday	$$⊢\left(\mathrm{bday}\left(E\right)\in \mathrm{On}\wedge x\in \mathrm{No}\right)\to \left(x\in \mathrm{Old}\left(\mathrm{bday}\left(E\right)\right)\leftrightarrow \mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\right)$$
68	65 66 67	sylancr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to \left(x\in \mathrm{Old}\left(\mathrm{bday}\left(E\right)\right)\leftrightarrow \mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\right)$$
69	64 68	mpbird	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to x\in \mathrm{Old}\left(\mathrm{bday}\left(E\right)\right)$$
70	61 62 69	mulsproplem3	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( D x.s x ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( D x.s x ) e. No ) with typecode |-
71	57	adantr	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ 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. 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 ) )
72	2	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to C\in \mathrm{No}$$
73	71 72 69	mulsproplem3	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( C x.s x ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( C x.s x ) e. No ) with typecode |-
74	70 73	subscld	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( D x.s x ) -s ( C x.s x ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( D x.s x ) -s ( C x.s x ) ) e. No ) with typecode |-
75	31	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 |-
76		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 |-
77	75 76	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 |-
78		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 |-
79	78 50	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 |-
80	79 38	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 |-
81	77 80	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 |-
82	81	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 |-
83	82	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 ) )
84	83	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 ) )
85	1 84	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 ) )
86	85 3 5	mulsproplem11	Could not format ( ph -> ( D x.s F ) e. No ) : No typesetting found for |- ( ph -> ( D x.s F ) e. No ) with typecode |-
87	31	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 |-
88		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 |-
89	87 88	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 |-
90		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 |-
91	90 36	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 |-
92	91 38	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 |-
93	89 92	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 |-
94	93	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 |-
95	94	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 ) )
96	95	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 ) )
97	1 96	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 ) )
98	97 2 5	mulsproplem11	Could not format ( ph -> ( C x.s F ) e. No ) : No typesetting found for |- ( ph -> ( C x.s F ) e. No ) with typecode |-
99	86 98	subscld	Could not format ( ph -> ( ( D x.s F ) -s ( C x.s F ) ) e. No ) : No typesetting found for |- ( ph -> ( ( D x.s F ) -s ( C x.s F ) ) e. No ) with typecode |-
100	99	adantr	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( D x.s F ) -s ( C x.s F ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( D x.s F ) -s ( C x.s F ) ) e. No ) with typecode |-
101	1	mulsproplemcbv	Could not format ( ph -> A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
102	101	adantr	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
103		onelss	$$⊢\mathrm{bday}\left(E\right)\in \mathrm{On}\to \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\to \mathrm{bday}\left(x\right)\subseteq \mathrm{bday}\left(E\right)\right)$$
104	65 64 103	mpsyl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to \mathrm{bday}\left(x\right)\subseteq \mathrm{bday}\left(E\right)$$
105		simprl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)$$
106	104 105	sseqtrd	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to \mathrm{bday}\left(x\right)\subseteq \mathrm{bday}\left(F\right)$$
107		bdayelon	$$⊢\mathrm{bday}\left(x\right)\in \mathrm{On}$$
108		bdayelon	$$⊢\mathrm{bday}\left(F\right)\in \mathrm{On}$$
109		bdayelon	$$⊢\mathrm{bday}\left(D\right)\in \mathrm{On}$$
110		naddss2	Could not format ( ( ( bday ` x ) e. On /\ ( bday ` F ) e. On /\ ( bday ` D ) e. On ) -> ( ( bday ` x ) C_ ( bday ` F ) <-> ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) ) ) : No typesetting found for |- ( ( ( bday ` x ) e. On /\ ( bday ` F ) e. On /\ ( bday ` D ) e. On ) -> ( ( bday ` x ) C_ ( bday ` F ) <-> ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) ) ) with typecode |-
111	107 108 109 110	mp3an	Could not format ( ( bday ` x ) C_ ( bday ` F ) <-> ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) ) : No typesetting found for |- ( ( bday ` x ) C_ ( bday ` F ) <-> ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) ) with typecode |-
112	106 111	sylib	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) ) with typecode |-
113		unss2	Could not format ( ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) -> ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) -> ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) with typecode |-
114	112 113	syl	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) with typecode |-
115		bdayelon	$$⊢\mathrm{bday}\left(C\right)\in \mathrm{On}$$
116		naddss2	Could not format ( ( ( bday ` x ) e. On /\ ( bday ` F ) e. On /\ ( bday ` C ) e. On ) -> ( ( bday ` x ) C_ ( bday ` F ) <-> ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) ) ) : No typesetting found for |- ( ( ( bday ` x ) e. On /\ ( bday ` F ) e. On /\ ( bday ` C ) e. On ) -> ( ( bday ` x ) C_ ( bday ` F ) <-> ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) ) ) with typecode |-
117	107 108 115 116	mp3an	Could not format ( ( bday ` x ) C_ ( bday ` F ) <-> ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) ) : No typesetting found for |- ( ( bday ` x ) C_ ( bday ` F ) <-> ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) ) with typecode |-
118	106 117	sylib	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) ) with typecode |-
119		unss1	Could not format ( ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) -> ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) -> ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
120	118 119	syl	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
121		unss12	Could not format ( ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) /\ ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) 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 ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) /\ ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) 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 |-
122	114 120 121	syl2anc	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) 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 |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) 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 |-
123		unss2	Could not format ( ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) 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 ) ) ) ) -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) 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 ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) 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 ) ) ) ) -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) 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 |-
124	122 123	syl	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) 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 |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) 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 |-
125	124	sseld	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 |-
126	125	imim1d	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
127	126	ralimd6v	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
128	102 127	mpd	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) u. ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
129	4	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to E\in \mathrm{No}$$
130	6	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to C{<}_{s}D$$
131		simprr2	$$⊢\left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\to E{<}_{s}x$$
132	131	adantl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to E{<}_{s}x$$
133	64	olcd	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to \left(\mathrm{bday}\left(E\right)\in \mathrm{bday}\left(x\right)\vee \mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\right)$$
134	128 72 62 129 66 130 132 133	mulsproplem13	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( C x.s x ) -s ( C x.s E ) ) ( ( C x.s x ) -s ( C x.s E ) )
135	45	adantr	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( D x.s E ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( D x.s E ) e. No ) with typecode |-
136	58	adantr	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( C x.s E ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( C x.s E ) e. No ) with typecode |-
137	135 70 136 73	sltsubsub3bd	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( D x.s E ) -s ( C x.s E ) ) ( ( C x.s x ) -s ( C x.s E ) ) ( ( ( D x.s E ) -s ( C x.s E ) ) ( ( C x.s x ) -s ( C x.s E ) )
138	134 137	mpbird	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( D x.s E ) -s ( C x.s E ) ) ( ( D x.s E ) -s ( C x.s E ) )
139		naddss2	Could not format ( ( ( bday ` x ) e. On /\ ( bday ` E ) e. On /\ ( bday ` C ) e. On ) -> ( ( bday ` x ) C_ ( bday ` E ) <-> ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( ( bday ` x ) e. On /\ ( bday ` E ) e. On /\ ( bday ` C ) e. On ) -> ( ( bday ` x ) C_ ( bday ` E ) <-> ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) ) ) with typecode |-
140	107 65 115 139	mp3an	Could not format ( ( bday ` x ) C_ ( bday ` E ) <-> ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) ) : No typesetting found for |- ( ( bday ` x ) C_ ( bday ` E ) <-> ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) ) with typecode |-
141	104 140	sylib	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) ) with typecode |-
142		unss1	Could not format ( ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) -> ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) -> ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) with typecode |-
143	141 142	syl	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) with typecode |-
144		naddss2	Could not format ( ( ( bday ` x ) e. On /\ ( bday ` E ) e. On /\ ( bday ` D ) e. On ) -> ( ( bday ` x ) C_ ( bday ` E ) <-> ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( ( bday ` x ) e. On /\ ( bday ` E ) e. On /\ ( bday ` D ) e. On ) -> ( ( bday ` x ) C_ ( bday ` E ) <-> ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
145	107 65 109 144	mp3an	Could not format ( ( bday ` x ) C_ ( bday ` E ) <-> ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) ) : No typesetting found for |- ( ( bday ` x ) C_ ( bday ` E ) <-> ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) ) with typecode |-
146	104 145	sylib	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) ) with typecode |-
147		unss2	Could not format ( ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) -> ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) -> ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
148	146 147	syl	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
149		unss12	Could not format ( ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) /\ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) 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 ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) /\ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) 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 |-
150	143 148 149	syl2anc	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) 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 |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) 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 |-
151		unss2	Could not format ( ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) ) 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 ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) ) 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 |-
152	150 151	syl	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) ) 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 |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) ) 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 |-
153	152	sseld	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) ) -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) ) -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 |-
154	153	imim1d	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
155	154	ralimd6v	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
156	102 155	mpd	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` x ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` x ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
157	5	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to F\in \mathrm{No}$$
158		simprr3	$$⊢\left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\to x{<}_{s}F$$
159	158	adantl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to x{<}_{s}F$$
160	64 105	eleqtrd	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to \mathrm{bday}\left(x\right)\in \mathrm{bday}\left(F\right)$$
161	160	orcd	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(E\right)\wedge E{<}_{s}x\wedge x{<}_{s}F\right)\right)\right)\right)\to \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(x\right)\right)$$
162	156 72 62 66 157 130 159 161	mulsproplem13	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( C x.s F ) -s ( C x.s x ) ) ( ( C x.s F ) -s ( C x.s x ) )
163	86	adantr	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( D x.s F ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( D x.s F ) e. No ) with typecode |-
164	98	adantr	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( C x.s F ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( C x.s F ) e. No ) with typecode |-
165	70 163 73 164	sltsubsub3bd	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( D x.s x ) -s ( C x.s x ) ) ( ( C x.s F ) -s ( C x.s x ) ) ( ( ( D x.s x ) -s ( C x.s x ) ) ( ( C x.s F ) -s ( C x.s x ) )
166	162 165	mpbird	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( D x.s x ) -s ( C x.s x ) ) ( ( D x.s x ) -s ( C x.s x ) )
167	60 74 100 138 166	slttrd	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( D x.s E ) -s ( C x.s E ) ) ( ( D x.s E ) -s ( C x.s E ) )
168	45 86 58 98	sltsubsub3bd	Could not format ( ph -> ( ( ( D x.s E ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) ) ( ( ( D x.s E ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
169	168	adantr	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( ( D x.s E ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) ) ( ( ( D x.s E ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
170	167 169	mpbid	Could not format ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
171	170	anassrs	Could not format ( ( ( ph /\ ( bday ` E ) = ( bday ` F ) ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
172	22 171	rexlimddv	Could not format ( ( ph /\ ( bday ` E ) = ( bday ` F ) ) -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
173	65	onordi	$$⊢\mathrm{Ord}\mathrm{bday}\left(E\right)$$
174	108	onordi	$$⊢\mathrm{Ord}\mathrm{bday}\left(F\right)$$
175		ordtri3or	$$⊢\left(\mathrm{Ord}\mathrm{bday}\left(E\right)\wedge \mathrm{Ord}\mathrm{bday}\left(F\right)\right)\to \left(\mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)$$
176	173 174 175	mp2an	$$⊢\left(\mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)$$
177		df-3or	$$⊢\left(\mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\leftrightarrow \left(\left(\mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\right)\vee \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)$$
178		or32	$$⊢\left(\left(\mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\right)\vee \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\leftrightarrow \left(\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)\vee \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\right)$$
179	177 178	bitri	$$⊢\left(\mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)\leftrightarrow \left(\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)\vee \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\right)$$
180	176 179	mpbi	$$⊢\left(\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)\vee \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\right)$$
181	180	a1i	$$⊢\phi \to \left(\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)\vee \mathrm{bday}\left(E\right)=\mathrm{bday}\left(F\right)\right)$$
182	16 172 181	mpjaodan	Could not format ( ph -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )