English
For n ≠ 0, the base-2 logarithm of n is not equal to the p-adic valuation of n+1.
Русский
Для n ≠ 0 логарифм по основанию 2 числа n не равен p-адической оценке числа n+1.
LaTeX
$$$\\forall n \\in \\mathbb{N},\\ n \\neq 0 \\Rightarrow \\log_2 n \\neq \\operatorname{padicValNat}(2, n+1)$$$
Lean4
/-- This is false for prime numbers other than 2:
for `p = 3`, `n = 1`, one has `log 3 1 = padicValNat 3 2 = 0`. -/
theorem log_ne_padicValNat_succ {n : ℕ} (hn : n ≠ 0) : log 2 n ≠ padicValNat 2 (n + 1) :=
by
rw [Ne, log_eq_iff (by simp [hn])]
rintro ⟨h1, h2⟩
rw [← Nat.lt_add_one_iff, ← mul_one (2 ^ _)] at h1
rw [← add_one_le_iff, Nat.pow_succ] at h2
refine not_dvd_of_lt_of_lt_mul_succ h1 (lt_of_le_of_ne' h2 ?_) pow_padicValNat_dvd
exact pow_succ_padicValNat_not_dvd (p := 2) n.succ_ne_zero ∘ dvd_of_eq
