Proof of Theorem mulsproplemcbv
Step | Hyp | Ref
| Expression |
1 | | mulsproplem.1 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 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 | | fveq2 6879 |
. . . . . . 7
⊢ (𝑎 = 𝑔 → ( bday
‘𝑎) = ( bday ‘𝑔)) |
3 | 2 | oveq1d 7409 |
. . . . . 6
⊢ (𝑎 = 𝑔 → (( bday
‘𝑎) +no ( bday ‘𝑏)) = (( bday
‘𝑔) +no ( bday ‘𝑏))) |
4 | 3 | uneq1d 4159 |
. . . . 5
⊢ (𝑎 = 𝑔 → ((( bday
‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday
‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒))))) = ((( bday
‘𝑔) +no ( bday ‘𝑏)) ∪ (((( bday
‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒)))))) |
5 | 4 | eleq1d 2818 |
. . . 4
⊢ (𝑎 = 𝑔 → (((( 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 ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸))))))) |
6 | | oveq1 7401 |
. . . . . 6
⊢ (𝑎 = 𝑔 → (𝑎 ·s 𝑏) = (𝑔 ·s 𝑏)) |
7 | 6 | eleq1d 2818 |
. . . . 5
⊢ (𝑎 = 𝑔 → ((𝑎 ·s 𝑏) ∈ No
↔ (𝑔
·s 𝑏)
∈ No )) |
8 | 7 | anbi1d 630 |
. . . 4
⊢ (𝑎 = 𝑔 → (((𝑎 ·s 𝑏) ∈ No
∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s 𝑏) ∈ No
∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
9 | 5, 8 | imbi12d 344 |
. . 3
⊢ (𝑎 = 𝑔 → ((((( 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
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s 𝑏) ∈ No
∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))) |
10 | | fveq2 6879 |
. . . . . . 7
⊢ (𝑏 = ℎ → ( bday
‘𝑏) = ( bday ‘ℎ)) |
11 | 10 | oveq2d 7410 |
. . . . . 6
⊢ (𝑏 = ℎ → (( bday
‘𝑔) +no ( bday ‘𝑏)) = (( bday
‘𝑔) +no ( bday ‘ℎ))) |
12 | 11 | uneq1d 4159 |
. . . . 5
⊢ (𝑏 = ℎ → ((( bday
‘𝑔) +no ( bday ‘𝑏)) ∪ (((( bday
‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒))))) = ((( bday
‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday
‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒)))))) |
13 | 12 | eleq1d 2818 |
. . . 4
⊢ (𝑏 = ℎ → (((( 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 ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸))))))) |
14 | | oveq2 7402 |
. . . . . 6
⊢ (𝑏 = ℎ → (𝑔 ·s 𝑏) = (𝑔 ·s ℎ)) |
15 | 14 | eleq1d 2818 |
. . . . 5
⊢ (𝑏 = ℎ → ((𝑔 ·s 𝑏) ∈ No
↔ (𝑔
·s ℎ)
∈ No )) |
16 | 15 | anbi1d 630 |
. . . 4
⊢ (𝑏 = ℎ → (((𝑔 ·s 𝑏) ∈ No
∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s ℎ) ∈ No
∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
17 | 13, 16 | imbi12d 344 |
. . 3
⊢ (𝑏 = ℎ → ((((( 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
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No
∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))) |
18 | | fveq2 6879 |
. . . . . . . . 9
⊢ (𝑐 = 𝑖 → ( bday
‘𝑐) = ( bday ‘𝑖)) |
19 | 18 | oveq1d 7409 |
. . . . . . . 8
⊢ (𝑐 = 𝑖 → (( bday
‘𝑐) +no ( bday ‘𝑒)) = (( bday
‘𝑖) +no ( bday ‘𝑒))) |
20 | 19 | uneq1d 4159 |
. . . . . . 7
⊢ (𝑐 = 𝑖 → ((( bday
‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) = ((( bday
‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓)))) |
21 | 18 | oveq1d 7409 |
. . . . . . . 8
⊢ (𝑐 = 𝑖 → (( bday
‘𝑐) +no ( bday ‘𝑓)) = (( bday
‘𝑖) +no ( bday ‘𝑓))) |
22 | 21 | uneq1d 4159 |
. . . . . . 7
⊢ (𝑐 = 𝑖 → ((( bday
‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒))) = ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒)))) |
23 | 20, 22 | uneq12d 4161 |
. . . . . 6
⊢ (𝑐 = 𝑖 → (((( bday
‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒)))) = (((( bday
‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒))))) |
24 | 23 | uneq2d 4160 |
. . . . 5
⊢ (𝑐 = 𝑖 → ((( bday
‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday
‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒))))) = ((( bday
‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday
‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒)))))) |
25 | 24 | eleq1d 2818 |
. . . 4
⊢ (𝑐 = 𝑖 → (((( 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 ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸))))))) |
26 | | breq1 5145 |
. . . . . . 7
⊢ (𝑐 = 𝑖 → (𝑐 <s 𝑑 ↔ 𝑖 <s 𝑑)) |
27 | 26 | anbi1d 630 |
. . . . . 6
⊢ (𝑐 = 𝑖 → ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) ↔ (𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓))) |
28 | | oveq1 7401 |
. . . . . . . 8
⊢ (𝑐 = 𝑖 → (𝑐 ·s 𝑓) = (𝑖 ·s 𝑓)) |
29 | | oveq1 7401 |
. . . . . . . 8
⊢ (𝑐 = 𝑖 → (𝑐 ·s 𝑒) = (𝑖 ·s 𝑒)) |
30 | 28, 29 | oveq12d 7412 |
. . . . . . 7
⊢ (𝑐 = 𝑖 → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) = ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒))) |
31 | 30 | breq1d 5152 |
. . . . . 6
⊢ (𝑐 = 𝑖 → (((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) ↔ ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) |
32 | 27, 31 | imbi12d 344 |
. . . . 5
⊢ (𝑐 = 𝑖 → (((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))) ↔ ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) |
33 | 32 | anbi2d 629 |
. . . 4
⊢ (𝑐 = 𝑖 → (((𝑔 ·s ℎ) ∈ No
∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s ℎ) ∈ No
∧ ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
34 | 25, 33 | imbi12d 344 |
. . 3
⊢ (𝑐 = 𝑖 → ((((( 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
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No
∧ ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))) |
35 | | fveq2 6879 |
. . . . . . . . 9
⊢ (𝑑 = 𝑗 → ( bday
‘𝑑) = ( bday ‘𝑗)) |
36 | 35 | oveq1d 7409 |
. . . . . . . 8
⊢ (𝑑 = 𝑗 → (( bday
‘𝑑) +no ( bday ‘𝑓)) = (( bday
‘𝑗) +no ( bday ‘𝑓))) |
37 | 36 | uneq2d 4160 |
. . . . . . 7
⊢ (𝑑 = 𝑗 → ((( bday
‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) = ((( bday
‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑓)))) |
38 | 35 | oveq1d 7409 |
. . . . . . . 8
⊢ (𝑑 = 𝑗 → (( bday
‘𝑑) +no ( bday ‘𝑒)) = (( bday
‘𝑗) +no ( bday ‘𝑒))) |
39 | 38 | uneq2d 4160 |
. . . . . . 7
⊢ (𝑑 = 𝑗 → ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒))) = ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑒)))) |
40 | 37, 39 | uneq12d 4161 |
. . . . . 6
⊢ (𝑑 = 𝑗 → (((( bday
‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒)))) = (((( bday
‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑒))))) |
41 | 40 | uneq2d 4160 |
. . . . 5
⊢ (𝑑 = 𝑗 → ((( bday
‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday
‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑑) +no ( bday ‘𝑒))))) = ((( bday
‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday
‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑒)))))) |
42 | 41 | eleq1d 2818 |
. . . 4
⊢ (𝑑 = 𝑗 → (((( 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 ‘𝑓)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑒))))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸))))))) |
43 | | breq2 5146 |
. . . . . . 7
⊢ (𝑑 = 𝑗 → (𝑖 <s 𝑑 ↔ 𝑖 <s 𝑗)) |
44 | 43 | anbi1d 630 |
. . . . . 6
⊢ (𝑑 = 𝑗 → ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) ↔ (𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓))) |
45 | | oveq1 7401 |
. . . . . . . 8
⊢ (𝑑 = 𝑗 → (𝑑 ·s 𝑓) = (𝑗 ·s 𝑓)) |
46 | | oveq1 7401 |
. . . . . . . 8
⊢ (𝑑 = 𝑗 → (𝑑 ·s 𝑒) = (𝑗 ·s 𝑒)) |
47 | 45, 46 | oveq12d 7412 |
. . . . . . 7
⊢ (𝑑 = 𝑗 → ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) = ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))) |
48 | 47 | breq2d 5154 |
. . . . . 6
⊢ (𝑑 = 𝑗 → (((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) ↔ ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))) |
49 | 44, 48 | imbi12d 344 |
. . . . 5
⊢ (𝑑 = 𝑗 → (((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))) ↔ ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))))) |
50 | 49 | anbi2d 629 |
. . . 4
⊢ (𝑑 = 𝑗 → (((𝑔 ·s ℎ) ∈ No
∧ ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s ℎ) ∈ No
∧ ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))))) |
51 | 42, 50 | imbi12d 344 |
. . 3
⊢ (𝑑 = 𝑗 → ((((( 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
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No
∧ ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))))))) |
52 | | fveq2 6879 |
. . . . . . . . 9
⊢ (𝑒 = 𝑘 → ( bday
‘𝑒) = ( bday ‘𝑘)) |
53 | 52 | oveq2d 7410 |
. . . . . . . 8
⊢ (𝑒 = 𝑘 → (( bday
‘𝑖) +no ( bday ‘𝑒)) = (( bday
‘𝑖) +no ( bday ‘𝑘))) |
54 | 53 | uneq1d 4159 |
. . . . . . 7
⊢ (𝑒 = 𝑘 → ((( bday
‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑓))) = ((( bday
‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑓)))) |
55 | 52 | oveq2d 7410 |
. . . . . . . 8
⊢ (𝑒 = 𝑘 → (( bday
‘𝑗) +no ( bday ‘𝑒)) = (( bday
‘𝑗) +no ( bday ‘𝑘))) |
56 | 55 | uneq2d 4160 |
. . . . . . 7
⊢ (𝑒 = 𝑘 → ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑒))) = ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑘)))) |
57 | 54, 56 | uneq12d 4161 |
. . . . . 6
⊢ (𝑒 = 𝑘 → (((( bday
‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑒)))) = (((( bday
‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑘))))) |
58 | 57 | uneq2d 4160 |
. . . . 5
⊢ (𝑒 = 𝑘 → ((( bday
‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday
‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑒))))) = ((( bday
‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday
‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑘)))))) |
59 | 58 | eleq1d 2818 |
. . . 4
⊢ (𝑒 = 𝑘 → (((( 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 ‘𝑓)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸))))))) |
60 | | breq1 5145 |
. . . . . . 7
⊢ (𝑒 = 𝑘 → (𝑒 <s 𝑓 ↔ 𝑘 <s 𝑓)) |
61 | 60 | anbi2d 629 |
. . . . . 6
⊢ (𝑒 = 𝑘 → ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) ↔ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓))) |
62 | | oveq2 7402 |
. . . . . . . 8
⊢ (𝑒 = 𝑘 → (𝑖 ·s 𝑒) = (𝑖 ·s 𝑘)) |
63 | 62 | oveq2d 7410 |
. . . . . . 7
⊢ (𝑒 = 𝑘 → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) = ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘))) |
64 | | oveq2 7402 |
. . . . . . . 8
⊢ (𝑒 = 𝑘 → (𝑗 ·s 𝑒) = (𝑗 ·s 𝑘)) |
65 | 64 | oveq2d 7410 |
. . . . . . 7
⊢ (𝑒 = 𝑘 → ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)) = ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))) |
66 | 63, 65 | breq12d 5155 |
. . . . . 6
⊢ (𝑒 = 𝑘 → (((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)) ↔ ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))) |
67 | 61, 66 | imbi12d 344 |
. . . . 5
⊢ (𝑒 = 𝑘 → (((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))) ↔ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))))) |
68 | 67 | anbi2d 629 |
. . . 4
⊢ (𝑒 = 𝑘 → (((𝑔 ·s ℎ) ∈ No
∧ ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))) ↔ ((𝑔 ·s ℎ) ∈ No
∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))))) |
69 | 59, 68 | imbi12d 344 |
. . 3
⊢ (𝑒 = 𝑘 → ((((( 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
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No
∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))))))) |
70 | | fveq2 6879 |
. . . . . . . . 9
⊢ (𝑓 = 𝑙 → ( bday
‘𝑓) = ( bday ‘𝑙)) |
71 | 70 | oveq2d 7410 |
. . . . . . . 8
⊢ (𝑓 = 𝑙 → (( bday
‘𝑗) +no ( bday ‘𝑓)) = (( bday
‘𝑗) +no ( bday ‘𝑙))) |
72 | 71 | uneq2d 4160 |
. . . . . . 7
⊢ (𝑓 = 𝑙 → ((( bday
‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑓))) = ((( bday
‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑙)))) |
73 | 70 | oveq2d 7410 |
. . . . . . . 8
⊢ (𝑓 = 𝑙 → (( bday
‘𝑖) +no ( bday ‘𝑓)) = (( bday
‘𝑖) +no ( bday ‘𝑙))) |
74 | 73 | uneq1d 4159 |
. . . . . . 7
⊢ (𝑓 = 𝑙 → ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑘))) = ((( bday
‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑘)))) |
75 | 72, 74 | uneq12d 4161 |
. . . . . 6
⊢ (𝑓 = 𝑙 → (((( bday
‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑘)))) = (((( bday
‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday
‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑘))))) |
76 | 75 | uneq2d 4160 |
. . . . 5
⊢ (𝑓 = 𝑙 → ((( bday
‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday
‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday
‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑘))))) = ((( bday
‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday
‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday
‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑘)))))) |
77 | 76 | eleq1d 2818 |
. . . 4
⊢ (𝑓 = 𝑙 → (((( 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 ‘𝑙)) ∪ (( bday
‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸))))))) |
78 | | breq2 5146 |
. . . . . . 7
⊢ (𝑓 = 𝑙 → (𝑘 <s 𝑓 ↔ 𝑘 <s 𝑙)) |
79 | 78 | anbi2d 629 |
. . . . . 6
⊢ (𝑓 = 𝑙 → ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) ↔ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙))) |
80 | | oveq2 7402 |
. . . . . . . 8
⊢ (𝑓 = 𝑙 → (𝑖 ·s 𝑓) = (𝑖 ·s 𝑙)) |
81 | 80 | oveq1d 7409 |
. . . . . . 7
⊢ (𝑓 = 𝑙 → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) = ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘))) |
82 | | oveq2 7402 |
. . . . . . . 8
⊢ (𝑓 = 𝑙 → (𝑗 ·s 𝑓) = (𝑗 ·s 𝑙)) |
83 | 82 | oveq1d 7409 |
. . . . . . 7
⊢ (𝑓 = 𝑙 → ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)) = ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))) |
84 | 81, 83 | breq12d 5155 |
. . . . . 6
⊢ (𝑓 = 𝑙 → (((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)) ↔ ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))) |
85 | 79, 84 | imbi12d 344 |
. . . . 5
⊢ (𝑓 = 𝑙 → (((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))) ↔ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))) |
86 | 85 | anbi2d 629 |
. . . 4
⊢ (𝑓 = 𝑙 → (((𝑔 ·s ℎ) ∈ No
∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))) ↔ ((𝑔 ·s ℎ) ∈ No
∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))) |
87 | 77, 86 | imbi12d 344 |
. . 3
⊢ (𝑓 = 𝑙 → ((((( 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
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No
∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))) |
88 | 9, 17, 34, 51, 69, 87 | cbvral6vw 3242 |
. 2
⊢
(∀𝑎 ∈
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 ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))))) →
((𝑔 ·s
ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))) |
89 | 1, 88 | sylib 217 |
1
⊢ (𝜑 → ∀𝑔 ∈ 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 𝑘)))))) |