Theorem: factors
Proof state before:
case a
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
⊢ ?a * z ≠ 0

case a
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
⊢ ℤ
Tactic:
apply right_ne_zero_of_mul
Proof state after:
case a.a
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
⊢ ?a.a✝ * (?a * z) ≠ 0

case a.a
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
⊢ ℤ

case a
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
⊢ ℤ