case h
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ x ∈ Ioo 0 ⊤ ↔ x ∈ ⋃ (n : ℤ), Ico (y ^ n) (y ^ (n + 1))
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
⊢ Ioo 0 ⊤ = ⋃ (n : ℤ), Ico (y ^ n) (y ^ (n + 1))
ext x
case h
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ 0 < x ∧ x < ⊤ ↔ ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)
case h
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ x ∈ Ioo 0 ⊤ ↔ x ∈ ⋃ (n : ℤ), Ico (y ^ n) (y ^ (n + 1))
simp only [mem_iUnion, mem_Ioo, mem_Ico]
case h.mp
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ 0 < x ∧ x < ⊤ → ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)

case h.mpr
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ (∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)) → 0 < x ∧ x < ⊤
case h
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ 0 < x ∧ x < ⊤ ↔ ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)
constructor
case h.mp.intro
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
hx : 0 < x
h'x : x < ⊤
⊢ ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)
case h.mp
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ 0 < x ∧ x < ⊤ → ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)
rintro ⟨hx, h'x⟩
no goals
case h.mp.intro
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
hx : 0 < x
h'x : x < ⊤
⊢ ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)
exact exists_mem_Ico_zpow hx.ne' h'x.ne hy h'y
case h.mpr.intro.intro
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x ∧ x < ⊤
case h.mpr
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ (∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)) → 0 < x ∧ x < ⊤
rintro ⟨n, hn, h'n⟩
case h.mpr.intro.intro.left
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x

case h.mpr.intro.intro.right
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ x < ⊤
case h.mpr.intro.intro
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x ∧ x < ⊤
constructor
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < y ^ n
case h.mpr.intro.intro.left
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x
apply lt_of_lt_of_le _ hn
no goals
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < y ^ n
exact ENNReal.zpow_pos (zero_lt_one.trans hy).ne' h'y _
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ y ^ (n + 1) < ⊤
case h.mpr.intro.intro.right
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ x < ⊤
apply lt_trans h'n _
no goals
α : Type ?u.661501
β : Type ?u.661504
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ y ^ (n + 1) < ⊤
exact ENNReal.zpow_lt_top (zero_lt_one.trans hy).ne' h'y _