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