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

Proof

Step	Hyp	Ref	Expression
1		uzind4s.1	$$⊢M\in \mathbb{Z}\to \underset{\dot{}}{[}M/k\underset{\dot{}}{]}\phi$$
2		uzind4s.2	$$⊢k\in {\mathbb{Z}}_{\ge M}\to \left(\phi \to \underset{\dot{}}{[}\left(k+1\right)/k\underset{\dot{}}{]}\phi \right)$$
3		dfsbcq2	$$⊢j=M\to \left(\left[j/k\right]\phi \leftrightarrow \underset{\dot{}}{[}M/k\underset{\dot{}}{]}\phi \right)$$
4		sbequ	$$⊢j=m\to \left(\left[j/k\right]\phi \leftrightarrow \left[m/k\right]\phi \right)$$
5		dfsbcq2	$$⊢j=m+1\to \left(\left[j/k\right]\phi \leftrightarrow \underset{\dot{}}{[}\left(m+1\right)/k\underset{\dot{}}{]}\phi \right)$$
6		dfsbcq2	$$⊢j=N\to \left(\left[j/k\right]\phi \leftrightarrow \underset{\dot{}}{[}N/k\underset{\dot{}}{]}\phi \right)$$
7		nfv	$$⊢Ⅎkm\in {\mathbb{Z}}_{\ge M}$$
8		nfs1v	$$⊢Ⅎk\left[m/k\right]\phi$$
9		nfsbc1v	$$⊢Ⅎk\underset{\dot{}}{[}\left(m+1\right)/k\underset{\dot{}}{]}\phi$$
10	8 9	nfim	$$⊢Ⅎk\left(\left[m/k\right]\phi \to \underset{\dot{}}{[}\left(m+1\right)/k\underset{\dot{}}{]}\phi \right)$$
11	7 10	nfim	$$⊢Ⅎk\left(m\in {\mathbb{Z}}_{\ge M}\to \left(\left[m/k\right]\phi \to \underset{\dot{}}{[}\left(m+1\right)/k\underset{\dot{}}{]}\phi \right)\right)$$
12		eleq1w	$$⊢k=m\to \left(k\in {\mathbb{Z}}_{\ge M}\leftrightarrow m\in {\mathbb{Z}}_{\ge M}\right)$$
13		sbequ12	$$⊢k=m\to \left(\phi \leftrightarrow \left[m/k\right]\phi \right)$$
14		oveq1	$$⊢k=m\to k+1=m+1$$
15	14	sbceq1d	$$⊢k=m\to \left(\underset{\dot{}}{[}\left(k+1\right)/k\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(m+1\right)/k\underset{\dot{}}{]}\phi \right)$$
16	13 15	imbi12d	$$⊢k=m\to \left(\left(\phi \to \underset{\dot{}}{[}\left(k+1\right)/k\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\left[m/k\right]\phi \to \underset{\dot{}}{[}\left(m+1\right)/k\underset{\dot{}}{]}\phi \right)\right)$$
17	12 16	imbi12d	$$⊢k=m\to \left(\left(k\in {\mathbb{Z}}_{\ge M}\to \left(\phi \to \underset{\dot{}}{[}\left(k+1\right)/k\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \left(m\in {\mathbb{Z}}_{\ge M}\to \left(\left[m/k\right]\phi \to \underset{\dot{}}{[}\left(m+1\right)/k\underset{\dot{}}{]}\phi \right)\right)\right)$$
18	11 17 2	chvarfv	$$⊢m\in {\mathbb{Z}}_{\ge M}\to \left(\left[m/k\right]\phi \to \underset{\dot{}}{[}\left(m+1\right)/k\underset{\dot{}}{]}\phi \right)$$
19	3 4 5 6 1 18	uzind4	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \underset{\dot{}}{[}N/k\underset{\dot{}}{]}\phi$$