MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulsproplem13 Structured version   Visualization version   GIF version

Theorem mulsproplem13 28168
Description: Lemma for surreal multiplication. Remove the restriction on 𝐶 and 𝐷 from mulsproplem12 28167. (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.
StepHypRef 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 𝑒))))))
21adantr 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 )
43adantr 480 . . 3 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → 𝐶 No )
5 mulsproplem.3 . . . 4 (𝜑𝐷 No )
65adantr 480 . . 3 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → 𝐷 No )
7 mulsproplem.4 . . . 4 (𝜑𝐸 No )
87adantr 480 . . 3 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → 𝐸 No )
9 mulsproplem.5 . . . 4 (𝜑𝐹 No )
109adantr 480 . . 3 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → 𝐹 No )
11 mulsproplem.6 . . . 4 (𝜑𝐶 <s 𝐷)
1211adantr 480 . . 3 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → 𝐶 <s 𝐷)
13 mulsproplem.7 . . . 4 (𝜑𝐸 <s 𝐹)
1413adantr 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 𝐸)))
1716adantr 480 . . 3 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)))
182, 4, 6, 8, 10, 12, 14, 15, 17mulsproplem12 28167 . 2 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
193adantr 480 . . . 4 ((𝜑 ∧ ( bday 𝐶) = ( bday 𝐷)) → 𝐶 No )
205adantr 480 . . . 4 ((𝜑 ∧ ( bday 𝐶) = ( bday 𝐷)) → 𝐷 No )
21 simpr 484 . . . 4 ((𝜑 ∧ ( bday 𝐶) = ( bday 𝐷)) → ( bday 𝐶) = ( bday 𝐷))
2211adantr 480 . . . 4 ((𝜑 ∧ ( bday 𝐶) = ( bday 𝐷)) → 𝐶 <s 𝐷)
23 nodense 27751 . . . 4 (((𝐶 No 𝐷 No ) ∧ (( bday 𝐶) = ( bday 𝐷) ∧ 𝐶 <s 𝐷)) → ∃𝑥 No (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷))
2419, 20, 21, 22, 23syl22anc 839 . . 3 ((𝜑 ∧ ( bday 𝐶) = ( bday 𝐷)) → ∃𝑥 No (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷))
25 unidm 4166 . . . . . . . . . . . . . . . 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 4166 . . . . . . . . . . . . . . . 16 ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = (( bday ‘ 0s ) +no ( bday ‘ 0s ))
27 bday0s 27887 . . . . . . . . . . . . . . . . . 18 ( bday ‘ 0s ) = ∅
2827, 27oveq12i 7442 . . . . . . . . . . . . . . . . 17 (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no ∅)
29 0elon 6439 . . . . . . . . . . . . . . . . . 18 ∅ ∈ On
30 naddrid 8719 . . . . . . . . . . . . . . . . . 18 (∅ ∈ On → (∅ +no ∅) = ∅)
3129, 30ax-mp 5 . . . . . . . . . . . . . . . . 17 (∅ +no ∅) = ∅
3228, 31eqtri 2762 . . . . . . . . . . . . . . . 16 (( bday ‘ 0s ) +no ( bday ‘ 0s )) = ∅
3325, 26, 323eqtri 2766 . . . . . . . . . . . . . . 15 (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) = ∅
3433uneq2i 4174 . . . . . . . . . . . . . 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 4399 . . . . . . . . . . . . . 14 ((( bday 𝐶) +no ( bday 𝐹)) ∪ ∅) = (( bday 𝐶) +no ( bday 𝐹))
3634, 35eqtri 2762 . . . . . . . . . . . . 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 4187 . . . . . . . . . . . . . . 15 (( bday 𝐶) +no ( bday 𝐹)) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))
38 ssun2 4188 . . . . . . . . . . . . . . 15 ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
3937, 38sstri 4004 . . . . . . . . . . . . . 14 (( bday 𝐶) +no ( bday 𝐹)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
40 ssun2 4188 . . . . . . . . . . . . . 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 𝐸)))))
4139, 40sstri 4004 . . . . . . . . . . . . 13 (( bday 𝐶) +no ( bday 𝐹)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
4236, 41eqsstri 4029 . . . . . . . . . . . 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 𝐸)))))
4342sseli 3990 . . . . . . . . . . 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 𝐸))))))
4443imim1i 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 𝑒))))))
45446ralimi 3124 . . . . . . . . 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 𝑒))))))
461, 45syl 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 𝑒))))))
4746, 3, 9mulsproplem11 28166 . . . . . . 7 (𝜑 → (𝐶 ·s 𝐹) ∈ No )
4833uneq2i 4174 . . . . . . . . . . . . . 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 4399 . . . . . . . . . . . . . 14 ((( bday 𝐶) +no ( bday 𝐸)) ∪ ∅) = (( bday 𝐶) +no ( bday 𝐸))
5048, 49eqtri 2762 . . . . . . . . . . . . 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 4187 . . . . . . . . . . . . . . 15 (( bday 𝐶) +no ( bday 𝐸)) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹)))
52 ssun1 4187 . . . . . . . . . . . . . . 15 ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
5351, 52sstri 4004 . . . . . . . . . . . . . 14 (( bday 𝐶) +no ( bday 𝐸)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
5453, 40sstri 4004 . . . . . . . . . . . . 13 (( bday 𝐶) +no ( bday 𝐸)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
5550, 54eqsstri 4029 . . . . . . . . . . . 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 𝐸)))))
5655sseli 3990 . . . . . . . . . . 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 𝐸))))))
5756imim1i 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 𝑒))))))
58576ralimi 3124 . . . . . . . . 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 𝑒))))))
591, 58syl 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 𝑒))))))
6059, 3, 7mulsproplem11 28166 . . . . . . 7 (𝜑 → (𝐶 ·s 𝐸) ∈ No )
6147, 60subscld 28107 . . . . . 6 (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) ∈ No )
6261adantr 480 . . . . 5 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) ∈ No )
6346adantr 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 1220 . . . . . . . . 9 ((( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷))) → ( bday 𝑥) ∈ ( bday 𝐶))
6564adantl 481 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ( bday 𝑥) ∈ ( bday 𝐶))
66 bdayelon 27835 . . . . . . . . 9 ( bday 𝐶) ∈ On
67 simprrl 781 . . . . . . . . 9 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝑥 No )
68 oldbday 27953 . . . . . . . . 9 ((( bday 𝐶) ∈ On ∧ 𝑥 No ) → (𝑥 ∈ ( O ‘( bday 𝐶)) ↔ ( bday 𝑥) ∈ ( bday 𝐶)))
6966, 67, 68sylancr 587 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (𝑥 ∈ ( O ‘( bday 𝐶)) ↔ ( bday 𝑥) ∈ ( bday 𝐶)))
7065, 69mpbird 257 . . . . . . 7 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝑥 ∈ ( O ‘( bday 𝐶)))
719adantr 480 . . . . . . 7 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝐹 No )
7263, 70, 71mulsproplem2 28157 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (𝑥 ·s 𝐹) ∈ No )
7359adantr 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 𝑒))))))
747adantr 480 . . . . . . 7 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝐸 No )
7573, 70, 74mulsproplem2 28157 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (𝑥 ·s 𝐸) ∈ No )
7672, 75subscld 28107 . . . . 5 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((𝑥 ·s 𝐹) -s (𝑥 ·s 𝐸)) ∈ No )
7733uneq2i 4174 . . . . . . . . . . . . . 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 4399 . . . . . . . . . . . . . 14 ((( bday 𝐷) +no ( bday 𝐹)) ∪ ∅) = (( bday 𝐷) +no ( bday 𝐹))
7977, 78eqtri 2762 . . . . . . . . . . . . 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 4188 . . . . . . . . . . . . . . 15 (( bday 𝐷) +no ( bday 𝐹)) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹)))
8180, 52sstri 4004 . . . . . . . . . . . . . 14 (( bday 𝐷) +no ( bday 𝐹)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
8281, 40sstri 4004 . . . . . . . . . . . . 13 (( bday 𝐷) +no ( bday 𝐹)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
8379, 82eqsstri 4029 . . . . . . . . . . . 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 𝐸)))))
8483sseli 3990 . . . . . . . . . . 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 𝐸))))))
8584imim1i 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 𝑒))))))
86856ralimi 3124 . . . . . . . . 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 𝑒))))))
871, 86syl 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 𝑒))))))
8887, 5, 9mulsproplem11 28166 . . . . . . 7 (𝜑 → (𝐷 ·s 𝐹) ∈ No )
8933uneq2i 4174 . . . . . . . . . . . . . 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 4399 . . . . . . . . . . . . . 14 ((( bday 𝐷) +no ( bday 𝐸)) ∪ ∅) = (( bday 𝐷) +no ( bday 𝐸))
9189, 90eqtri 2762 . . . . . . . . . . . . 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 4188 . . . . . . . . . . . . . . 15 (( bday 𝐷) +no ( bday 𝐸)) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))
9392, 38sstri 4004 . . . . . . . . . . . . . 14 (( bday 𝐷) +no ( bday 𝐸)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
9493, 40sstri 4004 . . . . . . . . . . . . 13 (( bday 𝐷) +no ( bday 𝐸)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
9591, 94eqsstri 4029 . . . . . . . . . . . 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 𝐸)))))
9695sseli 3990 . . . . . . . . . . 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 𝐸))))))
9796imim1i 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 𝑒))))))
98976ralimi 3124 . . . . . . . . 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 𝑒))))))
991, 98syl 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 𝑒))))))
10099, 5, 7mulsproplem11 28166 . . . . . . 7 (𝜑 → (𝐷 ·s 𝐸) ∈ No )
10188, 100subscld 28107 . . . . . 6 (𝜑 → ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)) ∈ No )
102101adantr 480 . . . . 5 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)) ∈ No )
1031mulsproplemcbv 28155 . . . . . . . 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 𝑘))))))
104103adantr 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 6427 . . . . . . . . . . . . . . . 16 (( bday 𝐶) ∈ On → (( bday 𝑥) ∈ ( bday 𝐶) → ( bday 𝑥) ⊆ ( bday 𝐶)))
10666, 65, 105mpsyl 68 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ( bday 𝑥) ⊆ ( bday 𝐶))
107 simprl 771 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ( bday 𝐶) = ( bday 𝐷))
108106, 107sseqtrd 4035 . . . . . . . . . . . . . 14 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ( bday 𝑥) ⊆ ( bday 𝐷))
109 bdayelon 27835 . . . . . . . . . . . . . . 15 ( bday 𝑥) ∈ On
110 bdayelon 27835 . . . . . . . . . . . . . . 15 ( bday 𝐷) ∈ On
111 bdayelon 27835 . . . . . . . . . . . . . . 15 ( bday 𝐹) ∈ On
112 naddss1 8725 . . . . . . . . . . . . . . 15 ((( bday 𝑥) ∈ On ∧ ( bday 𝐷) ∈ On ∧ ( bday 𝐹) ∈ On) → (( bday 𝑥) ⊆ ( bday 𝐷) ↔ (( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐷) +no ( bday 𝐹))))
113109, 110, 111, 112mp3an 1460 . . . . . . . . . . . . . 14 (( bday 𝑥) ⊆ ( bday 𝐷) ↔ (( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐷) +no ( bday 𝐹)))
114108, 113sylib 218 . . . . . . . . . . . . 13 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐷) +no ( bday 𝐹)))
115 unss2 4196 . . . . . . . . . . . . 13 ((( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐷) +no ( bday 𝐹)) → ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝑥) +no ( bday 𝐹))) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))))
116114, 115syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝑥) +no ( bday 𝐹))) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))))
117 bdayelon 27835 . . . . . . . . . . . . . . 15 ( bday 𝐸) ∈ On
118 naddss1 8725 . . . . . . . . . . . . . . 15 ((( bday 𝑥) ∈ On ∧ ( bday 𝐷) ∈ On ∧ ( bday 𝐸) ∈ On) → (( bday 𝑥) ⊆ ( bday 𝐷) ↔ (( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐷) +no ( bday 𝐸))))
119109, 110, 117, 118mp3an 1460 . . . . . . . . . . . . . 14 (( bday 𝑥) ⊆ ( bday 𝐷) ↔ (( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐷) +no ( bday 𝐸)))
120108, 119sylib 218 . . . . . . . . . . . . 13 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐷) +no ( bday 𝐸)))
121 unss2 4196 . . . . . . . . . . . . 13 ((( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐷) +no ( bday 𝐸)) → ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝑥) +no ( bday 𝐸))) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
122120, 121syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝑥) +no ( bday 𝐸))) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
123 unss12 4197 . . . . . . . . . . . 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 𝐸)))))
124116, 122, 123syl2anc 584 . . . . . . . . . . 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 4196 . . . . . . . . . . 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 𝐸))))))
126124, 125syl 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 𝐸))))))
127126sseld 3993 . . . . . . . . 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 𝐸)))))))
128127imim1d 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 𝑘)))))))
129128ralimd6v 3207 . . . . . . 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 𝑘)))))))
130104, 129mpd 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 𝑘))))))
1313adantr 480 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝐶 No )
132 simprr2 1221 . . . . . . 7 ((( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷))) → 𝐶 <s 𝑥)
133132adantl 481 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝐶 <s 𝑥)
13413adantr 480 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝐸 <s 𝐹)
13565olcd 874 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (( bday 𝐶) ∈ ( bday 𝑥) ∨ ( bday 𝑥) ∈ ( bday 𝐶)))
13616adantr 480 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)))
137130, 131, 67, 74, 71, 133, 134, 135, 136mulsproplem12 28167 . . . . 5 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝑥 ·s 𝐹) -s (𝑥 ·s 𝐸)))
138 naddss1 8725 . . . . . . . . . . . . . . 15 ((( bday 𝑥) ∈ On ∧ ( bday 𝐶) ∈ On ∧ ( bday 𝐸) ∈ On) → (( bday 𝑥) ⊆ ( bday 𝐶) ↔ (( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐶) +no ( bday 𝐸))))
139109, 66, 117, 138mp3an 1460 . . . . . . . . . . . . . 14 (( bday 𝑥) ⊆ ( bday 𝐶) ↔ (( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐶) +no ( bday 𝐸)))
140106, 139sylib 218 . . . . . . . . . . . . 13 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐶) +no ( bday 𝐸)))
141 unss1 4194 . . . . . . . . . . . . 13 ((( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐶) +no ( bday 𝐸)) → ((( bday 𝑥) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))))
142140, 141syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((( bday 𝑥) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))))
143 naddss1 8725 . . . . . . . . . . . . . . 15 ((( bday 𝑥) ∈ On ∧ ( bday 𝐶) ∈ On ∧ ( bday 𝐹) ∈ On) → (( bday 𝑥) ⊆ ( bday 𝐶) ↔ (( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐶) +no ( bday 𝐹))))
144109, 66, 111, 143mp3an 1460 . . . . . . . . . . . . . 14 (( bday 𝑥) ⊆ ( bday 𝐶) ↔ (( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐶) +no ( bday 𝐹)))
145106, 144sylib 218 . . . . . . . . . . . . 13 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐶) +no ( bday 𝐹)))
146 unss1 4194 . . . . . . . . . . . . 13 ((( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐶) +no ( bday 𝐹)) → ((( bday 𝑥) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
147145, 146syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((( bday 𝑥) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
148 unss12 4197 . . . . . . . . . . . 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 𝐸)))))
149142, 147, 148syl2anc 584 . . . . . . . . . . 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 4196 . . . . . . . . . . 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 𝐸))))))
151149, 150syl 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 𝐸))))))
152151sseld 3993 . . . . . . . . 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 𝐸)))))))
153152imim1d 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 𝑘)))))))
154153ralimd6v 3207 . . . . . . 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 𝑘)))))))
155104, 154mpd 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 𝑘))))))
1565adantr 480 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝐷 No )
157 simprr3 1222 . . . . . . 7 ((( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷))) → 𝑥 <s 𝐷)
158157adantl 481 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝑥 <s 𝐷)
15965, 107eleqtrd 2840 . . . . . . 7 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ( bday 𝑥) ∈ ( bday 𝐷))
160159orcd 873 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (( bday 𝑥) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝑥)))
161155, 67, 156, 74, 71, 158, 134, 160, 136mulsproplem12 28167 . . . . 5 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((𝑥 ·s 𝐹) -s (𝑥 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
16262, 76, 102, 137, 161slttrd 27818 . . . 4 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
163162anassrs 467 . . 3 (((𝜑 ∧ ( bday 𝐶) = ( bday 𝐷)) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
16424, 163rexlimddv 3158 . 2 ((𝜑 ∧ ( bday 𝐶) = ( bday 𝐷)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
16566onordi 6496 . . . . 5 Ord ( bday 𝐶)
166110onordi 6496 . . . . 5 Ord ( bday 𝐷)
167 ordtri3or 6417 . . . . 5 ((Ord ( bday 𝐶) ∧ Ord ( bday 𝐷)) → (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐶) = ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)))
168165, 166, 167mp2an 692 . . . 4 (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐶) = ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))
169 df-3or 1087 . . . . 5 ((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐶) = ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)) ↔ ((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐶) = ( bday 𝐷)) ∨ ( bday 𝐷) ∈ ( bday 𝐶)))
170 or32 925 . . . . 5 (((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐶) = ( bday 𝐷)) ∨ ( bday 𝐷) ∈ ( bday 𝐶)) ↔ ((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)) ∨ ( bday 𝐶) = ( bday 𝐷)))
171169, 170bitri 275 . . . 4 ((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐶) = ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)) ↔ ((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)) ∨ ( bday 𝐶) = ( bday 𝐷)))
172168, 171mpbi 230 . . 3 ((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)) ∨ ( bday 𝐶) = ( bday 𝐷))
173172a1i 11 . 2 (𝜑 → ((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)) ∨ ( bday 𝐶) = ( bday 𝐷)))
17418, 164, 173mpjaodan 960 1 (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 847  w3o 1085  w3a 1086   = wceq 1536  wcel 2105  wral 3058  wrex 3067  cun 3960  wss 3962  c0 4338   class class class wbr 5147  Ord word 6384  Oncon0 6385  cfv 6562  (class class class)co 7430   +no cnadd 8701   No csur 27698   <s cslt 27699   bday cbday 27700   0s c0s 27881   O cold 27896   -s csubs 28066   ·s cmuls 28146
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-ot 4639  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-1o 8504  df-2o 8505  df-nadd 8702  df-no 27701  df-slt 27702  df-bday 27703  df-sle 27804  df-sslt 27840  df-scut 27842  df-0s 27883  df-made 27900  df-old 27901  df-left 27903  df-right 27904  df-norec 27985  df-norec2 27996  df-adds 28007  df-negs 28067  df-subs 28068  df-muls 28147
This theorem is referenced by:  mulsproplem14  28169
  Copyright terms: Public domain W3C validator