Metamath Proof Explorer


Theorem uzind

Description: Induction on the upper integers that start at M . The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by NM, 5-Jul-2005)

Ref Expression
Hypotheses uzind.1 ( 𝑗 = 𝑀 → ( 𝜑𝜓 ) )
uzind.2 ( 𝑗 = 𝑘 → ( 𝜑𝜒 ) )
uzind.3 ( 𝑗 = ( 𝑘 + 1 ) → ( 𝜑𝜃 ) )
uzind.4 ( 𝑗 = 𝑁 → ( 𝜑𝜏 ) )
uzind.5 ( 𝑀 ∈ ℤ → 𝜓 )
uzind.6 ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀𝑘 ) → ( 𝜒𝜃 ) )
Assertion uzind ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁 ) → 𝜏 )

Proof

Step Hyp Ref Expression
1 uzind.1 ( 𝑗 = 𝑀 → ( 𝜑𝜓 ) )
2 uzind.2 ( 𝑗 = 𝑘 → ( 𝜑𝜒 ) )
3 uzind.3 ( 𝑗 = ( 𝑘 + 1 ) → ( 𝜑𝜃 ) )
4 uzind.4 ( 𝑗 = 𝑁 → ( 𝜑𝜏 ) )
5 uzind.5 ( 𝑀 ∈ ℤ → 𝜓 )
6 uzind.6 ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀𝑘 ) → ( 𝜒𝜃 ) )
7 zre ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
8 7 leidd ( 𝑀 ∈ ℤ → 𝑀𝑀 )
9 8 5 jca ( 𝑀 ∈ ℤ → ( 𝑀𝑀𝜓 ) )
10 9 ancli ( 𝑀 ∈ ℤ → ( 𝑀 ∈ ℤ ∧ ( 𝑀𝑀𝜓 ) ) )
11 breq2 ( 𝑗 = 𝑀 → ( 𝑀𝑗𝑀𝑀 ) )
12 11 1 anbi12d ( 𝑗 = 𝑀 → ( ( 𝑀𝑗𝜑 ) ↔ ( 𝑀𝑀𝜓 ) ) )
13 12 elrab ( 𝑀 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀𝑗𝜑 ) } ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑀𝑀𝜓 ) ) )
14 10 13 sylibr ( 𝑀 ∈ ℤ → 𝑀 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀𝑗𝜑 ) } )
15 peano2z ( 𝑘 ∈ ℤ → ( 𝑘 + 1 ) ∈ ℤ )
16 15 a1i ( 𝑀 ∈ ℤ → ( 𝑘 ∈ ℤ → ( 𝑘 + 1 ) ∈ ℤ ) )
17 16 adantrd ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀𝑘𝜒 ) ) → ( 𝑘 + 1 ) ∈ ℤ ) )
18 zre ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
19 ltp1 ( 𝑘 ∈ ℝ → 𝑘 < ( 𝑘 + 1 ) )
20 19 adantl ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → 𝑘 < ( 𝑘 + 1 ) )
21 peano2re ( 𝑘 ∈ ℝ → ( 𝑘 + 1 ) ∈ ℝ )
22 21 ancli ( 𝑘 ∈ ℝ → ( 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) )
23 lelttr ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) → ( ( 𝑀𝑘𝑘 < ( 𝑘 + 1 ) ) → 𝑀 < ( 𝑘 + 1 ) ) )
24 23 3expb ( ( 𝑀 ∈ ℝ ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) ) → ( ( 𝑀𝑘𝑘 < ( 𝑘 + 1 ) ) → 𝑀 < ( 𝑘 + 1 ) ) )
25 22 24 sylan2 ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 𝑀𝑘𝑘 < ( 𝑘 + 1 ) ) → 𝑀 < ( 𝑘 + 1 ) ) )
26 20 25 mpan2d ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑀𝑘𝑀 < ( 𝑘 + 1 ) ) )
27 ltle ( ( 𝑀 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) → ( 𝑀 < ( 𝑘 + 1 ) → 𝑀 ≤ ( 𝑘 + 1 ) ) )
28 21 27 sylan2 ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑀 < ( 𝑘 + 1 ) → 𝑀 ≤ ( 𝑘 + 1 ) ) )
29 26 28 syld ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑀𝑘𝑀 ≤ ( 𝑘 + 1 ) ) )
30 7 18 29 syl2an ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑀𝑘𝑀 ≤ ( 𝑘 + 1 ) ) )
31 30 adantrd ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑀𝑘𝜒 ) → 𝑀 ≤ ( 𝑘 + 1 ) ) )
32 31 expimpd ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀𝑘𝜒 ) ) → 𝑀 ≤ ( 𝑘 + 1 ) ) )
33 6 3exp ( 𝑀 ∈ ℤ → ( 𝑘 ∈ ℤ → ( 𝑀𝑘 → ( 𝜒𝜃 ) ) ) )
34 33 imp4d ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀𝑘𝜒 ) ) → 𝜃 ) )
35 32 34 jcad ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀𝑘𝜒 ) ) → ( 𝑀 ≤ ( 𝑘 + 1 ) ∧ 𝜃 ) ) )
36 17 35 jcad ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀𝑘𝜒 ) ) → ( ( 𝑘 + 1 ) ∈ ℤ ∧ ( 𝑀 ≤ ( 𝑘 + 1 ) ∧ 𝜃 ) ) ) )
37 breq2 ( 𝑗 = 𝑘 → ( 𝑀𝑗𝑀𝑘 ) )
38 37 2 anbi12d ( 𝑗 = 𝑘 → ( ( 𝑀𝑗𝜑 ) ↔ ( 𝑀𝑘𝜒 ) ) )
39 38 elrab ( 𝑘 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀𝑗𝜑 ) } ↔ ( 𝑘 ∈ ℤ ∧ ( 𝑀𝑘𝜒 ) ) )
40 breq2 ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑀𝑗𝑀 ≤ ( 𝑘 + 1 ) ) )
41 40 3 anbi12d ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑀𝑗𝜑 ) ↔ ( 𝑀 ≤ ( 𝑘 + 1 ) ∧ 𝜃 ) ) )
42 41 elrab ( ( 𝑘 + 1 ) ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀𝑗𝜑 ) } ↔ ( ( 𝑘 + 1 ) ∈ ℤ ∧ ( 𝑀 ≤ ( 𝑘 + 1 ) ∧ 𝜃 ) ) )
43 36 39 42 3imtr4g ( 𝑀 ∈ ℤ → ( 𝑘 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀𝑗𝜑 ) } → ( 𝑘 + 1 ) ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀𝑗𝜑 ) } ) )
44 43 ralrimiv ( 𝑀 ∈ ℤ → ∀ 𝑘 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀𝑗𝜑 ) } ( 𝑘 + 1 ) ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀𝑗𝜑 ) } )
45 peano5uzti ( 𝑀 ∈ ℤ → ( ( 𝑀 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀𝑗𝜑 ) } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀𝑗𝜑 ) } ( 𝑘 + 1 ) ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀𝑗𝜑 ) } ) → { 𝑤 ∈ ℤ ∣ 𝑀𝑤 } ⊆ { 𝑗 ∈ ℤ ∣ ( 𝑀𝑗𝜑 ) } ) )
46 14 44 45 mp2and ( 𝑀 ∈ ℤ → { 𝑤 ∈ ℤ ∣ 𝑀𝑤 } ⊆ { 𝑗 ∈ ℤ ∣ ( 𝑀𝑗𝜑 ) } )
47 46 sseld ( 𝑀 ∈ ℤ → ( 𝑁 ∈ { 𝑤 ∈ ℤ ∣ 𝑀𝑤 } → 𝑁 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀𝑗𝜑 ) } ) )
48 breq2 ( 𝑤 = 𝑁 → ( 𝑀𝑤𝑀𝑁 ) )
49 48 elrab ( 𝑁 ∈ { 𝑤 ∈ ℤ ∣ 𝑀𝑤 } ↔ ( 𝑁 ∈ ℤ ∧ 𝑀𝑁 ) )
50 breq2 ( 𝑗 = 𝑁 → ( 𝑀𝑗𝑀𝑁 ) )
51 50 4 anbi12d ( 𝑗 = 𝑁 → ( ( 𝑀𝑗𝜑 ) ↔ ( 𝑀𝑁𝜏 ) ) )
52 51 elrab ( 𝑁 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀𝑗𝜑 ) } ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑀𝑁𝜏 ) ) )
53 47 49 52 3imtr3g ( 𝑀 ∈ ℤ → ( ( 𝑁 ∈ ℤ ∧ 𝑀𝑁 ) → ( 𝑁 ∈ ℤ ∧ ( 𝑀𝑁𝜏 ) ) ) )
54 53 3impib ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁 ) → ( 𝑁 ∈ ℤ ∧ ( 𝑀𝑁𝜏 ) ) )
55 54 simprrd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁 ) → 𝜏 )