Metamath Proof Explorer

Theorem uzind3

Description: Induction on the upper integers that start at an integer M . The first four hypotheses give us the substitution instances we need, and the last two are the basis and the induction step. (Contributed by NM, 26-Jul-2005)

Ref Expression
Hypotheses uzind3.1 ⊢ j = M → φ ↔ ψ
uzind3.2 ⊢ j = m → φ ↔ χ
uzind3.3 ⊢ j = m + 1 → φ ↔ θ
uzind3.4 ⊢ j = N → φ ↔ τ
uzind3.5 ⊢ M ∈ ℤ → ψ
uzind3.6 ⊢ M ∈ ℤ ∧ m ∈ k ∈ ℤ | M ≤ k → χ → θ
Assertion uzind3 ⊢ M ∈ ℤ ∧ N ∈ k ∈ ℤ | M ≤ k → τ

Proof

Step Hyp Ref Expression
1 uzind3.1 ⊢ j = M → φ ↔ ψ
2 uzind3.2 ⊢ j = m → φ ↔ χ
3 uzind3.3 ⊢ j = m + 1 → φ ↔ θ
4 uzind3.4 ⊢ j = N → φ ↔ τ
5 uzind3.5 ⊢ M ∈ ℤ → ψ
6 uzind3.6 ⊢ M ∈ ℤ ∧ m ∈ k ∈ ℤ | M ≤ k → χ → θ
7 breq2 ⊢ k = N → M ≤ k ↔ M ≤ N
8 7 elrab ⊢ N ∈ k ∈ ℤ | M ≤ k ↔ N ∈ ℤ ∧ M ≤ N
9 breq2 ⊢ k = m → M ≤ k ↔ M ≤ m
10 9 elrab ⊢ m ∈ k ∈ ℤ | M ≤ k ↔ m ∈ ℤ ∧ M ≤ m
11 10 6 sylan2br ⊢ M ∈ ℤ ∧ m ∈ ℤ ∧ M ≤ m → χ → θ
12 11 3impb ⊢ M ∈ ℤ ∧ m ∈ ℤ ∧ M ≤ m → χ → θ
13 1 2 3 4 5 12 uzind ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N → τ
14 13 3expb ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N → τ
15 8 14 sylan2b ⊢ M ∈ ℤ ∧ N ∈ k ∈ ℤ | M ≤ k → τ