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