intro N hN hcontra
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ (a : ℝ), 1 < a → a.log = 0 → a ^ ((1 - r) / 2) = 0
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 1 < N
hcontra : N.log = 0
⊢ N ^ ((1 - r) / 2) = 0