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	|- ( 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	|- ( ph -> C e. No )
	mulsproplem.3	|- ( ph -> D e. No )
	mulsproplem.4	|- ( ph -> E e. No )
	mulsproplem.5	|- ( ph -> F e. No )
	mulsproplem.6	|- ( ph -> C
	mulsproplem.7	|- ( ph -> E
Assertion	mulsproplem14	|- ( ph -> ( ( C x.s F ) -s ( C x.s E ) )

Proof

Step	Hyp	Ref	Expression
1		mulsproplem.1	|- ( 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 ) )
2		mulsproplem.2	|- ( ph -> C e. No )
3		mulsproplem.3	|- ( ph -> D e. No )
4		mulsproplem.4	|- ( ph -> E e. No )
5		mulsproplem.5	|- ( ph -> F e. No )
6		mulsproplem.6	|- ( ph -> C
7		mulsproplem.7	|- ( ph -> E
8	1	adantr	|- ( ( 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 ) )
9	2	adantr	|- ( ( ph /\ ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) ) -> C e. No )
10	3	adantr	|- ( ( ph /\ ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) ) -> D e. No )
11	4	adantr	|- ( ( ph /\ ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) ) -> E e. No )
12	5	adantr	|- ( ( ph /\ ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. No )
13	6	adantr	|- ( ( ph /\ ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) ) -> C
14	7	adantr	|- ( ( ph /\ ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) ) -> E
15		simpr	|- ( ( ph /\ ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) )
16	8 9 10 11 12 13 14 15	mulsproplem13	|- ( ( ph /\ ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
17	4	adantr	|- ( ( ph /\ ( bday ` E ) = ( bday ` F ) ) -> E e. No )
18	5	adantr	|- ( ( ph /\ ( bday ` E ) = ( bday ` F ) ) -> F e. No )
19		simpr	|- ( ( ph /\ ( bday ` E ) = ( bday ` F ) ) -> ( bday ` E ) = ( bday ` F ) )
20	7	adantr	|- ( ( ph /\ ( bday ` E ) = ( bday ` F ) ) -> E
21		nodense	|- ( ( ( E e. No /\ F e. No ) /\ ( ( bday ` E ) = ( bday ` F ) /\ E E. x e. No ( ( bday ` x ) e. ( bday ` E ) /\ E
22	17 18 19 20 21	syl22anc	|- ( ( ph /\ ( bday ` E ) = ( bday ` F ) ) -> E. x e. No ( ( bday ` x ) e. ( bday ` E ) /\ E
23		unidm	|- ( ( ( ( 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 ) ) )
24		unidm	|- ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = ( ( bday ` 0s ) +no ( bday ` 0s ) )
25		bday0s	|- ( bday ` 0s ) = (/)
26	25 25	oveq12i	|- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) )
27		0elon	|- (/) e. On
28		naddrid	|- ( (/) e. On -> ( (/) +no (/) ) = (/) )
29	27 28	ax-mp	|- ( (/) +no (/) ) = (/)
30	26 29	eqtri	|- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/)
31	23 24 30	3eqtri	|- ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = (/)
32	31	uneq2i	|- ( ( ( 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. (/) )
33		un0	|- ( ( ( bday ` D ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` D ) +no ( bday ` E ) )
34	32 33	eqtri	|- ( ( ( 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 ) )
35		ssun2	|- ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) )
36		ssun2	|- ( ( ( 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 ) ) ) )
37	35 36	sstri	|- ( ( 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 ) ) ) )
38		ssun2	|- ( ( ( ( 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 ) ) ) ) )
39	37 38	sstri	|- ( ( 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 ) ) ) ) )
40	34 39	eqsstri	|- ( ( ( 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 ) ) ) ) )
41	40	sseli	|- ( ( ( ( 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 ) ) ) ) ) )
42	41	imim1i	|- ( ( ( ( ( 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 ) )
43	42	6ralimi	|- ( 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 ) )
44	1 43	syl	|- ( 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 ) )
45	44 3 4	mulsproplem11	|- ( ph -> ( D x.s E ) e. No )
46	31	uneq2i	|- ( ( ( 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. (/) )
47		un0	|- ( ( ( bday ` C ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` E ) )
48	46 47	eqtri	|- ( ( ( 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 ) )
49		ssun1	|- ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) )
50		ssun1	|- ( ( ( 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 ) ) ) )
51	49 50	sstri	|- ( ( 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 ) ) ) )
52	51 38	sstri	|- ( ( 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 ) ) ) ) )
53	48 52	eqsstri	|- ( ( ( 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 ) ) ) ) )
54	53	sseli	|- ( ( ( ( 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 ) ) ) ) ) )
55	54	imim1i	|- ( ( ( ( ( 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 ) )
56	55	6ralimi	|- ( 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 ) )
57	1 56	syl	|- ( 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 ) )
58	57 2 4	mulsproplem11	|- ( ph -> ( C x.s E ) e. No )
59	45 58	subscld	|- ( ph -> ( ( D x.s E ) -s ( C x.s E ) ) e. No )
60	59	adantr	|- ( ( 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 )
61	44	adantr	|- ( ( 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 ) )
62	3	adantr	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E D e. No )
63		simprr1	|- ( ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( bday ` x ) e. ( bday ` E ) )
64	63	adantl	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( bday ` x ) e. ( bday ` E ) )
65		bdayelon	|- ( bday ` E ) e. On
66		simprrl	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E x e. No )
67		oldbday	|- ( ( ( bday ` E ) e. On /\ x e. No ) -> ( x e. ( _Old ` ( bday ` E ) ) <-> ( bday ` x ) e. ( bday ` E ) ) )
68	65 66 67	sylancr	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( x e. ( _Old ` ( bday ` E ) ) <-> ( bday ` x ) e. ( bday ` E ) ) )
69	64 68	mpbird	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E x e. ( _Old ` ( bday ` E ) ) )
70	61 62 69	mulsproplem3	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( D x.s x ) e. No )
71	57	adantr	|- ( ( 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 ) )
72	2	adantr	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E C e. No )
73	71 72 69	mulsproplem3	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( C x.s x ) e. No )
74	70 73	subscld	|- ( ( 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 )
75	31	uneq2i	|- ( ( ( 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. (/) )
76		un0	|- ( ( ( bday ` D ) +no ( bday ` F ) ) u. (/) ) = ( ( bday ` D ) +no ( bday ` F ) )
77	75 76	eqtri	|- ( ( ( 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 ) )
78		ssun2	|- ( ( bday ` D ) +no ( bday ` F ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) )
79	78 50	sstri	|- ( ( 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 ) ) ) )
80	79 38	sstri	|- ( ( 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 ) ) ) ) )
81	77 80	eqsstri	|- ( ( ( 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 ) ) ) ) )
82	81	sseli	|- ( ( ( ( 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 ) ) ) ) ) )
83	82	imim1i	|- ( ( ( ( ( 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 ) )
84	83	6ralimi	|- ( 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 ) )
85	1 84	syl	|- ( 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 ) )
86	85 3 5	mulsproplem11	|- ( ph -> ( D x.s F ) e. No )
87	31	uneq2i	|- ( ( ( 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. (/) )
88		un0	|- ( ( ( bday ` C ) +no ( bday ` F ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` F ) )
89	87 88	eqtri	|- ( ( ( 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 ) )
90		ssun1	|- ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) )
91	90 36	sstri	|- ( ( 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 ) ) ) )
92	91 38	sstri	|- ( ( 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 ) ) ) ) )
93	89 92	eqsstri	|- ( ( ( 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 ) ) ) ) )
94	93	sseli	|- ( ( ( ( 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 ) ) ) ) ) )
95	94	imim1i	|- ( ( ( ( ( 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 ) )
96	95	6ralimi	|- ( 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 ) )
97	1 96	syl	|- ( 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 ) )
98	97 2 5	mulsproplem11	|- ( ph -> ( C x.s F ) e. No )
99	86 98	subscld	|- ( ph -> ( ( D x.s F ) -s ( C x.s F ) ) e. No )
100	99	adantr	|- ( ( 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 )
101	1	mulsproplemcbv	|- ( 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 ) )
102	101	adantr	|- ( ( 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 ) )
103		onelss	|- ( ( bday ` E ) e. On -> ( ( bday ` x ) e. ( bday ` E ) -> ( bday ` x ) C_ ( bday ` E ) ) )
104	65 64 103	mpsyl	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( bday ` x ) C_ ( bday ` E ) )
105		simprl	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( bday ` E ) = ( bday ` F ) )
106	104 105	sseqtrd	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( bday ` x ) C_ ( bday ` F ) )
107		bdayelon	|- ( bday ` x ) e. On
108		bdayelon	|- ( bday ` F ) e. On
109		bdayelon	|- ( bday ` D ) e. On
110		naddss2	|- ( ( ( 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 ) ) ) )
111	107 108 109 110	mp3an	|- ( ( bday ` x ) C_ ( bday ` F ) <-> ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) )
112	106 111	sylib	|- ( ( 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 ) ) )
113		unss2	|- ( ( ( 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 ) ) ) )
114	112 113	syl	|- ( ( 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 ) ) ) )
115		bdayelon	|- ( bday ` C ) e. On
116		naddss2	|- ( ( ( 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 ) ) ) )
117	107 108 115 116	mp3an	|- ( ( bday ` x ) C_ ( bday ` F ) <-> ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) )
118	106 117	sylib	|- ( ( 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 ) ) )
119		unss1	|- ( ( ( 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 ) ) ) )
120	118 119	syl	|- ( ( 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 ) ) ) )
121		unss12	|- ( ( ( ( ( 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 ) ) ) ) )
122	114 120 121	syl2anc	|- ( ( 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 ) ) ) ) )
123		unss2	|- ( ( ( ( ( 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 ) ) ) ) ) )
124	122 123	syl	|- ( ( 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 ) ) ) ) ) )
125	124	sseld	|- ( ( 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 ) ) ) ) ) ) )
126	125	imim1d	|- ( ( 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 ) )
127	126	ralimd6v	|- ( ( 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 ) )
128	102 127	mpd	|- ( ( 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 ) )
129	4	adantr	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E E e. No )
130	6	adantr	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E C
131		simprr2	|- ( ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E E
132	131	adantl	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E E
133	64	olcd	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( bday ` E ) e. ( bday ` x ) \/ ( bday ` x ) e. ( bday ` E ) ) )
134	128 72 62 129 66 130 132 133	mulsproplem13	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( C x.s x ) -s ( C x.s E ) )
135	45	adantr	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( D x.s E ) e. No )
136	58	adantr	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( C x.s E ) e. No )
137	135 70 136 73	sltsubsub3bd	|- ( ( 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 ) )
138	134 137	mpbird	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( D x.s E ) -s ( C x.s E ) )
139		naddss2	|- ( ( ( 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 ) ) ) )
140	107 65 115 139	mp3an	|- ( ( bday ` x ) C_ ( bday ` E ) <-> ( ( bday ` C ) +no ( bday ` x ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) )
141	104 140	sylib	|- ( ( 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 ) ) )
142		unss1	|- ( ( ( 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 ) ) ) )
143	141 142	syl	|- ( ( 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 ) ) ) )
144		naddss2	|- ( ( ( 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 ) ) ) )
145	107 65 109 144	mp3an	|- ( ( bday ` x ) C_ ( bday ` E ) <-> ( ( bday ` D ) +no ( bday ` x ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) )
146	104 145	sylib	|- ( ( 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 ) ) )
147		unss2	|- ( ( ( 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 ) ) ) )
148	146 147	syl	|- ( ( 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 ) ) ) )
149		unss12	|- ( ( ( ( ( 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 ) ) ) ) )
150	143 148 149	syl2anc	|- ( ( 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 ) ) ) ) )
151		unss2	|- ( ( ( ( ( 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 ) ) ) ) ) )
152	150 151	syl	|- ( ( 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 ) ) ) ) ) )
153	152	sseld	|- ( ( 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 ) ) ) ) ) ) )
154	153	imim1d	|- ( ( 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 ) )
155	154	ralimd6v	|- ( ( 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 ) )
156	102 155	mpd	|- ( ( 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 ) )
157	5	adantr	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E F e. No )
158		simprr3	|- ( ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E x
159	158	adantl	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E x
160	64 105	eleqtrd	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( bday ` x ) e. ( bday ` F ) )
161	160	orcd	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( bday ` x ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` x ) ) )
162	156 72 62 66 157 130 159 161	mulsproplem13	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( C x.s F ) -s ( C x.s x ) )
163	86	adantr	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( D x.s F ) e. No )
164	98	adantr	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( C x.s F ) e. No )
165	70 163 73 164	sltsubsub3bd	|- ( ( 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 ) )
166	162 165	mpbird	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( D x.s x ) -s ( C x.s x ) )
167	60 74 100 138 166	slttrd	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( D x.s E ) -s ( C x.s E ) )
168	45 86 58 98	sltsubsub3bd	|- ( ph -> ( ( ( D x.s E ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
169	168	adantr	|- ( ( 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 ) )
170	167 169	mpbid	|- ( ( ph /\ ( ( bday ` E ) = ( bday ` F ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( C x.s F ) -s ( C x.s E ) )
171	170	anassrs	|- ( ( ( ph /\ ( bday ` E ) = ( bday ` F ) ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` E ) /\ E ( ( C x.s F ) -s ( C x.s E ) )
172	22 171	rexlimddv	|- ( ( ph /\ ( bday ` E ) = ( bday ` F ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
173	65	onordi	|- Ord ( bday ` E )
174	108	onordi	|- Ord ( bday ` F )
175		ordtri3or	|- ( ( Ord ( bday ` E ) /\ Ord ( bday ` F ) ) -> ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` E ) = ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) )
176	173 174 175	mp2an	|- ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` E ) = ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) )
177		df-3or	|- ( ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` E ) = ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) <-> ( ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` E ) = ( bday ` F ) ) \/ ( bday ` F ) e. ( bday ` E ) ) )
178		or32	|- ( ( ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` E ) = ( bday ` F ) ) \/ ( bday ` F ) e. ( bday ` E ) ) <-> ( ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) \/ ( bday ` E ) = ( bday ` F ) ) )
179	177 178	bitri	|- ( ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` E ) = ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) <-> ( ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) \/ ( bday ` E ) = ( bday ` F ) ) )
180	176 179	mpbi	|- ( ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) \/ ( bday ` E ) = ( bday ` F ) )
181	180	a1i	|- ( ph -> ( ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) \/ ( bday ` E ) = ( bday ` F ) ) )
182	16 172 181	mpjaodan	|- ( ph -> ( ( C x.s F ) -s ( C x.s E ) )