Theorem fzrevral3

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

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

Proof

Step	Hyp	Ref	Expression
1		zaddcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
2		fzrevral	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 ↔ ∀ 𝑘 ∈ ( ( ( 𝑀 + 𝑁 ) − 𝑁 ) ... ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) [ ( ( 𝑀 + 𝑁 ) − 𝑘 ) / 𝑗 ] 𝜑 ) )
3	1 2	mpd3an3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 ↔ ∀ 𝑘 ∈ ( ( ( 𝑀 + 𝑁 ) − 𝑁 ) ... ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) [ ( ( 𝑀 + 𝑁 ) − 𝑘 ) / 𝑗 ] 𝜑 ) )
4		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
5		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
6		pncan	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
7		pncan2	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑀 + 𝑁 ) − 𝑀 ) = 𝑁 )
8	6 7	oveq12d	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( ( 𝑀 + 𝑁 ) − 𝑁 ) ... ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) = ( 𝑀 ... 𝑁 ) )
9	4 5 8	syl2an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑀 + 𝑁 ) − 𝑁 ) ... ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) = ( 𝑀 ... 𝑁 ) )
10	9	raleqdv	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑘 ∈ ( ( ( 𝑀 + 𝑁 ) − 𝑁 ) ... ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) [ ( ( 𝑀 + 𝑁 ) − 𝑘 ) / 𝑗 ] 𝜑 ↔ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) [ ( ( 𝑀 + 𝑁 ) − 𝑘 ) / 𝑗 ] 𝜑 ) )
11	3 10	bitrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 ↔ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) [ ( ( 𝑀 + 𝑁 ) − 𝑘 ) / 𝑗 ] 𝜑 ) )