Proof of Theorem mulsproplem6
| Step | Hyp | Ref
| Expression |
| 1 | | leftssno 27919 |
. . . 4
⊢ ( L
‘𝐵) ⊆ No |
| 2 | | mulsproplem6.4 |
. . . 4
⊢ (𝜑 → 𝑄 ∈ ( L ‘𝐵)) |
| 3 | 1, 2 | sselid 3981 |
. . 3
⊢ (𝜑 → 𝑄 ∈ No
) |
| 4 | | mulsproplem6.6 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ ( L ‘𝐵)) |
| 5 | 1, 4 | sselid 3981 |
. . 3
⊢ (𝜑 → 𝑊 ∈ No
) |
| 6 | | sltlin 27794 |
. . 3
⊢ ((𝑄 ∈
No ∧ 𝑊 ∈
No ) → (𝑄 <s 𝑊 ∨ 𝑄 = 𝑊 ∨ 𝑊 <s 𝑄)) |
| 7 | 3, 5, 6 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝑄 <s 𝑊 ∨ 𝑄 = 𝑊 ∨ 𝑊 <s 𝑄)) |
| 8 | | mulsproplem.1 |
. . . . . . . . 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 ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))))) →
((𝑎 ·s
𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
| 9 | | leftssold 27917 |
. . . . . . . . . 10
⊢ ( L
‘𝐴) ⊆ ( O
‘( bday ‘𝐴)) |
| 10 | | mulsproplem6.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ( L ‘𝐴)) |
| 11 | 9, 10 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ( O ‘(
bday ‘𝐴))) |
| 12 | | mulsproplem6.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ No
) |
| 13 | 8, 11, 12 | mulsproplem2 28143 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 ·s 𝐵) ∈ No
) |
| 14 | | mulsproplem6.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ No
) |
| 15 | | leftssold 27917 |
. . . . . . . . . 10
⊢ ( L
‘𝐵) ⊆ ( O
‘( bday ‘𝐵)) |
| 16 | 15, 2 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ ( O ‘(
bday ‘𝐵))) |
| 17 | 8, 14, 16 | mulsproplem3 28144 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ·s 𝑄) ∈ No
) |
| 18 | 13, 17 | addscld 28013 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) ∈ No
) |
| 19 | 8, 11, 16 | mulsproplem4 28145 |
. . . . . . 7
⊢ (𝜑 → (𝑃 ·s 𝑄) ∈ No
) |
| 20 | 18, 19 | subscld 28093 |
. . . . . 6
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) ∈ No
) |
| 21 | 20 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) ∈ No
) |
| 22 | 15, 4 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ ( O ‘(
bday ‘𝐵))) |
| 23 | 8, 14, 22 | mulsproplem3 28144 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ·s 𝑊) ∈ No
) |
| 24 | 13, 23 | addscld 28013 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) ∈ No
) |
| 25 | 8, 11, 22 | mulsproplem4 28145 |
. . . . . . 7
⊢ (𝜑 → (𝑃 ·s 𝑊) ∈ No
) |
| 26 | 24, 25 | subscld 28093 |
. . . . . 6
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊)) ∈ No
) |
| 27 | 26 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊)) ∈ No
) |
| 28 | | rightssold 27918 |
. . . . . . . . . 10
⊢ ( R
‘𝐴) ⊆ ( O
‘( bday ‘𝐴)) |
| 29 | | mulsproplem6.5 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ ( R ‘𝐴)) |
| 30 | 28, 29 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → 𝑉 ∈ ( O ‘(
bday ‘𝐴))) |
| 31 | 8, 30, 12 | mulsproplem2 28143 |
. . . . . . . 8
⊢ (𝜑 → (𝑉 ·s 𝐵) ∈ No
) |
| 32 | 31, 23 | addscld 28013 |
. . . . . . 7
⊢ (𝜑 → ((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) ∈ No
) |
| 33 | 8, 30, 22 | mulsproplem4 28145 |
. . . . . . 7
⊢ (𝜑 → (𝑉 ·s 𝑊) ∈ No
) |
| 34 | 32, 33 | subscld 28093 |
. . . . . 6
⊢ (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) ∈ No
) |
| 35 | 34 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) ∈ No
) |
| 36 | | ssltleft 27909 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
No → ( L ‘𝐴) <<s {𝐴}) |
| 37 | 14, 36 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ( L ‘𝐴) <<s {𝐴}) |
| 38 | | snidg 4660 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
No → 𝐴 ∈
{𝐴}) |
| 39 | 14, 38 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ {𝐴}) |
| 40 | 37, 10, 39 | ssltsepcd 27839 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 <s 𝐴) |
| 41 | | 0sno 27871 |
. . . . . . . . . . . 12
⊢
0s ∈ No |
| 42 | 41 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0s ∈ No ) |
| 43 | | leftssno 27919 |
. . . . . . . . . . . 12
⊢ ( L
‘𝐴) ⊆ No |
| 44 | 43, 10 | sselid 3981 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ No
) |
| 45 | | bday0s 27873 |
. . . . . . . . . . . . . . . 16
⊢ ( bday ‘ 0s ) = ∅ |
| 46 | 45, 45 | oveq12i 7443 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no
∅) |
| 47 | | 0elon 6438 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ On |
| 48 | | naddrid 8721 |
. . . . . . . . . . . . . . . 16
⊢ (∅
∈ On → (∅ +no ∅) = ∅) |
| 49 | 47, 48 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (∅
+no ∅) = ∅ |
| 50 | 46, 49 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) =
∅ |
| 51 | 50 | uneq1i 4164 |
. . . . . . . . . . . . 13
⊢ ((( 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
‘𝑄))))) |
| 52 | | 0un 4396 |
. . . . . . . . . . . . 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
‘𝑄)))) |
| 53 | 51, 52 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ ((( 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
‘𝑄)))) |
| 54 | | oldbdayim 27927 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ( O ‘( bday ‘𝐴)) → ( bday
‘𝑃) ∈
( bday ‘𝐴)) |
| 55 | 11, 54 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (
bday ‘𝑃)
∈ ( bday ‘𝐴)) |
| 56 | | oldbdayim 27927 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑄 ∈ ( O ‘( bday ‘𝐵)) → ( bday
‘𝑄) ∈
( bday ‘𝐵)) |
| 57 | 16, 56 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (
bday ‘𝑄)
∈ ( bday ‘𝐵)) |
| 58 | | bdayelon 27821 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝐴) ∈ On |
| 59 | | bdayelon 27821 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝐵) ∈ On |
| 60 | | naddel12 8738 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → ((( bday ‘𝑃) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑄) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 61 | 58, 59, 60 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑃) ∈ ( bday
‘𝐴) ∧
( bday ‘𝑄) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
| 62 | 55, 57, 61 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑃) +no
( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
| 63 | | oldbdayim 27927 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ ( O ‘( bday ‘𝐵)) → ( bday
‘𝑊) ∈
( bday ‘𝐵)) |
| 64 | 22, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (
bday ‘𝑊)
∈ ( bday ‘𝐵)) |
| 65 | | bdayelon 27821 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝑊) ∈ On |
| 66 | | naddel2 8726 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑊) ∈ On ∧ (
bday ‘𝐵)
∈ On ∧ ( bday ‘𝐴) ∈ On) → ((
bday ‘𝑊)
∈ ( bday ‘𝐵) ↔ (( bday
‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
| 67 | 65, 59, 58, 66 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑊) ∈ ( bday
‘𝐵) ↔
(( bday ‘𝐴) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
| 68 | 64, 67 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝐴) +no
( bday ‘𝑊)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
| 69 | 62, 68 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑃) +no
( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
| 70 | | naddel12 8738 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → ((( bday ‘𝑃) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑊) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑃) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 71 | 58, 59, 70 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑃) ∈ ( bday
‘𝐴) ∧
( bday ‘𝑊) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑃) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
| 72 | 55, 64, 71 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑃) +no
( bday ‘𝑊)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
| 73 | | bdayelon 27821 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝑄) ∈ On |
| 74 | | naddel2 8726 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑄) ∈ On ∧ (
bday ‘𝐵)
∈ On ∧ ( bday ‘𝐴) ∈ On) → ((
bday ‘𝑄)
∈ ( bday ‘𝐵) ↔ (( bday
‘𝐴) +no ( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
| 75 | 73, 59, 58, 74 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑄) ∈ ( bday
‘𝐵) ↔
(( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
| 76 | 57, 75 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝐴) +no
( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
| 77 | 72, 76 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑃) +no
( bday ‘𝑊)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝐴) +no ( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
| 78 | | bdayelon 27821 |
. . . . . . . . . . . . . . . . . 18
⊢ ( bday ‘𝑃) ∈ On |
| 79 | | naddcl 8715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑃) ∈ On ∧ (
bday ‘𝑄)
∈ On) → (( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
On) |
| 80 | 78, 73, 79 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
On |
| 81 | | naddcl 8715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝑊)
∈ On) → (( bday ‘𝐴) +no ( bday
‘𝑊)) ∈
On) |
| 82 | 58, 65, 81 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝐴) +no ( bday
‘𝑊)) ∈
On |
| 83 | 80, 82 | onun2i 6506 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑊))) ∈
On |
| 84 | | naddcl 8715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑃) ∈ On ∧ (
bday ‘𝑊)
∈ On) → (( bday ‘𝑃) +no ( bday
‘𝑊)) ∈
On) |
| 85 | 78, 65, 84 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑃) +no ( bday
‘𝑊)) ∈
On |
| 86 | | naddcl 8715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝑄)
∈ On) → (( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
On) |
| 87 | 58, 73, 86 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
On |
| 88 | 85, 87 | onun2i 6506 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑃) +no ( bday
‘𝑊)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
On |
| 89 | | naddcl 8715 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) |
| 90 | 58, 59, 89 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On |
| 91 | | onunel 6489 |
. . . . . . . . . . . . . . . 16
⊢
((((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑊))) ∈
On ∧ ((( bday ‘𝑃) +no ( bday
‘𝑊)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
On ∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → ((((( 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
‘𝐵))))) |
| 92 | 83, 88, 90, 91 | mp3an 1463 |
. . . . . . . . . . . . . . 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
‘𝑊)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 93 | | onunel 6489 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝑊)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑊))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
| 94 | 80, 82, 90, 93 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑊))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 95 | | onunel 6489 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑃) +no ( bday
‘𝑊)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝑄)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑃) +no ( bday
‘𝑊)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
| 96 | 85, 87, 90, 95 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑃) +no ( bday
‘𝑊)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 97 | 94, 96 | anbi12i 628 |
. . . . . . . . . . . . . . 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
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝑃) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
| 98 | 92, 97 | bitri 275 |
. . . . . . . . . . . . . 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
‘𝐵))))) |
| 99 | 69, 77, 98 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((
bday ‘𝑃) +no
( bday ‘𝑄)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑊))) ∪ ((( bday
‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑄)))) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
| 100 | | elun1 4182 |
. . . . . . . . . . . . 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
‘𝐸)))))) |
| 101 | 99, 100 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((
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 ‘𝐸)))))) |
| 102 | 53, 101 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → (((
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 ‘𝐸)))))) |
| 103 | 8, 42, 42, 44, 14, 3, 5, 102 | mulsproplem1 28142 |
. . . . . . . . . 10
⊢ (𝜑 → (( 0s
·s 0s ) ∈ No
∧ ((𝑃 <s 𝐴 ∧ 𝑄 <s 𝑊) → ((𝑃 ·s 𝑊) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝐴 ·s 𝑄))))) |
| 104 | 103 | simprd 495 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 <s 𝐴 ∧ 𝑄 <s 𝑊) → ((𝑃 ·s 𝑊) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝐴 ·s 𝑄)))) |
| 105 | 40, 104 | mpand 695 |
. . . . . . . 8
⊢ (𝜑 → (𝑄 <s 𝑊 → ((𝑃 ·s 𝑊) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝐴 ·s 𝑄)))) |
| 106 | 105 | imp 406 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → ((𝑃 ·s 𝑊) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝐴 ·s 𝑄))) |
| 107 | 25, 23, 19, 17 | sltsubsub3bd 28115 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑃 ·s 𝑊) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝐴 ·s 𝑄)) ↔ ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊)))) |
| 108 | 17, 19 | subscld 28093 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄)) ∈ No
) |
| 109 | 23, 25 | subscld 28093 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊)) ∈ No
) |
| 110 | 108, 109,
13 | sltadd2d 28030 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊)) ↔ ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄))) <s ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊))))) |
| 111 | 107, 110 | bitrd 279 |
. . . . . . . 8
⊢ (𝜑 → (((𝑃 ·s 𝑊) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝐴 ·s 𝑄)) ↔ ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄))) <s ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊))))) |
| 112 | 111 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·s 𝑊) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝐴 ·s 𝑄)) ↔ ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄))) <s ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊))))) |
| 113 | 106, 112 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄))) <s ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊)))) |
| 114 | 13, 17, 19 | addsubsassd 28111 |
. . . . . . 7
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) = ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄)))) |
| 115 | 114 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) = ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄)))) |
| 116 | 13, 23, 25 | addsubsassd 28111 |
. . . . . . 7
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊)) = ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊)))) |
| 117 | 116 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊)) = ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊)))) |
| 118 | 113, 115,
117 | 3brtr4d 5175 |
. . . . 5
⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊))) |
| 119 | | lltropt 27911 |
. . . . . . . . . . 11
⊢ ( L
‘𝐴) <<s ( R
‘𝐴) |
| 120 | 119 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ( L ‘𝐴) <<s ( R ‘𝐴)) |
| 121 | 120, 10, 29 | ssltsepcd 27839 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 <s 𝑉) |
| 122 | | ssltleft 27909 |
. . . . . . . . . . 11
⊢ (𝐵 ∈
No → ( L ‘𝐵) <<s {𝐵}) |
| 123 | 12, 122 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ( L ‘𝐵) <<s {𝐵}) |
| 124 | | snidg 4660 |
. . . . . . . . . . 11
⊢ (𝐵 ∈
No → 𝐵 ∈
{𝐵}) |
| 125 | 12, 124 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ {𝐵}) |
| 126 | 123, 4, 125 | ssltsepcd 27839 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 <s 𝐵) |
| 127 | | rightssno 27920 |
. . . . . . . . . . . 12
⊢ ( R
‘𝐴) ⊆ No |
| 128 | 127, 29 | sselid 3981 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑉 ∈ No
) |
| 129 | 50 | uneq1i 4164 |
. . . . . . . . . . . . 13
⊢ ((( 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
‘𝑊))))) |
| 130 | | 0un 4396 |
. . . . . . . . . . . . 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
‘𝑊)))) |
| 131 | 129, 130 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ ((( 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
‘𝑊)))) |
| 132 | | oldbdayim 27927 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 ∈ ( O ‘( bday ‘𝐴)) → ( bday
‘𝑉) ∈
( bday ‘𝐴)) |
| 133 | 30, 132 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (
bday ‘𝑉)
∈ ( bday ‘𝐴)) |
| 134 | | bdayelon 27821 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝑉) ∈ On |
| 135 | | naddel1 8725 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑉) ∈ On ∧ (
bday ‘𝐴)
∈ On ∧ ( bday ‘𝐵) ∈ On) → ((
bday ‘𝑉)
∈ ( bday ‘𝐴) ↔ (( bday
‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
| 136 | 134, 58, 59, 135 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑉) ∈ ( bday
‘𝐴) ↔
(( bday ‘𝑉) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
| 137 | 133, 136 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑉) +no
( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
| 138 | 72, 137 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑃) +no
( bday ‘𝑊)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
| 139 | | naddel1 8725 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑃) ∈ On ∧ (
bday ‘𝐴)
∈ On ∧ ( bday ‘𝐵) ∈ On) → ((
bday ‘𝑃)
∈ ( bday ‘𝐴) ↔ (( bday
‘𝑃) +no ( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
| 140 | 78, 58, 59, 139 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑃) ∈ ( bday
‘𝐴) ↔
(( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
| 141 | 55, 140 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑃) +no
( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
| 142 | | naddel12 8738 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → ((( bday ‘𝑉) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑊) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑉) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 143 | 58, 59, 142 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑉) ∈ ( bday
‘𝐴) ∧
( bday ‘𝑊) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑉) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
| 144 | 133, 64, 143 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑉) +no
( bday ‘𝑊)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
| 145 | 141, 144 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑃) +no
( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
| 146 | | naddcl 8715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑉) ∈ On ∧ (
bday ‘𝐵)
∈ On) → (( bday ‘𝑉) +no ( bday
‘𝐵)) ∈
On) |
| 147 | 134, 59, 146 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑉) +no ( bday
‘𝐵)) ∈
On |
| 148 | 85, 147 | onun2i 6506 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑃) +no ( bday
‘𝑊)) ∪
(( bday ‘𝑉) +no ( bday
‘𝐵))) ∈
On |
| 149 | | naddcl 8715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑃) ∈ On ∧ (
bday ‘𝐵)
∈ On) → (( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
On) |
| 150 | 78, 59, 149 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
On |
| 151 | | naddcl 8715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑉) ∈ On ∧ (
bday ‘𝑊)
∈ On) → (( bday ‘𝑉) +no ( bday
‘𝑊)) ∈
On) |
| 152 | 134, 65, 151 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑉) +no ( bday
‘𝑊)) ∈
On |
| 153 | 150, 152 | onun2i 6506 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑊))) ∈
On |
| 154 | | onunel 6489 |
. . . . . . . . . . . . . . . 16
⊢
((((( bday ‘𝑃) +no ( bday
‘𝑊)) ∪
(( bday ‘𝑉) +no ( bday
‘𝐵))) ∈
On ∧ ((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑊))) ∈
On ∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → ((((( 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
‘𝐵))))) |
| 155 | 148, 153,
90, 154 | mp3an 1463 |
. . . . . . . . . . . . . . 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
‘𝐵)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑊))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 156 | | onunel 6489 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑃) +no ( bday
‘𝑊)) ∈ On
∧ (( bday ‘𝑉) +no ( bday
‘𝐵)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑃) +no ( bday
‘𝑊)) ∪
(( bday ‘𝑉) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑉) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
| 157 | 85, 147, 90, 156 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑃) +no ( bday
‘𝑊)) ∪
(( bday ‘𝑉) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑉) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 158 | | onunel 6489 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑃) +no ( bday
‘𝐵)) ∈ On
∧ (( bday ‘𝑉) +no ( bday
‘𝑊)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑊))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑉) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
| 159 | 150, 152,
90, 158 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑊))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑉) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 160 | 157, 159 | anbi12i 628 |
. . . . . . . . . . . . . . 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
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑉) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
| 161 | 155, 160 | bitri 275 |
. . . . . . . . . . . . . 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
‘𝐵))))) |
| 162 | 138, 145,
161 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((
bday ‘𝑃) +no
( bday ‘𝑊)) ∪ (( bday
‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday
‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday
‘𝑉) +no ( bday ‘𝑊)))) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
| 163 | | elun1 4182 |
. . . . . . . . . . . . 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
‘𝐸)))))) |
| 164 | 162, 163 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((
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 ‘𝐸)))))) |
| 165 | 131, 164 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → (((
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 ‘𝐸)))))) |
| 166 | 8, 42, 42, 44, 128, 5, 12, 165 | mulsproplem1 28142 |
. . . . . . . . . 10
⊢ (𝜑 → (( 0s
·s 0s ) ∈ No
∧ ((𝑃 <s 𝑉 ∧ 𝑊 <s 𝐵) → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊))))) |
| 167 | 166 | simprd 495 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 <s 𝑉 ∧ 𝑊 <s 𝐵) → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)))) |
| 168 | 121, 126,
167 | mp2and 699 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊))) |
| 169 | 13, 25 | subscld 28093 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) ∈ No
) |
| 170 | 31, 33 | subscld 28093 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) ∈ No
) |
| 171 | 169, 170,
23 | sltadd1d 28031 |
. . . . . . . 8
⊢ (𝜑 → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) ↔ (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) +s (𝐴 ·s 𝑊)) <s (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) +s (𝐴 ·s 𝑊)))) |
| 172 | 168, 171 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) +s (𝐴 ·s 𝑊)) <s (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) +s (𝐴 ·s 𝑊))) |
| 173 | 13, 23, 25 | addsubsd 28112 |
. . . . . . 7
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊)) = (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) +s (𝐴 ·s 𝑊))) |
| 174 | 31, 23, 33 | addsubsd 28112 |
. . . . . . 7
⊢ (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) = (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) +s (𝐴 ·s 𝑊))) |
| 175 | 172, 173,
174 | 3brtr4d 5175 |
. . . . . 6
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊))) |
| 176 | 175 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊))) |
| 177 | 21, 27, 35, 118, 176 | slttrd 27804 |
. . . 4
⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊))) |
| 178 | 177 | ex 412 |
. . 3
⊢ (𝜑 → (𝑄 <s 𝑊 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))) |
| 179 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑄 = 𝑊 → (𝐴 ·s 𝑄) = (𝐴 ·s 𝑊)) |
| 180 | 179 | oveq2d 7447 |
. . . . . 6
⊢ (𝑄 = 𝑊 → ((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) = ((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊))) |
| 181 | | oveq2 7439 |
. . . . . 6
⊢ (𝑄 = 𝑊 → (𝑃 ·s 𝑄) = (𝑃 ·s 𝑊)) |
| 182 | 180, 181 | oveq12d 7449 |
. . . . 5
⊢ (𝑄 = 𝑊 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) = (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊))) |
| 183 | 182 | breq1d 5153 |
. . . 4
⊢ (𝑄 = 𝑊 → ((((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) ↔ (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))) |
| 184 | 175, 183 | syl5ibrcom 247 |
. . 3
⊢ (𝜑 → (𝑄 = 𝑊 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))) |
| 185 | 20 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) ∈ No
) |
| 186 | 31, 17 | addscld 28013 |
. . . . . . 7
⊢ (𝜑 → ((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) ∈ No
) |
| 187 | 8, 30, 16 | mulsproplem4 28145 |
. . . . . . 7
⊢ (𝜑 → (𝑉 ·s 𝑄) ∈ No
) |
| 188 | 186, 187 | subscld 28093 |
. . . . . 6
⊢ (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑉 ·s 𝑄)) ∈ No
) |
| 189 | 188 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑉 ·s 𝑄)) ∈ No
) |
| 190 | 34 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) ∈ No
) |
| 191 | 123, 2, 125 | ssltsepcd 27839 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 <s 𝐵) |
| 192 | 50 | uneq1i 4164 |
. . . . . . . . . . . . 13
⊢ ((( 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
‘𝑄))))) |
| 193 | | 0un 4396 |
. . . . . . . . . . . . 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
‘𝑄)))) |
| 194 | 192, 193 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ ((( 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
‘𝑄)))) |
| 195 | 62, 137 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑃) +no
( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
| 196 | | naddel12 8738 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → ((( bday ‘𝑉) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑄) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑉) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 197 | 58, 59, 196 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑉) ∈ ( bday
‘𝐴) ∧
( bday ‘𝑄) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑉) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
| 198 | 133, 57, 197 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑉) +no
( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
| 199 | 141, 198 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑃) +no
( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝑉) +no ( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
| 200 | 80, 147 | onun2i 6506 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑉) +no ( bday
‘𝐵))) ∈
On |
| 201 | | naddcl 8715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑉) ∈ On ∧ (
bday ‘𝑄)
∈ On) → (( bday ‘𝑉) +no ( bday
‘𝑄)) ∈
On) |
| 202 | 134, 73, 201 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑉) +no ( bday
‘𝑄)) ∈
On |
| 203 | 150, 202 | onun2i 6506 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑄))) ∈
On |
| 204 | | onunel 6489 |
. . . . . . . . . . . . . . . 16
⊢
((((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑉) +no ( bday
‘𝐵))) ∈
On ∧ ((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑄))) ∈
On ∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → ((((( 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
‘𝐵))))) |
| 205 | 200, 203,
90, 204 | mp3an 1463 |
. . . . . . . . . . . . . . 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
‘𝐵)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 206 | | onunel 6489 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈ On
∧ (( bday ‘𝑉) +no ( bday
‘𝐵)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑉) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑉) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
| 207 | 80, 147, 90, 206 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑉) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑉) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 208 | | onunel 6489 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑃) +no ( bday
‘𝐵)) ∈ On
∧ (( bday ‘𝑉) +no ( bday
‘𝑄)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑉) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
| 209 | 150, 202,
90, 208 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑉) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 210 | 207, 209 | anbi12i 628 |
. . . . . . . . . . . . . . 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
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑉) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
| 211 | 205, 210 | bitri 275 |
. . . . . . . . . . . . . 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
‘𝐵))))) |
| 212 | 195, 199,
211 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((
bday ‘𝑃) +no
( bday ‘𝑄)) ∪ (( bday
‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday
‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday
‘𝑉) +no ( bday ‘𝑄)))) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
| 213 | | elun1 4182 |
. . . . . . . . . . . . 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
‘𝐸)))))) |
| 214 | 212, 213 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((
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 ‘𝐸)))))) |
| 215 | 194, 214 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → (((
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 ‘𝐸)))))) |
| 216 | 8, 42, 42, 44, 128, 3, 12, 215 | mulsproplem1 28142 |
. . . . . . . . . 10
⊢ (𝜑 → (( 0s
·s 0s ) ∈ No
∧ ((𝑃 <s 𝑉 ∧ 𝑄 <s 𝐵) → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑄))))) |
| 217 | 216 | simprd 495 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 <s 𝑉 ∧ 𝑄 <s 𝐵) → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑄)))) |
| 218 | 121, 191,
217 | mp2and 699 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑄))) |
| 219 | 13, 19 | subscld 28093 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) ∈ No
) |
| 220 | 31, 187 | subscld 28093 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑄)) ∈ No
) |
| 221 | 219, 220,
17 | sltadd1d 28031 |
. . . . . . . 8
⊢ (𝜑 → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑄)) ↔ (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄)) <s (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑄)) +s (𝐴 ·s 𝑄)))) |
| 222 | 218, 221 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄)) <s (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑄)) +s (𝐴 ·s 𝑄))) |
| 223 | 13, 17, 19 | addsubsd 28112 |
. . . . . . 7
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) = (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄))) |
| 224 | 31, 17, 187 | addsubsd 28112 |
. . . . . . 7
⊢ (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑉 ·s 𝑄)) = (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑄)) +s (𝐴 ·s 𝑄))) |
| 225 | 222, 223,
224 | 3brtr4d 5175 |
. . . . . 6
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑉 ·s 𝑄))) |
| 226 | 225 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑉 ·s 𝑄))) |
| 227 | | ssltright 27910 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
No → {𝐴}
<<s ( R ‘𝐴)) |
| 228 | 14, 227 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → {𝐴} <<s ( R ‘𝐴)) |
| 229 | 228, 39, 29 | ssltsepcd 27839 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 <s 𝑉) |
| 230 | 50 | uneq1i 4164 |
. . . . . . . . . . . . 13
⊢ ((( 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
‘𝑊))))) |
| 231 | | 0un 4396 |
. . . . . . . . . . . . 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
‘𝑊)))) |
| 232 | 230, 231 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ ((( 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
‘𝑊)))) |
| 233 | 68, 198 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝐴) +no
( bday ‘𝑊)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝑉) +no ( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
| 234 | 76, 144 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝐴) +no
( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
| 235 | 82, 202 | onun2i 6506 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝐴) +no ( bday
‘𝑊)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑄))) ∈
On |
| 236 | 87, 152 | onun2i 6506 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝐴) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑊))) ∈
On |
| 237 | | onunel 6489 |
. . . . . . . . . . . . . . . 16
⊢
((((( bday ‘𝐴) +no ( bday
‘𝑊)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑄))) ∈
On ∧ ((( bday ‘𝐴) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑊))) ∈
On ∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → ((((( 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
‘𝐵))))) |
| 238 | 235, 236,
90, 237 | mp3an 1463 |
. . . . . . . . . . . . . . 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
‘𝑄)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑊))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 239 | | onunel 6489 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝐴) +no ( bday
‘𝑊)) ∈ On
∧ (( bday ‘𝑉) +no ( bday
‘𝑄)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝐴) +no ( bday
‘𝑊)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝐴) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑉) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
| 240 | 82, 202, 90, 239 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝐴) +no ( bday
‘𝑊)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝐴) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑉) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 241 | | onunel 6489 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝐴) +no ( bday
‘𝑄)) ∈ On
∧ (( bday ‘𝑉) +no ( bday
‘𝑊)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝐴) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑊))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑉) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
| 242 | 87, 152, 90, 241 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝐴) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑉) +no ( bday
‘𝑊))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑉) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
| 243 | 240, 242 | anbi12i 628 |
. . . . . . . . . . . . . . 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
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑉) +no ( bday
‘𝑊)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
| 244 | 238, 243 | bitri 275 |
. . . . . . . . . . . . . 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
‘𝐵))))) |
| 245 | 233, 234,
244 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((
bday ‘𝐴) +no
( bday ‘𝑊)) ∪ (( bday
‘𝑉) +no ( bday ‘𝑄))) ∪ ((( bday
‘𝐴) +no ( bday ‘𝑄)) ∪ (( bday
‘𝑉) +no ( bday ‘𝑊)))) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
| 246 | | elun1 4182 |
. . . . . . . . . . . . 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
‘𝐸)))))) |
| 247 | 245, 246 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((
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 ‘𝐸)))))) |
| 248 | 232, 247 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → (((
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 ‘𝐸)))))) |
| 249 | 8, 42, 42, 14, 128, 5, 3, 248 | mulsproplem1 28142 |
. . . . . . . . . 10
⊢ (𝜑 → (( 0s
·s 0s ) ∈ No
∧ ((𝐴 <s 𝑉 ∧ 𝑊 <s 𝑄) → ((𝐴 ·s 𝑄) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑄) -s (𝑉 ·s 𝑊))))) |
| 250 | 249 | simprd 495 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 <s 𝑉 ∧ 𝑊 <s 𝑄) → ((𝐴 ·s 𝑄) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑄) -s (𝑉 ·s 𝑊)))) |
| 251 | 229, 250 | mpand 695 |
. . . . . . . 8
⊢ (𝜑 → (𝑊 <s 𝑄 → ((𝐴 ·s 𝑄) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑄) -s (𝑉 ·s 𝑊)))) |
| 252 | 251 | imp 406 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → ((𝐴 ·s 𝑄) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑄) -s (𝑉 ·s 𝑊))) |
| 253 | 17, 187, 23, 33 | sltsubsubbd 28113 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴 ·s 𝑄) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑄) -s (𝑉 ·s 𝑊)) ↔ ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊)))) |
| 254 | 17, 187 | subscld 28093 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄)) ∈ No
) |
| 255 | 23, 33 | subscld 28093 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊)) ∈ No
) |
| 256 | 254, 255,
31 | sltadd2d 28030 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊)) ↔ ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄))) <s ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊))))) |
| 257 | 253, 256 | bitrd 279 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴 ·s 𝑄) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑄) -s (𝑉 ·s 𝑊)) ↔ ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄))) <s ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊))))) |
| 258 | 257 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝐴 ·s 𝑄) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑄) -s (𝑉 ·s 𝑊)) ↔ ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄))) <s ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊))))) |
| 259 | 252, 258 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄))) <s ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊)))) |
| 260 | 31, 17, 187 | addsubsassd 28111 |
. . . . . . 7
⊢ (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑉 ·s 𝑄)) = ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄)))) |
| 261 | 260 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑉 ·s 𝑄)) = ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄)))) |
| 262 | 31, 23, 33 | addsubsassd 28111 |
. . . . . . 7
⊢ (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) = ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊)))) |
| 263 | 262 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) = ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊)))) |
| 264 | 259, 261,
263 | 3brtr4d 5175 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑉 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊))) |
| 265 | 185, 189,
190, 226, 264 | slttrd 27804 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊))) |
| 266 | 265 | ex 412 |
. . 3
⊢ (𝜑 → (𝑊 <s 𝑄 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))) |
| 267 | 178, 184,
266 | 3jaod 1431 |
. 2
⊢ (𝜑 → ((𝑄 <s 𝑊 ∨ 𝑄 = 𝑊 ∨ 𝑊 <s 𝑄) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))) |
| 268 | 7, 267 | mpd 15 |
1
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊))) |