Theorem addsprop

Description: Inductively show that surreal addition is closed and compatible with less-than. This proof follows from induction on the birthdays of the surreal numbers involved. This pattern occurs throughout surreal development. Theorem 3.1 of Gonshor p. 14. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Assertion	addsprop	Could not format assertion : No typesetting found for |- ( ( X e. No /\ Y e. No /\ Z e. No ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X )

Proof

Step	Hyp	Ref	Expression
1		bdayelon	$$⊢\mathrm{bday}\left(X\right)\in \mathrm{On}$$
2		bdayelon	$$⊢\mathrm{bday}\left(Y\right)\in \mathrm{On}$$
3		naddcl	Could not format ( ( ( bday ` X ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) : No typesetting found for |- ( ( ( bday ` X ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) with typecode |-
4	1 2 3	mp2an	Could not format ( ( bday ` X ) +no ( bday ` Y ) ) e. On : No typesetting found for |- ( ( bday ` X ) +no ( bday ` Y ) ) e. On with typecode |-
5		bdayelon	$$⊢\mathrm{bday}\left(Z\right)\in \mathrm{On}$$
6		naddcl	Could not format ( ( ( bday ` X ) e. On /\ ( bday ` Z ) e. On ) -> ( ( bday ` X ) +no ( bday ` Z ) ) e. On ) : No typesetting found for |- ( ( ( bday ` X ) e. On /\ ( bday ` Z ) e. On ) -> ( ( bday ` X ) +no ( bday ` Z ) ) e. On ) with typecode |-
7	1 5 6	mp2an	Could not format ( ( bday ` X ) +no ( bday ` Z ) ) e. On : No typesetting found for |- ( ( bday ` X ) +no ( bday ` Z ) ) e. On with typecode |-
8	4 7	onun2i	Could not format ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) e. On : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) e. On with typecode |-
9		risset	Could not format ( ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) e. On <-> E. a e. On a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) e. On <-> E. a e. On a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
10	8 9	mpbi	Could not format E. a e. On a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) : No typesetting found for |- E. a e. On a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) with typecode |-
11		eqeq1	Could not format ( a = b -> ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) <-> b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) ) ) : No typesetting found for |- ( a = b -> ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) <-> b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) ) ) with typecode |-
12	11	imbi1d	Could not format ( a = b -> ( ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
13	12	ralbidv	Could not format ( a = b -> ( A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. z e. No ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. z e. No ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
14	13	2ralbidv	Could not format ( a = b -> ( A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
15		fveq2	$$⊢x=p\to \mathrm{bday}\left(x\right)=\mathrm{bday}\left(p\right)$$
16	15	oveq1d	Could not format ( x = p -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` p ) +no ( bday ` y ) ) ) : No typesetting found for |- ( x = p -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` p ) +no ( bday ` y ) ) ) with typecode |-
17	15	oveq1d	Could not format ( x = p -> ( ( bday ` x ) +no ( bday ` z ) ) = ( ( bday ` p ) +no ( bday ` z ) ) ) : No typesetting found for |- ( x = p -> ( ( bday ` x ) +no ( bday ` z ) ) = ( ( bday ` p ) +no ( bday ` z ) ) ) with typecode |-
18	16 17	uneq12d	Could not format ( x = p -> ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) = ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) ) : No typesetting found for |- ( x = p -> ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) = ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) ) with typecode |-
19	18	eqeq2d	Could not format ( x = p -> ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) <-> b = ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) ) ) : No typesetting found for |- ( x = p -> ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) <-> b = ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) ) ) with typecode |-
20		oveq1	Could not format ( x = p -> ( x +s y ) = ( p +s y ) ) : No typesetting found for |- ( x = p -> ( x +s y ) = ( p +s y ) ) with typecode |-
21	20	eleq1d	Could not format ( x = p -> ( ( x +s y ) e. No <-> ( p +s y ) e. No ) ) : No typesetting found for |- ( x = p -> ( ( x +s y ) e. No <-> ( p +s y ) e. No ) ) with typecode |-
22		oveq2	Could not format ( x = p -> ( y +s x ) = ( y +s p ) ) : No typesetting found for |- ( x = p -> ( y +s x ) = ( y +s p ) ) with typecode |-
23		oveq2	Could not format ( x = p -> ( z +s x ) = ( z +s p ) ) : No typesetting found for |- ( x = p -> ( z +s x ) = ( z +s p ) ) with typecode |-
24	22 23	breq12d	Could not format ( x = p -> ( ( y +s x ) ( y +s p ) ( ( y +s x ) ( y +s p )
25	24	imbi2d	Could not format ( x = p -> ( ( y ( y +s x ) ( y ( y +s p ) ( ( y ( y +s x ) ( y ( y +s p )
26	21 25	anbi12d	Could not format ( x = p -> ( ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( p +s y ) e. No /\ ( y ( y +s p ) ( ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( p +s y ) e. No /\ ( y ( y +s p )
27	19 26	imbi12d	Could not format ( x = p -> ( ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( b = ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) -> ( ( p +s y ) e. No /\ ( y ( y +s p ) ( ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( b = ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) -> ( ( p +s y ) e. No /\ ( y ( y +s p )
28		fveq2	$$⊢y=q\to \mathrm{bday}\left(y\right)=\mathrm{bday}\left(q\right)$$
29	28	oveq2d	Could not format ( y = q -> ( ( bday ` p ) +no ( bday ` y ) ) = ( ( bday ` p ) +no ( bday ` q ) ) ) : No typesetting found for |- ( y = q -> ( ( bday ` p ) +no ( bday ` y ) ) = ( ( bday ` p ) +no ( bday ` q ) ) ) with typecode |-
30	29	uneq1d	Could not format ( y = q -> ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) ) : No typesetting found for |- ( y = q -> ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) ) with typecode |-
31	30	eqeq2d	Could not format ( y = q -> ( b = ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) <-> b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) ) ) : No typesetting found for |- ( y = q -> ( b = ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) <-> b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) ) ) with typecode |-
32		oveq2	Could not format ( y = q -> ( p +s y ) = ( p +s q ) ) : No typesetting found for |- ( y = q -> ( p +s y ) = ( p +s q ) ) with typecode |-
33	32	eleq1d	Could not format ( y = q -> ( ( p +s y ) e. No <-> ( p +s q ) e. No ) ) : No typesetting found for |- ( y = q -> ( ( p +s y ) e. No <-> ( p +s q ) e. No ) ) with typecode |-
34		breq1	$$⊢y=q\to \left(y{<}_{s}z\leftrightarrow q{<}_{s}z\right)$$
35		oveq1	Could not format ( y = q -> ( y +s p ) = ( q +s p ) ) : No typesetting found for |- ( y = q -> ( y +s p ) = ( q +s p ) ) with typecode |-
36	35	breq1d	Could not format ( y = q -> ( ( y +s p ) ( q +s p ) ( ( y +s p ) ( q +s p )
37	34 36	imbi12d	Could not format ( y = q -> ( ( y ( y +s p ) ( q ( q +s p ) ( ( y ( y +s p ) ( q ( q +s p )
38	33 37	anbi12d	Could not format ( y = q -> ( ( ( p +s y ) e. No /\ ( y ( y +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( ( p +s y ) e. No /\ ( y ( y +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p )
39	31 38	imbi12d	Could not format ( y = q -> ( ( b = ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) -> ( ( p +s y ) e. No /\ ( y ( y +s p ) ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( b = ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) -> ( ( p +s y ) e. No /\ ( y ( y +s p ) ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p )
40		fveq2	$$⊢z=r\to \mathrm{bday}\left(z\right)=\mathrm{bday}\left(r\right)$$
41	40	oveq2d	Could not format ( z = r -> ( ( bday ` p ) +no ( bday ` z ) ) = ( ( bday ` p ) +no ( bday ` r ) ) ) : No typesetting found for |- ( z = r -> ( ( bday ` p ) +no ( bday ` z ) ) = ( ( bday ` p ) +no ( bday ` r ) ) ) with typecode |-
42	41	uneq2d	Could not format ( z = r -> ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) ) : No typesetting found for |- ( z = r -> ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) ) with typecode |-
43	42	eqeq2d	Could not format ( z = r -> ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) <-> b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) ) ) : No typesetting found for |- ( z = r -> ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) <-> b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) ) ) with typecode |-
44		breq2	$$⊢z=r\to \left(q{<}_{s}z\leftrightarrow q{<}_{s}r\right)$$
45		oveq1	Could not format ( z = r -> ( z +s p ) = ( r +s p ) ) : No typesetting found for |- ( z = r -> ( z +s p ) = ( r +s p ) ) with typecode |-
46	45	breq2d	Could not format ( z = r -> ( ( q +s p ) ( q +s p ) ( ( q +s p ) ( q +s p )
47	44 46	imbi12d	Could not format ( z = r -> ( ( q ( q +s p ) ( q ( q +s p ) ( ( q ( q +s p ) ( q ( q +s p )
48	47	anbi2d	Could not format ( z = r -> ( ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p )
49	43 48	imbi12d	Could not format ( z = r -> ( ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p )
50	27 39 49	cbvral3vw	Could not format ( A. x e. No A. y e. No A. z e. No ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( x +s y ) e. No /\ ( y ( y +s x ) A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p )
51	14 50	bitrdi	Could not format ( a = b -> ( A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p )
52		ralrot3	Could not format ( A. p e. No A. q e. No A. b e. a A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. b e. a A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p ) A. b e. a A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p )
53		ralcom	Could not format ( A. b e. a A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. r e. No A. b e. a ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p ) A. r e. No A. b e. a ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p )
54		r19.23v	Could not format ( A. b e. a ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( E. b e. a b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p ) ( E. b e. a b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p )
55		risset	Could not format ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a <-> E. b e. a b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a <-> E. b e. a b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) ) with typecode |-
56	55	imbi1i	Could not format ( ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( E. b e. a b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p ) ( E. b e. a b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p )
57	54 56	bitr4i	Could not format ( A. b e. a ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p )
58	57	ralbii	Could not format ( A. r e. No A. b e. a ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p ) A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p )
59	53 58	bitri	Could not format ( A. b e. a A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p ) A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p )
60	59	2ralbii	Could not format ( A. p e. No A. q e. No A. b e. a A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p ) A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p )
61	52 60	bitr3i	Could not format ( A. b e. a A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p ) A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p )
62		eleq2	Could not format ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a <-> ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) ) ) : No typesetting found for |- ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a <-> ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) ) ) with typecode |-
63	62	imbi1d	Could not format ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p )
64	63	ralbidv	Could not format ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p )
65	64	2ralbidv	Could not format ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p )
66	65	anbi1d	Could not format ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p )
67	66	biimpcd	Could not format ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p ) ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p )
68		simpl	Could not format ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p ) A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p )
69		simprll	Could not format ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) x e. No ) : No typesetting found for |- ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) x e. No ) with typecode |-
70		simprlr	Could not format ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) y e. No ) : No typesetting found for |- ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) y e. No ) with typecode |-
71	68 69 70	addsproplem3	Could not format ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( x +s y ) e. No /\ ( { a | E. b e. ( _Left ` x ) a = ( b +s y ) } u. { c | E. d e. ( _Left ` y ) c = ( x +s d ) } ) < ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( x +s y ) e. No /\ ( { a | E. b e. ( _Left ` x ) a = ( b +s y ) } u. { c | E. d e. ( _Left ` y ) c = ( x +s d ) } ) <
72	71	simp1d	Could not format ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( x +s y ) e. No ) : No typesetting found for |- ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( x +s y ) e. No ) with typecode |-
73	68	adantr	Could not format ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( p +s q ) e. No /\ ( q ( q +s p ) A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p )
74	69	adantr	Could not format ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) x e. No ) : No typesetting found for |- ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) x e. No ) with typecode |-
75	70	adantr	Could not format ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) y e. No ) : No typesetting found for |- ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) y e. No ) with typecode |-
76		simplrr	Could not format ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) z e. No ) : No typesetting found for |- ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) z e. No ) with typecode |-
77		simpr	Could not format ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) y ( ( p +s q ) e. No /\ ( q ( q +s p ) y
78	73 74 75 76 77	addsproplem7	Could not format ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( y +s x ) ( ( p +s q ) e. No /\ ( q ( q +s p ) ( y +s x )
79	78	ex	Could not format ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( y ( y +s x ) ( ( p +s q ) e. No /\ ( q ( q +s p ) ( y ( y +s x )
80	72 79	jca	Could not format ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( p +s q ) e. No /\ ( q ( q +s p ) ( ( x +s y ) e. No /\ ( y ( y +s x )
81	67 80	syl6	Could not format ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( p +s q ) e. No /\ ( q ( q +s p ) ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
82	81	anassrs	Could not format ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( p +s q ) e. No /\ ( q ( q +s p ) ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
83	82	ralrimiva	Could not format ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( p +s q ) e. No /\ ( q ( q +s p ) A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
84	83	ralrimivva	Could not format ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( p +s q ) e. No /\ ( q ( q +s p ) A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
85	61 84	sylbi	Could not format ( A. b e. a A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( p +s q ) e. No /\ ( q ( q +s p ) A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
86	85	a1i	Could not format ( a e. On -> ( A. b e. a A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( A. b e. a A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q ( q +s p ) A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
87	51 86	tfis2	Could not format ( a e. On -> A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
88		fveq2	$$⊢x=X\to \mathrm{bday}\left(x\right)=\mathrm{bday}\left(X\right)$$
89	88	oveq1d	Could not format ( x = X -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` X ) +no ( bday ` y ) ) ) : No typesetting found for |- ( x = X -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` X ) +no ( bday ` y ) ) ) with typecode |-
90	88	oveq1d	Could not format ( x = X -> ( ( bday ` x ) +no ( bday ` z ) ) = ( ( bday ` X ) +no ( bday ` z ) ) ) : No typesetting found for |- ( x = X -> ( ( bday ` x ) +no ( bday ` z ) ) = ( ( bday ` X ) +no ( bday ` z ) ) ) with typecode |-
91	89 90	uneq12d	Could not format ( x = X -> ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) = ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) ) : No typesetting found for |- ( x = X -> ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) = ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) ) with typecode |-
92	91	eqeq2d	Could not format ( x = X -> ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) <-> a = ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) ) ) : No typesetting found for |- ( x = X -> ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) <-> a = ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) ) ) with typecode |-
93		oveq1	Could not format ( x = X -> ( x +s y ) = ( X +s y ) ) : No typesetting found for |- ( x = X -> ( x +s y ) = ( X +s y ) ) with typecode |-
94	93	eleq1d	Could not format ( x = X -> ( ( x +s y ) e. No <-> ( X +s y ) e. No ) ) : No typesetting found for |- ( x = X -> ( ( x +s y ) e. No <-> ( X +s y ) e. No ) ) with typecode |-
95		oveq2	Could not format ( x = X -> ( y +s x ) = ( y +s X ) ) : No typesetting found for |- ( x = X -> ( y +s x ) = ( y +s X ) ) with typecode |-
96		oveq2	Could not format ( x = X -> ( z +s x ) = ( z +s X ) ) : No typesetting found for |- ( x = X -> ( z +s x ) = ( z +s X ) ) with typecode |-
97	95 96	breq12d	Could not format ( x = X -> ( ( y +s x ) ( y +s X ) ( ( y +s x ) ( y +s X )
98	97	imbi2d	Could not format ( x = X -> ( ( y ( y +s x ) ( y ( y +s X ) ( ( y ( y +s x ) ( y ( y +s X )
99	94 98	anbi12d	Could not format ( x = X -> ( ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( X +s y ) e. No /\ ( y ( y +s X ) ( ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( X +s y ) e. No /\ ( y ( y +s X )
100	92 99	imbi12d	Could not format ( x = X -> ( ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( a = ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) -> ( ( X +s y ) e. No /\ ( y ( y +s X ) ( ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( a = ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) -> ( ( X +s y ) e. No /\ ( y ( y +s X )
101		fveq2	$$⊢y=Y\to \mathrm{bday}\left(y\right)=\mathrm{bday}\left(Y\right)$$
102	101	oveq2d	Could not format ( y = Y -> ( ( bday ` X ) +no ( bday ` y ) ) = ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( y = Y -> ( ( bday ` X ) +no ( bday ` y ) ) = ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
103	102	uneq1d	Could not format ( y = Y -> ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) ) : No typesetting found for |- ( y = Y -> ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) ) with typecode |-
104	103	eqeq2d	Could not format ( y = Y -> ( a = ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) <-> a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) ) ) : No typesetting found for |- ( y = Y -> ( a = ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) <-> a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) ) ) with typecode |-
105		oveq2	Could not format ( y = Y -> ( X +s y ) = ( X +s Y ) ) : No typesetting found for |- ( y = Y -> ( X +s y ) = ( X +s Y ) ) with typecode |-
106	105	eleq1d	Could not format ( y = Y -> ( ( X +s y ) e. No <-> ( X +s Y ) e. No ) ) : No typesetting found for |- ( y = Y -> ( ( X +s y ) e. No <-> ( X +s Y ) e. No ) ) with typecode |-
107		breq1	$$⊢y=Y\to \left(y{<}_{s}z\leftrightarrow Y{<}_{s}z\right)$$
108		oveq1	Could not format ( y = Y -> ( y +s X ) = ( Y +s X ) ) : No typesetting found for |- ( y = Y -> ( y +s X ) = ( Y +s X ) ) with typecode |-
109	108	breq1d	Could not format ( y = Y -> ( ( y +s X ) ( Y +s X ) ( ( y +s X ) ( Y +s X )
110	107 109	imbi12d	Could not format ( y = Y -> ( ( y ( y +s X ) ( Y ( Y +s X ) ( ( y ( y +s X ) ( Y ( Y +s X )
111	106 110	anbi12d	Could not format ( y = Y -> ( ( ( X +s y ) e. No /\ ( y ( y +s X ) ( ( X +s Y ) e. No /\ ( Y ( Y +s X ) ( ( ( X +s y ) e. No /\ ( y ( y +s X ) ( ( X +s Y ) e. No /\ ( Y ( Y +s X )
112	104 111	imbi12d	Could not format ( y = Y -> ( ( a = ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) -> ( ( X +s y ) e. No /\ ( y ( y +s X ) ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X ) ( ( a = ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) -> ( ( X +s y ) e. No /\ ( y ( y +s X ) ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X )
113		fveq2	$$⊢z=Z\to \mathrm{bday}\left(z\right)=\mathrm{bday}\left(Z\right)$$
114	113	oveq2d	Could not format ( z = Z -> ( ( bday ` X ) +no ( bday ` z ) ) = ( ( bday ` X ) +no ( bday ` Z ) ) ) : No typesetting found for |- ( z = Z -> ( ( bday ` X ) +no ( bday ` z ) ) = ( ( bday ` X ) +no ( bday ` Z ) ) ) with typecode |-
115	114	uneq2d	Could not format ( z = Z -> ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( z = Z -> ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
116	115	eqeq2d	Could not format ( z = Z -> ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) <-> a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) ) : No typesetting found for |- ( z = Z -> ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) <-> a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) ) with typecode |-
117		breq2	$$⊢z=Z\to \left(Y{<}_{s}z\leftrightarrow Y{<}_{s}Z\right)$$
118		oveq1	Could not format ( z = Z -> ( z +s X ) = ( Z +s X ) ) : No typesetting found for |- ( z = Z -> ( z +s X ) = ( Z +s X ) ) with typecode |-
119	118	breq2d	Could not format ( z = Z -> ( ( Y +s X ) ( Y +s X ) ( ( Y +s X ) ( Y +s X )
120	117 119	imbi12d	Could not format ( z = Z -> ( ( Y ( Y +s X ) ( Y ( Y +s X ) ( ( Y ( Y +s X ) ( Y ( Y +s X )
121	120	anbi2d	Could not format ( z = Z -> ( ( ( X +s Y ) e. No /\ ( Y ( Y +s X ) ( ( X +s Y ) e. No /\ ( Y ( Y +s X ) ( ( ( X +s Y ) e. No /\ ( Y ( Y +s X ) ( ( X +s Y ) e. No /\ ( Y ( Y +s X )
122	116 121	imbi12d	Could not format ( z = Z -> ( ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X ) ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X ) ( ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X ) ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X )
123	100 112 122	rspc3v	Could not format ( ( X e. No /\ Y e. No /\ Z e. No ) -> ( A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X ) ( A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X )
124	87 123	syl5com	Could not format ( a e. On -> ( ( X e. No /\ Y e. No /\ Z e. No ) -> ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X ) ( ( X e. No /\ Y e. No /\ Z e. No ) -> ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X )
125	124	com23	Could not format ( a e. On -> ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( X e. No /\ Y e. No /\ Z e. No ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X ) ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( X e. No /\ Y e. No /\ Z e. No ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X )
126	125	rexlimiv	Could not format ( E. a e. On a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( X e. No /\ Y e. No /\ Z e. No ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X ) ( ( X e. No /\ Y e. No /\ Z e. No ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X )
127	10 126	ax-mp	Could not format ( ( X e. No /\ Y e. No /\ Z e. No ) -> ( ( X +s Y ) e. No /\ ( Y ( Y +s X ) ( ( X +s Y ) e. No /\ ( Y ( Y +s X )