BT002E

divisor_one

Stable · empty-context checked

Every natural divisor of one equals one.

Exact expanded PA statement

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

Structural proof guide

Every natural divisor of one equals one.

Direct prerequisites: mul_eq_one_components. The authored body proceeds by case analysis (2), intermediate claims (1).

Proof neighborhood

Direct dependencies

BT0020 mul_eq_one_components

Direct dependents

BT002X coprime_one_right BT002Y coprime_one_left BT0031 is_gcd_one_to_coprime BT004I beta_modulus_coprime_base BT00VB factorial_prime_le_of_divides

Formal native tactic body

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

  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