PA0003

prime_divisor_eq_one_or_self

Stable checked-use theorem · independently closed

Every divisor of a prime is one or the prime itself.

Exact expanded PA statement

forall p g. (~(p = 1) /\ forall c d. p = c * d -> c = 1 \/ d = 1) -> (exists x. p = g * x) -> g = 1 \/ p = g

Structural proof guide

Generated structural guide

Every divisor of a prime is one or the prime itself.

Use the direct prerequisites mul_one as previously established PA formulas.

The proof proceeds by case analysis (3), intermediate claims (1), equality transport (1).

Referenced ingredients

PA0002 mul_one

Proof neighborhood

Direct dependencies

PA0002 mul_one

Direct dependents

PA0038 euclid_prime_dvd_product PA003M prime_coprime_or_divides PA006V distinct_primes_left_not_divide_right PA00D8 distinct_odd_prime_half_products_ne PA00DO distinct_primes_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 g
  3. 0003intro hp
  4. 0004intro hdiv
  5. 0005cases hp
  6. 0006cases hdiv
  7. 0007specialize hp_right g
  8. 0008specialize hp_right x
  9. 0009have hfactor : g = 1 \/ x = 1
  10. 0010apply hp_right
  11. 0011exact hdiv_witness
  12. 0012cases hfactor
  13. 0013left
  14. 0014exact hfactor_left
  15. 0015right
  16. 0016trans g * x
  17. 0017exact hdiv_witness
  18. 0018rewrite hfactor_right
  19. 0019apply mul_one