Proof of Theorem mulsproplem2
| 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 27901 | . . . 4
⊢ ( O
‘( bday ‘𝐴)) ⊆  No | 
| 3 |  | mulsproplem2.1 | . . . 4
⊢ (𝜑 → 𝑋 ∈ ( O ‘(
bday ‘𝐴))) | 
| 4 | 2, 3 | sselid 3980 | . . 3
⊢ (𝜑 → 𝑋 ∈  No
) | 
| 5 |  | mulsproplem2.2 | . . 3
⊢ (𝜑 → 𝐵 ∈  No
) | 
| 6 |  | 0sno 27872 | . . . 4
⊢ 
0s ∈  No | 
| 7 | 6 | a1i 11 | . . 3
⊢ (𝜑 → 0s ∈  No ) | 
| 8 |  | bday0s 27874 | . . . . . . . . . . . 12
⊢ ( bday ‘ 0s ) = ∅ | 
| 9 | 8, 8 | oveq12i 7444 | . . . . . . . . . . 11
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no
∅) | 
| 10 |  | 0elon 6437 | . . . . . . . . . . . 12
⊢ ∅
∈ On | 
| 11 |  | naddrid 8722 | . . . . . . . . . . . 12
⊢ (∅
∈ On → (∅ +no ∅) = ∅) | 
| 12 | 10, 11 | ax-mp 5 | . . . . . . . . . . 11
⊢ (∅
+no ∅) = ∅ | 
| 13 | 9, 12 | eqtri 2764 | . . . . . . . . . 10
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) =
∅ | 
| 14 | 13, 13 | uneq12i 4165 | . . . . . . . . 9
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = (∅ ∪
∅) | 
| 15 |  | un0 4393 | . . . . . . . . 9
⊢ (∅
∪ ∅) = ∅ | 
| 16 | 14, 15 | eqtri 2764 | . . . . . . . 8
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) =
∅ | 
| 17 | 16, 16 | uneq12i 4165 | . . . . . . 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 2764 | . . . . . 6
⊢ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) =
∅ | 
| 19 | 18 | uneq2i 4164 | . . . . 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 4393 | . . . . 5
⊢ ((( bday ‘𝑋) +no ( bday
‘𝐵)) ∪
∅) = (( bday ‘𝑋) +no ( bday
‘𝐵)) | 
| 21 | 19, 20 | eqtri 2764 | . . . 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 27928 | . . . . . . 7
⊢ (𝑋 ∈ ( O ‘( bday ‘𝐴)) → ( bday
‘𝑋) ∈
( bday ‘𝐴)) | 
| 23 | 3, 22 | syl 17 | . . . . . 6
⊢ (𝜑 → (
bday ‘𝑋)
∈ ( bday ‘𝐴)) | 
| 24 |  | bdayelon 27822 | . . . . . . 7
⊢ ( bday ‘𝑋) ∈ On | 
| 25 |  | bdayelon 27822 | . . . . . . 7
⊢ ( bday ‘𝐴) ∈ On | 
| 26 |  | bdayelon 27822 | . . . . . . 7
⊢ ( bday ‘𝐵) ∈ On | 
| 27 |  | naddel1 8726 | . . . . . . 7
⊢ ((( bday ‘𝑋) ∈ On ∧ (
bday ‘𝐴)
∈ On ∧ ( bday ‘𝐵) ∈ On) → ((
bday ‘𝑋)
∈ ( bday ‘𝐴) ↔ (( bday
‘𝑋) +no ( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) | 
| 28 | 24, 25, 26, 27 | mp3an 1462 | . . . . . 6
⊢ (( bday ‘𝑋) ∈ ( bday
‘𝐴) ↔
(( bday ‘𝑋) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) | 
| 29 | 23, 28 | sylib 218 | . . . . 5
⊢ (𝜑 → ((
bday ‘𝑋) +no
( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) | 
| 30 |  | elun1 4181 | . . . . 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 2844 | . . 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, 4, 5, 7, 7, 7, 7, 32 | mulsproplem1 28143 | . 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
) |