Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
case intro.inl
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
pdivlcm_h : l ∣ ↑p
K6 : ↑p ∣ 2 * ↑p
⊢ False

case intro.inl.h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
pdivlcm_h : lcm l ↑p = ↑p
⊢ normalize ↑p = ↑p

case intro.inr
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False
Tactic:
apply absurd (dvd_trans pdivlcm_h K6) h
Proof state after:
case intro.inl.h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
pdivlcm_h : lcm l ↑p = ↑p
⊢ normalize ↑p = ↑p

case intro.inr
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False