PA0038

euclid_prime_dvd_product

Stable checked-use theorem · independently closed

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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.

Read the argument

Proof checkpoints

36 script commands · 14 reading checkpoints · 5 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (4)
prime divisor eq one or selfgcd exists relationalis gcd one to coprimegauss coprime cancel
01Fix variables and assumptionsL1–5

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro hp
  5. L5
    intro hab
02Establish hgL6–7

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gcd exists relational.

  1. L6
    have 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)
  2. L7
    apply gcd_exists_relational
03Separate the logical casesL8–8

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L8
    cases hg
04Establish hgfullL9–10

Establish this local claim before using it. It is not an additional assumption.

  1. L9
    have 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)
  2. L10
    exact hg_witness
05Separate the logical casesL11–12

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L11
    cases hg_witness
  2. L12
    cases hg_witness_left
06Establish hfactorL13–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime divisor eq one or self.

  1. L13
    have hfactor : x = 1 \/ p = x
  2. L14
    specialize prime_divisor_eq_one_or_self p
  3. L15
    specialize prime_divisor_eq_one_or_self x
  4. L16
    apply prime_divisor_eq_one_or_self
  5. L17
    exact hp
  6. L18
    exact hg_witness_left_left
07Separate the logical casesL19–20

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L19
    cases hfactor
  2. L20
    right
08Use earlier factsL21–21

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L21
    apply gauss_coprime_cancel
09Establish hcopL22–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply is gcd one to coprime.

  1. L22
    have hcop : forall d. (exists u. p = d * u) -> (exists v. a = d * v) -> d = 1
  2. L23
    apply is_gcd_one_to_coprime
10Establish hg1L24–31

Establish this local claim before using it. It is not an additional assumption.

  1. L24
    have 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)
  2. L25
    rewrite <- hfactor_left
  3. L26
    rewrite <- hfactor_left
  4. L27
    rewrite <- hfactor_left
  5. L28
    exact hgfull
  6. L29
    exact hg1
  7. L30
    exact hcop
  8. L31
    exact hab
11Separate the logical casesL32–33

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L32
    left
  2. L33
    cases hg_witness_left_right
12Construct an explicit witnessL34–34

Supply the displayed value, then prove that it has the required property.

  1. L34
    exists x1
13Calculate and transport equalitiesL35–35

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L35
    rewrite hfactor_right
14Use earlier factsL36–36

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L36
    exact hg_witness_left_right_witness

Library-wide reading audit

Original exact command ledger · 36 lines
  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