Theorem uzind4

Description: Induction on the upper set of integers that starts 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, 7-Sep-2005)

	Ref	Expression
Hypotheses	uzind4.1	⊢ ( 𝑗 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
	uzind4.2	⊢ ( 𝑗 = 𝑘 → ( 𝜑 ↔ 𝜒 ) )
	uzind4.3	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
	uzind4.4	⊢ ( 𝑗 = 𝑁 → ( 𝜑 ↔ 𝜏 ) )
	uzind4.5	⊢ ( 𝑀 ∈ ℤ → 𝜓 )
	uzind4.6	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜒 → 𝜃 ) )
Assertion	uzind4	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝜏 )

Proof

Step	Hyp	Ref	Expression
1		uzind4.1	⊢ ( 𝑗 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
2		uzind4.2	⊢ ( 𝑗 = 𝑘 → ( 𝜑 ↔ 𝜒 ) )
3		uzind4.3	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
4		uzind4.4	⊢ ( 𝑗 = 𝑁 → ( 𝜑 ↔ 𝜏 ) )
5		uzind4.5	⊢ ( 𝑀 ∈ ℤ → 𝜓 )
6		uzind4.6	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜒 → 𝜃 ) )
7		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
8		breq2	⊢ ( 𝑚 = 𝑁 → ( 𝑀 ≤ 𝑚 ↔ 𝑀 ≤ 𝑁 ) )
9		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
10		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑁 )
11	8 9 10	elrabd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ { 𝑚 ∈ ℤ ∣ 𝑀 ≤ 𝑚 } )
12		breq2	⊢ ( 𝑚 = 𝑘 → ( 𝑀 ≤ 𝑚 ↔ 𝑀 ≤ 𝑘 ) )
13	12	elrab	⊢ ( 𝑘 ∈ { 𝑚 ∈ ℤ ∣ 𝑀 ≤ 𝑚 } ↔ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) )
14		eluz2	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) )
15	14	biimpri	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
16	15	3expb	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
17	13 16	sylan2b	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ { 𝑚 ∈ ℤ ∣ 𝑀 ≤ 𝑚 } ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
18	17 6	syl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ { 𝑚 ∈ ℤ ∣ 𝑀 ≤ 𝑚 } ) → ( 𝜒 → 𝜃 ) )
19	1 2 3 4 5 18	uzind3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ { 𝑚 ∈ ℤ ∣ 𝑀 ≤ 𝑚 } ) → 𝜏 )
20	7 11 19	syl2anc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝜏 )