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 τ