PA0038

euclid_prime_dvd_product

Stable checked-use theorem · independently closed

A prime dividing a product divides at least one factor (Euclid's lemma).

Exact expanded PA statement

forall p a b. (~(p = 1) /\ forall c d. p = c * d -> c = 1 \/ d = 1) -> (exists k. a * b = p * k) -> (exists u. a = p * u) \/ exists v. b = p * v

Structural proof guide

Generated structural guide

A prime dividing a product divides at least one factor (Euclid's lemma).

Use the direct prerequisites prime_divisor_eq_one_or_self, gcd_exists_relational, is_gcd_one_to_coprime, gauss_coprime_cancel as previously established PA formulas.

The proof proceeds by case analysis (5), intermediate claims (5), equality transport (4).

Referenced ingredients

PA0003 prime_divisor_eq_one_or_self PA0036 gcd_exists_relational PA0037 is_gcd_one_to_coprime PA001P gauss_coprime_cancel

Proof neighborhood

Direct dependencies

PA0003 prime_divisor_eq_one_or_self PA0036 gcd_exists_relational PA0037 is_gcd_one_to_coprime PA001P gauss_coprime_cancel

Direct dependents

PA0072 gauss_half_range_signed_choices PA008B prime_mul_index_map_exists_up_to PA00AG prime_bounded_square_one_cases PA00D8 distinct_odd_prime_half_products_ne PA00DN prime_nondivisor_bounded_scaled_remainder_nonzero

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro hp
  5. 0005intro hab
  6. 0006have hg : exists g. (((exists x. p = g * x) /\ (exists y. a = g * y)) /\ forall c. (exists u. p = c * u) -> (exists v. a = c * v) -> exists w. g = c * w)
  7. 0007apply gcd_exists_relational
  8. 0008cases hg
  9. 0009have hgfull : (((exists u. p = x * u) /\ (exists v. a = x * v)) /\ forall c. (exists s. p = c * s) -> (exists t. a = c * t) -> exists w. x = c * w)
  10. 0010exact hg_witness
  11. 0011cases hg_witness
  12. 0012cases hg_witness_left
  13. 0013have hfactor : x = 1 \/ p = x
  14. 0014specialize prime_divisor_eq_one_or_self p
  15. 0015specialize prime_divisor_eq_one_or_self x
  16. 0016apply prime_divisor_eq_one_or_self
  17. 0017exact hp
  18. 0018exact hg_witness_left_left
  19. 0019cases hfactor
  20. 0020right
  21. 0021apply gauss_coprime_cancel
  22. 0022have hcop : forall d. (exists u. p = d * u) -> (exists v. a = d * v) -> d = 1
  23. 0023apply is_gcd_one_to_coprime
  24. 0024have hg1 : (((exists u. p = 1 * u) /\ (exists v. a = 1 * v)) /\ forall c. (exists s. p = c * s) -> (exists t. a = c * t) -> exists w. 1 = c * w)
  25. 0025rewrite <- hfactor_left
  26. 0026rewrite <- hfactor_left
  27. 0027rewrite <- hfactor_left
  28. 0028exact hgfull
  29. 0029exact hg1
  30. 0030exact hcop
  31. 0031exact hab
  32. 0032left
  33. 0033cases hg_witness_left_right
  34. 0034exists x1
  35. 0035rewrite hfactor_right
  36. 0036exact hg_witness_left_right_witness