Metamath Proof Explorer


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 ( 𝑁 ∈ ( ℤ𝑀 ) → 𝜏 )