| Step | Hyp | Ref
| Expression |
| 1 | | 0z 12624 |
. . . 4
⊢ 0 ∈
ℤ |
| 2 | | fzrevral 13652 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 0 ∈
ℤ) → (∀𝑗
∈ (𝑀...𝑁)𝜑 ↔ ∀𝑥 ∈ ((0 − 𝑁)...(0 − 𝑀))[(0 − 𝑥) / 𝑗]𝜑)) |
| 3 | 1, 2 | mp3an3 1452 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑥 ∈ ((0 − 𝑁)...(0 − 𝑀))[(0 − 𝑥) / 𝑗]𝜑)) |
| 4 | 3 | 3adant3 1133 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) →
(∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑥 ∈ ((0 − 𝑁)...(0 − 𝑀))[(0 − 𝑥) / 𝑗]𝜑)) |
| 5 | | zsubcl 12659 |
. . . . 5
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → (0 − 𝑁) ∈ ℤ) |
| 6 | 1, 5 | mpan 690 |
. . . 4
⊢ (𝑁 ∈ ℤ → (0
− 𝑁) ∈
ℤ) |
| 7 | | zsubcl 12659 |
. . . . 5
⊢ ((0
∈ ℤ ∧ 𝑀
∈ ℤ) → (0 − 𝑀) ∈ ℤ) |
| 8 | 1, 7 | mpan 690 |
. . . 4
⊢ (𝑀 ∈ ℤ → (0
− 𝑀) ∈
ℤ) |
| 9 | | id 22 |
. . . 4
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℤ) |
| 10 | | fzrevral 13652 |
. . . 4
⊢ (((0
− 𝑁) ∈ ℤ
∧ (0 − 𝑀) ∈
ℤ ∧ 𝐾 ∈
ℤ) → (∀𝑥
∈ ((0 − 𝑁)...(0
− 𝑀))[(0
− 𝑥) / 𝑗]𝜑 ↔ ∀𝑘 ∈ ((𝐾 − (0 − 𝑀))...(𝐾 − (0 − 𝑁)))[(𝐾 − 𝑘) / 𝑥][(0 − 𝑥) / 𝑗]𝜑)) |
| 11 | 6, 8, 9, 10 | syl3an 1161 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) →
(∀𝑥 ∈ ((0
− 𝑁)...(0 −
𝑀))[(0 − 𝑥) / 𝑗]𝜑 ↔ ∀𝑘 ∈ ((𝐾 − (0 − 𝑀))...(𝐾 − (0 − 𝑁)))[(𝐾 − 𝑘) / 𝑥][(0 − 𝑥) / 𝑗]𝜑)) |
| 12 | 11 | 3com12 1124 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) →
(∀𝑥 ∈ ((0
− 𝑁)...(0 −
𝑀))[(0 − 𝑥) / 𝑗]𝜑 ↔ ∀𝑘 ∈ ((𝐾 − (0 − 𝑀))...(𝐾 − (0 − 𝑁)))[(𝐾 − 𝑘) / 𝑥][(0 − 𝑥) / 𝑗]𝜑)) |
| 13 | | ovex 7464 |
. . . . 5
⊢ (𝐾 − 𝑘) ∈ V |
| 14 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = (𝐾 − 𝑘) → (0 − 𝑥) = (0 − (𝐾 − 𝑘))) |
| 15 | 14 | sbcco3gw 4425 |
. . . . 5
⊢ ((𝐾 − 𝑘) ∈ V → ([(𝐾 − 𝑘) / 𝑥][(0 − 𝑥) / 𝑗]𝜑 ↔ [(0 − (𝐾 − 𝑘)) / 𝑗]𝜑)) |
| 16 | 13, 15 | ax-mp 5 |
. . . 4
⊢
([(𝐾 −
𝑘) / 𝑥][(0 − 𝑥) / 𝑗]𝜑 ↔ [(0 − (𝐾 − 𝑘)) / 𝑗]𝜑) |
| 17 | 16 | ralbii 3093 |
. . 3
⊢
(∀𝑘 ∈
((𝐾 − (0 −
𝑀))...(𝐾 − (0 − 𝑁)))[(𝐾 − 𝑘) / 𝑥][(0 − 𝑥) / 𝑗]𝜑 ↔ ∀𝑘 ∈ ((𝐾 − (0 − 𝑀))...(𝐾 − (0 − 𝑁)))[(0 − (𝐾 − 𝑘)) / 𝑗]𝜑) |
| 18 | | zcn 12618 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
| 19 | | zcn 12618 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
| 20 | | zcn 12618 |
. . . . . 6
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℂ) |
| 21 | | df-neg 11495 |
. . . . . . . . . . 11
⊢ -𝑀 = (0 − 𝑀) |
| 22 | 21 | oveq2i 7442 |
. . . . . . . . . 10
⊢ (𝐾 − -𝑀) = (𝐾 − (0 − 𝑀)) |
| 23 | | subneg 11558 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝐾 − -𝑀) = (𝐾 + 𝑀)) |
| 24 | | addcom 11447 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝐾 + 𝑀) = (𝑀 + 𝐾)) |
| 25 | 23, 24 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝐾 − -𝑀) = (𝑀 + 𝐾)) |
| 26 | 22, 25 | eqtr3id 2791 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝐾 − (0 − 𝑀)) = (𝑀 + 𝐾)) |
| 27 | 26 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝐾 − (0 − 𝑀)) = (𝑀 + 𝐾)) |
| 28 | | df-neg 11495 |
. . . . . . . . . . 11
⊢ -𝑁 = (0 − 𝑁) |
| 29 | 28 | oveq2i 7442 |
. . . . . . . . . 10
⊢ (𝐾 − -𝑁) = (𝐾 − (0 − 𝑁)) |
| 30 | | subneg 11558 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝐾 − -𝑁) = (𝐾 + 𝑁)) |
| 31 | | addcom 11447 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝐾 + 𝑁) = (𝑁 + 𝐾)) |
| 32 | 30, 31 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝐾 − -𝑁) = (𝑁 + 𝐾)) |
| 33 | 29, 32 | eqtr3id 2791 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝐾 − (0 − 𝑁)) = (𝑁 + 𝐾)) |
| 34 | 33 | 3adant2 1132 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝐾 − (0 − 𝑁)) = (𝑁 + 𝐾)) |
| 35 | 27, 34 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝐾 − (0 − 𝑀))...(𝐾 − (0 − 𝑁))) = ((𝑀 + 𝐾)...(𝑁 + 𝐾))) |
| 36 | 35 | 3coml 1128 |
. . . . . 6
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐾 ∈ ℂ) → ((𝐾 − (0 − 𝑀))...(𝐾 − (0 − 𝑁))) = ((𝑀 + 𝐾)...(𝑁 + 𝐾))) |
| 37 | 18, 19, 20, 36 | syl3an 1161 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝐾 − (0 − 𝑀))...(𝐾 − (0 − 𝑁))) = ((𝑀 + 𝐾)...(𝑁 + 𝐾))) |
| 38 | 37 | raleqdv 3326 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) →
(∀𝑘 ∈ ((𝐾 − (0 − 𝑀))...(𝐾 − (0 − 𝑁)))[(0 − (𝐾 − 𝑘)) / 𝑗]𝜑 ↔ ∀𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))[(0 − (𝐾 − 𝑘)) / 𝑗]𝜑)) |
| 39 | | elfzelz 13564 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) → 𝑘 ∈ ℤ) |
| 40 | 39 | zcnd 12723 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) → 𝑘 ∈ ℂ) |
| 41 | | df-neg 11495 |
. . . . . . . . 9
⊢ -(𝐾 − 𝑘) = (0 − (𝐾 − 𝑘)) |
| 42 | | negsubdi2 11568 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → -(𝐾 − 𝑘) = (𝑘 − 𝐾)) |
| 43 | 41, 42 | eqtr3id 2791 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (0
− (𝐾 − 𝑘)) = (𝑘 − 𝐾)) |
| 44 | 20, 40, 43 | syl2an 596 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) → (0 − (𝐾 − 𝑘)) = (𝑘 − 𝐾)) |
| 45 | 44 | sbceq1d 3793 |
. . . . . 6
⊢ ((𝐾 ∈ ℤ ∧ 𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) → ([(0 − (𝐾 − 𝑘)) / 𝑗]𝜑 ↔ [(𝑘 − 𝐾) / 𝑗]𝜑)) |
| 46 | 45 | ralbidva 3176 |
. . . . 5
⊢ (𝐾 ∈ ℤ →
(∀𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))[(0 − (𝐾 − 𝑘)) / 𝑗]𝜑 ↔ ∀𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))[(𝑘 − 𝐾) / 𝑗]𝜑)) |
| 47 | 46 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) →
(∀𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))[(0 − (𝐾 − 𝑘)) / 𝑗]𝜑 ↔ ∀𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))[(𝑘 − 𝐾) / 𝑗]𝜑)) |
| 48 | 38, 47 | bitrd 279 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) →
(∀𝑘 ∈ ((𝐾 − (0 − 𝑀))...(𝐾 − (0 − 𝑁)))[(0 − (𝐾 − 𝑘)) / 𝑗]𝜑 ↔ ∀𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))[(𝑘 − 𝐾) / 𝑗]𝜑)) |
| 49 | 17, 48 | bitrid 283 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) →
(∀𝑘 ∈ ((𝐾 − (0 − 𝑀))...(𝐾 − (0 − 𝑁)))[(𝐾 − 𝑘) / 𝑥][(0 − 𝑥) / 𝑗]𝜑 ↔ ∀𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))[(𝑘 − 𝐾) / 𝑗]𝜑)) |
| 50 | 4, 12, 49 | 3bitrd 305 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) →
(∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))[(𝑘 − 𝐾) / 𝑗]𝜑)) |