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	$$⊢\phi \to \forall a\in \mathrm{No}\forall b\in \mathrm{No}\forall c\in \mathrm{No}\forall d\in \mathrm{No}\forall e\in \mathrm{No}\forall f\in \mathrm{No}\left(\left(\mathrm{bday}\left(a\right)+\mathrm{bday}\left(b\right)\right)\cup \left(\left(\left(\mathrm{bday}\left(c\right)+\mathrm{bday}\left(e\right)\right)\cup \left(\mathrm{bday}\left(d\right)+\mathrm{bday}\left(f\right)\right)\right)\cup \left(\left(\mathrm{bday}\left(c\right)+\mathrm{bday}\left(f\right)\right)\cup \left(\mathrm{bday}\left(d\right)+\mathrm{bday}\left(e\right)\right)\right)\right)\in \left(\left(\mathrm{bday}\left(A\right)+\mathrm{bday}\left(B\right)\right)\cup \left(\left(\left(\mathrm{bday}\left(C\right)+\mathrm{bday}\left(E\right)\right)\cup \left(\mathrm{bday}\left(D\right)+\mathrm{bday}\left(F\right)\right)\right)\cup \left(\left(\mathrm{bday}\left(C\right)+\mathrm{bday}\left(F\right)\right)\cup \left(\mathrm{bday}\left(D\right)+\mathrm{bday}\left(E\right)\right)\right)\right)\right)\to \left(a{\cdot }_{s}b\in \mathrm{No}\wedge \left(\left(c{<}_{s}d\wedge e{<}_{s}f\right)\to \left(\left(c{\cdot }_{s}f\right){-}_s\left(c{\cdot }_{s}e\right)\right){<}_s\left(\left(d{\cdot }_{s}f\right){-}_s\left(d{\cdot }_{s}e\right)\right)\right)\right)\right)$$
	mulsproplem.2	$$⊢\phi \to C\in \mathrm{No}$$
	mulsproplem.3	$$⊢\phi \to D\in \mathrm{No}$$
	mulsproplem.4	$$⊢\phi \to E\in \mathrm{No}$$
	mulsproplem.5	$$⊢\phi \to F\in \mathrm{No}$$
	mulsproplem.6	$$⊢\phi \to C{<}_{s}D$$
	mulsproplem.7	$$⊢\phi \to E{<}_{s}F$$
Assertion	mulsproplem14	$$⊢\phi \to \left(\left(C{\cdot }_{s}F\right){-}_s\left(C{\cdot }_{s}E\right)\right){<}_s\left(\left(D{\cdot }_{s}F\right){-}_s\left(D{\cdot }_{s}E\right)\right)$$

Proof

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