𝓕 : Type ?u.832658
𝕜 : Type ?u.832661
α : Type ?u.832664
ι : Type ?u.832667
κ : Type ?u.832670
E : Type u_1
F : Type ?u.832676
G : Type ?u.832679
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
h : ‖a / b‖ ≤ r
⊢ ‖(a / b) ^ n‖ ≤ n • r
𝓕 : Type ?u.832658
𝕜 : Type ?u.832661
α : Type ?u.832664
ι : Type ?u.832667
κ : Type ?u.832670
E : Type u_1
F : Type ?u.832676
G : Type ?u.832679
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
h : a ∈ closedBall b r
⊢ a ^ n ∈ closedBall (b ^ n) (n • r)
simp only [mem_closedBall, dist_eq_norm_div, ← div_pow] at h⊢
𝓕 : Type ?u.832658
𝕜 : Type ?u.832661
α : Type ?u.832664
ι : Type ?u.832667
κ : Type ?u.832670
E : Type u_1
F : Type ?u.832676
G : Type ?u.832679
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
h : ‖a / b‖ ≤ r
⊢ ↑n * ‖a / b‖ ≤ n • r
𝓕 : Type ?u.832658
𝕜 : Type ?u.832661
α : Type ?u.832664
ι : Type ?u.832667
κ : Type ?u.832670
E : Type u_1
F : Type ?u.832676
G : Type ?u.832679
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
h : ‖a / b‖ ≤ r
⊢ ‖(a / b) ^ n‖ ≤ n • r
refine' (norm_pow_le_mul_norm n (a / b)).trans _
no goals
𝓕 : Type ?u.832658
𝕜 : Type ?u.832661
α : Type ?u.832664
ι : Type ?u.832667
κ : Type ?u.832670
E : Type u_1
F : Type ?u.832676
G : Type ?u.832679
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
h : ‖a / b‖ ≤ r
⊢ ↑n * ‖a / b‖ ≤ n • r
simpa only [nsmul_eq_mul] using mul_le_mul_of_nonneg_left h n.cast_nonneg