Metamath Proof Explorer

Theorem fzoshftral

Description: Shift the scanning order inside of a universal quantification restricted to a half-open integer range, analogous to fzshftral . (Contributed by Alexander van der Vekens, 23-Sep-2018)

Ref Expression
Assertion fzoshftral ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ..^ ( 𝑁 + 𝐾 ) ) [ ( 𝑘 − 𝐾 ) / 𝑗 ] 𝜑 ) )

Proof

Step Hyp Ref Expression
1 fzoval ⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
2 1 3ad2ant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
3 2 raleqdv ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) 𝜑 ↔ ∀ 𝑗 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝜑 ) )
4 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
5 fzshftral ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( ( 𝑁 − 1 ) + 𝐾 ) ) [ ( 𝑘 − 𝐾 ) / 𝑗 ] 𝜑 ) )
6 4 5 syl3an2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( ( 𝑁 − 1 ) + 𝐾 ) ) [ ( 𝑘 − 𝐾 ) / 𝑗 ] 𝜑 ) )
7 zaddcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 + 𝐾 ) ∈ ℤ )
8 7 3adant1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 + 𝐾 ) ∈ ℤ )
9 fzoval ⊢ ( ( 𝑁 + 𝐾 ) ∈ ℤ → ( ( 𝑀 + 𝐾 ) ..^ ( 𝑁 + 𝐾 ) ) = ( ( 𝑀 + 𝐾 ) ... ( ( 𝑁 + 𝐾 ) − 1 ) ) )
10 8 9 syl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 + 𝐾 ) ..^ ( 𝑁 + 𝐾 ) ) = ( ( 𝑀 + 𝐾 ) ... ( ( 𝑁 + 𝐾 ) − 1 ) ) )
11 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
12 11 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝑁 ∈ ℂ )
13 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
14 13 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝐾 ∈ ℂ )
15 1cnd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 1 ∈ ℂ )
16 12 14 15 addsubd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑁 + 𝐾 ) − 1 ) = ( ( 𝑁 − 1 ) + 𝐾 ) )
17 16 3adant1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑁 + 𝐾 ) − 1 ) = ( ( 𝑁 − 1 ) + 𝐾 ) )
18 17 oveq2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 + 𝐾 ) ... ( ( 𝑁 + 𝐾 ) − 1 ) ) = ( ( 𝑀 + 𝐾 ) ... ( ( 𝑁 − 1 ) + 𝐾 ) ) )
19 10 18 eqtr2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 + 𝐾 ) ... ( ( 𝑁 − 1 ) + 𝐾 ) ) = ( ( 𝑀 + 𝐾 ) ..^ ( 𝑁 + 𝐾 ) ) )
20 19 raleqdv ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( ( 𝑁 − 1 ) + 𝐾 ) ) [ ( 𝑘 − 𝐾 ) / 𝑗 ] 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ..^ ( 𝑁 + 𝐾 ) ) [ ( 𝑘 − 𝐾 ) / 𝑗 ] 𝜑 ) )
21 3 6 20 3bitrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ..^ ( 𝑁 + 𝐾 ) ) [ ( 𝑘 − 𝐾 ) / 𝑗 ] 𝜑 ) )