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

Metamath Proof Explorer

Theorem fzind2

Description: Induction on the integers from M to N inclusive. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. Version of fzind using integer range definitions. (Contributed by Mario Carneiro, 6-Feb-2016)

Ref Expression
Hypotheses fzind2.1 ⊢ ( 𝑥 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
fzind2.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
fzind2.3 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
fzind2.4 ⊢ ( 𝑥 = 𝐾 → ( 𝜑 ↔ 𝜏 ) )
fzind2.5 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝜓 )
fzind2.6 ⊢ ( 𝑦 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝜒 → 𝜃 ) )
Assertion fzind2 ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝜏 )

Proof

Step Hyp Ref Expression
1 fzind2.1 ⊢ ( 𝑥 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
2 fzind2.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3 fzind2.3 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
4 fzind2.4 ⊢ ( 𝑥 = 𝐾 → ( 𝜑 ↔ 𝜏 ) )
5 fzind2.5 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝜓 )
6 fzind2.6 ⊢ ( 𝑦 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝜒 → 𝜃 ) )
7 elfz2 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
8 anass ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) ) )
9 df-3an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) )
10 9 anbi1i ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) ↔ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
11 3anass ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
12 11 anbi2i ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) ) )
13 8 10 12 3bitr4i ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
14 7 13 bitri ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
15 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
16 15 5 sylbir ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝜓 )
17 3anass ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ↔ ( 𝑦 ∈ ℤ ∧ ( 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) )
18 elfzo ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑦 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) )
19 18 6 biimtrrdi ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( 𝜒 → 𝜃 ) ) )
20 19 3coml ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( 𝜒 → 𝜃 ) ) )
21 20 3expa ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( 𝜒 → 𝜃 ) ) )
22 21 impr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ ℤ ∧ ( 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) ) → ( 𝜒 → 𝜃 ) )
23 17 22 sylan2b ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 𝜒 → 𝜃 ) )
24 1 2 3 4 16 23 fzind ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) → 𝜏 )
25 14 24 sylbi ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝜏 )