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

Metamath Proof Explorer

Theorem uzind4s2

Description: Induction on the upper set of integers that starts at an integer M , using explicit substitution. The hypotheses are the basis and the induction step. Use this instead of uzind4s when j and k must be distinct in [. ( k + 1 ) / j ]. ph . (Contributed by NM, 16-Nov-2005)

Ref Expression
Hypotheses uzind4s2.1 
|- ( M e. ZZ -> [. M / j ]. ph )
uzind4s2.2 
|- ( k e. ( ZZ>= ` M ) -> ( [. k / j ]. ph -> [. ( k + 1 ) / j ]. ph ) )
Assertion uzind4s2 
|- ( N e. ( ZZ>= ` M ) -> [. N / j ]. ph )

Proof

Step Hyp Ref Expression
1 uzind4s2.1 
 |-  ( M e. ZZ -> [. M / j ]. ph )
2 uzind4s2.2 
 |-  ( k e. ( ZZ>= ` M ) -> ( [. k / j ]. ph -> [. ( k + 1 ) / j ]. ph ) )
3 dfsbcq 
 |-  ( m = M -> ( [. m / j ]. ph <-> [. M / j ]. ph ) )
4 dfsbcq 
 |-  ( m = n -> ( [. m / j ]. ph <-> [. n / j ]. ph ) )
5 dfsbcq 
 |-  ( m = ( n + 1 ) -> ( [. m / j ]. ph <-> [. ( n + 1 ) / j ]. ph ) )
6 dfsbcq 
 |-  ( m = N -> ( [. m / j ]. ph <-> [. N / j ]. ph ) )
7 dfsbcq 
 |-  ( k = n -> ( [. k / j ]. ph <-> [. n / j ]. ph ) )
8 oveq1 
 |-  ( k = n -> ( k + 1 ) = ( n + 1 ) )
9 8 sbceq1d 
 |-  ( k = n -> ( [. ( k + 1 ) / j ]. ph <-> [. ( n + 1 ) / j ]. ph ) )
10 7 9 imbi12d 
 |-  ( k = n -> ( ( [. k / j ]. ph -> [. ( k + 1 ) / j ]. ph ) <-> ( [. n / j ]. ph -> [. ( n + 1 ) / j ]. ph ) ) )
11 10 2 vtoclga 
 |-  ( n e. ( ZZ>= ` M ) -> ( [. n / j ]. ph -> [. ( n + 1 ) / j ]. ph ) )
12 3 4 5 6 1 11 uzind4 
 |-  ( N e. ( ZZ>= ` M ) -> [. N / j ]. ph )