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\in \mathbb{Z}\to \underset{\dot{}}{[}M/j\underset{\dot{}}{]}\phi$$
	uzind4s2.2	$$⊢k\in {\mathbb{Z}}_{\ge M}\to \left(\underset{\dot{}}{[}k/j\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}\left(k+1\right)/j\underset{\dot{}}{]}\phi \right)$$
Assertion	uzind4s2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \underset{\dot{}}{[}N/j\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		uzind4s2.1	$$⊢M\in \mathbb{Z}\to \underset{\dot{}}{[}M/j\underset{\dot{}}{]}\phi$$
2		uzind4s2.2	$$⊢k\in {\mathbb{Z}}_{\ge M}\to \left(\underset{\dot{}}{[}k/j\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}\left(k+1\right)/j\underset{\dot{}}{]}\phi \right)$$
3		dfsbcq	$$⊢m=M\to \left(\underset{\dot{}}{[}m/j\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}M/j\underset{\dot{}}{]}\phi \right)$$
4		dfsbcq	$$⊢m=n\to \left(\underset{\dot{}}{[}m/j\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}n/j\underset{\dot{}}{]}\phi \right)$$
5		dfsbcq	$$⊢m=n+1\to \left(\underset{\dot{}}{[}m/j\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(n+1\right)/j\underset{\dot{}}{]}\phi \right)$$
6		dfsbcq	$$⊢m=N\to \left(\underset{\dot{}}{[}m/j\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}N/j\underset{\dot{}}{]}\phi \right)$$
7		dfsbcq	$$⊢k=n\to \left(\underset{\dot{}}{[}k/j\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}n/j\underset{\dot{}}{]}\phi \right)$$
8		oveq1	$$⊢k=n\to k+1=n+1$$
9	8	sbceq1d	$$⊢k=n\to \left(\underset{\dot{}}{[}\left(k+1\right)/j\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(n+1\right)/j\underset{\dot{}}{]}\phi \right)$$
10	7 9	imbi12d	$$⊢k=n\to \left(\left(\underset{\dot{}}{[}k/j\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}\left(k+1\right)/j\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}n/j\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}\left(n+1\right)/j\underset{\dot{}}{]}\phi \right)\right)$$
11	10 2	vtoclga	$$⊢n\in {\mathbb{Z}}_{\ge M}\to \left(\underset{\dot{}}{[}n/j\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}\left(n+1\right)/j\underset{\dot{}}{]}\phi \right)$$
12	3 4 5 6 1 11	uzind4	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \underset{\dot{}}{[}N/j\underset{\dot{}}{]}\phi$$