Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ 3 ^ 2 ∣ p ^ 2 + 3 * q ^ ?m.72510

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ
Tactic:
refine' dvd_trans _ Int.gcd_dvd_right
Proof state after:
case refine'_1
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ 3 ^ 2 ∣ ↑(?refine'_2.gcd (p ^ 2 + 3 * q ^ ?m.72510))

case refine'_2
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℤ

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ