Theorem fz1eqin

Description: Express a one-based finite range as the intersection of lower integers with NN . (Contributed by Stefan O'Rear, 9-Oct-2014)

	Ref	Expression
Assertion	fz1eqin	⊢ ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) = ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) )

Proof

Step	Hyp	Ref	Expression
1		1z	⊢ 1 ∈ ℤ
2		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
3		elfz1	⊢ ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑎 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ∧ 𝑎 ≤ 𝑁 ) ) )
4	1 2 3	sylancr	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑎 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ∧ 𝑎 ≤ 𝑁 ) ) )
5		3anass	⊢ ( ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ∧ 𝑎 ≤ 𝑁 ) ↔ ( 𝑎 ∈ ℤ ∧ ( 1 ≤ 𝑎 ∧ 𝑎 ≤ 𝑁 ) ) )
6		ancom	⊢ ( ( 1 ≤ 𝑎 ∧ 𝑎 ≤ 𝑁 ) ↔ ( 𝑎 ≤ 𝑁 ∧ 1 ≤ 𝑎 ) )
7	6	anbi2i	⊢ ( ( 𝑎 ∈ ℤ ∧ ( 1 ≤ 𝑎 ∧ 𝑎 ≤ 𝑁 ) ) ↔ ( 𝑎 ∈ ℤ ∧ ( 𝑎 ≤ 𝑁 ∧ 1 ≤ 𝑎 ) ) )
8		anandi	⊢ ( ( 𝑎 ∈ ℤ ∧ ( 𝑎 ≤ 𝑁 ∧ 1 ≤ 𝑎 ) ) ↔ ( ( 𝑎 ∈ ℤ ∧ 𝑎 ≤ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) ) )
9	5 7 8	3bitri	⊢ ( ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ∧ 𝑎 ≤ 𝑁 ) ↔ ( ( 𝑎 ∈ ℤ ∧ 𝑎 ≤ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) ) )
10	4 9	bitrdi	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑎 ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝑎 ∈ ℤ ∧ 𝑎 ≤ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) ) ) )
11		elin	⊢ ( 𝑎 ∈ ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ↔ ( 𝑎 ∈ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑎 ∈ ℕ ) )
12		ellz1	⊢ ( 𝑁 ∈ ℤ → ( 𝑎 ∈ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ↔ ( 𝑎 ∈ ℤ ∧ 𝑎 ≤ 𝑁 ) ) )
13	2 12	syl	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑎 ∈ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ↔ ( 𝑎 ∈ ℤ ∧ 𝑎 ≤ 𝑁 ) ) )
14		elnnz1	⊢ ( 𝑎 ∈ ℕ ↔ ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) )
15	14	a1i	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑎 ∈ ℕ ↔ ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) ) )
16	13 15	anbi12d	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑎 ∈ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑎 ∈ ℕ ) ↔ ( ( 𝑎 ∈ ℤ ∧ 𝑎 ≤ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) ) ) )
17	11 16	syl5bb	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑎 ∈ ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ↔ ( ( 𝑎 ∈ ℤ ∧ 𝑎 ≤ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) ) ) )
18	10 17	bitr4d	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑎 ∈ ( 1 ... 𝑁 ) ↔ 𝑎 ∈ ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) )
19	18	eqrdv	⊢ ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) = ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) )