Theorem: interval_induction (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
⊢ P a b
Tactic:
set n := ⌊b⌋ - ⌊a⌋ with hn
State after:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ := ⌊b⌋ - ⌊a⌋
hn : n = ⌊b⌋ - ⌊a⌋
⊢ P a b

State before:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ := ⌊b⌋ - ⌊a⌋
hn : n = ⌊b⌋ - ⌊a⌋
⊢ P a b
Tactic:
clear_value n
State after:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ
hn : n = ⌊b⌋ - ⌊a⌋
⊢ P a b

State before:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ
hn : n = ⌊b⌋ - ⌊a⌋
⊢ P a b
Tactic:
have : 0 ≤ n := by simp only [hn, sub_nonneg, ge_iff_le, Int.floor_le_floor _ _ (hab.le)]
State after:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ
hn : n = ⌊b⌋ - ⌊a⌋
this : 0 ≤ n
⊢ P a b

State before:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ
hn : n = ⌊b⌋ - ⌊a⌋
this : 0 ≤ n
⊢ P a b
Tactic:
lift n to ℕ using this
State after:
case intro
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℕ
hn : ↑n = ⌊b⌋ - ⌊a⌋
⊢ P a b

State before:
case intro
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℕ
hn : ↑n = ⌊b⌋ - ⌊a⌋
⊢ P a b
Tactic:
exact interval_induction_aux_int n P base step a b hab hn
State after:
no goals

State before:
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ
hn : n = ⌊b⌋ - ⌊a⌋
⊢ 0 ≤ n
Tactic:
simp only [hn, sub_nonneg, ge_iff_le, Int.floor_le_floor _ _ (hab.le)]
State after:
no goals