This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) 𝜑 ↔ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 ) )