fzoval

Description: Value of the half-open integer set in terms of the closed integer set. (Contributed by Stefan O'Rear, 14-Aug-2015)

		Ref	Expression
	Assertion	fzoval	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$

Step	Hyp	Ref	Expression
1		id	$⊢ m = M \to m = M$
2		oveq1	$⊢ n = N \to n - 1 = N - 1$
3	1 2	oveqan12d	$⊢ (m = M \land n = N) \to (m \dots n - 1) = (M \dots N - 1)$
4		df-fzo	$⊢ ..^= (m \in ℤ, n \in ℤ ⟼ (m \dots n - 1))$
5		ovex	$⊢ (M \dots N - 1) \in V$
6	3 4 5	ovmpoa	$⊢ (M \in ℤ \land N \in ℤ) \to (M ..^N) = (M \dots N - 1)$
7		simpl	$⊢ (M \in ℤ \land N \in ℤ) \to M \in ℤ$
8		fzof	$⊢ ..^: ℤ \times ℤ ⟶ 𝒫 ℤ$
9	8	fdmi	$⊢ dom ..^= ℤ \times ℤ$
10	9	ndmov	$⊢ \neg (M \in ℤ \land N \in ℤ) \to (M ..^N) = \emptyset$
11	7 10	nsyl5	$⊢ \neg M \in ℤ \to (M ..^N) = \emptyset$
12		simpl	$⊢ (M \in ℤ \land N - 1 \in ℤ) \to M \in ℤ$
13		fzf	$⊢ \dots : ℤ \times ℤ ⟶ 𝒫 ℤ$
14	13	fdmi	$⊢ dom \dots = ℤ \times ℤ$
15	14	ndmov	$⊢ \neg (M \in ℤ \land N - 1 \in ℤ) \to (M \dots N - 1) = \emptyset$
16	12 15	nsyl5	$⊢ \neg M \in ℤ \to (M \dots N - 1) = \emptyset$
17	11 16	eqtr4d	$⊢ \neg M \in ℤ \to (M ..^N) = (M \dots N - 1)$
18	17	adantr	$⊢ (\neg M \in ℤ \land N \in ℤ) \to (M ..^N) = (M \dots N - 1)$
19	6 18	pm2.61ian	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$

Metamath Proof Explorer