Metamath Proof Explorer

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 ⊢ N ∈ ℕ 0 → 1 … N = ℤ ∖ ℤ ≥ N + 1 ∩ ℕ

Proof

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