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