Metamath Proof Explorer

Theorem uzind2

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

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

Proof

Step Hyp Ref Expression
1 uzind2.1 ⊢ j = M + 1 → φ ↔ ψ
2 uzind2.2 ⊢ j = k → φ ↔ χ
3 uzind2.3 ⊢ j = k + 1 → φ ↔ θ
4 uzind2.4 ⊢ j = N → φ ↔ τ
5 uzind2.5 ⊢ M ∈ ℤ → ψ
6 uzind2.6 ⊢ M ∈ ℤ ∧ k ∈ ℤ ∧ M < k → χ → θ
7 zltp1le ⊢ M ∈ ℤ ∧ N ∈ ℤ → M < N ↔ M + 1 ≤ N
8 peano2z ⊢ M ∈ ℤ → M + 1 ∈ ℤ
9 1 imbi2d ⊢ j = M + 1 → M ∈ ℤ → φ ↔ M ∈ ℤ → ψ
10 2 imbi2d ⊢ j = k → M ∈ ℤ → φ ↔ M ∈ ℤ → χ
11 3 imbi2d ⊢ j = k + 1 → M ∈ ℤ → φ ↔ M ∈ ℤ → θ
12 4 imbi2d ⊢ j = N → M ∈ ℤ → φ ↔ M ∈ ℤ → τ
13 5 a1i ⊢ M + 1 ∈ ℤ → M ∈ ℤ → ψ
14 zltp1le ⊢ M ∈ ℤ ∧ k ∈ ℤ → M < k ↔ M + 1 ≤ k
15 6 3expia ⊢ M ∈ ℤ ∧ k ∈ ℤ → M < k → χ → θ
16 14 15 sylbird ⊢ M ∈ ℤ ∧ k ∈ ℤ → M + 1 ≤ k → χ → θ
17 16 ex ⊢ M ∈ ℤ → k ∈ ℤ → M + 1 ≤ k → χ → θ
18 17 com3l ⊢ k ∈ ℤ → M + 1 ≤ k → M ∈ ℤ → χ → θ
19 18 imp ⊢ k ∈ ℤ ∧ M + 1 ≤ k → M ∈ ℤ → χ → θ
20 19 3adant1 ⊢ M + 1 ∈ ℤ ∧ k ∈ ℤ ∧ M + 1 ≤ k → M ∈ ℤ → χ → θ
21 20 a2d ⊢ M + 1 ∈ ℤ ∧ k ∈ ℤ ∧ M + 1 ≤ k → M ∈ ℤ → χ → M ∈ ℤ → θ
22 9 10 11 12 13 21 uzind ⊢ M + 1 ∈ ℤ ∧ N ∈ ℤ ∧ M + 1 ≤ N → M ∈ ℤ → τ
23 22 3exp ⊢ M + 1 ∈ ℤ → N ∈ ℤ → M + 1 ≤ N → M ∈ ℤ → τ
24 8 23 syl ⊢ M ∈ ℤ → N ∈ ℤ → M + 1 ≤ N → M ∈ ℤ → τ
25 24 com34 ⊢ M ∈ ℤ → N ∈ ℤ → M ∈ ℤ → M + 1 ≤ N → τ
26 25 pm2.43a ⊢ M ∈ ℤ → N ∈ ℤ → M + 1 ≤ N → τ
27 26 imp ⊢ M ∈ ℤ ∧ N ∈ ℤ → M + 1 ≤ N → τ
28 7 27 sylbid ⊢ M ∈ ℤ ∧ N ∈ ℤ → M < N → τ
29 28 3impia ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M < N → τ