Proof of Theorem mulsproplem3
Step | Hyp | Ref
| Expression |
1 | | mulsproplem.1 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ 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 | | mulsproplem3.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ No
) |
3 | | oldssno 27703 |
. . . 4
⊢ ( O
‘( bday ‘𝐵)) ⊆ No
|
4 | | mulsproplem3.2 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ ( O ‘(
bday ‘𝐵))) |
5 | 3, 4 | sselid 3980 |
. . 3
⊢ (𝜑 → 𝑌 ∈ No
) |
6 | | 0sno 27674 |
. . . 4
⊢
0s ∈ No |
7 | 6 | a1i 11 |
. . 3
⊢ (𝜑 → 0s ∈ No ) |
8 | | bday0s 27676 |
. . . . . . . . . . . 12
⊢ ( bday ‘ 0s ) = ∅ |
9 | 8, 8 | oveq12i 7424 |
. . . . . . . . . . 11
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no
∅) |
10 | | 0elon 6418 |
. . . . . . . . . . . 12
⊢ ∅
∈ On |
11 | | naddrid 8688 |
. . . . . . . . . . . 12
⊢ (∅
∈ On → (∅ +no ∅) = ∅) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (∅
+no ∅) = ∅ |
13 | 9, 12 | eqtri 2759 |
. . . . . . . . . 10
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) =
∅ |
14 | 13, 13 | uneq12i 4161 |
. . . . . . . . 9
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = (∅ ∪
∅) |
15 | | un0 4390 |
. . . . . . . . 9
⊢ (∅
∪ ∅) = ∅ |
16 | 14, 15 | eqtri 2759 |
. . . . . . . 8
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) =
∅ |
17 | 16, 16 | uneq12i 4161 |
. . . . . . 7
⊢ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) = (∅ ∪
∅) |
18 | 17, 15 | eqtri 2759 |
. . . . . 6
⊢ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) =
∅ |
19 | 18 | uneq2i 4160 |
. . . . 5
⊢ ((( 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
‘𝑌)) ∪
∅) |
20 | | un0 4390 |
. . . . 5
⊢ ((( bday ‘𝐴) +no ( bday
‘𝑌)) ∪
∅) = (( bday ‘𝐴) +no ( bday
‘𝑌)) |
21 | 19, 20 | eqtri 2759 |
. . . 4
⊢ ((( 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
‘𝑌)) |
22 | | oldbdayim 27730 |
. . . . . . 7
⊢ (𝑌 ∈ ( O ‘( bday ‘𝐵)) → ( bday
‘𝑌) ∈
( bday ‘𝐵)) |
23 | 4, 22 | syl 17 |
. . . . . 6
⊢ (𝜑 → (
bday ‘𝑌)
∈ ( bday ‘𝐵)) |
24 | | bdayelon 27624 |
. . . . . . 7
⊢ ( bday ‘𝑌) ∈ On |
25 | | bdayelon 27624 |
. . . . . . 7
⊢ ( bday ‘𝐵) ∈ On |
26 | | bdayelon 27624 |
. . . . . . 7
⊢ ( bday ‘𝐴) ∈ On |
27 | | naddel2 8693 |
. . . . . . 7
⊢ ((( bday ‘𝑌) ∈ On ∧ (
bday ‘𝐵)
∈ On ∧ ( bday ‘𝐴) ∈ On) → ((
bday ‘𝑌)
∈ ( bday ‘𝐵) ↔ (( bday
‘𝐴) +no ( bday ‘𝑌)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
28 | 24, 25, 26, 27 | mp3an 1460 |
. . . . . 6
⊢ (( bday ‘𝑌) ∈ ( bday
‘𝐵) ↔
(( bday ‘𝐴) +no ( bday
‘𝑌)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
29 | 23, 28 | sylib 217 |
. . . . 5
⊢ (𝜑 → ((
bday ‘𝐴) +no
( bday ‘𝑌)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
30 | | elun1 4176 |
. . . . 5
⊢ ((( bday ‘𝐴) +no ( bday
‘𝑌)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) →
(( bday ‘𝐴) +no ( bday
‘𝑌)) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))))) |
31 | 29, 30 | syl 17 |
. . . 4
⊢ (𝜑 → ((
bday ‘𝐴) +no
( bday ‘𝑌)) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) |
32 | 21, 31 | eqeltrid 2836 |
. . 3
⊢ (𝜑 → (((
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
‘𝐸)))))) |
33 | 1, 2, 5, 7, 7, 7, 7, 32 | mulsproplem1 27931 |
. 2
⊢ (𝜑 → ((𝐴 ·s 𝑌) ∈ No
∧ (( 0s <s 0s ∧ 0s <s
0s ) → (( 0s ·s 0s )
-s ( 0s ·s 0s )) <s ((
0s ·s 0s ) -s (
0s ·s 0s ))))) |
34 | 33 | simpld 494 |
1
⊢ (𝜑 → (𝐴 ·s 𝑌) ∈ No
) |