case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
⊢ a * b ≤ b ^ succ (log b a)

case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
⊢ b ^ succ (log b a) ≤ a * b
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
⊢ a * b = b ^ succ (log b a)
apply le_antisymm
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
⊢ a * b ≤ b ^ succ (log b a)
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
⊢ a * b ≤ b ^ succ (log b a)
have hbl := principal_mul_isLimit hb₂ hb
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => (fun x x_2 => x * x_2) a x) = (fun x x_1 => x * x_1) a b
⊢ a * b ≤ b ^ succ (log b a)
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
⊢ a * b ≤ b ^ succ (log b a)
have := IsNormal.bsup_eq.{u, u} (mul_isNormal (Ordinal.pos_iff_ne_zero.2 ha)) hbl
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
⊢ a * b ≤ b ^ succ (log b a)
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => (fun x x_2 => x * x_2) a x) = (fun x x_1 => x * x_1) a b
⊢ a * b ≤ b ^ succ (log b a)
dsimp at this
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
⊢ ∀ (i : Ordinal), i < b → a * i ≤ b ^ succ (log b a)
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
⊢ a * b ≤ b ^ succ (log b a)
rw [← this, bsup_le_iff]
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal
hcb : c < b
⊢ a * c ≤ b ^ succ (log b a)
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
⊢ ∀ (i : Ordinal), i < b → a * i ≤ b ^ succ (log b a)
intro c hcb
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal
hcb : c < b
hb₁ : 1 < b
⊢ a * c ≤ b ^ succ (log b a)
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal
hcb : c < b
⊢ a * c ≤ b ^ succ (log b a)
have hb₁ : 1 < b := (lt_succ 1).trans (by simpa using hb₂)
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a * c ≤ b ^ succ (log b a)
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal
hcb : c < b
hb₁ : 1 < b
⊢ a * c ≤ b ^ succ (log b a)
have hbo₀ : (b^b.log a) ≠ 0 := Ordinal.pos_iff_ne_zero.1 (opow_pos _ (zero_lt_one.trans hb₁))
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * succ (a / b ^ log b a) * c ≤ b ^ succ (log b a)
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a * c ≤ b ^ succ (log b a)
apply le_trans (mul_le_mul_right' (le_of_lt (lt_mul_succ_div a hbo₀)) c)
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * (succ (a / b ^ log b a) * c) ≤ b ^ log b a * b
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * succ (a / b ^ log b a) * c ≤ b ^ succ (log b a)
rw [mul_assoc, opow_succ]
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a / b ^ log b a < b
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * (succ (a / b ^ log b a) * c) ≤ b ^ log b a * b
refine' mul_le_mul_left' (le_of_lt (hb (hbl.2 _ _) hcb)) _
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a < b ^ succ (log b a)
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a / b ^ log b a < b
rw [div_lt hbo₀, ← opow_succ]
no goals
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a < b ^ succ (log b a)
exact lt_opow_succ_log_self hb₁ _
no goals
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal
hcb : c < b
⊢ succ 1 < b
simpa using hb₂
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
⊢ b ^ log b a * b ≤ a * b
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
⊢ b ^ succ (log b a) ≤ a * b
rw [opow_succ]
no goals
case a
a b : Ordinal
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
⊢ b ^ log b a * b ≤ a * b
exact mul_le_mul_right' (opow_log_le_self b ha) b