PA0019

multiple_refl

Stable checked-use theorem · independently closed

Every natural number is a multiple of itself.

Exact expanded PA statement

forall a. exists q. a = a * q

Structural proof guide

Generated structural guide

Every natural number is a multiple of itself.

Use the direct prerequisites mul_one as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA0002 mul_one

Proof neighborhood

Direct dependencies

PA0002 mul_one

Direct dependents

PA001F is_gcd_zero_right PA001P gauss_coprime_cancel PA001Q beta_moduli_coprime_of_gap_dvd PA0035 gcd_exists_up_to

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 a
  2. 0002exists 1
  3. 0003symm
  4. 0004apply mul_one