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

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h4 : m ^ e ≡ c (MOD p) := Exists.intro t h3
State after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
⊢ ↑c ^ d ≡ ↑m (MOD p)

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h5 : [m ^ e]_p = [c]_p := (cc_eq_iff_congr _ _ _).rtl h4
State after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m ^ e]_p = [↑c]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m ^ e]_p = [↑c]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
rewrite [←Exercise_7_4_5_Nat] at h5
State after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
by_cases h6 : p ∣ m
State after:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
⊢ ↑c ^ d ≡ ↑m (MOD p)

case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
⊢ ↑c ^ d ≡ ↑m (MOD p)

State before:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h7 : m ≡ 0 (MOD p) := by
  obtain (j : Nat) (h8 : m = p * j) from h6
  apply Exists.intro (↑j : Int)   rewrite [h8, Nat.cast_mul]
  ring
  done
State after:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
⊢ ↑c ^ d ≡ ↑m (MOD p)

State before:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h8 : [m]_p = [0]_p := (cc_eq_iff_congr _ _ _).rtl h7
State after:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)

State before:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h9 : 0 < (e * d) := by
  rewrite [h2]
  have h10 : 0 ≤ (p - 1) * s := Nat.zero_le _
  linarith
  done
State after:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
⊢ ↑c ^ d ≡ ↑m (MOD p)

State before:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h10 : (0 : Int) ^ (e * d) = 0 := zero_pow h9
State after:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ ↑c ^ d ≡ ↑m (MOD p)

State before:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h11 : [c ^ d]_p = [m]_p :=
  calc [c ^ d]_p
    _ = [c]_p ^ d := by rw [Exercise_7_4_5_Nat]
    _ = ([m]_p ^ e) ^ d := by rw [h5]
    _ = [m]_p ^ (e * d) := by ring
    _ = [0]_p ^ (e * d) := by rw [h8]
    _ = [0 ^ (e * d)]_p := Exercise_7_4_5_Int _ _ _
    _ = [0]_p := by rw [h10]
    _ = [m]_p := by rw [h8]
State after:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
h11 : [↑c ^ d]_p = [↑m]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)

State before:
case pos
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
h11 : [↑c ^ d]_p = [↑m]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
show c ^ d ≡ m (MOD p)  from (cc_eq_iff_congr _ _ _).ltr h11
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
⊢ ↑m ≡ 0 (MOD p)
Tactic:
obtain (j : Nat) (h8 : m = p * j) from h6
State after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
j : ℕ
h8 : m = p * j
⊢ ↑m ≡ 0 (MOD p)

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
j : ℕ
h8 : m = p * j
⊢ ↑m ≡ 0 (MOD p)
Tactic:
apply Exists.intro (↑j : Int)
State after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
j : ℕ
h8 : m = p * j
⊢ ↑m - 0 = ↑p * ↑j

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
j : ℕ
h8 : m = p * j
⊢ ↑m - 0 = ↑p * ↑j
Tactic:
rewrite [h8, Nat.cast_mul]
State after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
j : ℕ
h8 : m = p * j
⊢ ↑p * ↑j - 0 = ↑p * ↑j

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
j : ℕ
h8 : m = p * j
⊢ ↑p * ↑j - 0 = ↑p * ↑j
Tactic:
ring
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
⊢ 0 < e * d
Tactic:
rewrite [h2]
State after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
⊢ 0 < (p - 1) * s + 1

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
⊢ 0 < (p - 1) * s + 1
Tactic:
have h10 : 0 ≤ (p - 1) * s := Nat.zero_le _
State after:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h10 : 0 ≤ (p - 1) * s
⊢ 0 < (p - 1) * s + 1

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h10 : 0 ≤ (p - 1) * s
⊢ 0 < (p - 1) * s + 1
Tactic:
linarith
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ [↑c ^ d]_p = [↑c]_p ^ d
Tactic:
rw [Exercise_7_4_5_Nat]
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ [↑c]_p ^ d = ([↑m]_p ^ e) ^ d
Tactic:
rw [h5]
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ ([↑m]_p ^ e) ^ d = [↑m]_p ^ (e * d)
Tactic:
ring
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ [↑m]_p ^ (e * d) = [0]_p ^ (e * d)
Tactic:
rw [h8]
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ [0 ^ (e * d)]_p = [0]_p
Tactic:
rw [h10]
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : p ∣ m
h7 : ↑m ≡ 0 (MOD p)
h8 : [↑m]_p = [0]_p
h9 : 0 < e * d
h10 : 0 ^ (e * d) = 0
⊢ [0]_p = [↑m]_p
Tactic:
rw [h8]
State after:
no goals

State before:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h7 : rel_prime m p := rel_prime_of_prime_not_dvd h1 h6
State after:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
⊢ ↑c ^ d ≡ ↑m (MOD p)

State before:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h8 : rel_prime p m := rel_prime_symm h7
State after:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
⊢ ↑c ^ d ≡ ↑m (MOD p)

State before:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h9 : NeZero p := prime_NeZero h1
State after:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
⊢ ↑c ^ d ≡ ↑m (MOD p)

State before:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h10 : (1 : Int) ^ s = 1 := by ring
State after:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
h10 : 1 ^ s = 1
⊢ ↑c ^ d ≡ ↑m (MOD p)

State before:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
h10 : 1 ^ s = 1
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
have h11 : [c ^ d]_p = [m]_p :=
  calc [c ^ d]_p
    _ = [c]_p ^ d := by rw [Exercise_7_4_5_Nat]
    _ = ([m]_p ^ e) ^ d := by rw [h5]
    _ = [m]_p ^ (e * d) := by ring
    _ = [m]_p ^ ((p - 1) * s + 1) := by rw [h2]
    _ = ([m]_p ^ (p - 1)) ^ s * [m]_p := by ring
    _ = ([m]_p ^ (phi p)) ^ s * [m]_p := by rw [phi_prime h1]
    _ = [1]_p ^ s * [m]_p := by rw [Theorem_7_4_2 h8]
    _ = [1 ^ s]_p * [m]_p := by rw [Exercise_7_4_5_Int]
    _ = [1]_p * [m]_p := by rw [h10]
    _ = [m]_p * [1]_p := by ring
    _ = [m]_p := Theorem_7_3_6_7 _
State after:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
h10 : 1 ^ s = 1
h11 : [↑c ^ d]_p = [↑m]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)

State before:
case neg
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
h10 : 1 ^ s = 1
h11 : [↑c ^ d]_p = [↑m]_p
⊢ ↑c ^ d ≡ ↑m (MOD p)
Tactic:
show c ^ d ≡ m (MOD p)  from (cc_eq_iff_congr _ _ _).ltr h11
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
⊢ 1 ^ s = 1
Tactic:
ring
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
h10 : 1 ^ s = 1
⊢ [↑c ^ d]_p = [↑c]_p ^ d
Tactic:
rw [Exercise_7_4_5_Nat]
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
h10 : 1 ^ s = 1
⊢ [↑c]_p ^ d = ([↑m]_p ^ e) ^ d
Tactic:
rw [h5]
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
h10 : 1 ^ s = 1
⊢ ([↑m]_p ^ e) ^ d = [↑m]_p ^ (e * d)
Tactic:
ring
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
h10 : 1 ^ s = 1
⊢ [↑m]_p ^ (e * d) = [↑m]_p ^ ((p - 1) * s + 1)
Tactic:
rw [h2]
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
h10 : 1 ^ s = 1
⊢ [↑m]_p ^ ((p - 1) * s + 1) = ([↑m]_p ^ (p - 1)) ^ s * [↑m]_p
Tactic:
ring
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
h10 : 1 ^ s = 1
⊢ ([↑m]_p ^ (p - 1)) ^ s * [↑m]_p = ([↑m]_p ^ phi p) ^ s * [↑m]_p
Tactic:
rw [phi_prime h1]
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
h10 : 1 ^ s = 1
⊢ ([↑m]_p ^ phi p) ^ s * [↑m]_p = [1]_p ^ s * [↑m]_p
Tactic:
rw [Theorem_7_4_2 h8]
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
h10 : 1 ^ s = 1
⊢ [1]_p ^ s * [↑m]_p = [1 ^ s]_p * [↑m]_p
Tactic:
rw [Exercise_7_4_5_Int]
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
h10 : 1 ^ s = 1
⊢ [1 ^ s]_p * [↑m]_p = [1]_p * [↑m]_p
Tactic:
rw [h10]
State after:
no goals

State before:
p e d m c s : ℕ
t : ℤ
h1 : prime p
h2 : e * d = (p - 1) * s + 1
h3 : ↑m ^ e - ↑c = ↑p * t
h4 : ↑m ^ e ≡ ↑c (MOD p)
h5 : [↑m]_p ^ e = [↑c]_p
h6 : ¬p ∣ m
h7 : rel_prime m p
h8 : rel_prime p m
h9 : NeZero p
h10 : 1 ^ s = 1
⊢ [1]_p * [↑m]_p = [↑m]_p * [1]_p
Tactic:
ring
State after:
no goals