BT003N

euclid_prime_dvd_product

Stable · empty-context checked

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

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

Direct prerequisites: prime_divisor_eq_one_or_self, gcd_exists_relational, is_gcd_one_to_coprime, gauss_coprime_cancel. The authored body proceeds by case analysis (5), intermediate claims (5), equality transport (4).

Proof neighborhood

Direct dependencies

BT003M prime_divisor_eq_one_or_self BT002V gcd_exists_relational BT0031 is_gcd_one_to_coprime BT0039 gauss_coprime_cancel

Direct dependents

BT00QO prime_nondivisor_mul BT00VB factorial_prime_le_of_divides BT00VC choose_prime_divides_between

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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