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 27901 | . . . 4
⊢ ( O
‘( bday ‘𝐴)) ⊆  No | 
| 3 |  | mulsproplem4.1 | . . . 4
⊢ (𝜑 → 𝑋 ∈ ( O ‘(
bday ‘𝐴))) | 
| 4 | 2, 3 | sselid 3980 | . . 3
⊢ (𝜑 → 𝑋 ∈  No
) | 
| 5 |  | oldssno 27901 | . . . 4
⊢ ( O
‘( bday ‘𝐵)) ⊆  No | 
| 6 |  | mulsproplem4.2 | . . . 4
⊢ (𝜑 → 𝑌 ∈ ( O ‘(
bday ‘𝐵))) | 
| 7 | 5, 6 | sselid 3980 | . . 3
⊢ (𝜑 → 𝑌 ∈  No
) | 
| 8 |  | 0sno 27872 | . . . 4
⊢ 
0s ∈  No | 
| 9 | 8 | a1i 11 | . . 3
⊢ (𝜑 → 0s ∈  No ) | 
| 10 |  | bday0s 27874 | . . . . . . . . . . . 12
⊢ ( bday ‘ 0s ) = ∅ | 
| 11 | 10, 10 | oveq12i 7444 | . . . . . . . . . . 11
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no
∅) | 
| 12 |  | 0elon 6437 | . . . . . . . . . . . 12
⊢ ∅
∈ On | 
| 13 |  | naddrid 8722 | . . . . . . . . . . . 12
⊢ (∅
∈ On → (∅ +no ∅) = ∅) | 
| 14 | 12, 13 | ax-mp 5 | . . . . . . . . . . 11
⊢ (∅
+no ∅) = ∅ | 
| 15 | 11, 14 | eqtri 2764 | . . . . . . . . . 10
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) =
∅ | 
| 16 | 15, 15 | uneq12i 4165 | . . . . . . . . 9
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = (∅ ∪
∅) | 
| 17 |  | un0 4393 | . . . . . . . . 9
⊢ (∅
∪ ∅) = ∅ | 
| 18 | 16, 17 | eqtri 2764 | . . . . . . . 8
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) =
∅ | 
| 19 | 18, 18 | uneq12i 4165 | . . . . . . 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 2764 | . . . . . 6
⊢ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) =
∅ | 
| 21 | 20 | 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
‘𝑌)) ∪
∅) | 
| 22 |  | un0 4393 | . . . . 5
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
∅) = (( bday ‘𝑋) +no ( bday
‘𝑌)) | 
| 23 | 21, 22 | 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
‘𝑌)) | 
| 24 |  | oldbdayim 27928 | . . . . . . 7
⊢ (𝑋 ∈ ( O ‘( bday ‘𝐴)) → ( bday
‘𝑋) ∈
( bday ‘𝐴)) | 
| 25 | 3, 24 | syl 17 | . . . . . 6
⊢ (𝜑 → (
bday ‘𝑋)
∈ ( bday ‘𝐴)) | 
| 26 |  | oldbdayim 27928 | . . . . . . 7
⊢ (𝑌 ∈ ( O ‘( bday ‘𝐵)) → ( bday
‘𝑌) ∈
( bday ‘𝐵)) | 
| 27 | 6, 26 | syl 17 | . . . . . 6
⊢ (𝜑 → (
bday ‘𝑌)
∈ ( bday ‘𝐵)) | 
| 28 |  | bdayelon 27822 | . . . . . . 7
⊢ ( bday ‘𝐴) ∈ On | 
| 29 |  | bdayelon 27822 | . . . . . . 7
⊢ ( bday ‘𝐵) ∈ On | 
| 30 |  | naddel12 8739 | . . . . . . 7
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → ((( bday ‘𝑋) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑌) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 31 | 28, 29, 30 | mp2an 692 | . . . . . 6
⊢ ((( bday ‘𝑋) ∈ ( bday
‘𝐴) ∧
( bday ‘𝑌) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) | 
| 32 | 25, 27, 31 | syl2anc 584 | . . . . 5
⊢ (𝜑 → ((
bday ‘𝑋) +no
( bday ‘𝑌)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) | 
| 33 |  | 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
‘𝐸)))))) | 
| 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 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
‘𝐸)))))) | 
| 36 | 1, 4, 7, 9, 9, 9, 9, 35 | 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 ))))) | 
| 37 | 36 | simpld 494 | 1
⊢ (𝜑 → (𝑋 ·s 𝑌) ∈  No
) |