Step | Hyp | Ref
| Expression |
1 | | mulsproplem.1 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑎 ∈ 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 | | unidm 4150 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) = ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) |
3 | | unidm 4150 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = (( bday ‘ 0s ) +no ( bday ‘ 0s )) |
4 | | bday0s 27296 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ( bday ‘ 0s ) = ∅ |
5 | 4, 4 | oveq12i 7408 |
. . . . . . . . . . . . . . . . . . 19
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no
∅) |
6 | | 0elon 6410 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅
∈ On |
7 | | naddrid 8670 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∅
∈ On → (∅ +no ∅) = ∅) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∅
+no ∅) = ∅ |
9 | 5, 8 | eqtri 2761 |
. . . . . . . . . . . . . . . . . 18
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) =
∅ |
10 | 3, 9 | eqtri 2761 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) =
∅ |
11 | 2, 10 | eqtri 2761 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) =
∅ |
12 | 11 | uneq2i 4158 |
. . . . . . . . . . . . . . 15
⊢ ((( 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
‘𝐹)) ∪
∅) |
13 | | un0 4388 |
. . . . . . . . . . . . . . 15
⊢ ((( bday ‘𝐷) +no ( bday
‘𝐹)) ∪
∅) = (( bday ‘𝐷) +no ( bday
‘𝐹)) |
14 | 12, 13 | eqtri 2761 |
. . . . . . . . . . . . . 14
⊢ ((( 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
‘𝐹)) |
15 | | ssun2 4171 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝐷) +no ( bday
‘𝐹)) ⊆
((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) |
16 | | ssun1 4170 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ⊆
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))) |
17 | 15, 16 | sstri 3989 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝐷) +no ( bday
‘𝐹)) ⊆
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))) |
18 | | ssun2 4171 |
. . . . . . . . . . . . . . 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
‘𝐸))))) |
19 | 17, 18 | sstri 3989 |
. . . . . . . . . . . . . 14
⊢ (( bday ‘𝐷) +no ( bday
‘𝐹)) ⊆
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))))) |
20 | 14, 19 | eqsstri 4014 |
. . . . . . . . . . . . 13
⊢ ((( 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
‘𝐸))))) |
21 | 20 | sseli 3976 |
. . . . . . . . . . . 12
⊢ (((( bday ‘𝑎) +no ( bday
‘𝑏)) ∪
(((( bday ‘𝑐) +no ( bday
‘𝑒)) ∪
(( bday ‘𝑑) +no ( bday
‘𝑓))) ∪
((( bday ‘𝑐) +no ( bday
‘𝑓)) ∪
(( bday ‘𝑑) +no ( bday
‘𝑒))))) ∈
((( 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
‘𝑒))))) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))))) |
22 | 21 | imim1i 63 |
. . . . . . . . . . 11
⊢
((((( 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 𝑒))))) → (((( bday
‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday
‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday
‘𝐷) +no ( bday ‘𝐹)) ∪ (((( bday
‘ 0s ) +no ( bday ‘
0s )) ∪ (( bday ‘
0s ) +no ( bday ‘ 0s
))) ∪ ((( bday ‘ 0s ) +no
( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈
No ∧ ((𝑐 <s
𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
23 | 22 | 6ralimi 3128 |
. . . . . . . . . 10
⊢
(∀𝑎 ∈
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 𝑒))))) → ∀𝑎 ∈ 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈
No ∧ ((𝑐 <s
𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
24 | 1, 23 | syl 17 |
. . . . . . . . 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈
No ∧ ((𝑐 <s
𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
25 | | mulsproplem.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ No
) |
26 | | mulsproplem.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ No
) |
27 | 24, 25, 26 | mulsproplem10 27548 |
. . . . . . . 8
⊢ (𝜑 → ((𝐷 ·s 𝐹) ∈ No
∧ ({𝑔 ∣
∃𝑝 ∈ ( L
‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐷)∃𝑠 ∈ ( R ‘𝐹)ℎ = (((𝑟 ·s 𝐹) +s (𝐷 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐷 ·s 𝐹)} ∧ {(𝐷 ·s 𝐹)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐷)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐷 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))) |
28 | 27 | simp2d 1144 |
. . . . . . 7
⊢ (𝜑 → ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐷)∃𝑠 ∈ ( R ‘𝐹)ℎ = (((𝑟 ·s 𝐹) +s (𝐷 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐷 ·s 𝐹)}) |
29 | 28 | adantr 482 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐷)∃𝑠 ∈ ( R ‘𝐹)ℎ = (((𝑟 ·s 𝐹) +s (𝐷 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐷 ·s 𝐹)}) |
30 | | simprl 770 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → ( bday
‘𝐶) ∈
( bday ‘𝐷)) |
31 | | bdayelon 27245 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝐷) ∈ On |
32 | | mulsproplem.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ No
) |
33 | 32 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐶 ∈ No
) |
34 | | oldbday 27362 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝐷) ∈ On ∧ 𝐶 ∈ No )
→ (𝐶 ∈ ( O
‘( bday ‘𝐷)) ↔ ( bday
‘𝐶) ∈
( bday ‘𝐷))) |
35 | 31, 33, 34 | sylancr 588 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → (𝐶 ∈ ( O ‘(
bday ‘𝐷))
↔ ( bday ‘𝐶) ∈ ( bday
‘𝐷))) |
36 | 30, 35 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐶 ∈ ( O ‘(
bday ‘𝐷))) |
37 | | mulsproplem.6 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 <s 𝐷) |
38 | 37 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐶 <s 𝐷) |
39 | | breq1 5147 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐶 → (𝑥 <s 𝐷 ↔ 𝐶 <s 𝐷)) |
40 | | leftval 27325 |
. . . . . . . . . . 11
⊢ ( L
‘𝐷) = {𝑥 ∈ ( O ‘( bday ‘𝐷)) ∣ 𝑥 <s 𝐷} |
41 | 39, 40 | elrab2 3684 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ( L ‘𝐷) ↔ (𝐶 ∈ ( O ‘(
bday ‘𝐷))
∧ 𝐶 <s 𝐷)) |
42 | 36, 38, 41 | sylanbrc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐶 ∈ ( L ‘𝐷)) |
43 | | simprr 772 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → ( bday
‘𝐸) ∈
( bday ‘𝐹)) |
44 | | bdayelon 27245 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝐹) ∈ On |
45 | | mulsproplem.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 ∈ No
) |
46 | 45 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐸 ∈ No
) |
47 | | oldbday 27362 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝐹) ∈ On ∧ 𝐸 ∈ No )
→ (𝐸 ∈ ( O
‘( bday ‘𝐹)) ↔ ( bday
‘𝐸) ∈
( bday ‘𝐹))) |
48 | 44, 46, 47 | sylancr 588 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → (𝐸 ∈ ( O ‘(
bday ‘𝐹))
↔ ( bday ‘𝐸) ∈ ( bday
‘𝐹))) |
49 | 43, 48 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐸 ∈ ( O ‘(
bday ‘𝐹))) |
50 | | mulsproplem.7 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 <s 𝐹) |
51 | 50 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐸 <s 𝐹) |
52 | | breq1 5147 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐸 → (𝑥 <s 𝐹 ↔ 𝐸 <s 𝐹)) |
53 | | leftval 27325 |
. . . . . . . . . . 11
⊢ ( L
‘𝐹) = {𝑥 ∈ ( O ‘( bday ‘𝐹)) ∣ 𝑥 <s 𝐹} |
54 | 52, 53 | elrab2 3684 |
. . . . . . . . . 10
⊢ (𝐸 ∈ ( L ‘𝐹) ↔ (𝐸 ∈ ( O ‘(
bday ‘𝐹))
∧ 𝐸 <s 𝐹)) |
55 | 49, 51, 54 | sylanbrc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐸 ∈ ( L ‘𝐹)) |
56 | | eqid 2733 |
. . . . . . . . . 10
⊢ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) |
57 | | oveq1 7403 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝐶 → (𝑝 ·s 𝐹) = (𝐶 ·s 𝐹)) |
58 | 57 | oveq1d 7411 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝐶 → ((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞))) |
59 | | oveq1 7403 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝐶 → (𝑝 ·s 𝑞) = (𝐶 ·s 𝑞)) |
60 | 58, 59 | oveq12d 7414 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝐶 → (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞))) |
61 | 60 | eqeq2d 2744 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝐶 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞)))) |
62 | | oveq2 7404 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 𝐸 → (𝐷 ·s 𝑞) = (𝐷 ·s 𝐸)) |
63 | 62 | oveq2d 7412 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 𝐸 → ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸))) |
64 | | oveq2 7404 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 𝐸 → (𝐶 ·s 𝑞) = (𝐶 ·s 𝐸)) |
65 | 63, 64 | oveq12d 7414 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝐸 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸))) |
66 | 65 | eqeq2d 2744 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝐸 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)))) |
67 | 61, 66 | rspc2ev 3622 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ( L ‘𝐷) ∧ 𝐸 ∈ ( L ‘𝐹) ∧ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸))) → ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))) |
68 | 56, 67 | mp3an3 1451 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ( L ‘𝐷) ∧ 𝐸 ∈ ( L ‘𝐹)) → ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))) |
69 | 42, 55, 68 | syl2anc 585 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))) |
70 | | ovex 7429 |
. . . . . . . . 9
⊢ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) ∈ V |
71 | | eqeq1 2737 |
. . . . . . . . . 10
⊢ (𝑔 = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) → (𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)))) |
72 | 71 | 2rexbidv 3220 |
. . . . . . . . 9
⊢ (𝑔 = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) → (∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)))) |
73 | 70, 72 | elab 3666 |
. . . . . . . 8
⊢ ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) ∈ {𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ↔ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))) |
74 | 69, 73 | sylibr 233 |
. . . . . . 7
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) ∈ {𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))}) |
75 | | elun1 4174 |
. . . . . . 7
⊢ ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) ∈ {𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))} → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) ∈ ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐷)∃𝑠 ∈ ( R ‘𝐹)ℎ = (((𝑟 ·s 𝐹) +s (𝐷 ·s 𝑠)) -s (𝑟 ·s 𝑠))})) |
76 | 74, 75 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) ∈ ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐷)∃𝑠 ∈ ( R ‘𝐹)ℎ = (((𝑟 ·s 𝐹) +s (𝐷 ·s 𝑠)) -s (𝑟 ·s 𝑠))})) |
77 | | ovex 7429 |
. . . . . . . 8
⊢ (𝐷 ·s 𝐹) ∈ V |
78 | 77 | snid 4660 |
. . . . . . 7
⊢ (𝐷 ·s 𝐹) ∈ {(𝐷 ·s 𝐹)} |
79 | 78 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → (𝐷 ·s 𝐹) ∈ {(𝐷 ·s 𝐹)}) |
80 | 29, 76, 79 | ssltsepcd 27262 |
. . . . 5
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹)) |
81 | 11 | uneq2i 4158 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((( 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
‘𝐹)) ∪
∅) |
82 | | un0 4388 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
∅) = (( bday ‘𝐶) +no ( bday
‘𝐹)) |
83 | 81, 82 | eqtri 2761 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( 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
‘𝐹)) |
84 | | ssun1 4170 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (( bday ‘𝐶) +no ( bday
‘𝐹)) ⊆
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))) |
85 | | ssun2 4171 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))) ⊆
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))) |
86 | 84, 85 | sstri 3989 |
. . . . . . . . . . . . . . . . . . 19
⊢ (( bday ‘𝐶) +no ( bday
‘𝐹)) ⊆
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))) |
87 | 86, 18 | sstri 3989 |
. . . . . . . . . . . . . . . . . 18
⊢ (( bday ‘𝐶) +no ( bday
‘𝐹)) ⊆
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))))) |
88 | 83, 87 | eqsstri 4014 |
. . . . . . . . . . . . . . . . 17
⊢ ((( 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
‘𝐸))))) |
89 | 88 | sseli 3976 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑎) +no ( bday
‘𝑏)) ∪
(((( bday ‘𝑐) +no ( bday
‘𝑒)) ∪
(( bday ‘𝑑) +no ( bday
‘𝑓))) ∪
((( bday ‘𝑐) +no ( bday
‘𝑓)) ∪
(( bday ‘𝑑) +no ( bday
‘𝑒))))) ∈
((( 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
‘𝑒))))) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))))) |
90 | 89 | imim1i 63 |
. . . . . . . . . . . . . . 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
‘𝐸))))) →
((𝑎 ·s
𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) → (((( bday
‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday
‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (((( bday
‘ 0s ) +no ( bday ‘
0s )) ∪ (( bday ‘
0s ) +no ( bday ‘ 0s
))) ∪ ((( bday ‘ 0s ) +no
( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈
No ∧ ((𝑐 <s
𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
91 | 90 | 6ralimi 3128 |
. . . . . . . . . . . . . 14
⊢
(∀𝑎 ∈
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 𝑒))))) → ∀𝑎 ∈ 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈
No ∧ ((𝑐 <s
𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
92 | 1, 91 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑎 ∈ 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈
No ∧ ((𝑐 <s
𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
93 | 92, 32, 26 | mulsproplem10 27548 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 ·s 𝐹) ∈ No
∧ ({𝑔 ∣
∃𝑝 ∈ ( L
‘𝐶)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐶 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐹)ℎ = (((𝑟 ·s 𝐹) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐶 ·s 𝐹)} ∧ {(𝐶 ·s 𝐹)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐶)∃𝑢 ∈ ( R ‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))) |
94 | 93 | simp1d 1143 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 ·s 𝐹) ∈ No
) |
95 | 11 | uneq2i 4158 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((( 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
‘𝐸)) ∪
∅) |
96 | | un0 4388 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((( bday ‘𝐷) +no ( bday
‘𝐸)) ∪
∅) = (( bday ‘𝐷) +no ( bday
‘𝐸)) |
97 | 95, 96 | eqtri 2761 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( 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
‘𝐸)) |
98 | | ssun2 4171 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (( bday ‘𝐷) +no ( bday
‘𝐸)) ⊆
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))) |
99 | 98, 85 | sstri 3989 |
. . . . . . . . . . . . . . . . . . 19
⊢ (( bday ‘𝐷) +no ( bday
‘𝐸)) ⊆
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))) |
100 | 99, 18 | sstri 3989 |
. . . . . . . . . . . . . . . . . 18
⊢ (( bday ‘𝐷) +no ( bday
‘𝐸)) ⊆
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))))) |
101 | 97, 100 | eqsstri 4014 |
. . . . . . . . . . . . . . . . 17
⊢ ((( 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
‘𝐸))))) |
102 | 101 | sseli 3976 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑎) +no ( bday
‘𝑏)) ∪
(((( bday ‘𝑐) +no ( bday
‘𝑒)) ∪
(( bday ‘𝑑) +no ( bday
‘𝑓))) ∪
((( bday ‘𝑐) +no ( bday
‘𝑓)) ∪
(( bday ‘𝑑) +no ( bday
‘𝑒))))) ∈
((( 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
‘𝑒))))) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))))) |
103 | 102 | imim1i 63 |
. . . . . . . . . . . . . . 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
‘𝐸))))) →
((𝑎 ·s
𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) → (((( bday
‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday
‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday
‘𝐷) +no ( bday ‘𝐸)) ∪ (((( bday
‘ 0s ) +no ( bday ‘
0s )) ∪ (( bday ‘
0s ) +no ( bday ‘ 0s
))) ∪ ((( bday ‘ 0s ) +no
( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈
No ∧ ((𝑐 <s
𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
104 | 103 | 6ralimi 3128 |
. . . . . . . . . . . . . 14
⊢
(∀𝑎 ∈
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 𝑒))))) → ∀𝑎 ∈ 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈
No ∧ ((𝑐 <s
𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
105 | 1, 104 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑎 ∈ 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈
No ∧ ((𝑐 <s
𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
106 | 105, 25, 45 | mulsproplem10 27548 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐷 ·s 𝐸) ∈ No
∧ ({𝑔 ∣
∃𝑝 ∈ ( L
‘𝐷)∃𝑞 ∈ ( L ‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐷)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐷 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐷 ·s 𝐸)} ∧ {(𝐷 ·s 𝐸)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐷)∃𝑤 ∈ ( L ‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))) |
107 | 106 | simp1d 1143 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷 ·s 𝐸) ∈ No
) |
108 | 94, 107 | addscomd 27418 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹))) |
109 | 108 | oveq1d 7411 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐶 ·s 𝐸))) |
110 | 11 | uneq2i 4158 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( 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
‘𝐸)) ∪
∅) |
111 | | un0 4388 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
∅) = (( bday ‘𝐶) +no ( bday
‘𝐸)) |
112 | 110, 111 | eqtri 2761 |
. . . . . . . . . . . . . . . . 17
⊢ ((( 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
‘𝐸)) |
113 | | ssun1 4170 |
. . . . . . . . . . . . . . . . . . 19
⊢ (( bday ‘𝐶) +no ( bday
‘𝐸)) ⊆
((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) |
114 | 113, 16 | sstri 3989 |
. . . . . . . . . . . . . . . . . 18
⊢ (( bday ‘𝐶) +no ( bday
‘𝐸)) ⊆
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))) |
115 | 114, 18 | sstri 3989 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝐶) +no ( bday
‘𝐸)) ⊆
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))))) |
116 | 112, 115 | eqsstri 4014 |
. . . . . . . . . . . . . . . 16
⊢ ((( 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
‘𝐸))))) |
117 | 116 | sseli 3976 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑎) +no ( bday
‘𝑏)) ∪
(((( bday ‘𝑐) +no ( bday
‘𝑒)) ∪
(( bday ‘𝑑) +no ( bday
‘𝑓))) ∪
((( bday ‘𝑐) +no ( bday
‘𝑓)) ∪
(( bday ‘𝑑) +no ( bday
‘𝑒))))) ∈
((( 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
‘𝑒))))) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))))) |
118 | 117 | imim1i 63 |
. . . . . . . . . . . . . 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
‘𝐸))))) →
((𝑎 ·s
𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) → (((( bday
‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday
‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (((( bday
‘ 0s ) +no ( bday ‘
0s )) ∪ (( bday ‘
0s ) +no ( bday ‘ 0s
))) ∪ ((( bday ‘ 0s ) +no
( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈
No ∧ ((𝑐 <s
𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
119 | 118 | 6ralimi 3128 |
. . . . . . . . . . . . 13
⊢
(∀𝑎 ∈
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 𝑒))))) → ∀𝑎 ∈ 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈
No ∧ ((𝑐 <s
𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
120 | 1, 119 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑎 ∈ 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈
No ∧ ((𝑐 <s
𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
121 | 120, 32, 45 | mulsproplem10 27548 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐶 ·s 𝐸) ∈ No
∧ ({𝑔 ∣
∃𝑝 ∈ ( L
‘𝐶)∃𝑞 ∈ ( L ‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐶 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐶 ·s 𝐸)} ∧ {(𝐶 ·s 𝐸)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐶)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐶 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))) |
122 | 121 | simp1d 1143 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 ·s 𝐸) ∈ No
) |
123 | 107, 94, 122 | addsubsassd 27515 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐶 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)))) |
124 | 109, 123 | eqtrd 2773 |
. . . . . . . 8
⊢ (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)))) |
125 | 124 | breq1d 5154 |
. . . . . . 7
⊢ (𝜑 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))) <s (𝐷 ·s 𝐹))) |
126 | 94, 122 | subscld 27502 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) ∈ No
) |
127 | 27 | simp1d 1143 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 ·s 𝐹) ∈ No
) |
128 | 107, 126,
127 | sltaddsub2d 27526 |
. . . . . . 7
⊢ (𝜑 → (((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))) <s (𝐷 ·s 𝐹) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))) |
129 | 125, 128 | bitrd 279 |
. . . . . 6
⊢ (𝜑 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))) |
130 | 129 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))) |
131 | 80, 130 | mpbid 231 |
. . . 4
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))) |
132 | 131 | anassrs 469 |
. . 3
⊢ (((𝜑 ∧ (
bday ‘𝐶)
∈ ( bday ‘𝐷)) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))) |
133 | 106 | simp3d 1145 |
. . . . . . 7
⊢ (𝜑 → {(𝐷 ·s 𝐸)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐷)∃𝑤 ∈ ( L ‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) -s (𝑣 ·s 𝑤))})) |
134 | 133 | adantr 482 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → {(𝐷 ·s 𝐸)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐷)∃𝑤 ∈ ( L ‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) -s (𝑣 ·s 𝑤))})) |
135 | | ovex 7429 |
. . . . . . . 8
⊢ (𝐷 ·s 𝐸) ∈ V |
136 | 135 | snid 4660 |
. . . . . . 7
⊢ (𝐷 ·s 𝐸) ∈ {(𝐷 ·s 𝐸)} |
137 | 136 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → (𝐷 ·s 𝐸) ∈ {(𝐷 ·s 𝐸)}) |
138 | | simprl 770 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → ( bday
‘𝐶) ∈
( bday ‘𝐷)) |
139 | 32 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐶 ∈ No
) |
140 | 31, 139, 34 | sylancr 588 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → (𝐶 ∈ ( O ‘(
bday ‘𝐷))
↔ ( bday ‘𝐶) ∈ ( bday
‘𝐷))) |
141 | 138, 140 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐶 ∈ ( O ‘(
bday ‘𝐷))) |
142 | 37 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐶 <s 𝐷) |
143 | 141, 142,
41 | sylanbrc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐶 ∈ ( L ‘𝐷)) |
144 | | simprr 772 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → ( bday
‘𝐹) ∈
( bday ‘𝐸)) |
145 | | bdayelon 27245 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝐸) ∈ On |
146 | 26 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐹 ∈ No
) |
147 | | oldbday 27362 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝐸) ∈ On ∧ 𝐹 ∈ No )
→ (𝐹 ∈ ( O
‘( bday ‘𝐸)) ↔ ( bday
‘𝐹) ∈
( bday ‘𝐸))) |
148 | 145, 146,
147 | sylancr 588 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → (𝐹 ∈ ( O ‘(
bday ‘𝐸))
↔ ( bday ‘𝐹) ∈ ( bday
‘𝐸))) |
149 | 144, 148 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐹 ∈ ( O ‘(
bday ‘𝐸))) |
150 | 50 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐸 <s 𝐹) |
151 | | breq2 5148 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐹 → (𝐸 <s 𝑥 ↔ 𝐸 <s 𝐹)) |
152 | | rightval 27326 |
. . . . . . . . . . 11
⊢ ( R
‘𝐸) = {𝑥 ∈ ( O ‘( bday ‘𝐸)) ∣ 𝐸 <s 𝑥} |
153 | 151, 152 | elrab2 3684 |
. . . . . . . . . 10
⊢ (𝐹 ∈ ( R ‘𝐸) ↔ (𝐹 ∈ ( O ‘(
bday ‘𝐸))
∧ 𝐸 <s 𝐹)) |
154 | 149, 150,
153 | sylanbrc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐹 ∈ ( R ‘𝐸)) |
155 | | eqid 2733 |
. . . . . . . . . 10
⊢ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) |
156 | | oveq1 7403 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝐶 → (𝑡 ·s 𝐸) = (𝐶 ·s 𝐸)) |
157 | 156 | oveq1d 7411 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝐶 → ((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢))) |
158 | | oveq1 7403 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝐶 → (𝑡 ·s 𝑢) = (𝐶 ·s 𝑢)) |
159 | 157, 158 | oveq12d 7414 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝐶 → (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢))) |
160 | 159 | eqeq2d 2744 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝐶 → ((((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢)))) |
161 | | oveq2 7404 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝐹 → (𝐷 ·s 𝑢) = (𝐷 ·s 𝐹)) |
162 | 161 | oveq2d 7412 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝐹 → ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹))) |
163 | | oveq2 7404 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝐹 → (𝐶 ·s 𝑢) = (𝐶 ·s 𝐹)) |
164 | 162, 163 | oveq12d 7414 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝐹 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹))) |
165 | 164 | eqeq2d 2744 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝐹 → ((((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)))) |
166 | 160, 165 | rspc2ev 3622 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ( L ‘𝐷) ∧ 𝐹 ∈ ( R ‘𝐸) ∧ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹))) → ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))) |
167 | 155, 166 | mp3an3 1451 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ( L ‘𝐷) ∧ 𝐹 ∈ ( R ‘𝐸)) → ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))) |
168 | 143, 154,
167 | syl2anc 585 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))) |
169 | | ovex 7429 |
. . . . . . . . 9
⊢ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ∈ V |
170 | | eqeq1 2737 |
. . . . . . . . . 10
⊢ (𝑖 = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) → (𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)))) |
171 | 170 | 2rexbidv 3220 |
. . . . . . . . 9
⊢ (𝑖 = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) → (∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)))) |
172 | 169, 171 | elab 3666 |
. . . . . . . 8
⊢ ((((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ∈ {𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ↔ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))) |
173 | 168, 172 | sylibr 233 |
. . . . . . 7
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ∈ {𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))}) |
174 | | elun1 4174 |
. . . . . . 7
⊢ ((((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ∈ {𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))} → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ∈ ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐷)∃𝑤 ∈ ( L ‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) -s (𝑣 ·s 𝑤))})) |
175 | 173, 174 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ∈ ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐷)∃𝑤 ∈ ( L ‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) -s (𝑣 ·s 𝑤))})) |
176 | 134, 137,
175 | ssltsepcd 27262 |
. . . . 5
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → (𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹))) |
177 | 122, 127 | addscomd 27418 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸))) |
178 | 177 | oveq1d 7411 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐶 ·s 𝐹))) |
179 | 127, 122,
94 | addsubsassd 27515 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐶 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)))) |
180 | 178, 179 | eqtrd 2773 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)))) |
181 | 180 | breq2d 5156 |
. . . . . . . 8
⊢ (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ (𝐷 ·s 𝐸) <s ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))) |
182 | 122, 94 | subscld 27502 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)) ∈ No
) |
183 | 107, 127,
182 | sltsubadd2d 27524 |
. . . . . . . 8
⊢ (𝜑 → (((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)) ↔ (𝐷 ·s 𝐸) <s ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))) |
184 | 181, 183 | bitr4d 282 |
. . . . . . 7
⊢ (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)))) |
185 | 107, 127,
122, 94 | sltsubsub2bd 27518 |
. . . . . . 7
⊢ (𝜑 → (((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))) |
186 | 184, 185 | bitrd 279 |
. . . . . 6
⊢ (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))) |
187 | 186 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))) |
188 | 176, 187 | mpbid 231 |
. . . 4
⊢ ((𝜑 ∧ ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))) |
189 | 188 | anassrs 469 |
. . 3
⊢ (((𝜑 ∧ (
bday ‘𝐶)
∈ ( bday ‘𝐷)) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))) |
190 | | mulsproplem12.2 |
. . . 4
⊢ (𝜑 → ((
bday ‘𝐸)
∈ ( bday ‘𝐹) ∨ ( bday
‘𝐹) ∈
( bday ‘𝐸))) |
191 | 190 | adantr 482 |
. . 3
⊢ ((𝜑 ∧ (
bday ‘𝐶)
∈ ( bday ‘𝐷)) → (( bday
‘𝐸) ∈
( bday ‘𝐹) ∨ ( bday
‘𝐹) ∈
( bday ‘𝐸))) |
192 | 132, 189,
191 | mpjaodan 958 |
. 2
⊢ ((𝜑 ∧ (
bday ‘𝐶)
∈ ( bday ‘𝐷)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))) |
193 | 93 | simp3d 1145 |
. . . . . . 7
⊢ (𝜑 → {(𝐶 ·s 𝐹)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐶)∃𝑢 ∈ ( R ‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))})) |
194 | 193 | adantr 482 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → {(𝐶 ·s 𝐹)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐶)∃𝑢 ∈ ( R ‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))})) |
195 | | ovex 7429 |
. . . . . . . 8
⊢ (𝐶 ·s 𝐹) ∈ V |
196 | 195 | snid 4660 |
. . . . . . 7
⊢ (𝐶 ·s 𝐹) ∈ {(𝐶 ·s 𝐹)} |
197 | 196 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → (𝐶 ·s 𝐹) ∈ {(𝐶 ·s 𝐹)}) |
198 | | simprl 770 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → ( bday
‘𝐷) ∈
( bday ‘𝐶)) |
199 | | bdayelon 27245 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝐶) ∈ On |
200 | 25 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐷 ∈ No
) |
201 | | oldbday 27362 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝐶) ∈ On ∧ 𝐷 ∈ No )
→ (𝐷 ∈ ( O
‘( bday ‘𝐶)) ↔ ( bday
‘𝐷) ∈
( bday ‘𝐶))) |
202 | 199, 200,
201 | sylancr 588 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → (𝐷 ∈ ( O ‘(
bday ‘𝐶))
↔ ( bday ‘𝐷) ∈ ( bday
‘𝐶))) |
203 | 198, 202 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐷 ∈ ( O ‘(
bday ‘𝐶))) |
204 | 37 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐶 <s 𝐷) |
205 | | breq2 5148 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐷 → (𝐶 <s 𝑥 ↔ 𝐶 <s 𝐷)) |
206 | | rightval 27326 |
. . . . . . . . . . 11
⊢ ( R
‘𝐶) = {𝑥 ∈ ( O ‘( bday ‘𝐶)) ∣ 𝐶 <s 𝑥} |
207 | 205, 206 | elrab2 3684 |
. . . . . . . . . 10
⊢ (𝐷 ∈ ( R ‘𝐶) ↔ (𝐷 ∈ ( O ‘(
bday ‘𝐶))
∧ 𝐶 <s 𝐷)) |
208 | 203, 204,
207 | sylanbrc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐷 ∈ ( R ‘𝐶)) |
209 | | simprr 772 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → ( bday
‘𝐸) ∈
( bday ‘𝐹)) |
210 | 45 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐸 ∈ No
) |
211 | 44, 210, 47 | sylancr 588 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → (𝐸 ∈ ( O ‘(
bday ‘𝐹))
↔ ( bday ‘𝐸) ∈ ( bday
‘𝐹))) |
212 | 209, 211 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐸 ∈ ( O ‘(
bday ‘𝐹))) |
213 | 50 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐸 <s 𝐹) |
214 | 212, 213,
54 | sylanbrc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → 𝐸 ∈ ( L ‘𝐹)) |
215 | | eqid 2733 |
. . . . . . . . . 10
⊢ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) |
216 | | oveq1 7403 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝐷 → (𝑣 ·s 𝐹) = (𝐷 ·s 𝐹)) |
217 | 216 | oveq1d 7411 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐷 → ((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤))) |
218 | | oveq1 7403 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐷 → (𝑣 ·s 𝑤) = (𝐷 ·s 𝑤)) |
219 | 217, 218 | oveq12d 7414 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐷 → (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤))) |
220 | 219 | eqeq2d 2744 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝐷 → ((((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤)))) |
221 | | oveq2 7404 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝐸 → (𝐶 ·s 𝑤) = (𝐶 ·s 𝐸)) |
222 | 221 | oveq2d 7412 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝐸 → ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸))) |
223 | | oveq2 7404 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝐸 → (𝐷 ·s 𝑤) = (𝐷 ·s 𝐸)) |
224 | 222, 223 | oveq12d 7414 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝐸 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸))) |
225 | 224 | eqeq2d 2744 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝐸 → ((((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)))) |
226 | 220, 225 | rspc2ev 3622 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ ( R ‘𝐶) ∧ 𝐸 ∈ ( L ‘𝐹) ∧ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸))) → ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))) |
227 | 215, 226 | mp3an3 1451 |
. . . . . . . . 9
⊢ ((𝐷 ∈ ( R ‘𝐶) ∧ 𝐸 ∈ ( L ‘𝐹)) → ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))) |
228 | 208, 214,
227 | syl2anc 585 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))) |
229 | | ovex 7429 |
. . . . . . . . 9
⊢ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ∈ V |
230 | | eqeq1 2737 |
. . . . . . . . . 10
⊢ (𝑗 = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) → (𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)))) |
231 | 230 | 2rexbidv 3220 |
. . . . . . . . 9
⊢ (𝑗 = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) → (∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)))) |
232 | 229, 231 | elab 3666 |
. . . . . . . 8
⊢ ((((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ∈ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))} ↔ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))) |
233 | 228, 232 | sylibr 233 |
. . . . . . 7
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ∈ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))}) |
234 | | elun2 4175 |
. . . . . . 7
⊢ ((((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ∈ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))} → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ∈ ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐶)∃𝑢 ∈ ( R ‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))})) |
235 | 233, 234 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ∈ ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐶)∃𝑢 ∈ ( R ‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))})) |
236 | 194, 197,
235 | ssltsepcd 27262 |
. . . . 5
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → (𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸))) |
237 | 127, 122 | addscomd 27418 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹))) |
238 | 237 | oveq1d 7411 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐷 ·s 𝐸))) |
239 | 122, 127,
107 | addsubsassd 27515 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐷 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))) |
240 | 238, 239 | eqtrd 2773 |
. . . . . . . 8
⊢ (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))) |
241 | 240 | breq2d 5156 |
. . . . . . 7
⊢ (𝜑 → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ↔ (𝐶 ·s 𝐹) <s ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))) |
242 | 127, 107 | subscld 27502 |
. . . . . . . 8
⊢ (𝜑 → ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)) ∈ No
) |
243 | 94, 122, 242 | sltsubadd2d 27524 |
. . . . . . 7
⊢ (𝜑 → (((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)) ↔ (𝐶 ·s 𝐹) <s ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))) |
244 | 241, 243 | bitr4d 282 |
. . . . . 6
⊢ (𝜑 → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))) |
245 | 244 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))) |
246 | 236, 245 | mpbid 231 |
. . . 4
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))) |
247 | 246 | anassrs 469 |
. . 3
⊢ (((𝜑 ∧ (
bday ‘𝐷)
∈ ( bday ‘𝐶)) ∧ ( bday
‘𝐸) ∈
( bday ‘𝐹)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))) |
248 | 121 | simp2d 1144 |
. . . . . . 7
⊢ (𝜑 → ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐶)∃𝑞 ∈ ( L ‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐶 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐶 ·s 𝐸)}) |
249 | 248 | adantr 482 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐶)∃𝑞 ∈ ( L ‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐶 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐶 ·s 𝐸)}) |
250 | | simprl 770 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → ( bday
‘𝐷) ∈
( bday ‘𝐶)) |
251 | 25 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐷 ∈ No
) |
252 | 199, 251,
201 | sylancr 588 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → (𝐷 ∈ ( O ‘(
bday ‘𝐶))
↔ ( bday ‘𝐷) ∈ ( bday
‘𝐶))) |
253 | 250, 252 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐷 ∈ ( O ‘(
bday ‘𝐶))) |
254 | 37 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐶 <s 𝐷) |
255 | 253, 254,
207 | sylanbrc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐷 ∈ ( R ‘𝐶)) |
256 | | simprr 772 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → ( bday
‘𝐹) ∈
( bday ‘𝐸)) |
257 | 26 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐹 ∈ No
) |
258 | 145, 257,
147 | sylancr 588 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → (𝐹 ∈ ( O ‘(
bday ‘𝐸))
↔ ( bday ‘𝐹) ∈ ( bday
‘𝐸))) |
259 | 256, 258 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐹 ∈ ( O ‘(
bday ‘𝐸))) |
260 | 50 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐸 <s 𝐹) |
261 | 259, 260,
153 | sylanbrc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → 𝐹 ∈ ( R ‘𝐸)) |
262 | | eqid 2733 |
. . . . . . . . . 10
⊢ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) |
263 | | oveq1 7403 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝐷 → (𝑟 ·s 𝐸) = (𝐷 ·s 𝐸)) |
264 | 263 | oveq1d 7411 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝐷 → ((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠))) |
265 | | oveq1 7403 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝐷 → (𝑟 ·s 𝑠) = (𝐷 ·s 𝑠)) |
266 | 264, 265 | oveq12d 7414 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝐷 → (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠))) |
267 | 266 | eqeq2d 2744 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝐷 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠)))) |
268 | | oveq2 7404 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝐹 → (𝐶 ·s 𝑠) = (𝐶 ·s 𝐹)) |
269 | 268 | oveq2d 7412 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝐹 → ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹))) |
270 | | oveq2 7404 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝐹 → (𝐷 ·s 𝑠) = (𝐷 ·s 𝐹)) |
271 | 269, 270 | oveq12d 7414 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝐹 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹))) |
272 | 271 | eqeq2d 2744 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝐹 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)))) |
273 | 267, 272 | rspc2ev 3622 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ ( R ‘𝐶) ∧ 𝐹 ∈ ( R ‘𝐸) ∧ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹))) → ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))) |
274 | 262, 273 | mp3an3 1451 |
. . . . . . . . 9
⊢ ((𝐷 ∈ ( R ‘𝐶) ∧ 𝐹 ∈ ( R ‘𝐸)) → ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))) |
275 | 255, 261,
274 | syl2anc 585 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))) |
276 | | ovex 7429 |
. . . . . . . . 9
⊢ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) ∈ V |
277 | | eqeq1 2737 |
. . . . . . . . . 10
⊢ (ℎ = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) → (ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)))) |
278 | 277 | 2rexbidv 3220 |
. . . . . . . . 9
⊢ (ℎ = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) → (∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)))) |
279 | 276, 278 | elab 3666 |
. . . . . . . 8
⊢ ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) ∈ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))} ↔ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))) |
280 | 275, 279 | sylibr 233 |
. . . . . . 7
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) ∈ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |
281 | | elun2 4175 |
. . . . . . 7
⊢ ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) ∈ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))} → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) ∈ ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐶)∃𝑞 ∈ ( L ‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐶 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))})) |
282 | 280, 281 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) ∈ ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐶)∃𝑞 ∈ ( L ‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐶 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))})) |
283 | | ovex 7429 |
. . . . . . . 8
⊢ (𝐶 ·s 𝐸) ∈ V |
284 | 283 | snid 4660 |
. . . . . . 7
⊢ (𝐶 ·s 𝐸) ∈ {(𝐶 ·s 𝐸)} |
285 | 284 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → (𝐶 ·s 𝐸) ∈ {(𝐶 ·s 𝐸)}) |
286 | 249, 282,
285 | ssltsepcd 27262 |
. . . . 5
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸)) |
287 | 107, 94 | addscomd 27418 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸))) |
288 | 287 | oveq1d 7411 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐷 ·s 𝐹))) |
289 | 94, 107, 127 | addsubsassd 27515 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐷 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)))) |
290 | 288, 289 | eqtrd 2773 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)))) |
291 | 290 | breq1d 5154 |
. . . . . . . 8
⊢ (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))) <s (𝐶 ·s 𝐸))) |
292 | 107, 127 | subscld 27502 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) ∈ No
) |
293 | 94, 292, 122 | sltaddsub2d 27526 |
. . . . . . . 8
⊢ (𝜑 → (((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))) <s (𝐶 ·s 𝐸) ↔ ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)))) |
294 | 291, 293 | bitrd 279 |
. . . . . . 7
⊢ (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)))) |
295 | 294, 185 | bitrd 279 |
. . . . . 6
⊢ (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))) |
296 | 295 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))) |
297 | 286, 296 | mpbid 231 |
. . . 4
⊢ ((𝜑 ∧ ((
bday ‘𝐷)
∈ ( bday ‘𝐶) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))) |
298 | 297 | anassrs 469 |
. . 3
⊢ (((𝜑 ∧ (
bday ‘𝐷)
∈ ( bday ‘𝐶)) ∧ ( bday
‘𝐹) ∈
( bday ‘𝐸)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))) |
299 | 190 | adantr 482 |
. . 3
⊢ ((𝜑 ∧ (
bday ‘𝐷)
∈ ( bday ‘𝐶)) → (( bday
‘𝐸) ∈
( bday ‘𝐹) ∨ ( bday
‘𝐹) ∈
( bday ‘𝐸))) |
300 | 247, 298,
299 | mpjaodan 958 |
. 2
⊢ ((𝜑 ∧ (
bday ‘𝐷)
∈ ( bday ‘𝐶)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))) |
301 | | mulsproplem12.1 |
. 2
⊢ (𝜑 → ((
bday ‘𝐶)
∈ ( bday ‘𝐷) ∨ ( bday
‘𝐷) ∈
( bday ‘𝐶))) |
302 | 192, 300,
301 | mpjaodan 958 |
1
⊢ (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))) |