G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝ : LinearOrderedRing G
h : abs x ≠ 1
⊢ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝ : LinearOrderedRing G
h : abs x ≠ 1
⊢ orderOf x = 0
rw [orderOf_eq_zero_iff']
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝ : LinearOrderedRing G
h : abs x ≠ 1
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ False
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝ : LinearOrderedRing G
h : abs x ≠ 1
⊢ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
intro n hn hx
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝ : LinearOrderedRing G
h : abs x ≠ 1
n : ℕ
hn : 0 < n
hx : abs x ^ n = 1
⊢ False
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝ : LinearOrderedRing G
h : abs x ≠ 1
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ False
replace hx : |x| ^ n = 1 := by simpa only [abs_one, abs_pow] using congr_arg abs hx
case inl
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝ : LinearOrderedRing G
h✝ : abs x ≠ 1
n : ℕ
hn : 0 < n
hx : abs x ^ n = 1
h : abs x < 1
⊢ False

case inr
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝ : LinearOrderedRing G
h✝ : abs x ≠ 1
n : ℕ
hn : 0 < n
hx : abs x ^ n = 1
h : 1 < abs x
⊢ False
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝ : LinearOrderedRing G
h : abs x ≠ 1
n : ℕ
hn : 0 < n
hx : abs x ^ n = 1
⊢ False
cases' h.lt_or_lt with h h
no goals
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝ : LinearOrderedRing G
h : abs x ≠ 1
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ abs x ^ n = 1
simpa only [abs_one, abs_pow] using congr_arg abs hx
no goals
case inl
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝ : LinearOrderedRing G
h✝ : abs x ≠ 1
n : ℕ
hn : 0 < n
hx : abs x ^ n = 1
h : abs x < 1
⊢ False
exact ((pow_lt_one (abs_nonneg x) h hn.ne').ne hx).elim
no goals
case inr
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝ : LinearOrderedRing G
h✝ : abs x ≠ 1
n : ℕ
hn : 0 < n
hx : abs x ^ n = 1
h : 1 < abs x
⊢ False
exact ((one_lt_pow h hn.ne').ne' hx).elim