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

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 -> ( 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 )