| Step | Hyp | Ref
| Expression |
| 1 | | ovex 7464 |
. . . 4
⊢ (𝑗 − 𝐾) ∈ V |
| 2 | | eqid 2737 |
. . . 4
⊢ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ (𝑗 − 𝐾)) = (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ (𝑗 − 𝐾)) |
| 3 | 1, 2 | fnmpti 6711 |
. . 3
⊢ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ (𝑗 − 𝐾)) Fn ((𝑀 + 𝐾)...(𝑁 + 𝐾)) |
| 4 | 3 | a1i 11 |
. 2
⊢ (𝜑 → (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ (𝑗 − 𝐾)) Fn ((𝑀 + 𝐾)...(𝑁 + 𝐾))) |
| 5 | | ovex 7464 |
. . . 4
⊢ (𝑘 + 𝐾) ∈ V |
| 6 | | eqid 2737 |
. . . 4
⊢ (𝑘 ∈ (𝑀...𝑁) ↦ (𝑘 + 𝐾)) = (𝑘 ∈ (𝑀...𝑁) ↦ (𝑘 + 𝐾)) |
| 7 | 5, 6 | fnmpti 6711 |
. . 3
⊢ (𝑘 ∈ (𝑀...𝑁) ↦ (𝑘 + 𝐾)) Fn (𝑀...𝑁) |
| 8 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) → 𝑘 = (𝑗 − 𝐾)) |
| 9 | 8 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) → (𝑘 + 𝐾) = ((𝑗 − 𝐾) + 𝐾)) |
| 10 | | elfzelz 13564 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) → 𝑗 ∈ ℤ) |
| 11 | 10 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) → 𝑗 ∈ ℤ) |
| 12 | | mptfzshft.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ ℤ) |
| 13 | 12 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) → 𝐾 ∈ ℤ) |
| 14 | | zcn 12618 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
ℂ) |
| 15 | | zcn 12618 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℂ) |
| 16 | | npcan 11517 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ ℂ ∧ 𝐾 ∈ ℂ) → ((𝑗 − 𝐾) + 𝐾) = 𝑗) |
| 17 | 14, 15, 16 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑗 − 𝐾) + 𝐾) = 𝑗) |
| 18 | 11, 13, 17 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) → ((𝑗 − 𝐾) + 𝐾) = 𝑗) |
| 19 | 9, 18 | eqtr2d 2778 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) → 𝑗 = (𝑘 + 𝐾)) |
| 20 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) → 𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) |
| 21 | 19, 20 | eqeltrrd 2842 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) |
| 22 | | mptfzshft.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 23 | 22 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) → 𝑀 ∈ ℤ) |
| 24 | | mptfzshft.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 25 | 24 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) → 𝑁 ∈ ℤ) |
| 26 | 11, 13 | zsubcld 12727 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) → (𝑗 − 𝐾) ∈ ℤ) |
| 27 | 8, 26 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) → 𝑘 ∈ ℤ) |
| 28 | | fzaddel 13598 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))) |
| 29 | 23, 25, 27, 13, 28 | syl22anc 839 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))) |
| 30 | 21, 29 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) → 𝑘 ∈ (𝑀...𝑁)) |
| 31 | 30, 19 | jca 511 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑗 = (𝑘 + 𝐾))) |
| 32 | | simprr 773 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀...𝑁) ∧ 𝑗 = (𝑘 + 𝐾))) → 𝑗 = (𝑘 + 𝐾)) |
| 33 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀...𝑁) ∧ 𝑗 = (𝑘 + 𝐾))) → 𝑘 ∈ (𝑀...𝑁)) |
| 34 | 22 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀...𝑁) ∧ 𝑗 = (𝑘 + 𝐾))) → 𝑀 ∈ ℤ) |
| 35 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀...𝑁) ∧ 𝑗 = (𝑘 + 𝐾))) → 𝑁 ∈ ℤ) |
| 36 | | elfzelz 13564 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ) |
| 37 | 36 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀...𝑁) ∧ 𝑗 = (𝑘 + 𝐾))) → 𝑘 ∈ ℤ) |
| 38 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀...𝑁) ∧ 𝑗 = (𝑘 + 𝐾))) → 𝐾 ∈ ℤ) |
| 39 | 34, 35, 37, 38, 28 | syl22anc 839 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀...𝑁) ∧ 𝑗 = (𝑘 + 𝐾))) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))) |
| 40 | 33, 39 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀...𝑁) ∧ 𝑗 = (𝑘 + 𝐾))) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) |
| 41 | 32, 40 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀...𝑁) ∧ 𝑗 = (𝑘 + 𝐾))) → 𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) |
| 42 | 32 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀...𝑁) ∧ 𝑗 = (𝑘 + 𝐾))) → (𝑗 − 𝐾) = ((𝑘 + 𝐾) − 𝐾)) |
| 43 | | zcn 12618 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℂ) |
| 44 | | pncan 11514 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℂ ∧ 𝐾 ∈ ℂ) → ((𝑘 + 𝐾) − 𝐾) = 𝑘) |
| 45 | 43, 15, 44 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 + 𝐾) − 𝐾) = 𝑘) |
| 46 | 37, 38, 45 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀...𝑁) ∧ 𝑗 = (𝑘 + 𝐾))) → ((𝑘 + 𝐾) − 𝐾) = 𝑘) |
| 47 | 42, 46 | eqtr2d 2778 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀...𝑁) ∧ 𝑗 = (𝑘 + 𝐾))) → 𝑘 = (𝑗 − 𝐾)) |
| 48 | 41, 47 | jca 511 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀...𝑁) ∧ 𝑗 = (𝑘 + 𝐾))) → (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾))) |
| 49 | 31, 48 | impbida 801 |
. . . . 5
⊢ (𝜑 → ((𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ 𝑘 = (𝑗 − 𝐾)) ↔ (𝑘 ∈ (𝑀...𝑁) ∧ 𝑗 = (𝑘 + 𝐾)))) |
| 50 | 49 | mptcnv 6159 |
. . . 4
⊢ (𝜑 → ◡(𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ (𝑗 − 𝐾)) = (𝑘 ∈ (𝑀...𝑁) ↦ (𝑘 + 𝐾))) |
| 51 | 50 | fneq1d 6661 |
. . 3
⊢ (𝜑 → (◡(𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ (𝑗 − 𝐾)) Fn (𝑀...𝑁) ↔ (𝑘 ∈ (𝑀...𝑁) ↦ (𝑘 + 𝐾)) Fn (𝑀...𝑁))) |
| 52 | 7, 51 | mpbiri 258 |
. 2
⊢ (𝜑 → ◡(𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ (𝑗 − 𝐾)) Fn (𝑀...𝑁)) |
| 53 | | dff1o4 6856 |
. 2
⊢ ((𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ (𝑗 − 𝐾)):((𝑀 + 𝐾)...(𝑁 + 𝐾))–1-1-onto→(𝑀...𝑁) ↔ ((𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ (𝑗 − 𝐾)) Fn ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∧ ◡(𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ (𝑗 − 𝐾)) Fn (𝑀...𝑁))) |
| 54 | 4, 52, 53 | sylanbrc 583 |
1
⊢ (𝜑 → (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ (𝑗 − 𝐾)):((𝑀 + 𝐾)...(𝑁 + 𝐾))–1-1-onto→(𝑀...𝑁)) |