| 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 480 |
. . 3
⊢ ((𝜑 ∧ ((
bday ‘𝐸)
∈ ( bday ‘𝐹) ∨ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → ∀𝑎 ∈ No
∀𝑏 ∈ No ∀𝑐 ∈ No
∀𝑑 ∈ No ∀𝑒 ∈ No
∀𝑓 ∈ No (((( bday ‘𝑎) +no (
bday ‘𝑏))
∪ (((( bday ‘𝑐) +no ( bday
‘𝑒)) ∪
(( bday ‘𝑑) +no ( bday
‘𝑓))) ∪
((( bday ‘𝑐) +no ( bday
‘𝑓)) ∪
(( bday ‘𝑑) +no ( bday
‘𝑒))))) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))))) →
((𝑎 ·s
𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
| 3 | | mulsproplem.2 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ No
) |
| 4 | 3 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ((
bday ‘𝐸)
∈ ( bday ‘𝐹) ∨ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐶 ∈ No
) |
| 5 | | mulsproplem.3 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ No
) |
| 6 | 5 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ((
bday ‘𝐸)
∈ ( bday ‘𝐹) ∨ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐷 ∈ No
) |
| 7 | | mulsproplem.4 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ No
) |
| 8 | 7 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ((
bday ‘𝐸)
∈ ( bday ‘𝐹) ∨ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐸 ∈ No
) |
| 9 | | mulsproplem.5 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ No
) |
| 10 | 9 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ((
bday ‘𝐸)
∈ ( bday ‘𝐹) ∨ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐹 ∈ No
) |
| 11 | | mulsproplem.6 |
. . . 4
⊢ (𝜑 → 𝐶 <s 𝐷) |
| 12 | 11 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ((
bday ‘𝐸)
∈ ( bday ‘𝐹) ∨ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐶 <s 𝐷) |
| 13 | | mulsproplem.7 |
. . . 4
⊢ (𝜑 → 𝐸 <s 𝐹) |
| 14 | 13 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ((
bday ‘𝐸)
∈ ( bday ‘𝐹) ∨ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐸 <s 𝐹) |
| 15 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ ((
bday ‘𝐸)
∈ ( bday ‘𝐹) ∨ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → (( bday
‘𝐸) ∈
( bday ‘𝐹) ∨ ( bday
‘𝐹) ∈
( bday ‘𝐸))) |
| 16 | 2, 4, 6, 8, 10, 12, 14, 15 | mulsproplem13 28154 |
. 2
⊢ ((𝜑 ∧ ((
bday ‘𝐸)
∈ ( bday ‘𝐹) ∨ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))) |
| 17 | 7 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (
bday ‘𝐸) =
( bday ‘𝐹)) → 𝐸 ∈ No
) |
| 18 | 9 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (
bday ‘𝐸) =
( bday ‘𝐹)) → 𝐹 ∈ No
) |
| 19 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ (
bday ‘𝐸) =
( bday ‘𝐹)) → ( bday
‘𝐸) = ( bday ‘𝐹)) |
| 20 | 13 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (
bday ‘𝐸) =
( bday ‘𝐹)) → 𝐸 <s 𝐹) |
| 21 | | nodense 27737 |
. . . 4
⊢ (((𝐸 ∈
No ∧ 𝐹 ∈
No ) ∧ (( bday
‘𝐸) = ( bday ‘𝐹) ∧ 𝐸 <s 𝐹)) → ∃𝑥 ∈ No
(( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)) |
| 22 | 17, 18, 19, 20, 21 | syl22anc 839 |
. . 3
⊢ ((𝜑 ∧ (
bday ‘𝐸) =
( bday ‘𝐹)) → ∃𝑥 ∈ No
(( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)) |
| 23 | | unidm 4157 |
. . . . . . . . . . . . . . . . 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 4157 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = (( bday ‘ 0s ) +no ( bday ‘ 0s )) |
| 25 | | bday0s 27873 |
. . . . . . . . . . . . . . . . . . 19
⊢ ( bday ‘ 0s ) = ∅ |
| 26 | 25, 25 | oveq12i 7443 |
. . . . . . . . . . . . . . . . . 18
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no
∅) |
| 27 | | 0elon 6438 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∅
∈ On |
| 28 | | naddrid 8721 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∅
∈ On → (∅ +no ∅) = ∅) |
| 29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ (∅
+no ∅) = ∅ |
| 30 | 26, 29 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) =
∅ |
| 31 | 23, 24, 30 | 3eqtri 2769 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) =
∅ |
| 32 | 31 | uneq2i 4165 |
. . . . . . . . . . . . . . 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 4394 |
. . . . . . . . . . . . . . 15
⊢ ((( bday ‘𝐷) +no ( bday
‘𝐸)) ∪
∅) = (( bday ‘𝐷) +no ( bday
‘𝐸)) |
| 34 | 32, 33 | eqtri 2765 |
. . . . . . . . . . . . . 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 4179 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝐷) +no ( bday
‘𝐸)) ⊆
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))) |
| 36 | | ssun2 4179 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))) ⊆
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))) |
| 37 | 35, 36 | sstri 3993 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝐷) +no ( bday
‘𝐸)) ⊆
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))) |
| 38 | | ssun2 4179 |
. . . . . . . . . . . . . . 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 3993 |
. . . . . . . . . . . . . 14
⊢ (( bday ‘𝐷) +no ( bday
‘𝐸)) ⊆
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))))) |
| 40 | 34, 39 | eqsstri 4030 |
. . . . . . . . . . . . 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 3979 |
. . . . . . . . . . . 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 28152 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 ·s 𝐸) ∈ No
) |
| 46 | 31 | uneq2i 4165 |
. . . . . . . . . . . . . . 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 4394 |
. . . . . . . . . . . . . . 15
⊢ ((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
∅) = (( bday ‘𝐶) +no ( bday
‘𝐸)) |
| 48 | 46, 47 | eqtri 2765 |
. . . . . . . . . . . . . 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 4178 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝐶) +no ( bday
‘𝐸)) ⊆
((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) |
| 50 | | ssun1 4178 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ⊆
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))) |
| 51 | 49, 50 | sstri 3993 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝐶) +no ( bday
‘𝐸)) ⊆
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))) |
| 52 | 51, 38 | sstri 3993 |
. . . . . . . . . . . . . 14
⊢ (( bday ‘𝐶) +no ( bday
‘𝐸)) ⊆
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))))) |
| 53 | 48, 52 | eqsstri 4030 |
. . . . . . . . . . . . 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 3979 |
. . . . . . . . . . . 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 28152 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ·s 𝐸) ∈ No
) |
| 59 | 45, 58 | subscld 28093 |
. . . . . . 7
⊢ (𝜑 → ((𝐷 ·s 𝐸) -s (𝐶 ·s 𝐸)) ∈ No
) |
| 60 | 59 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → ((𝐷 ·s 𝐸) -s (𝐶 ·s 𝐸)) ∈ No
) |
| 61 | 44 | adantr 480 |
. . . . . . . 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 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → 𝐷 ∈ No
) |
| 63 | | simprr1 1222 |
. . . . . . . . . 10
⊢ ((( bday ‘𝐸) = ( bday
‘𝐹) ∧
(𝑥 ∈ No ∧ (( bday
‘𝑥) ∈
( bday ‘𝐸) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹))) → ( bday
‘𝑥) ∈
( bday ‘𝐸)) |
| 64 | 63 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → ( bday
‘𝑥) ∈
( bday ‘𝐸)) |
| 65 | | bdayelon 27821 |
. . . . . . . . . 10
⊢ ( bday ‘𝐸) ∈ On |
| 66 | | simprrl 781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → 𝑥 ∈ No
) |
| 67 | | oldbday 27939 |
. . . . . . . . . 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 257 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → 𝑥 ∈ ( O ‘(
bday ‘𝐸))) |
| 70 | 61, 62, 69 | mulsproplem3 28144 |
. . . . . . 7
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → (𝐷 ·s 𝑥) ∈ No
) |
| 71 | 57 | adantr 480 |
. . . . . . . 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 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → 𝐶 ∈ No
) |
| 73 | 71, 72, 69 | mulsproplem3 28144 |
. . . . . . 7
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → (𝐶 ·s 𝑥) ∈ No
) |
| 74 | 70, 73 | subscld 28093 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → ((𝐷 ·s 𝑥) -s (𝐶 ·s 𝑥)) ∈ No
) |
| 75 | 31 | uneq2i 4165 |
. . . . . . . . . . . . . . 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 4394 |
. . . . . . . . . . . . . . 15
⊢ ((( bday ‘𝐷) +no ( bday
‘𝐹)) ∪
∅) = (( bday ‘𝐷) +no ( bday
‘𝐹)) |
| 77 | 75, 76 | eqtri 2765 |
. . . . . . . . . . . . . 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 4179 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝐷) +no ( bday
‘𝐹)) ⊆
((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) |
| 79 | 78, 50 | sstri 3993 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝐷) +no ( bday
‘𝐹)) ⊆
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))) |
| 80 | 79, 38 | sstri 3993 |
. . . . . . . . . . . . . 14
⊢ (( bday ‘𝐷) +no ( bday
‘𝐹)) ⊆
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))))) |
| 81 | 77, 80 | eqsstri 4030 |
. . . . . . . . . . . . 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 3979 |
. . . . . . . . . . . 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 28152 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 ·s 𝐹) ∈ No
) |
| 87 | 31 | uneq2i 4165 |
. . . . . . . . . . . . . . 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 4394 |
. . . . . . . . . . . . . . 15
⊢ ((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
∅) = (( bday ‘𝐶) +no ( bday
‘𝐹)) |
| 89 | 87, 88 | eqtri 2765 |
. . . . . . . . . . . . . 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 4178 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝐶) +no ( bday
‘𝐹)) ⊆
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))) |
| 91 | 90, 36 | sstri 3993 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝐶) +no ( bday
‘𝐹)) ⊆
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))) |
| 92 | 91, 38 | sstri 3993 |
. . . . . . . . . . . . . 14
⊢ (( bday ‘𝐶) +no ( bday
‘𝐹)) ⊆
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))))) |
| 93 | 89, 92 | eqsstri 4030 |
. . . . . . . . . . . . 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 3979 |
. . . . . . . . . . . 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 28152 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ·s 𝐹) ∈ No
) |
| 99 | 86, 98 | subscld 28093 |
. . . . . . 7
⊢ (𝜑 → ((𝐷 ·s 𝐹) -s (𝐶 ·s 𝐹)) ∈ No
) |
| 100 | 99 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → ((𝐷 ·s 𝐹) -s (𝐶 ·s 𝐹)) ∈ No
) |
| 101 | 1 | mulsproplemcbv 28141 |
. . . . . . . . . 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 480 |
. . . . . . . . 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 6426 |
. . . . . . . . . . . . . . . . . 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 771 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → ( bday
‘𝐸) = ( bday ‘𝐹)) |
| 106 | 104, 105 | sseqtrd 4020 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → ( bday
‘𝑥) ⊆
( bday ‘𝐹)) |
| 107 | | bdayelon 27821 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝑥) ∈ On |
| 108 | | bdayelon 27821 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝐹) ∈ On |
| 109 | | bdayelon 27821 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝐷) ∈ On |
| 110 | | naddss2 8728 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑥) ∈ On ∧ (
bday ‘𝐹)
∈ On ∧ ( bday ‘𝐷) ∈ On) → ((
bday ‘𝑥)
⊆ ( bday ‘𝐹) ↔ (( bday
‘𝐷) +no ( bday ‘𝑥)) ⊆ (( bday
‘𝐷) +no ( bday ‘𝐹)))) |
| 111 | 107, 108,
109, 110 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑥) ⊆ ( bday
‘𝐹) ↔
(( bday ‘𝐷) +no ( bday
‘𝑥)) ⊆
(( bday ‘𝐷) +no ( bday
‘𝐹))) |
| 112 | 106, 111 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → (( bday
‘𝐷) +no ( bday ‘𝑥)) ⊆ (( bday
‘𝐷) +no ( bday ‘𝐹))) |
| 113 | | unss2 4187 |
. . . . . . . . . . . . . . 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 27821 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝐶) ∈ On |
| 116 | | naddss2 8728 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑥) ∈ On ∧ (
bday ‘𝐹)
∈ On ∧ ( bday ‘𝐶) ∈ On) → ((
bday ‘𝑥)
⊆ ( bday ‘𝐹) ↔ (( bday
‘𝐶) +no ( bday ‘𝑥)) ⊆ (( bday
‘𝐶) +no ( bday ‘𝐹)))) |
| 117 | 107, 108,
115, 116 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑥) ⊆ ( bday
‘𝐹) ↔
(( bday ‘𝐶) +no ( bday
‘𝑥)) ⊆
(( bday ‘𝐶) +no ( bday
‘𝐹))) |
| 118 | 106, 117 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → (( bday
‘𝐶) +no ( bday ‘𝑥)) ⊆ (( bday
‘𝐶) +no ( bday ‘𝐹))) |
| 119 | | unss1 4185 |
. . . . . . . . . . . . . . 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 4188 |
. . . . . . . . . . . . . 14
⊢
((((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝑥))) ⊆
((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∧
((( bday ‘𝐶) +no ( bday
‘𝑥)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))) ⊆
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))) →
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( 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 4187 |
. . . . . . . . . . . . 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 3982 |
. . . . . . . . . . 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 3210 |
. . . . . . . . 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 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → 𝐸 ∈ No
) |
| 130 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → 𝐶 <s 𝐷) |
| 131 | | simprr2 1223 |
. . . . . . . . 9
⊢ ((( bday ‘𝐸) = ( bday
‘𝐹) ∧
(𝑥 ∈ No ∧ (( bday
‘𝑥) ∈
( bday ‘𝐸) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹))) → 𝐸 <s 𝑥) |
| 132 | 131 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → 𝐸 <s 𝑥) |
| 133 | 64 | olcd 875 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → (( bday
‘𝐸) ∈
( bday ‘𝑥) ∨ ( bday
‘𝑥) ∈
( bday ‘𝐸))) |
| 134 | 128, 72, 62, 129, 66, 130, 132, 133 | mulsproplem13 28154 |
. . . . . . 7
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → ((𝐶 ·s 𝑥) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑥) -s (𝐷 ·s 𝐸))) |
| 135 | 45 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → (𝐷 ·s 𝐸) ∈ No
) |
| 136 | 58 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → (𝐶 ·s 𝐸) ∈ No
) |
| 137 | 135, 70, 136, 73 | sltsubsub3bd 28115 |
. . . . . . 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 257 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → ((𝐷 ·s 𝐸) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑥) -s (𝐶 ·s 𝑥))) |
| 139 | | naddss2 8728 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑥) ∈ On ∧ (
bday ‘𝐸)
∈ On ∧ ( bday ‘𝐶) ∈ On) → ((
bday ‘𝑥)
⊆ ( bday ‘𝐸) ↔ (( bday
‘𝐶) +no ( bday ‘𝑥)) ⊆ (( bday
‘𝐶) +no ( bday ‘𝐸)))) |
| 140 | 107, 65, 115, 139 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑥) ⊆ ( bday
‘𝐸) ↔
(( bday ‘𝐶) +no ( bday
‘𝑥)) ⊆
(( bday ‘𝐶) +no ( bday
‘𝐸))) |
| 141 | 104, 140 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → (( bday
‘𝐶) +no ( bday ‘𝑥)) ⊆ (( bday
‘𝐶) +no ( bday ‘𝐸))) |
| 142 | | unss1 4185 |
. . . . . . . . . . . . . . 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 8728 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑥) ∈ On ∧ (
bday ‘𝐸)
∈ On ∧ ( bday ‘𝐷) ∈ On) → ((
bday ‘𝑥)
⊆ ( bday ‘𝐸) ↔ (( bday
‘𝐷) +no ( bday ‘𝑥)) ⊆ (( bday
‘𝐷) +no ( bday ‘𝐸)))) |
| 145 | 107, 65, 109, 144 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑥) ⊆ ( bday
‘𝐸) ↔
(( bday ‘𝐷) +no ( bday
‘𝑥)) ⊆
(( bday ‘𝐷) +no ( bday
‘𝐸))) |
| 146 | 104, 145 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → (( bday
‘𝐷) +no ( bday ‘𝑥)) ⊆ (( bday
‘𝐷) +no ( bday ‘𝐸))) |
| 147 | | unss2 4187 |
. . . . . . . . . . . . . . 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 4188 |
. . . . . . . . . . . . . 14
⊢
((((( bday ‘𝐶) +no ( bday
‘𝑥)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ⊆
((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∧
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝑥))) ⊆
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))) →
(((( bday ‘𝐶) +no ( bday
‘𝑥)) ∪
(( 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 4187 |
. . . . . . . . . . . . 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 3982 |
. . . . . . . . . . 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 3210 |
. . . . . . . . 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 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → 𝐹 ∈ No
) |
| 158 | | simprr3 1224 |
. . . . . . . . 9
⊢ ((( bday ‘𝐸) = ( bday
‘𝐹) ∧
(𝑥 ∈ No ∧ (( bday
‘𝑥) ∈
( bday ‘𝐸) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹))) → 𝑥 <s 𝐹) |
| 159 | 158 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → 𝑥 <s 𝐹) |
| 160 | 64, 105 | eleqtrd 2843 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → ( bday
‘𝑥) ∈
( bday ‘𝐹)) |
| 161 | 160 | orcd 874 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → (( bday
‘𝑥) ∈
( bday ‘𝐹) ∨ ( bday
‘𝐹) ∈
( bday ‘𝑥))) |
| 162 | 156, 72, 62, 66, 157, 130, 159, 161 | mulsproplem13 28154 |
. . . . . . 7
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝑥)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝑥))) |
| 163 | 86 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → (𝐷 ·s 𝐹) ∈ No
) |
| 164 | 98 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → (𝐶 ·s 𝐹) ∈ No
) |
| 165 | 70, 163, 73, 164 | sltsubsub3bd 28115 |
. . . . . . 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 257 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → ((𝐷 ·s 𝑥) -s (𝐶 ·s 𝑥)) <s ((𝐷 ·s 𝐹) -s (𝐶 ·s 𝐹))) |
| 167 | 60, 74, 100, 138, 166 | slttrd 27804 |
. . . . 5
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → ((𝐷 ·s 𝐸) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐶 ·s 𝐹))) |
| 168 | 45, 86, 58, 98 | sltsubsub3bd 28115 |
. . . . . 6
⊢ (𝜑 → (((𝐷 ·s 𝐸) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))) |
| 169 | 168 | adantr 480 |
. . . . 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 232 |
. . . 4
⊢ ((𝜑 ∧ ((
bday ‘𝐸) =
( bday ‘𝐹) ∧ (𝑥 ∈ No
∧ (( bday ‘𝑥) ∈ ( bday
‘𝐸) ∧
𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹)))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))) |
| 171 | 170 | anassrs 467 |
. . 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 6495 |
. . . . 5
⊢ Ord
( bday ‘𝐸) |
| 174 | 108 | onordi 6495 |
. . . . 5
⊢ Ord
( bday ‘𝐹) |
| 175 | | ordtri3or 6416 |
. . . . 5
⊢ ((Ord
( bday ‘𝐸) ∧ Ord ( bday
‘𝐹)) →
(( bday ‘𝐸) ∈ ( bday
‘𝐹) ∨
( bday ‘𝐸) = ( bday
‘𝐹) ∨
( bday ‘𝐹) ∈ ( bday
‘𝐸))) |
| 176 | 173, 174,
175 | mp2an 692 |
. . . 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 926 |
. . . . 5
⊢ (((( bday ‘𝐸) ∈ ( bday
‘𝐹) ∨
( bday ‘𝐸) = ( bday
‘𝐹)) ∨
( bday ‘𝐹) ∈ ( bday
‘𝐸)) ↔
((( bday ‘𝐸) ∈ ( bday
‘𝐹) ∨
( bday ‘𝐹) ∈ ( bday
‘𝐸)) ∨
( bday ‘𝐸) = ( bday
‘𝐹))) |
| 179 | 177, 178 | bitri 275 |
. . . 4
⊢ ((( bday ‘𝐸) ∈ ( bday
‘𝐹) ∨
( bday ‘𝐸) = ( bday
‘𝐹) ∨
( bday ‘𝐹) ∈ ( bday
‘𝐸)) ↔
((( bday ‘𝐸) ∈ ( bday
‘𝐹) ∨
( bday ‘𝐹) ∈ ( bday
‘𝐸)) ∨
( bday ‘𝐸) = ( bday
‘𝐹))) |
| 180 | 176, 179 | mpbi 230 |
. . 3
⊢ ((( bday ‘𝐸) ∈ ( bday
‘𝐹) ∨
( bday ‘𝐹) ∈ ( bday
‘𝐸)) ∨
( bday ‘𝐸) = ( bday
‘𝐹)) |
| 181 | 180 | a1i 11 |
. 2
⊢ (𝜑 → (((
bday ‘𝐸)
∈ ( bday ‘𝐹) ∨ ( bday
‘𝐹) ∈
( bday ‘𝐸)) ∨ ( bday
‘𝐸) = ( bday ‘𝐹))) |
| 182 | 16, 172, 181 | mpjaodan 961 |
1
⊢ (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))) |