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→τ