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	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall j \in (M ..^N) φ \leftrightarrow \forall k \in (M + K ..^N + K) \underset{˙}{[} (k - K) / j \underset{˙}{]} φ)$

Proof

Step	Hyp	Ref	Expression
1		fzoval	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$
2	1	3ad2ant2	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (M ..^N) = (M \dots N - 1)$
3	2	raleqdv	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall j \in (M ..^N) φ \leftrightarrow \forall j \in (M \dots N - 1) φ)$
4		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
5		fzshftral	$⊢ (M \in ℤ \land N - 1 \in ℤ \land K \in ℤ) \to (\forall j \in (M \dots N - 1) φ \leftrightarrow \forall k \in (M + K \dots N - 1 + K) \underset{˙}{[} (k - K) / j \underset{˙}{]} φ)$
6	4 5	syl3an2	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall j \in (M \dots N - 1) φ \leftrightarrow \forall k \in (M + K \dots N - 1 + K) \underset{˙}{[} (k - K) / j \underset{˙}{]} φ)$
7		zaddcl	$⊢ (N \in ℤ \land K \in ℤ) \to N + K \in ℤ$
8	7	3adant1	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to N + K \in ℤ$
9		fzoval	$⊢ N + K \in ℤ \to (M + K ..^N + K) = (M + K \dots N + K - 1)$
10	8 9	syl	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (M + K ..^N + K) = (M + K \dots N + K - 1)$
11		zcn	$⊢ N \in ℤ \to N \in ℂ$
12	11	adantr	$⊢ (N \in ℤ \land K \in ℤ) \to N \in ℂ$
13		zcn	$⊢ K \in ℤ \to K \in ℂ$
14	13	adantl	$⊢ (N \in ℤ \land K \in ℤ) \to K \in ℂ$
15		1cnd	$⊢ (N \in ℤ \land K \in ℤ) \to 1 \in ℂ$
16	12 14 15	addsubd	$⊢ (N \in ℤ \land K \in ℤ) \to N + K - 1 = N - 1 + K$
17	16	3adant1	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to N + K - 1 = N - 1 + K$
18	17	oveq2d	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (M + K \dots N + K - 1) = (M + K \dots N - 1 + K)$
19	10 18	eqtr2d	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (M + K \dots N - 1 + K) = (M + K ..^N + K)$
20	19	raleqdv	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall k \in (M + K \dots N - 1 + K) \underset{˙}{[} (k - K) / j \underset{˙}{]} φ \leftrightarrow \forall k \in (M + K ..^N + K) \underset{˙}{[} (k - K) / j \underset{˙}{]} φ)$
21	3 6 20	3bitrd	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall j \in (M ..^N) φ \leftrightarrow \forall k \in (M + K ..^N + K) \underset{˙}{[} (k - K) / j \underset{˙}{]} φ)$

Metamath Proof Explorer

Theorem fzoshftral

Proof