English
If a ≠ 0, b is multiplicatively principal and b > 2, then a·b = b^{succ(log_b a)}.
Русский
Пусть a ≠ 0, b является главным по умножению и b > 2. Тогда a·b = b^{succ(log_b a)}.
LaTeX
$$$a \neq 0 \;\land\; \operatorname{Principal}(\cdot * \cdot)\ b \land 2 < b \ \Rightarrow\ a \cdot b = b^{\operatorname{succ}(\log_b a)}$$$
Lean4
theorem mul_eq_opow_log_succ (ha : a ≠ 0) (hb : Principal (· * ·) b) (hb₂ : 2 < b) : a * b = b ^ succ (log b a) :=
by
apply le_antisymm
· have hbl := isSuccLimit_of_principal_mul hb₂ hb
rw [(isNormal_mul_right (Ordinal.pos_iff_ne_zero.2 ha)).apply_of_isSuccLimit hbl, Ordinal.iSup_le_iff]
intro ⟨c, hcb⟩
have hb₁ : 1 < b := one_lt_two.trans hb₂
have hbo₀ : b ^ log b a ≠ 0 := Ordinal.pos_iff_ne_zero.1 (opow_pos _ (zero_lt_one.trans hb₁))
apply (mul_le_mul_right' (le_of_lt (lt_mul_succ_div a hbo₀)) c).trans
rw [mul_assoc, opow_succ]
refine mul_le_mul_left' (hb (hbl.succ_lt ?_) hcb).le _
rw [div_lt hbo₀, ← opow_succ]
exact lt_opow_succ_log_self hb₁ _
· rw [opow_succ]
exact mul_le_mul_right' (opow_log_le_self b ha) b
