Theorem fzrevral2

Description: Reversal of scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 25-Nov-2005)

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

Proof

Step	Hyp	Ref	Expression
1		zsubcl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 − 𝑁 ) ∈ ℤ )
2	1	3adant2	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 − 𝑁 ) ∈ ℤ )
3		zsubcl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ∈ ℤ )
4	3	3adant3	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ∈ ℤ )
5		simp1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℤ )
6		fzrevral	⊢ ( ( ( 𝐾 − 𝑁 ) ∈ ℤ ∧ ( 𝐾 − 𝑀 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝐾 − ( 𝐾 − 𝑀 ) ) ... ( 𝐾 − ( 𝐾 − 𝑁 ) ) ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 ) )
7	2 4 5 6	syl3anc	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝐾 − ( 𝐾 − 𝑀 ) ) ... ( 𝐾 − ( 𝐾 − 𝑁 ) ) ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 ) )
8		zcn	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
9		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
10		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
11		nncan	⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝐾 − ( 𝐾 − 𝑀 ) ) = 𝑀 )
12	11	3adant3	⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐾 − ( 𝐾 − 𝑀 ) ) = 𝑀 )
13		nncan	⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐾 − ( 𝐾 − 𝑁 ) ) = 𝑁 )
14	13	3adant2	⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐾 − ( 𝐾 − 𝑁 ) ) = 𝑁 )
15	12 14	oveq12d	⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝐾 − ( 𝐾 − 𝑀 ) ) ... ( 𝐾 − ( 𝐾 − 𝑁 ) ) ) = ( 𝑀 ... 𝑁 ) )
16	8 9 10 15	syl3an	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 − ( 𝐾 − 𝑀 ) ) ... ( 𝐾 − ( 𝐾 − 𝑁 ) ) ) = ( 𝑀 ... 𝑁 ) )
17	16	raleqdv	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑘 ∈ ( ( 𝐾 − ( 𝐾 − 𝑀 ) ) ... ( 𝐾 − ( 𝐾 − 𝑁 ) ) ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 ↔ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 ) )
18	7 17	bitrd	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) 𝜑 ↔ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 ) )
19	18	3coml	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) 𝜑 ↔ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 ) )