This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fz0add1fz1

Description: Translate membership in a 0-based half-open integer range into membership in a 1-based finite sequence of integers. (Contributed by Alexander van der Vekens, 23-Nov-2017)

Ref Expression
Assertion fz0add1fz1 ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑋 + 1 ) ∈ ( 1 ... 𝑁 ) )

Proof

Step Hyp Ref Expression
1 1z ⊢ 1 ∈ ℤ
2 fzoaddel ⊢ ( ( 𝑋 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ℤ ) → ( 𝑋 + 1 ) ∈ ( ( 0 + 1 ) ..^ ( 𝑁 + 1 ) ) )
3 1 2 mpan2 ⊢ ( 𝑋 ∈ ( 0 ..^ 𝑁 ) → ( 𝑋 + 1 ) ∈ ( ( 0 + 1 ) ..^ ( 𝑁 + 1 ) ) )
4 3 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑋 + 1 ) ∈ ( ( 0 + 1 ) ..^ ( 𝑁 + 1 ) ) )
5 0p1e1 ⊢ ( 0 + 1 ) = 1
6 5 oveq1i ⊢ ( ( 0 + 1 ) ..^ ( 𝑁 + 1 ) ) = ( 1 ..^ ( 𝑁 + 1 ) )
7 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
8 fzval3 ⊢ ( 𝑁 ∈ ℤ → ( 1 ... 𝑁 ) = ( 1 ..^ ( 𝑁 + 1 ) ) )
9 8 eqcomd ⊢ ( 𝑁 ∈ ℤ → ( 1 ..^ ( 𝑁 + 1 ) ) = ( 1 ... 𝑁 ) )
10 7 9 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 1 ..^ ( 𝑁 + 1 ) ) = ( 1 ... 𝑁 ) )
11 6 10 eqtrid ⊢ ( 𝑁 ∈ ℕ0 → ( ( 0 + 1 ) ..^ ( 𝑁 + 1 ) ) = ( 1 ... 𝑁 ) )
12 11 eleq2d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑋 + 1 ) ∈ ( ( 0 + 1 ) ..^ ( 𝑁 + 1 ) ) ↔ ( 𝑋 + 1 ) ∈ ( 1 ... 𝑁 ) ) )
13 12 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑋 + 1 ) ∈ ( ( 0 + 1 ) ..^ ( 𝑁 + 1 ) ) ↔ ( 𝑋 + 1 ) ∈ ( 1 ... 𝑁 ) ) )
14 4 13 mpbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑋 + 1 ) ∈ ( 1 ... 𝑁 ) )