Theorem mulsproplem6

Description: Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 5-Mar-2025)

	Ref	Expression
Hypotheses	mulsproplem.1	⊢ ( 𝜑 → ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
	mulsproplem6.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	mulsproplem6.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	mulsproplem6.3	⊢ ( 𝜑 → 𝑃 ∈ ( L ‘ 𝐴 ) )
	mulsproplem6.4	⊢ ( 𝜑 → 𝑄 ∈ ( L ‘ 𝐵 ) )
	mulsproplem6.5	⊢ ( 𝜑 → 𝑉 ∈ ( R ‘ 𝐴 ) )
	mulsproplem6.6	⊢ ( 𝜑 → 𝑊 ∈ ( L ‘ 𝐵 ) )
Assertion	mulsproplem6	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulsproplem.1	⊢ ( 𝜑 → ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
2		mulsproplem6.1	⊢ ( 𝜑 → 𝐴 ∈ No )
3		mulsproplem6.2	⊢ ( 𝜑 → 𝐵 ∈ No )
4		mulsproplem6.3	⊢ ( 𝜑 → 𝑃 ∈ ( L ‘ 𝐴 ) )
5		mulsproplem6.4	⊢ ( 𝜑 → 𝑄 ∈ ( L ‘ 𝐵 ) )
6		mulsproplem6.5	⊢ ( 𝜑 → 𝑉 ∈ ( R ‘ 𝐴 ) )
7		mulsproplem6.6	⊢ ( 𝜑 → 𝑊 ∈ ( L ‘ 𝐵 ) )
8		leftssno	⊢ ( L ‘ 𝐵 ) ⊆ No
9	8 5	sselid	⊢ ( 𝜑 → 𝑄 ∈ No )
10	8 7	sselid	⊢ ( 𝜑 → 𝑊 ∈ No )
11		sltlin	⊢ ( ( 𝑄 ∈ No ∧ 𝑊 ∈ No ) → ( 𝑄 <s 𝑊 ∨ 𝑄 = 𝑊 ∨ 𝑊 <s 𝑄 ) )
12	9 10 11	syl2anc	⊢ ( 𝜑 → ( 𝑄 <s 𝑊 ∨ 𝑄 = 𝑊 ∨ 𝑊 <s 𝑄 ) )
13		leftssold	⊢ ( L ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) )
14	13 4	sselid	⊢ ( 𝜑 → 𝑃 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
15	1 14 3	mulsproplem2	⊢ ( 𝜑 → ( 𝑃 ·s 𝐵 ) ∈ No )
16		leftssold	⊢ ( L ‘ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝐵 ) )
17	16 5	sselid	⊢ ( 𝜑 → 𝑄 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
18	1 2 17	mulsproplem3	⊢ ( 𝜑 → ( 𝐴 ·s 𝑄 ) ∈ No )
19	15 18	addscld	⊢ ( 𝜑 → ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) ∈ No )
20	1 14 17	mulsproplem4	⊢ ( 𝜑 → ( 𝑃 ·s 𝑄 ) ∈ No )
21	19 20	subscld	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) ∈ No )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑄 <s 𝑊 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) ∈ No )
23	16 7	sselid	⊢ ( 𝜑 → 𝑊 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
24	1 2 23	mulsproplem3	⊢ ( 𝜑 → ( 𝐴 ·s 𝑊 ) ∈ No )
25	15 24	addscld	⊢ ( 𝜑 → ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) ∈ No )
26	1 14 23	mulsproplem4	⊢ ( 𝜑 → ( 𝑃 ·s 𝑊 ) ∈ No )
27	25 26	subscld	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑃 ·s 𝑊 ) ) ∈ No )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝑄 <s 𝑊 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑃 ·s 𝑊 ) ) ∈ No )
29		rightssold	⊢ ( R ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) )
30	29 6	sselid	⊢ ( 𝜑 → 𝑉 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
31	1 30 3	mulsproplem2	⊢ ( 𝜑 → ( 𝑉 ·s 𝐵 ) ∈ No )
32	31 24	addscld	⊢ ( 𝜑 → ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) ∈ No )
33	1 30 23	mulsproplem4	⊢ ( 𝜑 → ( 𝑉 ·s 𝑊 ) ∈ No )
34	32 33	subscld	⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ∈ No )
35	34	adantr	⊢ ( ( 𝜑 ∧ 𝑄 <s 𝑊 ) → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ∈ No )
36		ssltleft	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) <<s { 𝐴 } )
37	2 36	syl	⊢ ( 𝜑 → ( L ‘ 𝐴 ) <<s { 𝐴 } )
38		snidg	⊢ ( 𝐴 ∈ No → 𝐴 ∈ { 𝐴 } )
39	2 38	syl	⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
40	37 4 39	ssltsepcd	⊢ ( 𝜑 → 𝑃 <s 𝐴 )
41		0sno	⊢ 0s ∈ No
42	41	a1i	⊢ ( 𝜑 → 0s ∈ No )
43		leftssno	⊢ ( L ‘ 𝐴 ) ⊆ No
44	43 4	sselid	⊢ ( 𝜑 → 𝑃 ∈ No )
45		bday0s	⊢ ( bday ‘ 0s ) = ∅
46	45 45	oveq12i	⊢ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) = ( ∅ +no ∅ )
47		0elon	⊢ ∅ ∈ On
48		naddrid	⊢ ( ∅ ∈ On → ( ∅ +no ∅ ) = ∅ )
49	47 48	ax-mp	⊢ ( ∅ +no ∅ ) = ∅
50	46 49	eqtri	⊢ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) = ∅
51	50	uneq1i	⊢ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ) ) = ( ∅ ∪ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ) )
52		0un	⊢ ( ∅ ∪ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ) ) = ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) )
53	51 52	eqtri	⊢ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ) ) = ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) )
54		oldbdayim	⊢ ( 𝑃 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → ( bday ‘ 𝑃 ) ∈ ( bday ‘ 𝐴 ) )
55	14 54	syl	⊢ ( 𝜑 → ( bday ‘ 𝑃 ) ∈ ( bday ‘ 𝐴 ) )
56		oldbdayim	⊢ ( 𝑄 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) → ( bday ‘ 𝑄 ) ∈ ( bday ‘ 𝐵 ) )
57	17 56	syl	⊢ ( 𝜑 → ( bday ‘ 𝑄 ) ∈ ( bday ‘ 𝐵 ) )
58		bdayelon	⊢ ( bday ‘ 𝐴 ) ∈ On
59		bdayelon	⊢ ( bday ‘ 𝐵 ) ∈ On
60		naddel12	⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( ( bday ‘ 𝑃 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑄 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
61	58 59 60	mp2an	⊢ ( ( ( bday ‘ 𝑃 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑄 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
62	55 57 61	syl2anc	⊢ ( 𝜑 → ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
63		oldbdayim	⊢ ( 𝑊 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) → ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) )
64	23 63	syl	⊢ ( 𝜑 → ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) )
65		bdayelon	⊢ ( bday ‘ 𝑊 ) ∈ On
66		naddel2	⊢ ( ( ( bday ‘ 𝑊 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ) → ( ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
67	65 59 58 66	mp3an	⊢ ( ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
68	64 67	sylib	⊢ ( 𝜑 → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
69	62 68	jca	⊢ ( 𝜑 → ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
70		naddel12	⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( ( bday ‘ 𝑃 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
71	58 59 70	mp2an	⊢ ( ( ( bday ‘ 𝑃 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
72	55 64 71	syl2anc	⊢ ( 𝜑 → ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
73		bdayelon	⊢ ( bday ‘ 𝑄 ) ∈ On
74		naddel2	⊢ ( ( ( bday ‘ 𝑄 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ) → ( ( bday ‘ 𝑄 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
75	73 59 58 74	mp3an	⊢ ( ( bday ‘ 𝑄 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
76	57 75	sylib	⊢ ( 𝜑 → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
77	72 76	jca	⊢ ( 𝜑 → ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
78		bdayelon	⊢ ( bday ‘ 𝑃 ) ∈ On
79		naddcl	⊢ ( ( ( bday ‘ 𝑃 ) ∈ On ∧ ( bday ‘ 𝑄 ) ∈ On ) → ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ On )
80	78 73 79	mp2an	⊢ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ On
81		naddcl	⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝑊 ) ∈ On ) → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ On )
82	58 65 81	mp2an	⊢ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ On
83	80 82	onun2i	⊢ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∈ On
84		naddcl	⊢ ( ( ( bday ‘ 𝑃 ) ∈ On ∧ ( bday ‘ 𝑊 ) ∈ On ) → ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ On )
85	78 65 84	mp2an	⊢ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ On
86		naddcl	⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝑄 ) ∈ On ) → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ On )
87	58 73 86	mp2an	⊢ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ On
88	85 87	onun2i	⊢ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ∈ On
89		naddcl	⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On )
90	58 59 89	mp2an	⊢ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On
91		onunel	⊢ ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∈ On ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ∈ On ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On ) → ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
92	83 88 90 91	mp3an	⊢ ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
93		onunel	⊢ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ On ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ On ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
94	80 82 90 93	mp3an	⊢ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
95		onunel	⊢ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ On ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ On ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
96	85 87 90 95	mp3an	⊢ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
97	94 96	anbi12i	⊢ ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ↔ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
98	92 97	bitri	⊢ ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
99	69 77 98	sylanbrc	⊢ ( 𝜑 → ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
100		elun1	⊢ ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) → ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
101	99 100	syl	⊢ ( 𝜑 → ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
102	53 101	eqeltrid	⊢ ( 𝜑 → ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
103	1 42 42 44 2 9 10 102	mulsproplem1	⊢ ( 𝜑 → ( ( 0s ·s 0s ) ∈ No ∧ ( ( 𝑃 <s 𝐴 ∧ 𝑄 <s 𝑊 ) → ( ( 𝑃 ·s 𝑊 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝐴 ·s 𝑄 ) ) ) ) )
104	103	simprd	⊢ ( 𝜑 → ( ( 𝑃 <s 𝐴 ∧ 𝑄 <s 𝑊 ) → ( ( 𝑃 ·s 𝑊 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝐴 ·s 𝑄 ) ) ) )
105	40 104	mpand	⊢ ( 𝜑 → ( 𝑄 <s 𝑊 → ( ( 𝑃 ·s 𝑊 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝐴 ·s 𝑄 ) ) ) )
106	105	imp	⊢ ( ( 𝜑 ∧ 𝑄 <s 𝑊 ) → ( ( 𝑃 ·s 𝑊 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝐴 ·s 𝑄 ) ) )
107	26 24 20 18	sltsubsub3bd	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝑊 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝐴 ·s 𝑄 ) ) ↔ ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑃 ·s 𝑊 ) ) ) )
108	18 20	subscld	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) ∈ No )
109	24 26	subscld	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑊 ) -s ( 𝑃 ·s 𝑊 ) ) ∈ No )
110	108 109 15	sltadd2d	⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑃 ·s 𝑊 ) ) ↔ ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) ) <s ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑃 ·s 𝑊 ) ) ) ) )
111	107 110	bitrd	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝑊 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝐴 ·s 𝑄 ) ) ↔ ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) ) <s ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑃 ·s 𝑊 ) ) ) ) )
112	111	adantr	⊢ ( ( 𝜑 ∧ 𝑄 <s 𝑊 ) → ( ( ( 𝑃 ·s 𝑊 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝐴 ·s 𝑄 ) ) ↔ ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) ) <s ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑃 ·s 𝑊 ) ) ) ) )
113	106 112	mpbid	⊢ ( ( 𝜑 ∧ 𝑄 <s 𝑊 ) → ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) ) <s ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑃 ·s 𝑊 ) ) ) )
114	15 18 20	addsubsassd	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) = ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) ) )
115	114	adantr	⊢ ( ( 𝜑 ∧ 𝑄 <s 𝑊 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) = ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) ) )
116	15 24 26	addsubsassd	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑃 ·s 𝑊 ) ) = ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑃 ·s 𝑊 ) ) ) )
117	116	adantr	⊢ ( ( 𝜑 ∧ 𝑄 <s 𝑊 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑃 ·s 𝑊 ) ) = ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑃 ·s 𝑊 ) ) ) )
118	113 115 117	3brtr4d	⊢ ( ( 𝜑 ∧ 𝑄 <s 𝑊 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑃 ·s 𝑊 ) ) )
119		lltropt	⊢ ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 )
120	119	a1i	⊢ ( 𝜑 → ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 ) )
121	120 4 6	ssltsepcd	⊢ ( 𝜑 → 𝑃 <s 𝑉 )
122		ssltleft	⊢ ( 𝐵 ∈ No → ( L ‘ 𝐵 ) <<s { 𝐵 } )
123	3 122	syl	⊢ ( 𝜑 → ( L ‘ 𝐵 ) <<s { 𝐵 } )
124		snidg	⊢ ( 𝐵 ∈ No → 𝐵 ∈ { 𝐵 } )
125	3 124	syl	⊢ ( 𝜑 → 𝐵 ∈ { 𝐵 } )
126	123 7 125	ssltsepcd	⊢ ( 𝜑 → 𝑊 <s 𝐵 )
127		rightssno	⊢ ( R ‘ 𝐴 ) ⊆ No
128	127 6	sselid	⊢ ( 𝜑 → 𝑉 ∈ No )
129	50	uneq1i	⊢ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ) = ( ∅ ∪ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) )
130		0un	⊢ ( ∅ ∪ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ) = ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) )
131	129 130	eqtri	⊢ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ) = ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) )
132		oldbdayim	⊢ ( 𝑉 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) )
133	30 132	syl	⊢ ( 𝜑 → ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) )
134		bdayelon	⊢ ( bday ‘ 𝑉 ) ∈ On
135		naddel1	⊢ ( ( ( bday ‘ 𝑉 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
136	134 58 59 135	mp3an	⊢ ( ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
137	133 136	sylib	⊢ ( 𝜑 → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
138	72 137	jca	⊢ ( 𝜑 → ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
139		naddel1	⊢ ( ( ( bday ‘ 𝑃 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝑃 ) ∈ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
140	78 58 59 139	mp3an	⊢ ( ( bday ‘ 𝑃 ) ∈ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
141	55 140	sylib	⊢ ( 𝜑 → ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
142		naddel12	⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
143	58 59 142	mp2an	⊢ ( ( ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
144	133 64 143	syl2anc	⊢ ( 𝜑 → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
145	141 144	jca	⊢ ( 𝜑 → ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
146		naddcl	⊢ ( ( ( bday ‘ 𝑉 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ On )
147	134 59 146	mp2an	⊢ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ On
148	85 147	onun2i	⊢ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ On
149		naddcl	⊢ ( ( ( bday ‘ 𝑃 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ On )
150	78 59 149	mp2an	⊢ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ On
151		naddcl	⊢ ( ( ( bday ‘ 𝑉 ) ∈ On ∧ ( bday ‘ 𝑊 ) ∈ On ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ On )
152	134 65 151	mp2an	⊢ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ On
153	150 152	onun2i	⊢ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ On
154		onunel	⊢ ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ On ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ On ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On ) → ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
155	148 153 90 154	mp3an	⊢ ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
156		onunel	⊢ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ On ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ On ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
157	85 147 90 156	mp3an	⊢ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
158		onunel	⊢ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ On ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ On ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
159	150 152 90 158	mp3an	⊢ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
160	157 159	anbi12i	⊢ ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ↔ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
161	155 160	bitri	⊢ ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
162	138 145 161	sylanbrc	⊢ ( 𝜑 → ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
163		elun1	⊢ ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) → ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
164	162 163	syl	⊢ ( 𝜑 → ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
165	131 164	eqeltrid	⊢ ( 𝜑 → ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
166	1 42 42 44 128 10 3 165	mulsproplem1	⊢ ( 𝜑 → ( ( 0s ·s 0s ) ∈ No ∧ ( ( 𝑃 <s 𝑉 ∧ 𝑊 <s 𝐵 ) → ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) ) ) )
167	166	simprd	⊢ ( 𝜑 → ( ( 𝑃 <s 𝑉 ∧ 𝑊 <s 𝐵 ) → ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
168	121 126 167	mp2and	⊢ ( 𝜑 → ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) )
169	15 26	subscld	⊢ ( 𝜑 → ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑊 ) ) ∈ No )
170	31 33	subscld	⊢ ( 𝜑 → ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) ∈ No )
171	169 170 24	sltadd1d	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) ) )
172	168 171	mpbid	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) )
173	15 24 26	addsubsd	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑃 ·s 𝑊 ) ) = ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) )
174	31 24 33	addsubsd	⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) = ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) )
175	172 173 174	3brtr4d	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑃 ·s 𝑊 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )
176	175	adantr	⊢ ( ( 𝜑 ∧ 𝑄 <s 𝑊 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑃 ·s 𝑊 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )
177	22 28 35 118 176	slttrd	⊢ ( ( 𝜑 ∧ 𝑄 <s 𝑊 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )
178	177	ex	⊢ ( 𝜑 → ( 𝑄 <s 𝑊 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ) )
179		oveq2	⊢ ( 𝑄 = 𝑊 → ( 𝐴 ·s 𝑄 ) = ( 𝐴 ·s 𝑊 ) )
180	179	oveq2d	⊢ ( 𝑄 = 𝑊 → ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) = ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) )
181		oveq2	⊢ ( 𝑄 = 𝑊 → ( 𝑃 ·s 𝑄 ) = ( 𝑃 ·s 𝑊 ) )
182	180 181	oveq12d	⊢ ( 𝑄 = 𝑊 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) = ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑃 ·s 𝑊 ) ) )
183	182	breq1d	⊢ ( 𝑄 = 𝑊 → ( ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑃 ·s 𝑊 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ) )
184	175 183	syl5ibrcom	⊢ ( 𝜑 → ( 𝑄 = 𝑊 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ) )
185	21	adantr	⊢ ( ( 𝜑 ∧ 𝑊 <s 𝑄 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) ∈ No )
186	31 18	addscld	⊢ ( 𝜑 → ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) ∈ No )
187	1 30 17	mulsproplem4	⊢ ( 𝜑 → ( 𝑉 ·s 𝑄 ) ∈ No )
188	186 187	subscld	⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑉 ·s 𝑄 ) ) ∈ No )
189	188	adantr	⊢ ( ( 𝜑 ∧ 𝑊 <s 𝑄 ) → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑉 ·s 𝑄 ) ) ∈ No )
190	34	adantr	⊢ ( ( 𝜑 ∧ 𝑊 <s 𝑄 ) → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ∈ No )
191	123 5 125	ssltsepcd	⊢ ( 𝜑 → 𝑄 <s 𝐵 )
192	50	uneq1i	⊢ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ) ) = ( ∅ ∪ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ) )
193		0un	⊢ ( ∅ ∪ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ) ) = ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) )
194	192 193	eqtri	⊢ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ) ) = ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) )
195	62 137	jca	⊢ ( 𝜑 → ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
196		naddel12	⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑄 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
197	58 59 196	mp2an	⊢ ( ( ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑄 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
198	133 57 197	syl2anc	⊢ ( 𝜑 → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
199	141 198	jca	⊢ ( 𝜑 → ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
200	80 147	onun2i	⊢ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ On
201		naddcl	⊢ ( ( ( bday ‘ 𝑉 ) ∈ On ∧ ( bday ‘ 𝑄 ) ∈ On ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ On )
202	134 73 201	mp2an	⊢ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ On
203	150 202	onun2i	⊢ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∈ On
204		onunel	⊢ ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ On ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∈ On ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On ) → ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
205	200 203 90 204	mp3an	⊢ ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
206		onunel	⊢ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ On ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ On ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
207	80 147 90 206	mp3an	⊢ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
208		onunel	⊢ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ On ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ On ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
209	150 202 90 208	mp3an	⊢ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
210	207 209	anbi12i	⊢ ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ↔ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
211	205 210	bitri	⊢ ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ∧ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
212	195 199 211	sylanbrc	⊢ ( 𝜑 → ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
213		elun1	⊢ ( ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) → ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
214	212 213	syl	⊢ ( 𝜑 → ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
215	194 214	eqeltrid	⊢ ( 𝜑 → ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∪ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
216	1 42 42 44 128 9 3 215	mulsproplem1	⊢ ( 𝜑 → ( ( 0s ·s 0s ) ∈ No ∧ ( ( 𝑃 <s 𝑉 ∧ 𝑄 <s 𝐵 ) → ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑄 ) ) ) ) )
217	216	simprd	⊢ ( 𝜑 → ( ( 𝑃 <s 𝑉 ∧ 𝑄 <s 𝐵 ) → ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑄 ) ) ) )
218	121 191 217	mp2and	⊢ ( 𝜑 → ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑄 ) ) )
219	15 20	subscld	⊢ ( 𝜑 → ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) ∈ No )
220	31 187	subscld	⊢ ( 𝜑 → ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑄 ) ) ∈ No )
221	219 220 18	sltadd1d	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑄 ) ) ↔ ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) +s ( 𝐴 ·s 𝑄 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑄 ) ) +s ( 𝐴 ·s 𝑄 ) ) ) )
222	218 221	mpbid	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) +s ( 𝐴 ·s 𝑄 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑄 ) ) +s ( 𝐴 ·s 𝑄 ) ) )
223	15 18 20	addsubsd	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) = ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) +s ( 𝐴 ·s 𝑄 ) ) )
224	31 18 187	addsubsd	⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑉 ·s 𝑄 ) ) = ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑄 ) ) +s ( 𝐴 ·s 𝑄 ) ) )
225	222 223 224	3brtr4d	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑉 ·s 𝑄 ) ) )
226	225	adantr	⊢ ( ( 𝜑 ∧ 𝑊 <s 𝑄 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑉 ·s 𝑄 ) ) )
227		ssltright	⊢ ( 𝐴 ∈ No → { 𝐴 } <<s ( R ‘ 𝐴 ) )
228	2 227	syl	⊢ ( 𝜑 → { 𝐴 } <<s ( R ‘ 𝐴 ) )
229	228 39 6	ssltsepcd	⊢ ( 𝜑 → 𝐴 <s 𝑉 )
230	50	uneq1i	⊢ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ) = ( ∅ ∪ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) )
231		0un	⊢ ( ∅ ∪ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ) = ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) )
232	230 231	eqtri	⊢ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ) = ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) )
233	68 198	jca	⊢ ( 𝜑 → ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
234	76 144	jca	⊢ ( 𝜑 → ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
235	82 202	onun2i	⊢ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∈ On
236	87 152	onun2i	⊢ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ On
237		onunel	⊢ ( ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∈ On ∧ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ On ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On ) → ( ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
238	235 236 90 237	mp3an	⊢ ( ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
239		onunel	⊢ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ On ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ On ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
240	82 202 90 239	mp3an	⊢ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
241		onunel	⊢ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ On ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ On ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
242	87 152 90 241	mp3an	⊢ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
243	240 242	anbi12i	⊢ ( ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ↔ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ∧ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
244	238 243	bitri	⊢ ( ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ∧ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
245	233 234 244	sylanbrc	⊢ ( 𝜑 → ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
246		elun1	⊢ ( ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) → ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
247	245 246	syl	⊢ ( 𝜑 → ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
248	232 247	eqeltrid	⊢ ( 𝜑 → ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑄 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
249	1 42 42 2 128 10 9 248	mulsproplem1	⊢ ( 𝜑 → ( ( 0s ·s 0s ) ∈ No ∧ ( ( 𝐴 <s 𝑉 ∧ 𝑊 <s 𝑄 ) → ( ( 𝐴 ·s 𝑄 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑄 ) -s ( 𝑉 ·s 𝑊 ) ) ) ) )
250	249	simprd	⊢ ( 𝜑 → ( ( 𝐴 <s 𝑉 ∧ 𝑊 <s 𝑄 ) → ( ( 𝐴 ·s 𝑄 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑄 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
251	229 250	mpand	⊢ ( 𝜑 → ( 𝑊 <s 𝑄 → ( ( 𝐴 ·s 𝑄 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑄 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
252	251	imp	⊢ ( ( 𝜑 ∧ 𝑊 <s 𝑄 ) → ( ( 𝐴 ·s 𝑄 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑄 ) -s ( 𝑉 ·s 𝑊 ) ) )
253	18 187 24 33	sltsubsubbd	⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝑄 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑄 ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( 𝐴 ·s 𝑄 ) -s ( 𝑉 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
254	18 187	subscld	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑄 ) -s ( 𝑉 ·s 𝑄 ) ) ∈ No )
255	24 33	subscld	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ∈ No )
256	254 255 31	sltadd2d	⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝑄 ) -s ( 𝑉 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑉 ·s 𝑄 ) ) ) <s ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) ) )
257	253 256	bitrd	⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝑄 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑄 ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑉 ·s 𝑄 ) ) ) <s ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) ) )
258	257	adantr	⊢ ( ( 𝜑 ∧ 𝑊 <s 𝑄 ) → ( ( ( 𝐴 ·s 𝑄 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑄 ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑉 ·s 𝑄 ) ) ) <s ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) ) )
259	252 258	mpbid	⊢ ( ( 𝜑 ∧ 𝑊 <s 𝑄 ) → ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑉 ·s 𝑄 ) ) ) <s ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
260	31 18 187	addsubsassd	⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑉 ·s 𝑄 ) ) = ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑉 ·s 𝑄 ) ) ) )
261	260	adantr	⊢ ( ( 𝜑 ∧ 𝑊 <s 𝑄 ) → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑉 ·s 𝑄 ) ) = ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑉 ·s 𝑄 ) ) ) )
262	31 24 33	addsubsassd	⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) = ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
263	262	adantr	⊢ ( ( 𝜑 ∧ 𝑊 <s 𝑄 ) → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) = ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
264	259 261 263	3brtr4d	⊢ ( ( 𝜑 ∧ 𝑊 <s 𝑄 ) → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑉 ·s 𝑄 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )
265	185 189 190 226 264	slttrd	⊢ ( ( 𝜑 ∧ 𝑊 <s 𝑄 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )
266	265	ex	⊢ ( 𝜑 → ( 𝑊 <s 𝑄 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ) )
267	178 184 266	3jaod	⊢ ( 𝜑 → ( ( 𝑄 <s 𝑊 ∨ 𝑄 = 𝑊 ∨ 𝑊 <s 𝑄 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ) )
268	12 267	mpd	⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )