internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Lemma_7_5_1
Proof 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 _
Proof 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)
Theorem: HTPI.Lemma_7_5_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof 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]
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof 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]
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof 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]
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof 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]
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof 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]
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof 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]
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof 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]
Proof state after:
no goals
Theorem: HTPI.Lemma_7_5_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_7_5_1
Proof 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]
Proof 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)
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof 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)
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof 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)
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof 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)
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof 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)
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof 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)
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof 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)
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof 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)
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof 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)
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof 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)
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof 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)
Theorem: HTPI.Theorem_7_5_1
Proof 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]
Proof 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)
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_7_5_1
Proof 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]
Proof 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
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_7_5_1
Proof 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]
Proof 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)
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_7_5_1
Proof 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]
Proof 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
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_7_5_1
Proof 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]
Proof 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)
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_7_5_1
Proof 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)
Proof 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
Theorem: HTPI.Theorem_7_5_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.invRel_def
Proof state before:
U V : Type
R : Rel U V
u : U
v : V
⊢ invRel R v u ↔ R u v
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.equinum_image
Proof state before:
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
⊢ A ∼ B
Tactic:
rewrite [←h2]
Proof state after:
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
⊢ A ∼ image f A