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 ⊢ j = M → φ ↔ ψ
uzind.2 ⊢ j = k → φ ↔ χ
uzind.3 ⊢ j = k + 1 → φ ↔ θ
uzind.4 ⊢ j = N → φ ↔ τ
uzind.5 ⊢ M ∈ ℤ → ψ
uzind.6 ⊢ M ∈ ℤ ∧ k ∈ ℤ ∧ M ≤ k → χ → θ
Assertion uzind ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N → τ

Proof

Step Hyp Ref Expression
1 uzind.1 ⊢ j = M → φ ↔ ψ
2 uzind.2 ⊢ j = k → φ ↔ χ
3 uzind.3 ⊢ j = k + 1 → φ ↔ θ
4 uzind.4 ⊢ j = N → φ ↔ τ
5 uzind.5 ⊢ M ∈ ℤ → ψ
6 uzind.6 ⊢ M ∈ ℤ ∧ k ∈ ℤ ∧ M ≤ k → χ → θ
7 zre ⊢ M ∈ ℤ → M ∈ ℝ
8 7 leidd ⊢ M ∈ ℤ → M ≤ M
9 8 5 jca ⊢ M ∈ ℤ → M ≤ M ∧ ψ
10 9 ancli ⊢ M ∈ ℤ → M ∈ ℤ ∧ M ≤ M ∧ ψ
11 breq2 ⊢ j = M → M ≤ j ↔ M ≤ M
12 11 1 anbi12d ⊢ j = M → M ≤ j ∧ φ ↔ M ≤ M ∧ ψ
13 12 elrab ⊢ M ∈ j ∈ ℤ | M ≤ j ∧ φ ↔ M ∈ ℤ ∧ M ≤ M ∧ ψ
14 10 13 sylibr ⊢ M ∈ ℤ → M ∈ j ∈ ℤ | M ≤ j ∧ φ
15 peano2z ⊢ k ∈ ℤ → k + 1 ∈ ℤ
16 15 a1i ⊢ M ∈ ℤ → k ∈ ℤ → k + 1 ∈ ℤ
17 16 adantrd ⊢ M ∈ ℤ → k ∈ ℤ ∧ M ≤ k ∧ χ → k + 1 ∈ ℤ
18 zre ⊢ k ∈ ℤ → k ∈ ℝ
19 ltp1 ⊢ k ∈ ℝ → k < k + 1
20 19 adantl ⊢ M ∈ ℝ ∧ k ∈ ℝ → k < k + 1
21 peano2re ⊢ k ∈ ℝ → k + 1 ∈ ℝ
22 21 ancli ⊢ k ∈ ℝ → k ∈ ℝ ∧ k + 1 ∈ ℝ
23 lelttr ⊢ M ∈ ℝ ∧ k ∈ ℝ ∧ k + 1 ∈ ℝ → M ≤ k ∧ k < k + 1 → M < k + 1
24 23 3expb ⊢ M ∈ ℝ ∧ k ∈ ℝ ∧ k + 1 ∈ ℝ → M ≤ k ∧ k < k + 1 → M < k + 1
25 22 24 sylan2 ⊢ M ∈ ℝ ∧ k ∈ ℝ → M ≤ k ∧ k < k + 1 → M < k + 1
26 20 25 mpan2d ⊢ M ∈ ℝ ∧ k ∈ ℝ → M ≤ k → M < k + 1
27 ltle ⊢ M ∈ ℝ ∧ k + 1 ∈ ℝ → M < k + 1 → M ≤ k + 1
28 21 27 sylan2 ⊢ M ∈ ℝ ∧ k ∈ ℝ → M < k + 1 → M ≤ k + 1
29 26 28 syld ⊢ M ∈ ℝ ∧ k ∈ ℝ → M ≤ k → M ≤ k + 1
30 7 18 29 syl2an ⊢ M ∈ ℤ ∧ k ∈ ℤ → M ≤ k → M ≤ k + 1
31 30 adantrd ⊢ M ∈ ℤ ∧ k ∈ ℤ → M ≤ k ∧ χ → M ≤ k + 1
32 31 expimpd ⊢ M ∈ ℤ → k ∈ ℤ ∧ M ≤ k ∧ χ → M ≤ k + 1
33 6 3exp ⊢ M ∈ ℤ → k ∈ ℤ → M ≤ k → χ → θ
34 33 imp4d ⊢ M ∈ ℤ → k ∈ ℤ ∧ M ≤ k ∧ χ → θ
35 32 34 jcad ⊢ M ∈ ℤ → k ∈ ℤ ∧ M ≤ k ∧ χ → M ≤ k + 1 ∧ θ
36 17 35 jcad ⊢ M ∈ ℤ → k ∈ ℤ ∧ M ≤ k ∧ χ → k + 1 ∈ ℤ ∧ M ≤ k + 1 ∧ θ
37 breq2 ⊢ j = k → M ≤ j ↔ M ≤ k
38 37 2 anbi12d ⊢ j = k → M ≤ j ∧ φ ↔ M ≤ k ∧ χ
39 38 elrab ⊢ k ∈ j ∈ ℤ | M ≤ j ∧ φ ↔ k ∈ ℤ ∧ M ≤ k ∧ χ
40 breq2 ⊢ j = k + 1 → M ≤ j ↔ M ≤ k + 1
41 40 3 anbi12d ⊢ j = k + 1 → M ≤ j ∧ φ ↔ M ≤ k + 1 ∧ θ
42 41 elrab ⊢ k + 1 ∈ j ∈ ℤ | M ≤ j ∧ φ ↔ k + 1 ∈ ℤ ∧ M ≤ k + 1 ∧ θ
43 36 39 42 3imtr4g ⊢ M ∈ ℤ → k ∈ j ∈ ℤ | M ≤ j ∧ φ → k + 1 ∈ j ∈ ℤ | M ≤ j ∧ φ
44 43 ralrimiv ⊢ M ∈ ℤ → ∀ k ∈ j ∈ ℤ | M ≤ j ∧ φ k + 1 ∈ j ∈ ℤ | M ≤ j ∧ φ
45 peano5uzti ⊢ M ∈ ℤ → M ∈ j ∈ ℤ | M ≤ j ∧ φ ∧ ∀ k ∈ j ∈ ℤ | M ≤ j ∧ φ k + 1 ∈ j ∈ ℤ | M ≤ j ∧ φ → w ∈ ℤ | M ≤ w ⊆ j ∈ ℤ | M ≤ j ∧ φ
46 14 44 45 mp2and ⊢ M ∈ ℤ → w ∈ ℤ | M ≤ w ⊆ j ∈ ℤ | M ≤ j ∧ φ
47 46 sseld ⊢ M ∈ ℤ → N ∈ w ∈ ℤ | M ≤ w → N ∈ j ∈ ℤ | M ≤ j ∧ φ
48 breq2 ⊢ w = N → M ≤ w ↔ M ≤ N
49 48 elrab ⊢ N ∈ w ∈ ℤ | M ≤ w ↔ N ∈ ℤ ∧ M ≤ N
50 breq2 ⊢ j = N → M ≤ j ↔ M ≤ N
51 50 4 anbi12d ⊢ j = N → M ≤ j ∧ φ ↔ M ≤ N ∧ τ
52 51 elrab ⊢ N ∈ j ∈ ℤ | M ≤ j ∧ φ ↔ N ∈ ℤ ∧ M ≤ N ∧ τ
53 47 49 52 3imtr3g ⊢ M ∈ ℤ → N ∈ ℤ ∧ M ≤ N → N ∈ ℤ ∧ M ≤ N ∧ τ
54 53 3impib ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N → N ∈ ℤ ∧ M ≤ N ∧ τ
55 54 simprrd ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N → τ