Metamath Proof Explorer

Theorem uzind4s

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. (Contributed by NM, 4-Nov-2005)

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

Proof

Step Hyp Ref Expression
1 uzind4s.1 
 |-  ( M e. ZZ -> [. M / k ]. ph )
2 uzind4s.2 
 |-  ( k e. ( ZZ>= ` M ) -> ( ph -> [. ( k + 1 ) / k ]. ph ) )
3 dfsbcq2 
 |-  ( j = M -> ( [ j / k ] ph <-> [. M / k ]. ph ) )
4 sbequ 
 |-  ( j = m -> ( [ j / k ] ph <-> [ m / k ] ph ) )
5 dfsbcq2 
 |-  ( j = ( m + 1 ) -> ( [ j / k ] ph <-> [. ( m + 1 ) / k ]. ph ) )
6 dfsbcq2 
 |-  ( j = N -> ( [ j / k ] ph <-> [. N / k ]. ph ) )
7 nfv 
 |-  F/ k m e. ( ZZ>= ` M )
8 nfs1v 
 |-  F/ k [ m / k ] ph
9 nfsbc1v 
 |-  F/ k [. ( m + 1 ) / k ]. ph
10 8 9 nfim 
 |-  F/ k ( [ m / k ] ph -> [. ( m + 1 ) / k ]. ph )
11 7 10 nfim 
 |-  F/ k ( m e. ( ZZ>= ` M ) -> ( [ m / k ] ph -> [. ( m + 1 ) / k ]. ph ) )
12 eleq1w 
 |-  ( k = m -> ( k e. ( ZZ>= ` M ) <-> m e. ( ZZ>= ` M ) ) )
13 sbequ12 
 |-  ( k = m -> ( ph <-> [ m / k ] ph ) )
14 oveq1 
 |-  ( k = m -> ( k + 1 ) = ( m + 1 ) )
15 14 sbceq1d 
 |-  ( k = m -> ( [. ( k + 1 ) / k ]. ph <-> [. ( m + 1 ) / k ]. ph ) )
16 13 15 imbi12d 
 |-  ( k = m -> ( ( ph -> [. ( k + 1 ) / k ]. ph ) <-> ( [ m / k ] ph -> [. ( m + 1 ) / k ]. ph ) ) )
17 12 16 imbi12d 
 |-  ( k = m -> ( ( k e. ( ZZ>= ` M ) -> ( ph -> [. ( k + 1 ) / k ]. ph ) ) <-> ( m e. ( ZZ>= ` M ) -> ( [ m / k ] ph -> [. ( m + 1 ) / k ]. ph ) ) ) )
18 11 17 2 chvarfv 
 |-  ( m e. ( ZZ>= ` M ) -> ( [ m / k ] ph -> [. ( m + 1 ) / k ]. ph ) )
19 3 4 5 6 1 18 uzind4 
 |-  ( N e. ( ZZ>= ` M ) -> [. N / k ]. ph )