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	7	con3i	$⊢ \neg M \in ℤ \to \neg (M \in ℤ \land N \in ℤ)$
9		fzof	$⊢ ..^: ℤ \times ℤ ⟶ 𝒫 ℤ$
10	9	fdmi	$⊢ dom ..^= ℤ \times ℤ$
11	10	ndmov	$⊢ \neg (M \in ℤ \land N \in ℤ) \to (M ..^N) = \emptyset$
12	8 11	syl	$⊢ \neg M \in ℤ \to (M ..^N) = \emptyset$
13		simpl	$⊢ (M \in ℤ \land N - 1 \in ℤ) \to M \in ℤ$
14	13	con3i	$⊢ \neg M \in ℤ \to \neg (M \in ℤ \land N - 1 \in ℤ)$
15		fzf	$⊢ \dots : ℤ \times ℤ ⟶ 𝒫 ℤ$
16	15	fdmi	$⊢ dom \dots = ℤ \times ℤ$
17	16	ndmov	$⊢ \neg (M \in ℤ \land N - 1 \in ℤ) \to (M \dots N - 1) = \emptyset$
18	14 17	syl	$⊢ \neg M \in ℤ \to (M \dots N - 1) = \emptyset$
19	12 18	eqtr4d	$⊢ \neg M \in ℤ \to (M ..^N) = (M \dots N - 1)$
20	19	adantr	$⊢ (\neg M \in ℤ \land N \in ℤ) \to (M ..^N) = (M \dots N - 1)$
21	6 20	pm2.61ian	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$

Metamath Proof Explorer