Theorem uzind4

Description: Induction on the upper set of integers that starts 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, 7-Sep-2005)

	Ref	Expression
Hypotheses	uzind4.1	|- ( j = M -> ( ph <-> ps ) )
	uzind4.2	|- ( j = k -> ( ph <-> ch ) )
	uzind4.3	|- ( j = ( k + 1 ) -> ( ph <-> th ) )
	uzind4.4	|- ( j = N -> ( ph <-> ta ) )
	uzind4.5	|- ( M e. ZZ -> ps )
	uzind4.6	|- ( k e. ( ZZ>= ` M ) -> ( ch -> th ) )
Assertion	uzind4	|- ( N e. ( ZZ>= ` M ) -> ta )

Proof

Step	Hyp	Ref	Expression
1		uzind4.1	|- ( j = M -> ( ph <-> ps ) )
2		uzind4.2	|- ( j = k -> ( ph <-> ch ) )
3		uzind4.3	|- ( j = ( k + 1 ) -> ( ph <-> th ) )
4		uzind4.4	|- ( j = N -> ( ph <-> ta ) )
5		uzind4.5	|- ( M e. ZZ -> ps )
6		uzind4.6	|- ( k e. ( ZZ>= ` M ) -> ( ch -> th ) )
7		eluzel2	|- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
8		breq2	|- ( m = N -> ( M <_ m <-> M <_ N ) )
9		eluzelz	|- ( N e. ( ZZ>= ` M ) -> N e. ZZ )
10		eluzle	|- ( N e. ( ZZ>= ` M ) -> M <_ N )
11	8 9 10	elrabd	|- ( N e. ( ZZ>= ` M ) -> N e. { m e. ZZ | M <_ m } )
12		breq2	|- ( m = k -> ( M <_ m <-> M <_ k ) )
13	12	elrab	|- ( k e. { m e. ZZ | M <_ m } <-> ( k e. ZZ /\ M <_ k ) )
14		eluz2	|- ( k e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ k e. ZZ /\ M <_ k ) )
15	14	biimpri	|- ( ( M e. ZZ /\ k e. ZZ /\ M <_ k ) -> k e. ( ZZ>= ` M ) )
16	15	3expb	|- ( ( M e. ZZ /\ ( k e. ZZ /\ M <_ k ) ) -> k e. ( ZZ>= ` M ) )
17	13 16	sylan2b	|- ( ( M e. ZZ /\ k e. { m e. ZZ | M <_ m } ) -> k e. ( ZZ>= ` M ) )
18	17 6	syl	|- ( ( M e. ZZ /\ k e. { m e. ZZ | M <_ m } ) -> ( ch -> th ) )
19	1 2 3 4 5 18	uzind3	|- ( ( M e. ZZ /\ N e. { m e. ZZ | M <_ m } ) -> ta )
20	7 11 19	syl2anc	|- ( N e. ( ZZ>= ` M ) -> ta )