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

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : [↑m]_n ^ e = [↑c]_n
⊢ [↑c]_n ^ d = [↑m]_n
Tactic:
rewrite [Exercise_7_4_5_Nat, cc_eq_iff_congr] at h1
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
⊢ [↑c]_n ^ d = [↑m]_n

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
⊢ [↑c]_n ^ d = [↑m]_n
Tactic:
rewrite [Exercise_7_4_5_Nat, cc_eq_iff_congr]
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
⊢ ↑c ^ d ≡ ↑m (MOD n)

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
⊢ ↑c ^ d ≡ ↑m (MOD n)
Tactic:
obtain (j : Int) (h2 : m ^ e - c = n * j) from h1
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑n * j
⊢ ↑c ^ d ≡ ↑m (MOD n)

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑n * j
⊢ ↑c ^ d ≡ ↑m (MOD n)
Tactic:
rewrite [n_pq, Nat.cast_mul] at h2
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
⊢ ↑c ^ d ≡ ↑m (MOD n)

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
⊢ ↑c ^ d ≡ ↑m (MOD n)
Tactic:
have h3 : e * d = (p - 1) * (k * (q - 1)) + 1 := by
  rewrite [ed_congr_1]
  ring
  done
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
⊢ ↑c ^ d ≡ ↑m (MOD n)

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
⊢ ↑c ^ d ≡ ↑m (MOD n)
Tactic:
have h4 : m ^ e - c = p * (q * j) := by
  rewrite [h2]
  ring
  done
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
⊢ ↑c ^ d ≡ ↑m (MOD n)

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
⊢ ↑c ^ d ≡ ↑m (MOD n)
Tactic:
have congr_p : c ^ d ≡ m (MOD p) := Lemma_7_5_1 p_prime h3 h4
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
⊢ ↑c ^ d ≡ ↑m (MOD n)

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
⊢ ↑c ^ d ≡ ↑m (MOD n)
Tactic:
have h5 : e * d = (q - 1) * (k * (p - 1)) + 1 := by
  rewrite [ed_congr_1]
  ring
  done
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
⊢ ↑c ^ d ≡ ↑m (MOD n)

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
⊢ ↑c ^ d ≡ ↑m (MOD n)
Tactic:
have h6 : m ^ e - c = q * (p * j) := by
  rewrite [h2]
  ring
  done
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
⊢ ↑c ^ d ≡ ↑m (MOD n)

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
⊢ ↑c ^ d ≡ ↑m (MOD n)
Tactic:
have congr_q : c ^ d ≡ m (MOD q) := Lemma_7_5_1 q_prime h5 h6
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
congr_q : ↑c ^ d ≡ ↑m (MOD q)
⊢ ↑c ^ d ≡ ↑m (MOD n)

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
congr_q : ↑c ^ d ≡ ↑m (MOD q)
⊢ ↑c ^ d ≡ ↑m (MOD n)
Tactic:
have h7 : ¬q ∣ p := by
  by_contra h8
  have h9 : q = 1 ∨ q = p := dvd_prime p_prime h8
  disj_syll h9 (prime_not_one q_prime)
  show False from p_ne_q h9.symm
  done
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
congr_q : ↑c ^ d ≡ ↑m (MOD q)
h7 : ¬q ∣ p
⊢ ↑c ^ d ≡ ↑m (MOD n)

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
congr_q : ↑c ^ d ≡ ↑m (MOD q)
h7 : ¬q ∣ p
⊢ ↑c ^ d ≡ ↑m (MOD n)
Tactic:
have h8 : rel_prime p q := rel_prime_of_prime_not_dvd q_prime h7
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
congr_q : ↑c ^ d ≡ ↑m (MOD q)
h7 : ¬q ∣ p
h8 : rel_prime p q
⊢ ↑c ^ d ≡ ↑m (MOD n)

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
congr_q : ↑c ^ d ≡ ↑m (MOD q)
h7 : ¬q ∣ p
h8 : rel_prime p q
⊢ ↑c ^ d ≡ ↑m (MOD n)
Tactic:
rewrite [n_pq, Lemma_7_4_5 _ _ h8]
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
congr_q : ↑c ^ d ≡ ↑m (MOD q)
h7 : ¬q ∣ p
h8 : rel_prime p q
⊢ ↑c ^ d ≡ ↑m (MOD p) ∧ ↑c ^ d ≡ ↑m (MOD q)

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
congr_q : ↑c ^ d ≡ ↑m (MOD q)
h7 : ¬q ∣ p
h8 : rel_prime p q
⊢ ↑c ^ d ≡ ↑m (MOD p) ∧ ↑c ^ d ≡ ↑m (MOD q)
Tactic:
show c ^ d ≡ m (MOD p) ∧ c ^ d ≡ m (MOD q) from
  And.intro congr_p congr_q
State after:
no goals

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
⊢ e * d = (p - 1) * (k * (q - 1)) + 1
Tactic:
rewrite [ed_congr_1]
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
⊢ k * (p - 1) * (q - 1) + 1 = (p - 1) * (k * (q - 1)) + 1

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
⊢ k * (p - 1) * (q - 1) + 1 = (p - 1) * (k * (q - 1)) + 1
Tactic:
ring
State after:
no goals

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
⊢ ↑m ^ e - ↑c = ↑p * (↑q * j)
Tactic:
rewrite [h2]
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
⊢ ↑p * ↑q * j = ↑p * (↑q * j)

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
⊢ ↑p * ↑q * j = ↑p * (↑q * j)
Tactic:
ring
State after:
no goals

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
⊢ e * d = (q - 1) * (k * (p - 1)) + 1
Tactic:
rewrite [ed_congr_1]
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
⊢ k * (p - 1) * (q - 1) + 1 = (q - 1) * (k * (p - 1)) + 1

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
⊢ k * (p - 1) * (q - 1) + 1 = (q - 1) * (k * (p - 1)) + 1
Tactic:
ring
State after:
no goals

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
⊢ ↑m ^ e - ↑c = ↑q * (↑p * j)
Tactic:
rewrite [h2]
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
⊢ ↑p * ↑q * j = ↑q * (↑p * j)

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
⊢ ↑p * ↑q * j = ↑q * (↑p * j)
Tactic:
ring
State after:
no goals

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
congr_q : ↑c ^ d ≡ ↑m (MOD q)
⊢ ¬q ∣ p
Tactic:
by_contra h8
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
congr_q : ↑c ^ d ≡ ↑m (MOD q)
h8 : q ∣ p
⊢ False

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
congr_q : ↑c ^ d ≡ ↑m (MOD q)
h8 : q ∣ p
⊢ False
Tactic:
have h9 : q = 1 ∨ q = p := dvd_prime p_prime h8
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
congr_q : ↑c ^ d ≡ ↑m (MOD q)
h8 : q ∣ p
h9 : q = 1 ∨ q = p
⊢ False

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
congr_q : ↑c ^ d ≡ ↑m (MOD q)
h8 : q ∣ p
h9 : q = 1 ∨ q = p
⊢ False
Tactic:
disj_syll h9 (prime_not_one q_prime)
State after:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
congr_q : ↑c ^ d ≡ ↑m (MOD q)
h8 : q ∣ p
h9 : q = p
⊢ False

State before:
p q n e d k m c : ℕ
p_prime : prime p
q_prime : prime q
p_ne_q : p ≠ q
n_pq : n = p * q
ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1
h1 : ↑m ^ e ≡ ↑c (MOD n)
j : ℤ
h2 : ↑m ^ e - ↑c = ↑p * ↑q * j
h3 : e * d = (p - 1) * (k * (q - 1)) + 1
h4 : ↑m ^ e - ↑c = ↑p * (↑q * j)
congr_p : ↑c ^ d ≡ ↑m (MOD p)
h5 : e * d = (q - 1) * (k * (p - 1)) + 1
h6 : ↑m ^ e - ↑c = ↑q * (↑p * j)
congr_q : ↑c ^ d ≡ ↑m (MOD q)
h8 : q ∣ p
h9 : q = p
⊢ False
Tactic:
show False from p_ne_q h9.symm
State after:
no goals