Description: Strong (or "total") induction principle over the naturals. (Contributed by Scott Fenton, 16-May-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nnsinds.1 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
nnsinds.2 | ⊢ ( 𝑥 = 𝑁 → ( 𝜑 ↔ 𝜒 ) ) | ||
nnsinds.3 | ⊢ ( 𝑥 ∈ ℕ → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑥 − 1 ) ) 𝜓 → 𝜑 ) ) | ||
Assertion | nnsinds | ⊢ ( 𝑁 ∈ ℕ → 𝜒 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnsinds.1 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
2 | nnsinds.2 | ⊢ ( 𝑥 = 𝑁 → ( 𝜑 ↔ 𝜒 ) ) | |
3 | nnsinds.3 | ⊢ ( 𝑥 ∈ ℕ → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑥 − 1 ) ) 𝜓 → 𝜑 ) ) | |
4 | elnnuz | ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) ) | |
5 | elnnuz | ⊢ ( 𝑥 ∈ ℕ ↔ 𝑥 ∈ ( ℤ≥ ‘ 1 ) ) | |
6 | 5 3 | sylbir | ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 1 ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑥 − 1 ) ) 𝜓 → 𝜑 ) ) |
7 | 1 2 6 | uzsinds | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 𝜒 ) |
8 | 4 7 | sylbi | ⊢ ( 𝑁 ∈ ℕ → 𝜒 ) |