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 -> ( ph <-> ps ) )
	uzind3.2	|- ( j = m -> ( ph <-> ch ) )
	uzind3.3	|- ( j = ( m + 1 ) -> ( ph <-> th ) )
	uzind3.4	|- ( j = N -> ( ph <-> ta ) )
	uzind3.5	|- ( M e. ZZ -> ps )
	uzind3.6	|- ( ( M e. ZZ /\ m e. { k e. ZZ | M <_ k } ) -> ( ch -> th ) )
Assertion	uzind3	|- ( ( M e. ZZ /\ N e. { k e. ZZ | M <_ k } ) -> ta )

Proof

Step	Hyp	Ref	Expression
1		uzind3.1	|- ( j = M -> ( ph <-> ps ) )
2		uzind3.2	|- ( j = m -> ( ph <-> ch ) )
3		uzind3.3	|- ( j = ( m + 1 ) -> ( ph <-> th ) )
4		uzind3.4	|- ( j = N -> ( ph <-> ta ) )
5		uzind3.5	|- ( M e. ZZ -> ps )
6		uzind3.6	|- ( ( M e. ZZ /\ m e. { k e. ZZ | M <_ k } ) -> ( ch -> th ) )
7		breq2	|- ( k = N -> ( M <_ k <-> M <_ N ) )
8	7	elrab	|- ( N e. { k e. ZZ | M <_ k } <-> ( N e. ZZ /\ M <_ N ) )
9		breq2	|- ( k = m -> ( M <_ k <-> M <_ m ) )
10	9	elrab	|- ( m e. { k e. ZZ | M <_ k } <-> ( m e. ZZ /\ M <_ m ) )
11	10 6	sylan2br	|- ( ( M e. ZZ /\ ( m e. ZZ /\ M <_ m ) ) -> ( ch -> th ) )
12	11	3impb	|- ( ( M e. ZZ /\ m e. ZZ /\ M <_ m ) -> ( ch -> th ) )
13	1 2 3 4 5 12	uzind	|- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ta )
14	13	3expb	|- ( ( M e. ZZ /\ ( N e. ZZ /\ M <_ N ) ) -> ta )
15	8 14	sylan2b	|- ( ( M e. ZZ /\ N e. { k e. ZZ | M <_ k } ) -> ta )