Theorem: HTPI.Theorem_7_3_7 (HTPILib/Chap7.lean)

State before:
m a : ℕ
⊢ invertible [↑a]_m ↔ rel_prime m a
Tactic:
apply Iff.intro
State after:
case mp
m a : ℕ
⊢ invertible [↑a]_m → rel_prime m a

case mpr
m a : ℕ
⊢ rel_prime m a → invertible [↑a]_m

State before:
case mp
m a : ℕ
⊢ invertible [↑a]_m → rel_prime m a
Tactic:
assume h1 : invertible [a]_m
State after:
case mp
m a : ℕ
h1 : invertible [↑a]_m
⊢ rel_prime m a

State before:
case mp
m a : ℕ
h1 : invertible [↑a]_m
⊢ rel_prime m a
Tactic:
define at h1
State after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
⊢ rel_prime m a

State before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
⊢ rel_prime m a
Tactic:
obtain (Y : ZMod m) (h2 : [a]_m * Y = [1]_m) from h1
State after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
h2 : [↑a]_m * Y = [1]_m
⊢ rel_prime m a

State before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
h2 : [↑a]_m * Y = [1]_m
⊢ rel_prime m a
Tactic:
obtain (b : Int) (h3 : Y = [b]_m) from cc_rep Y
State after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
h2 : [↑a]_m * Y = [1]_m
b : ℤ
h3 : Y = [b]_m
⊢ rel_prime m a

State before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
h2 : [↑a]_m * Y = [1]_m
b : ℤ
h3 : Y = [b]_m
⊢ rel_prime m a
Tactic:
rewrite [h3, mul_class, cc_eq_iff_congr] at h2
State after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ↑a * b ≡ 1 (MOD m)
h3 : Y = [b]_m
⊢ rel_prime m a

State before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ↑a * b ≡ 1 (MOD m)
h3 : Y = [b]_m
⊢ rel_prime m a
Tactic:
define at h2
State after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
⊢ rel_prime m a

State before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
⊢ rel_prime m a
Tactic:
obtain (c : Int) (h4 : a * b - 1 = m * c) from h2
State after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ rel_prime m a

State before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ rel_prime m a
Tactic:
rewrite [Exercise_7_2_6]
State after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ ∃ s t, s * ↑m + t * ↑a = 1

State before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ ∃ s t, s * ↑m + t * ↑a = 1
Tactic:
apply Exists.intro (-c)
State after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ ∃ t, -c * ↑m + t * ↑a = 1

State before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ ∃ t, -c * ↑m + t * ↑a = 1
Tactic:
apply Exists.intro b
State after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ -c * ↑m + b * ↑a = 1

State before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ -c * ↑m + b * ↑a = 1
Tactic:
show (-c) * m + b * a = 1 from
  calc (-c) * m + b * a
    _ = (-c) * m + (a * b - 1) + 1 := by ring
    _ = (-c) * m + m * c + 1 := by rw [h4]
    _ = 1 := by ring
State after:
no goals

State before:
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ -c * ↑m + b * ↑a = -c * ↑m + (↑a * b - 1) + 1
Tactic:
ring
State after:
no goals

State before:
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ -c * ↑m + (↑a * b - 1) + 1 = -c * ↑m + ↑m * c + 1
Tactic:
rw [h4]
State after:
no goals

State before:
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ -c * ↑m + ↑m * c + 1 = 1
Tactic:
ring
State after:
no goals

State before:
case mpr
m a : ℕ
⊢ rel_prime m a → invertible [↑a]_m
Tactic:
assume h1 : rel_prime m a
State after:
case mpr
m a : ℕ
h1 : rel_prime m a
⊢ invertible [↑a]_m

State before:
case mpr
m a : ℕ
h1 : rel_prime m a
⊢ invertible [↑a]_m
Tactic:
define
State after:
case mpr
m a : ℕ
h1 : rel_prime m a
⊢ ∃ Y, [↑a]_m * Y = [1]_m

State before:
case mpr
m a : ℕ
h1 : rel_prime m a
⊢ ∃ Y, [↑a]_m * Y = [1]_m
Tactic:
show ∃ (Y : ZMod m), [a]_m * Y = [1]_m from
  Exists.intro [gcd_c2 m a]_m (gcd_c2_inv h1)
State after:
no goals