PA000O

divisor_one

Stable checked-use theorem · independently closed

Every natural divisor of one equals one.

Exact expanded PA statement

forall d. (exists y. 1 = d * y) -> d = 1

Structural proof guide

Generated structural guide

Every natural divisor of one equals one.

Use the direct prerequisites mul_eq_one_components as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (1).

Referenced ingredients

PA000N mul_eq_one_components

Proof neighborhood

Direct dependencies

PA000N mul_eq_one_components

Direct dependents

PA000P coprime_one_left PA0015 beta_modulus_coprime_base PA0037 is_gcd_one_to_coprime

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 d
  2. 0002intro h
  3. 0003cases h
  4. 0004specialize mul_eq_one_components d
  5. 0005specialize mul_eq_one_components x
  6. 0006have parts : d = 1 /\ x = 1
  7. 0007apply mul_eq_one_components
  8. 0008symm
  9. 0009exact h_witness
  10. 0010cases parts
  11. 0011exact parts_left