Proof of Theorem mulsproplem4
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 | | oldssno 27703 |
. . . 4
⊢ ( O
‘( bday ‘𝐴)) ⊆ No
|
3 | | mulsproplem4.1 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ( O ‘(
bday ‘𝐴))) |
4 | 2, 3 | sselid 3980 |
. . 3
⊢ (𝜑 → 𝑋 ∈ No
) |
5 | | oldssno 27703 |
. . . 4
⊢ ( O
‘( bday ‘𝐵)) ⊆ No
|
6 | | mulsproplem4.2 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ ( O ‘(
bday ‘𝐵))) |
7 | 5, 6 | sselid 3980 |
. . 3
⊢ (𝜑 → 𝑌 ∈ No
) |
8 | | 0sno 27674 |
. . . 4
⊢
0s ∈ No |
9 | 8 | a1i 11 |
. . 3
⊢ (𝜑 → 0s ∈ No ) |
10 | | bday0s 27676 |
. . . . . . . . . . . 12
⊢ ( bday ‘ 0s ) = ∅ |
11 | 10, 10 | oveq12i 7424 |
. . . . . . . . . . 11
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no
∅) |
12 | | 0elon 6418 |
. . . . . . . . . . . 12
⊢ ∅
∈ On |
13 | | naddrid 8688 |
. . . . . . . . . . . 12
⊢ (∅
∈ On → (∅ +no ∅) = ∅) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (∅
+no ∅) = ∅ |
15 | 11, 14 | eqtri 2759 |
. . . . . . . . . 10
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) =
∅ |
16 | 15, 15 | uneq12i 4161 |
. . . . . . . . 9
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = (∅ ∪
∅) |
17 | | un0 4390 |
. . . . . . . . 9
⊢ (∅
∪ ∅) = ∅ |
18 | 16, 17 | eqtri 2759 |
. . . . . . . 8
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) =
∅ |
19 | 18, 18 | uneq12i 4161 |
. . . . . . 7
⊢ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) = (∅ ∪
∅) |
20 | 19, 17 | eqtri 2759 |
. . . . . 6
⊢ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) =
∅ |
21 | 20 | 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
‘𝑌)) ∪
∅) |
22 | | un0 4390 |
. . . . 5
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
∅) = (( bday ‘𝑋) +no ( bday
‘𝑌)) |
23 | 21, 22 | 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
‘𝑌)) |
24 | | oldbdayim 27730 |
. . . . . . 7
⊢ (𝑋 ∈ ( O ‘( bday ‘𝐴)) → ( bday
‘𝑋) ∈
( bday ‘𝐴)) |
25 | 3, 24 | syl 17 |
. . . . . 6
⊢ (𝜑 → (
bday ‘𝑋)
∈ ( bday ‘𝐴)) |
26 | | oldbdayim 27730 |
. . . . . . 7
⊢ (𝑌 ∈ ( O ‘( bday ‘𝐵)) → ( bday
‘𝑌) ∈
( bday ‘𝐵)) |
27 | 6, 26 | syl 17 |
. . . . . 6
⊢ (𝜑 → (
bday ‘𝑌)
∈ ( bday ‘𝐵)) |
28 | | bdayelon 27624 |
. . . . . . 7
⊢ ( bday ‘𝐴) ∈ On |
29 | | bdayelon 27624 |
. . . . . . 7
⊢ ( bday ‘𝐵) ∈ On |
30 | | naddel12 8705 |
. . . . . . 7
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → ((( bday ‘𝑋) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑌) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
31 | 28, 29, 30 | mp2an 689 |
. . . . . 6
⊢ ((( bday ‘𝑋) ∈ ( bday
‘𝐴) ∧
( bday ‘𝑌) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
32 | 25, 27, 31 | syl2anc 583 |
. . . . 5
⊢ (𝜑 → ((
bday ‘𝑋) +no
( bday ‘𝑌)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
33 | | 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
‘𝐸)))))) |
34 | 32, 33 | syl 17 |
. . . 4
⊢ (𝜑 → ((
bday ‘𝑋) +no
( bday ‘𝑌)) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) |
35 | 23, 34 | 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
‘𝐸)))))) |
36 | 1, 4, 7, 9, 9, 9, 9, 35 | 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 ))))) |
37 | 36 | simpld 494 |
1
⊢ (𝜑 → (𝑋 ·s 𝑌) ∈ No
) |