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

Theorem mulsproplem14 27514
Description: Lemma for surreal multiplication. Finally, we remove the restriction on 𝐸 and 𝐹 from mulsproplem12 27512 and mulsproplem13 27513. This completes the induction on surreal multiplication. mulsprop 27515 brings all this together technically. (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 𝐹)
Assertion
Ref Expression
mulsproplem14 (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓
Allowed substitution hints:   𝜑(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)

Proof of Theorem mulsproplem14
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 481 . . 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 481 . . 3 ((𝜑 ∧ (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐶 No )
5 mulsproplem.3 . . . 4 (𝜑𝐷 No )
65adantr 481 . . 3 ((𝜑 ∧ (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐷 No )
7 mulsproplem.4 . . . 4 (𝜑𝐸 No )
87adantr 481 . . 3 ((𝜑 ∧ (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐸 No )
9 mulsproplem.5 . . . 4 (𝜑𝐹 No )
109adantr 481 . . 3 ((𝜑 ∧ (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐹 No )
11 mulsproplem.6 . . . 4 (𝜑𝐶 <s 𝐷)
1211adantr 481 . . 3 ((𝜑 ∧ (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐶 <s 𝐷)
13 mulsproplem.7 . . . 4 (𝜑𝐸 <s 𝐹)
1413adantr 481 . . 3 ((𝜑 ∧ (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐸 <s 𝐹)
15 simpr 485 . . 3 ((𝜑 ∧ (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸))) → (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)))
162, 4, 6, 8, 10, 12, 14, 15mulsproplem13 27513 . 2 ((𝜑 ∧ (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
177adantr 481 . . . 4 ((𝜑 ∧ ( bday 𝐸) = ( bday 𝐹)) → 𝐸 No )
189adantr 481 . . . 4 ((𝜑 ∧ ( bday 𝐸) = ( bday 𝐹)) → 𝐹 No )
19 simpr 485 . . . 4 ((𝜑 ∧ ( bday 𝐸) = ( bday 𝐹)) → ( bday 𝐸) = ( bday 𝐹))
2013adantr 481 . . . 4 ((𝜑 ∧ ( bday 𝐸) = ( bday 𝐹)) → 𝐸 <s 𝐹)
21 nodense 27124 . . . 4 (((𝐸 No 𝐹 No ) ∧ (( bday 𝐸) = ( bday 𝐹) ∧ 𝐸 <s 𝐹)) → ∃𝑥 No (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹))
2217, 18, 19, 20, 21syl22anc 837 . . 3 ((𝜑 ∧ ( bday 𝐸) = ( bday 𝐹)) → ∃𝑥 No (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹))
23 unidm 4149 . . . . . . . . . . . . . . . . 17 (((( 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 )))
24 unidm 4149 . . . . . . . . . . . . . . . . 17 ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = (( bday ‘ 0s ) +no ( bday ‘ 0s ))
25 bday0s 27258 . . . . . . . . . . . . . . . . . . 19 ( bday ‘ 0s ) = ∅
2625, 25oveq12i 7406 . . . . . . . . . . . . . . . . . 18 (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no ∅)
27 0elon 6408 . . . . . . . . . . . . . . . . . . 19 ∅ ∈ On
28 naddrid 8667 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ On → (∅ +no ∅) = ∅)
2927, 28ax-mp 5 . . . . . . . . . . . . . . . . . 18 (∅ +no ∅) = ∅
3026, 29eqtri 2760 . . . . . . . . . . . . . . . . 17 (( bday ‘ 0s ) +no ( bday ‘ 0s )) = ∅
3123, 24, 303eqtri 2764 . . . . . . . . . . . . . . . 16 (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) = ∅
3231uneq2i 4157 . . . . . . . . . . . . . . 15 ((( 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 𝐸)) ∪ ∅)
33 un0 4387 . . . . . . . . . . . . . . 15 ((( bday 𝐷) +no ( bday 𝐸)) ∪ ∅) = (( bday 𝐷) +no ( bday 𝐸))
3432, 33eqtri 2760 . . . . . . . . . . . . . 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 ssun2 4170 . . . . . . . . . . . . . . . 16 (( bday 𝐷) +no ( bday 𝐸)) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))
36 ssun2 4170 . . . . . . . . . . . . . . . 16 ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
3735, 36sstri 3988 . . . . . . . . . . . . . . 15 (( bday 𝐷) +no ( bday 𝐸)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
38 ssun2 4170 . . . . . . . . . . . . . . 15 (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
3937, 38sstri 3988 . . . . . . . . . . . . . 14 (( bday 𝐷) +no ( bday 𝐸)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
4034, 39eqsstri 4013 . . . . . . . . . . . . 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 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
4140sseli 3975 . . . . . . . . . . . 12 (((( 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 𝐸))))))
4241imim1i 63 . . . . . . . . . . 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 𝐸))))) → ((𝑎 ·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 𝑒))))))
43426ralimi 3127 . . . . . . . . . 10 (∀𝑎 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 𝑒))))))
441, 43syl 17 . . . . . . . . 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 ‘ 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 𝑒))))))
4544, 5, 7mulsproplem11 27511 . . . . . . . 8 (𝜑 → (𝐷 ·s 𝐸) ∈ No )
4631uneq2i 4157 . . . . . . . . . . . . . . 15 ((( 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 𝐸)) ∪ ∅)
47 un0 4387 . . . . . . . . . . . . . . 15 ((( bday 𝐶) +no ( bday 𝐸)) ∪ ∅) = (( bday 𝐶) +no ( bday 𝐸))
4846, 47eqtri 2760 . . . . . . . . . . . . . 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 ssun1 4169 . . . . . . . . . . . . . . . 16 (( bday 𝐶) +no ( bday 𝐸)) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹)))
50 ssun1 4169 . . . . . . . . . . . . . . . 16 ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
5149, 50sstri 3988 . . . . . . . . . . . . . . 15 (( bday 𝐶) +no ( bday 𝐸)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
5251, 38sstri 3988 . . . . . . . . . . . . . 14 (( bday 𝐶) +no ( bday 𝐸)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
5348, 52eqsstri 4013 . . . . . . . . . . . . 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 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
5453sseli 3975 . . . . . . . . . . . 12 (((( 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 𝐸))))))
5554imim1i 63 . . . . . . . . . . 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 𝐸))))) → ((𝑎 ·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 𝑒))))))
56556ralimi 3127 . . . . . . . . . 10 (∀𝑎 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 𝑒))))))
571, 56syl 17 . . . . . . . . 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 ‘ 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 𝑒))))))
5857, 3, 7mulsproplem11 27511 . . . . . . . 8 (𝜑 → (𝐶 ·s 𝐸) ∈ No )
5945, 58subscld 27464 . . . . . . 7 (𝜑 → ((𝐷 ·s 𝐸) -s (𝐶 ·s 𝐸)) ∈ No )
6059adantr 481 . . . . . 6 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ((𝐷 ·s 𝐸) -s (𝐶 ·s 𝐸)) ∈ No )
6144adantr 481 . . . . . . . 8 ((𝜑 ∧ (( 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 𝑒))))))
625adantr 481 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → 𝐷 No )
63 simprr1 1221 . . . . . . . . . 10 ((( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹))) → ( bday 𝑥) ∈ ( bday 𝐸))
6463adantl 482 . . . . . . . . 9 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ( bday 𝑥) ∈ ( bday 𝐸))
65 bdayelon 27207 . . . . . . . . . 10 ( bday 𝐸) ∈ On
66 simprrl 779 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → 𝑥 No )
67 oldbday 27324 . . . . . . . . . 10 ((( bday 𝐸) ∈ On ∧ 𝑥 No ) → (𝑥 ∈ ( O ‘( bday 𝐸)) ↔ ( bday 𝑥) ∈ ( bday 𝐸)))
6865, 66, 67sylancr 587 . . . . . . . . 9 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (𝑥 ∈ ( O ‘( bday 𝐸)) ↔ ( bday 𝑥) ∈ ( bday 𝐸)))
6964, 68mpbird 256 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → 𝑥 ∈ ( O ‘( bday 𝐸)))
7061, 62, 69mulsproplem3 27503 . . . . . . 7 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (𝐷 ·s 𝑥) ∈ No )
7157adantr 481 . . . . . . . 8 ((𝜑 ∧ (( 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 𝑒))))))
723adantr 481 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → 𝐶 No )
7371, 72, 69mulsproplem3 27503 . . . . . . 7 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (𝐶 ·s 𝑥) ∈ No )
7470, 73subscld 27464 . . . . . 6 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ((𝐷 ·s 𝑥) -s (𝐶 ·s 𝑥)) ∈ No )
7531uneq2i 4157 . . . . . . . . . . . . . . 15 ((( 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 𝐹)) ∪ ∅)
76 un0 4387 . . . . . . . . . . . . . . 15 ((( bday 𝐷) +no ( bday 𝐹)) ∪ ∅) = (( bday 𝐷) +no ( bday 𝐹))
7775, 76eqtri 2760 . . . . . . . . . . . . . 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 ssun2 4170 . . . . . . . . . . . . . . . 16 (( bday 𝐷) +no ( bday 𝐹)) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹)))
7978, 50sstri 3988 . . . . . . . . . . . . . . 15 (( bday 𝐷) +no ( bday 𝐹)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
8079, 38sstri 3988 . . . . . . . . . . . . . 14 (( bday 𝐷) +no ( bday 𝐹)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
8177, 80eqsstri 4013 . . . . . . . . . . . . 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 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
8281sseli 3975 . . . . . . . . . . . 12 (((( 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 𝐸))))))
8382imim1i 63 . . . . . . . . . . 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 𝐸))))) → ((𝑎 ·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 𝑒))))))
84836ralimi 3127 . . . . . . . . . 10 (∀𝑎 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 𝑒))))))
851, 84syl 17 . . . . . . . . 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 ‘ 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 𝑒))))))
8685, 5, 9mulsproplem11 27511 . . . . . . . 8 (𝜑 → (𝐷 ·s 𝐹) ∈ No )
8731uneq2i 4157 . . . . . . . . . . . . . . 15 ((( 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 𝐹)) ∪ ∅)
88 un0 4387 . . . . . . . . . . . . . . 15 ((( bday 𝐶) +no ( bday 𝐹)) ∪ ∅) = (( bday 𝐶) +no ( bday 𝐹))
8987, 88eqtri 2760 . . . . . . . . . . . . . 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 ssun1 4169 . . . . . . . . . . . . . . . 16 (( bday 𝐶) +no ( bday 𝐹)) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))
9190, 36sstri 3988 . . . . . . . . . . . . . . 15 (( bday 𝐶) +no ( bday 𝐹)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
9291, 38sstri 3988 . . . . . . . . . . . . . 14 (( bday 𝐶) +no ( bday 𝐹)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
9389, 92eqsstri 4013 . . . . . . . . . . . . 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 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
9493sseli 3975 . . . . . . . . . . . 12 (((( 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 𝐸))))))
9594imim1i 63 . . . . . . . . . . 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 𝐸))))) → ((𝑎 ·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 𝑒))))))
96956ralimi 3127 . . . . . . . . . 10 (∀𝑎 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 𝑒))))))
971, 96syl 17 . . . . . . . . 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 ‘ 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 𝑒))))))
9897, 3, 9mulsproplem11 27511 . . . . . . . 8 (𝜑 → (𝐶 ·s 𝐹) ∈ No )
9986, 98subscld 27464 . . . . . . 7 (𝜑 → ((𝐷 ·s 𝐹) -s (𝐶 ·s 𝐹)) ∈ No )
10099adantr 481 . . . . . 6 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ((𝐷 ·s 𝐹) -s (𝐶 ·s 𝐹)) ∈ No )
1011mulsproplemcbv 27500 . . . . . . . . . 10 (𝜑 → ∀𝑔 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 𝑘))))))
102101adantr 481 . . . . . . . . 9 ((𝜑 ∧ (( 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 𝑘))))))
103 onelss 6396 . . . . . . . . . . . . . . . . . 18 (( bday 𝐸) ∈ On → (( bday 𝑥) ∈ ( bday 𝐸) → ( bday 𝑥) ⊆ ( bday 𝐸)))
10465, 64, 103mpsyl 68 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ( bday 𝑥) ⊆ ( bday 𝐸))
105 simprl 769 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ( bday 𝐸) = ( bday 𝐹))
106104, 105sseqtrd 4019 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ( bday 𝑥) ⊆ ( bday 𝐹))
107 bdayelon 27207 . . . . . . . . . . . . . . . . 17 ( bday 𝑥) ∈ On
108 bdayelon 27207 . . . . . . . . . . . . . . . . 17 ( bday 𝐹) ∈ On
109 bdayelon 27207 . . . . . . . . . . . . . . . . 17 ( bday 𝐷) ∈ On
110 naddss2 8674 . . . . . . . . . . . . . . . . 17 ((( bday 𝑥) ∈ On ∧ ( bday 𝐹) ∈ On ∧ ( bday 𝐷) ∈ On) → (( bday 𝑥) ⊆ ( bday 𝐹) ↔ (( bday 𝐷) +no ( bday 𝑥)) ⊆ (( bday 𝐷) +no ( bday 𝐹))))
111107, 108, 109, 110mp3an 1461 . . . . . . . . . . . . . . . 16 (( bday 𝑥) ⊆ ( bday 𝐹) ↔ (( bday 𝐷) +no ( bday 𝑥)) ⊆ (( bday 𝐷) +no ( bday 𝐹)))
112106, 111sylib 217 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (( bday 𝐷) +no ( bday 𝑥)) ⊆ (( bday 𝐷) +no ( bday 𝐹)))
113 unss2 4178 . . . . . . . . . . . . . . 15 ((( bday 𝐷) +no ( bday 𝑥)) ⊆ (( bday 𝐷) +no ( bday 𝐹)) → ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝑥))) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))))
114112, 113syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝑥))) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))))
115 bdayelon 27207 . . . . . . . . . . . . . . . . 17 ( bday 𝐶) ∈ On
116 naddss2 8674 . . . . . . . . . . . . . . . . 17 ((( bday 𝑥) ∈ On ∧ ( bday 𝐹) ∈ On ∧ ( bday 𝐶) ∈ On) → (( bday 𝑥) ⊆ ( bday 𝐹) ↔ (( bday 𝐶) +no ( bday 𝑥)) ⊆ (( bday 𝐶) +no ( bday 𝐹))))
117107, 108, 115, 116mp3an 1461 . . . . . . . . . . . . . . . 16 (( bday 𝑥) ⊆ ( bday 𝐹) ↔ (( bday 𝐶) +no ( bday 𝑥)) ⊆ (( bday 𝐶) +no ( bday 𝐹)))
118106, 117sylib 217 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (( bday 𝐶) +no ( bday 𝑥)) ⊆ (( bday 𝐶) +no ( bday 𝐹)))
119 unss1 4176 . . . . . . . . . . . . . . 15 ((( bday 𝐶) +no ( bday 𝑥)) ⊆ (( bday 𝐶) +no ( bday 𝐹)) → ((( bday 𝐶) +no ( bday 𝑥)) ∪ (( bday 𝐷) +no ( bday 𝐸))) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
120118, 119syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ((( bday 𝐶) +no ( bday 𝑥)) ∪ (( bday 𝐷) +no ( bday 𝐸))) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
121 unss12 4179 . . . . . . . . . . . . . 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 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝑥))) ∪ ((( bday 𝐶) +no ( bday 𝑥)) ∪ (( bday 𝐷) +no ( bday 𝐸)))) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
122114, 120, 121syl2anc 584 . . . . . . . . . . . . 13 ((𝜑 ∧ (( 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 𝐸)))))
123 unss2 4178 . . . . . . . . . . . . 13 ((((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝑥))) ∪ ((( bday 𝐶) +no ( bday 𝑥)) ∪ (( bday 𝐷) +no ( bday 𝐸)))) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))) → ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝑥))) ∪ ((( bday 𝐶) +no ( bday 𝑥)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
124122, 123syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (( 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 𝐸))))))
125124sseld 3978 . . . . . . . . . . 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 𝑥))) ∪ ((( bday 𝐶) +no ( bday 𝑥)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑙))) ∪ ((( bday 𝑖) +no ( bday 𝑙)) ∪ (( bday 𝑗) +no ( bday 𝑘))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))))
126125imim1d 82 . . . . . . . . . 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 𝐸))))) → ((𝑔 ·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 𝑘)))))))
127126ralimd6v 3208 . . . . . . . . 9 ((𝜑 ∧ (( 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 𝑘)))))))
128102, 127mpd 15 . . . . . . . 8 ((𝜑 ∧ (( 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 𝑘))))))
1297adantr 481 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → 𝐸 No )
13011adantr 481 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → 𝐶 <s 𝐷)
131 simprr2 1222 . . . . . . . . 9 ((( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹))) → 𝐸 <s 𝑥)
132131adantl 482 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → 𝐸 <s 𝑥)
13364olcd 872 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (( bday 𝐸) ∈ ( bday 𝑥) ∨ ( bday 𝑥) ∈ ( bday 𝐸)))
134128, 72, 62, 129, 66, 130, 132, 133mulsproplem13 27513 . . . . . . 7 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ((𝐶 ·s 𝑥) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑥) -s (𝐷 ·s 𝐸)))
13545adantr 481 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (𝐷 ·s 𝐸) ∈ No )
13658adantr 481 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (𝐶 ·s 𝐸) ∈ No )
137135, 70, 136, 73sltsubsub3bd 27481 . . . . . . 7 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (((𝐷 ·s 𝐸) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑥) -s (𝐶 ·s 𝑥)) ↔ ((𝐶 ·s 𝑥) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑥) -s (𝐷 ·s 𝐸))))
138134, 137mpbird 256 . . . . . 6 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ((𝐷 ·s 𝐸) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑥) -s (𝐶 ·s 𝑥)))
139 naddss2 8674 . . . . . . . . . . . . . . . . 17 ((( bday 𝑥) ∈ On ∧ ( bday 𝐸) ∈ On ∧ ( bday 𝐶) ∈ On) → (( bday 𝑥) ⊆ ( bday 𝐸) ↔ (( bday 𝐶) +no ( bday 𝑥)) ⊆ (( bday 𝐶) +no ( bday 𝐸))))
140107, 65, 115, 139mp3an 1461 . . . . . . . . . . . . . . . 16 (( bday 𝑥) ⊆ ( bday 𝐸) ↔ (( bday 𝐶) +no ( bday 𝑥)) ⊆ (( bday 𝐶) +no ( bday 𝐸)))
141104, 140sylib 217 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (( bday 𝐶) +no ( bday 𝑥)) ⊆ (( bday 𝐶) +no ( bday 𝐸)))
142 unss1 4176 . . . . . . . . . . . . . . 15 ((( bday 𝐶) +no ( bday 𝑥)) ⊆ (( bday 𝐶) +no ( bday 𝐸)) → ((( bday 𝐶) +no ( bday 𝑥)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))))
143141, 142syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ((( bday 𝐶) +no ( bday 𝑥)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))))
144 naddss2 8674 . . . . . . . . . . . . . . . . 17 ((( bday 𝑥) ∈ On ∧ ( bday 𝐸) ∈ On ∧ ( bday 𝐷) ∈ On) → (( bday 𝑥) ⊆ ( bday 𝐸) ↔ (( bday 𝐷) +no ( bday 𝑥)) ⊆ (( bday 𝐷) +no ( bday 𝐸))))
145107, 65, 109, 144mp3an 1461 . . . . . . . . . . . . . . . 16 (( bday 𝑥) ⊆ ( bday 𝐸) ↔ (( bday 𝐷) +no ( bday 𝑥)) ⊆ (( bday 𝐷) +no ( bday 𝐸)))
146104, 145sylib 217 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (( bday 𝐷) +no ( bday 𝑥)) ⊆ (( bday 𝐷) +no ( bday 𝐸)))
147 unss2 4178 . . . . . . . . . . . . . . 15 ((( bday 𝐷) +no ( bday 𝑥)) ⊆ (( bday 𝐷) +no ( bday 𝐸)) → ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝑥))) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
148146, 147syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝑥))) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
149 unss12 4179 . . . . . . . . . . . . . 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 𝑥)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝑥)))) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
150143, 148, 149syl2anc 584 . . . . . . . . . . . . 13 ((𝜑 ∧ (( 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 𝐸)))))
151 unss2 4178 . . . . . . . . . . . . 13 ((((( bday 𝐶) +no ( bday 𝑥)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝑥)))) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))) → ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝑥)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝑥))))) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
152150, 151syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (( 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 𝐸))))))
153152sseld 3978 . . . . . . . . . . 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 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝑥))))) → ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑙))) ∪ ((( bday 𝑖) +no ( bday 𝑙)) ∪ (( bday 𝑗) +no ( bday 𝑘))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))))
154153imim1d 82 . . . . . . . . . 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 𝐸))))) → ((𝑔 ·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 𝑘)))))))
155154ralimd6v 3208 . . . . . . . . 9 ((𝜑 ∧ (( 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 𝑘)))))))
156102, 155mpd 15 . . . . . . . 8 ((𝜑 ∧ (( 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 𝑘))))))
1579adantr 481 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → 𝐹 No )
158 simprr3 1223 . . . . . . . . 9 ((( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹))) → 𝑥 <s 𝐹)
159158adantl 482 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → 𝑥 <s 𝐹)
16064, 105eleqtrd 2835 . . . . . . . . 9 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ( bday 𝑥) ∈ ( bday 𝐹))
161160orcd 871 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (( bday 𝑥) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝑥)))
162156, 72, 62, 66, 157, 130, 159, 161mulsproplem13 27513 . . . . . . 7 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝑥)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝑥)))
16386adantr 481 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (𝐷 ·s 𝐹) ∈ No )
16498adantr 481 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (𝐶 ·s 𝐹) ∈ No )
16570, 163, 73, 164sltsubsub3bd 27481 . . . . . . 7 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (((𝐷 ·s 𝑥) -s (𝐶 ·s 𝑥)) <s ((𝐷 ·s 𝐹) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝑥)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝑥))))
166162, 165mpbird 256 . . . . . 6 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ((𝐷 ·s 𝑥) -s (𝐶 ·s 𝑥)) <s ((𝐷 ·s 𝐹) -s (𝐶 ·s 𝐹)))
16760, 74, 100, 138, 166slttrd 27191 . . . . 5 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ((𝐷 ·s 𝐸) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐶 ·s 𝐹)))
16845, 86, 58, 98sltsubsub3bd 27481 . . . . . 6 (𝜑 → (((𝐷 ·s 𝐸) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
169168adantr 481 . . . . 5 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → (((𝐷 ·s 𝐸) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
170167, 169mpbid 231 . . . 4 ((𝜑 ∧ (( bday 𝐸) = ( bday 𝐹) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹)))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
171170anassrs 468 . . 3 (((𝜑 ∧ ( bday 𝐸) = ( bday 𝐹)) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐸) ∧ 𝐸 <s 𝑥𝑥 <s 𝐹))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
17222, 171rexlimddv 3161 . 2 ((𝜑 ∧ ( bday 𝐸) = ( bday 𝐹)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
17365onordi 6465 . . . . 5 Ord ( bday 𝐸)
174108onordi 6465 . . . . 5 Ord ( bday 𝐹)
175 ordtri3or 6386 . . . . 5 ((Ord ( bday 𝐸) ∧ Ord ( bday 𝐹)) → (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐸) = ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)))
176173, 174, 175mp2an 690 . . . 4 (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐸) = ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸))
177 df-3or 1088 . . . . 5 ((( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐸) = ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)) ↔ ((( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐸) = ( bday 𝐹)) ∨ ( bday 𝐹) ∈ ( bday 𝐸)))
178 or32 924 . . . . 5 (((( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐸) = ( bday 𝐹)) ∨ ( bday 𝐹) ∈ ( bday 𝐸)) ↔ ((( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)) ∨ ( bday 𝐸) = ( bday 𝐹)))
179177, 178bitri 274 . . . 4 ((( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐸) = ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)) ↔ ((( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)) ∨ ( bday 𝐸) = ( bday 𝐹)))
180176, 179mpbi 229 . . 3 ((( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)) ∨ ( bday 𝐸) = ( bday 𝐹))
181180a1i 11 . 2 (𝜑 → ((( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)) ∨ ( bday 𝐸) = ( bday 𝐹)))
18216, 172, 181mpjaodan 957 1 (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845  w3o 1086  w3a 1087   = wceq 1541  wcel 2106  wral 3061  wrex 3070  cun 3943  wss 3945  c0 4319   class class class wbr 5142  Ord word 6353  Oncon0 6354  cfv 6533  (class class class)co 7394   +no cnadd 8649   No csur 27072   <s cslt 27073   bday cbday 27074   0s c0s 27252   O cold 27267   -s csubs 27424   ·s cmuls 27491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5357  ax-pr 5421  ax-un 7709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-ot 4632  df-uni 4903  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5568  df-eprel 5574  df-po 5582  df-so 5583  df-fr 5625  df-se 5626  df-we 5627  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  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 7350  df-ov 7397  df-oprab 7398  df-mpo 7399  df-1st 7959  df-2nd 7960  df-frecs 8250  df-wrecs 8281  df-recs 8355  df-1o 8450  df-2o 8451  df-nadd 8650  df-no 27075  df-slt 27076  df-bday 27077  df-sle 27177  df-sslt 27212  df-scut 27214  df-0s 27254  df-made 27271  df-old 27272  df-left 27274  df-right 27275  df-norec 27351  df-norec2 27362  df-adds 27373  df-negs 27425  df-subs 27426  df-muls 27492
This theorem is referenced by:  mulsprop  27515
  Copyright terms: Public domain W3C validator