Theorem mulsproplem13 27944

Description: Lemma for surreal multiplication. Remove the restriction on 𝐶 and 𝐷 from mulsproplem12 27943. (Contributed by Scott Fenton, 5-Mar-2025.)

Hypotheses

Ref	Expression
mulsproplem.1	⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
mulsproplem.2	⊢ (𝜑 → 𝐶 ∈ No )
mulsproplem.3	⊢ (𝜑 → 𝐷 ∈ No )
mulsproplem.4	⊢ (𝜑 → 𝐸 ∈ No )
mulsproplem.5	⊢ (𝜑 → 𝐹 ∈ No )
mulsproplem.6	⊢ (𝜑 → 𝐶 <s 𝐷)
mulsproplem.7	⊢ (𝜑 → 𝐸 <s 𝐹)
mulsproplem13.1	⊢ (𝜑 → (( bday ‘𝐸) ∈ ( bday ‘𝐹) ∨ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))

Assertion

Ref	Expression
mulsproplem13	⊢ (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))

Distinct variable groups:   𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓

Allowed substitution hints:   𝜑(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)

Proof of Theorem mulsproplem13

Dummy variables 𝑔 ℎ 𝑖 𝑗 𝑘 𝑙 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mulsproplem.1	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
2	1	adantr 480	. . 3 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶))) → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
3		mulsproplem.2	. . . 4 ⊢ (𝜑 → 𝐶 ∈ No )
4	3	adantr 480	. . 3 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶))) → 𝐶 ∈ No )
5		mulsproplem.3	. . . 4 ⊢ (𝜑 → 𝐷 ∈ No )
6	5	adantr 480	. . 3 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶))) → 𝐷 ∈ No )
7		mulsproplem.4	. . . 4 ⊢ (𝜑 → 𝐸 ∈ No )
8	7	adantr 480	. . 3 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶))) → 𝐸 ∈ No )
9		mulsproplem.5	. . . 4 ⊢ (𝜑 → 𝐹 ∈ No )
10	9	adantr 480	. . 3 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶))) → 𝐹 ∈ No )
11		mulsproplem.6	. . . 4 ⊢ (𝜑 → 𝐶 <s 𝐷)
12	11	adantr 480	. . 3 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶))) → 𝐶 <s 𝐷)
13		mulsproplem.7	. . . 4 ⊢ (𝜑 → 𝐸 <s 𝐹)
14	13	adantr 480	. . 3 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶))) → 𝐸 <s 𝐹)
15		simpr 484	. . 3 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶))) → (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶)))
16		mulsproplem13.1	. . . 4 ⊢ (𝜑 → (( bday ‘𝐸) ∈ ( bday ‘𝐹) ∨ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))
17	16	adantr 480	. . 3 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶))) → (( bday ‘𝐸) ∈ ( bday ‘𝐹) ∨ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))
18	2, 4, 6, 8, 10, 12, 14, 15, 17	mulsproplem12 27943	. 2 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
19	3	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ( bday ‘𝐶) = ( bday ‘𝐷)) → 𝐶 ∈ No )
20	5	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ( bday ‘𝐶) = ( bday ‘𝐷)) → 𝐷 ∈ No )
21		simpr 484	. . . 4 ⊢ ((𝜑 ∧ ( bday ‘𝐶) = ( bday ‘𝐷)) → ( bday ‘𝐶) = ( bday ‘𝐷))
22	11	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ( bday ‘𝐶) = ( bday ‘𝐷)) → 𝐶 <s 𝐷)
23		nodense 27541	. . . 4 ⊢ (((𝐶 ∈ No ∧ 𝐷 ∈ No ) ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ 𝐶 <s 𝐷)) → ∃𝑥 ∈ No (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷))
24	19, 20, 21, 22, 23	syl22anc 836	. . 3 ⊢ ((𝜑 ∧ ( bday ‘𝐶) = ( bday ‘𝐷)) → ∃𝑥 ∈ No (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷))
25		unidm 4144	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) = ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))
26		unidm 4144	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = (( bday ‘ 0s ) +no ( bday ‘ 0s ))
27		bday0s 27677	. . . . . . . . . . . . . . . . . 18 ⊢ ( bday ‘ 0s ) = ∅
28	27, 27	oveq12i 7413	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no ∅)
29		0elon 6408	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ On
30		naddrid 8678	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
31	29, 30	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∅ +no ∅) = ∅
32	28, 31	eqtri 2752	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = ∅
33	25, 26, 32	3eqtri 2756	. . . . . . . . . . . . . . 15 ⊢ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) = ∅
34	33	uneq2i 4152	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ ∅)
35		un0 4382	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ ∅) = (( bday ‘𝐶) +no ( bday ‘𝐹))
36	34, 35	eqtri 2752	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = (( bday ‘𝐶) +no ( bday ‘𝐹))
37		ssun1 4164	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))
38		ssun2 4165	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
39	37, 38	sstri 3983	. . . . . . . . . . . . . 14 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐹)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
40		ssun2 4165	. . . . . . . . . . . . . 14 ⊢ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
41	39, 40	sstri 3983	. . . . . . . . . . . . 13 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
42	36, 41	eqsstri 4008	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
43	42	sseli 3970	. . . . . . . . . . 11 ⊢ (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
44	43	imim1i 63	. . . . . . . . . 10 ⊢ ((((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) → (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
45	44	6ralimi 3119	. . . . . . . . 9 ⊢ (∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
46	1, 45	syl 17	. . . . . . . 8 ⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
47	46, 3, 9	mulsproplem11 27942	. . . . . . 7 ⊢ (𝜑 → (𝐶 ·s 𝐹) ∈ No )
48	33	uneq2i 4152	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ ∅)
49		un0 4382	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ ∅) = (( bday ‘𝐶) +no ( bday ‘𝐸))
50	48, 49	eqtri 2752	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = (( bday ‘𝐶) +no ( bday ‘𝐸))
51		ssun1 4164	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹)))
52		ssun1 4164	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
53	51, 52	sstri 3983	. . . . . . . . . . . . . 14 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐸)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
54	53, 40	sstri 3983	. . . . . . . . . . . . 13 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
55	50, 54	eqsstri 4008	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
56	55	sseli 3970	. . . . . . . . . . 11 ⊢ (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
57	56	imim1i 63	. . . . . . . . . 10 ⊢ ((((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) → (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
58	57	6ralimi 3119	. . . . . . . . 9 ⊢ (∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
59	1, 58	syl 17	. . . . . . . 8 ⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
60	59, 3, 7	mulsproplem11 27942	. . . . . . 7 ⊢ (𝜑 → (𝐶 ·s 𝐸) ∈ No )
61	47, 60	subscld 27889	. . . . . 6 ⊢ (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) ∈ No )
62	61	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) ∈ No )
63	46	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
64		simprr1 1218	. . . . . . . . 9 ⊢ ((( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷))) → ( bday ‘𝑥) ∈ ( bday ‘𝐶))
65	64	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ( bday ‘𝑥) ∈ ( bday ‘𝐶))
66		bdayelon 27625	. . . . . . . . 9 ⊢ ( bday ‘𝐶) ∈ On
67		simprrl 778	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝑥 ∈ No )
68		oldbday 27743	. . . . . . . . 9 ⊢ ((( bday ‘𝐶) ∈ On ∧ 𝑥 ∈ No ) → (𝑥 ∈ ( O ‘( bday ‘𝐶)) ↔ ( bday ‘𝑥) ∈ ( bday ‘𝐶)))
69	66, 67, 68	sylancr 586	. . . . . . . 8 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (𝑥 ∈ ( O ‘( bday ‘𝐶)) ↔ ( bday ‘𝑥) ∈ ( bday ‘𝐶)))
70	65, 69	mpbird 257	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝑥 ∈ ( O ‘( bday ‘𝐶)))
71	9	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝐹 ∈ No )
72	63, 70, 71	mulsproplem2 27933	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (𝑥 ·s 𝐹) ∈ No )
73	59	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
74	7	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝐸 ∈ No )
75	73, 70, 74	mulsproplem2 27933	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (𝑥 ·s 𝐸) ∈ No )
76	72, 75	subscld 27889	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((𝑥 ·s 𝐹) -s (𝑥 ·s 𝐸)) ∈ No )
77	33	uneq2i 4152	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐷) +no ( bday ‘𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = ((( bday ‘𝐷) +no ( bday ‘𝐹)) ∪ ∅)
78		un0 4382	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐷) +no ( bday ‘𝐹)) ∪ ∅) = (( bday ‘𝐷) +no ( bday ‘𝐹))
79	77, 78	eqtri 2752	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝐷) +no ( bday ‘𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = (( bday ‘𝐷) +no ( bday ‘𝐹))
80		ssun2 4165	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹)))
81	80, 52	sstri 3983	. . . . . . . . . . . . . 14 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐹)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
82	81, 40	sstri 3983	. . . . . . . . . . . . 13 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
83	79, 82	eqsstri 4008	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝐷) +no ( bday ‘𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
84	83	sseli 3970	. . . . . . . . . . 11 ⊢ (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐷) +no ( bday ‘𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
85	84	imim1i 63	. . . . . . . . . 10 ⊢ ((((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) → (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐷) +no ( bday ‘𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
86	85	6ralimi 3119	. . . . . . . . 9 ⊢ (∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐷) +no ( bday ‘𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
87	1, 86	syl 17	. . . . . . . 8 ⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐷) +no ( bday ‘𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
88	87, 5, 9	mulsproplem11 27942	. . . . . . 7 ⊢ (𝜑 → (𝐷 ·s 𝐹) ∈ No )
89	33	uneq2i 4152	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐷) +no ( bday ‘𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = ((( bday ‘𝐷) +no ( bday ‘𝐸)) ∪ ∅)
90		un0 4382	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐷) +no ( bday ‘𝐸)) ∪ ∅) = (( bday ‘𝐷) +no ( bday ‘𝐸))
91	89, 90	eqtri 2752	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝐷) +no ( bday ‘𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = (( bday ‘𝐷) +no ( bday ‘𝐸))
92		ssun2 4165	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))
93	92, 38	sstri 3983	. . . . . . . . . . . . . 14 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐸)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
94	93, 40	sstri 3983	. . . . . . . . . . . . 13 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
95	91, 94	eqsstri 4008	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝐷) +no ( bday ‘𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
96	95	sseli 3970	. . . . . . . . . . 11 ⊢ (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐷) +no ( bday ‘𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
97	96	imim1i 63	. . . . . . . . . 10 ⊢ ((((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) → (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐷) +no ( bday ‘𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
98	97	6ralimi 3119	. . . . . . . . 9 ⊢ (∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐷) +no ( bday ‘𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
99	1, 98	syl 17	. . . . . . . 8 ⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐷) +no ( bday ‘𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
100	99, 5, 7	mulsproplem11 27942	. . . . . . 7 ⊢ (𝜑 → (𝐷 ·s 𝐸) ∈ No )
101	88, 100	subscld 27889	. . . . . 6 ⊢ (𝜑 → ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)) ∈ No )
102	101	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)) ∈ No )
103	1	mulsproplemcbv 27931	. . . . . . . 8 ⊢ (𝜑 → ∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
104	103	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
105		onelss 6396	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝐶) ∈ On → (( bday ‘𝑥) ∈ ( bday ‘𝐶) → ( bday ‘𝑥) ⊆ ( bday ‘𝐶)))
106	66, 65, 105	mpsyl 68	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ( bday ‘𝑥) ⊆ ( bday ‘𝐶))
107		simprl 768	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ( bday ‘𝐶) = ( bday ‘𝐷))
108	106, 107	sseqtrd 4014	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ( bday ‘𝑥) ⊆ ( bday ‘𝐷))
109		bdayelon 27625	. . . . . . . . . . . . . . 15 ⊢ ( bday ‘𝑥) ∈ On
110		bdayelon 27625	. . . . . . . . . . . . . . 15 ⊢ ( bday ‘𝐷) ∈ On
111		bdayelon 27625	. . . . . . . . . . . . . . 15 ⊢ ( bday ‘𝐹) ∈ On
112		naddss1 8684	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝑥) ∈ On ∧ ( bday ‘𝐷) ∈ On ∧ ( bday ‘𝐹) ∈ On) → (( bday ‘𝑥) ⊆ ( bday ‘𝐷) ↔ (( bday ‘𝑥) +no ( bday ‘𝐹)) ⊆ (( bday ‘𝐷) +no ( bday ‘𝐹))))
113	109, 110, 111, 112	mp3an 1457	. . . . . . . . . . . . . 14 ⊢ (( bday ‘𝑥) ⊆ ( bday ‘𝐷) ↔ (( bday ‘𝑥) +no ( bday ‘𝐹)) ⊆ (( bday ‘𝐷) +no ( bday ‘𝐹)))
114	108, 113	sylib 217	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (( bday ‘𝑥) +no ( bday ‘𝐹)) ⊆ (( bday ‘𝐷) +no ( bday ‘𝐹)))
115		unss2 4173	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑥) +no ( bday ‘𝐹)) ⊆ (( bday ‘𝐷) +no ( bday ‘𝐹)) → ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐹))) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))))
116	114, 115	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐹))) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))))
117		bdayelon 27625	. . . . . . . . . . . . . . 15 ⊢ ( bday ‘𝐸) ∈ On
118		naddss1 8684	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝑥) ∈ On ∧ ( bday ‘𝐷) ∈ On ∧ ( bday ‘𝐸) ∈ On) → (( bday ‘𝑥) ⊆ ( bday ‘𝐷) ↔ (( bday ‘𝑥) +no ( bday ‘𝐸)) ⊆ (( bday ‘𝐷) +no ( bday ‘𝐸))))
119	109, 110, 117, 118	mp3an 1457	. . . . . . . . . . . . . 14 ⊢ (( bday ‘𝑥) ⊆ ( bday ‘𝐷) ↔ (( bday ‘𝑥) +no ( bday ‘𝐸)) ⊆ (( bday ‘𝐷) +no ( bday ‘𝐸)))
120	108, 119	sylib 217	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (( bday ‘𝑥) +no ( bday ‘𝐸)) ⊆ (( bday ‘𝐷) +no ( bday ‘𝐸)))
121		unss2 4173	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑥) +no ( bday ‘𝐸)) ⊆ (( bday ‘𝐷) +no ( bday ‘𝐸)) → ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐸))) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
122	120, 121	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐸))) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
123		unss12 4174	. . . . . . . . . . . 12 ⊢ ((((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐹))) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∧ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐸))) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))) → (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐸)))) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
124	116, 122, 123	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐸)))) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
125		unss2 4173	. . . . . . . . . . 11 ⊢ ((((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐸)))) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))) → ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐸))))) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
126	124, 125	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐸))))) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
127	126	sseld 3973	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐸))))) → ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))))
128	127	imim1d 82	. . . . . . . 8 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))) → (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))))
129	128	ralimd6v 3200	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))) → ∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))))
130	104, 129	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝑥) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
131	3	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝐶 ∈ No )
132		simprr2 1219	. . . . . . 7 ⊢ ((( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷))) → 𝐶 <s 𝑥)
133	132	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝐶 <s 𝑥)
134	13	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝐸 <s 𝐹)
135	65	olcd 871	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (( bday ‘𝐶) ∈ ( bday ‘𝑥) ∨ ( bday ‘𝑥) ∈ ( bday ‘𝐶)))
136	16	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (( bday ‘𝐸) ∈ ( bday ‘𝐹) ∨ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))
137	130, 131, 67, 74, 71, 133, 134, 135, 136	mulsproplem12 27943	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝑥 ·s 𝐹) -s (𝑥 ·s 𝐸)))
138		naddss1 8684	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝑥) ∈ On ∧ ( bday ‘𝐶) ∈ On ∧ ( bday ‘𝐸) ∈ On) → (( bday ‘𝑥) ⊆ ( bday ‘𝐶) ↔ (( bday ‘𝑥) +no ( bday ‘𝐸)) ⊆ (( bday ‘𝐶) +no ( bday ‘𝐸))))
139	109, 66, 117, 138	mp3an 1457	. . . . . . . . . . . . . 14 ⊢ (( bday ‘𝑥) ⊆ ( bday ‘𝐶) ↔ (( bday ‘𝑥) +no ( bday ‘𝐸)) ⊆ (( bday ‘𝐶) +no ( bday ‘𝐸)))
140	106, 139	sylib 217	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (( bday ‘𝑥) +no ( bday ‘𝐸)) ⊆ (( bday ‘𝐶) +no ( bday ‘𝐸)))
141		unss1 4171	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑥) +no ( bday ‘𝐸)) ⊆ (( bday ‘𝐶) +no ( bday ‘𝐸)) → ((( bday ‘𝑥) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))))
142	140, 141	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((( bday ‘𝑥) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))))
143		naddss1 8684	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝑥) ∈ On ∧ ( bday ‘𝐶) ∈ On ∧ ( bday ‘𝐹) ∈ On) → (( bday ‘𝑥) ⊆ ( bday ‘𝐶) ↔ (( bday ‘𝑥) +no ( bday ‘𝐹)) ⊆ (( bday ‘𝐶) +no ( bday ‘𝐹))))
144	109, 66, 111, 143	mp3an 1457	. . . . . . . . . . . . . 14 ⊢ (( bday ‘𝑥) ⊆ ( bday ‘𝐶) ↔ (( bday ‘𝑥) +no ( bday ‘𝐹)) ⊆ (( bday ‘𝐶) +no ( bday ‘𝐹)))
145	106, 144	sylib 217	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (( bday ‘𝑥) +no ( bday ‘𝐹)) ⊆ (( bday ‘𝐶) +no ( bday ‘𝐹)))
146		unss1 4171	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑥) +no ( bday ‘𝐹)) ⊆ (( bday ‘𝐶) +no ( bday ‘𝐹)) → ((( bday ‘𝑥) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
147	145, 146	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((( bday ‘𝑥) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
148		unss12 4174	. . . . . . . . . . . 12 ⊢ ((((( bday ‘𝑥) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∧ ((( bday ‘𝑥) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))) → (((( bday ‘𝑥) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝑥) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
149	142, 147, 148	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (((( bday ‘𝑥) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝑥) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
150		unss2 4173	. . . . . . . . . . 11 ⊢ ((((( bday ‘𝑥) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝑥) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))) → ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝑥) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝑥) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
151	149, 150	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝑥) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝑥) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
152	151	sseld 3973	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝑥) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝑥) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))))
153	152	imim1d 82	. . . . . . . 8 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))) → (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝑥) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝑥) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))))
154	153	ralimd6v 3200	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))) → ∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝑥) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝑥) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))))
155	104, 154	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝑥) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝑥) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
156	5	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝐷 ∈ No )
157		simprr3 1220	. . . . . . 7 ⊢ ((( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷))) → 𝑥 <s 𝐷)
158	157	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝑥 <s 𝐷)
159	65, 107	eleqtrd 2827	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ( bday ‘𝑥) ∈ ( bday ‘𝐷))
160	159	orcd 870	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (( bday ‘𝑥) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝑥)))
161	155, 67, 156, 74, 71, 158, 134, 160, 136	mulsproplem12 27943	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((𝑥 ·s 𝐹) -s (𝑥 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
162	62, 76, 102, 137, 161	slttrd 27608	. . . 4 ⊢ ((𝜑 ∧ (( bday ‘𝐶) = ( bday ‘𝐷) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
163	162	anassrs 467	. . 3 ⊢ (((𝜑 ∧ ( bday ‘𝐶) = ( bday ‘𝐷)) ∧ (𝑥 ∈ No ∧ (( bday ‘𝑥) ∈ ( bday ‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
164	24, 163	rexlimddv 3153	. 2 ⊢ ((𝜑 ∧ ( bday ‘𝐶) = ( bday ‘𝐷)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
165	66	onordi 6465	. . . . 5 ⊢ Ord ( bday ‘𝐶)
166	110	onordi 6465	. . . . 5 ⊢ Ord ( bday ‘𝐷)
167		ordtri3or 6386	. . . . 5 ⊢ ((Ord ( bday ‘𝐶) ∧ Ord ( bday ‘𝐷)) → (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐶) = ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶)))
168	165, 166, 167	mp2an 689	. . . 4 ⊢ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐶) = ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶))
169		df-3or 1085	. . . . 5 ⊢ ((( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐶) = ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) ↔ ((( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐶) = ( bday ‘𝐷)) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶)))
170		or32 922	. . . . 5 ⊢ (((( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐶) = ( bday ‘𝐷)) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) ↔ ((( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) ∨ ( bday ‘𝐶) = ( bday ‘𝐷)))
171	169, 170	bitri 275	. . . 4 ⊢ ((( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐶) = ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) ↔ ((( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) ∨ ( bday ‘𝐶) = ( bday ‘𝐷)))
172	168, 171	mpbi 229	. . 3 ⊢ ((( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) ∨ ( bday ‘𝐶) = ( bday ‘𝐷))
173	172	a1i 11	. 2 ⊢ (𝜑 → ((( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) ∨ ( bday ‘𝐶) = ( bday ‘𝐷)))
174	18, 164, 173	mpjaodan 955	1 ⊢ (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   ∨ w3o 1083   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  ∀wral 3053  ∃wrex 3062   ∪ cun 3938   ⊆ wss 3940  ∅c0 4314   class class class wbr 5138  Ord word 6353  Oncon0 6354  ‘cfv 6533  (class class class)co 7401   +no cnadd 8660   No csur 27489   <s cslt 27490   bday cbday 27491   0_s c0s 27671   O cold 27686   -_s csubs 27849   ·_s cmuls 27922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-ot 4629  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-1o 8461  df-2o 8462  df-nadd 8661  df-no 27492  df-slt 27493  df-bday 27494  df-sle 27594  df-sslt 27630  df-scut 27632  df-0s 27673  df-made 27690  df-old 27691  df-left 27693  df-right 27694  df-norec 27771  df-norec2 27782  df-adds 27793  df-negs 27850  df-subs 27851  df-muls 27923

This theorem is referenced by:  mulsproplem14  27945