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

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ [↑a]_m ^ phi m = [1]_m
Tactic:
have h2 : invertible (prod_seq m 0 (F m)) := Fprod_invertible m m
State after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
⊢ [↑a]_m ^ phi m = [1]_m

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
⊢ [↑a]_m ^ phi m = [1]_m
Tactic:
obtain (Y : ZMod m) (h3 : prod_seq m 0 (F m) * Y = [1]_m) from h2
State after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
Y : ZMod m
h3 : prod_seq m 0 (F m) * Y = [1]_m
⊢ [↑a]_m ^ phi m = [1]_m

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
Y : ZMod m
h3 : prod_seq m 0 (F m) * Y = [1]_m
⊢ [↑a]_m ^ phi m = [1]_m
Tactic:
show [a]_m ^ (phi m) = [1]_m from
  calc [a]_m ^ (phi m)
    _ = [a]_m ^ (phi m) * [1]_m := (Theorem_7_3_6_7 _).symm
    _ = [a]_m ^ (phi m) * (prod_seq m 0 (F m) * Y) := by rw [h3]
    _ = ([a]_m ^ (phi m) * prod_seq m 0 (F m)) * Y := by ring
    _ = prod_seq m 0 (F m ∘ G m a) * Y := by rw [FG_prod h1 m, phi_def]
    _ = prod_seq m 0 (F m) * Y := by
          rw [perm_prod (F m) m (G m a) (G_perm_below h1)]
    _ = [1]_m := by rw [h3]
State after:
no goals

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
Y : ZMod m
h3 : prod_seq m 0 (F m) * Y = [1]_m
⊢ [↑a]_m ^ phi m * [1]_m = [↑a]_m ^ phi m * (prod_seq m 0 (F m) * Y)
Tactic:
rw [h3]
State after:
no goals

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
Y : ZMod m
h3 : prod_seq m 0 (F m) * Y = [1]_m
⊢ [↑a]_m ^ phi m * (prod_seq m 0 (F m) * Y) = [↑a]_m ^ phi m * prod_seq m 0 (F m) * Y
Tactic:
ring
State after:
no goals

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
Y : ZMod m
h3 : prod_seq m 0 (F m) * Y = [1]_m
⊢ [↑a]_m ^ phi m * prod_seq m 0 (F m) * Y = prod_seq m 0 (F m ∘ G m a) * Y
Tactic:
rw [FG_prod h1 m, phi_def]
State after:
no goals

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
Y : ZMod m
h3 : prod_seq m 0 (F m) * Y = [1]_m
⊢ prod_seq m 0 (F m ∘ G m a) * Y = prod_seq m 0 (F m) * Y
Tactic:
rw [perm_prod (F m) m (G m a) (G_perm_below h1)]
State after:
no goals

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
Y : ZMod m
h3 : prod_seq m 0 (F m) * Y = [1]_m
⊢ prod_seq m 0 (F m) * Y = [1]_m
Tactic:
rw [h3]
State after:
no goals