This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )