BT0028

multiple_refl

Stable · empty-context checked

Every natural number is a multiple of itself.

Exact expanded PA statement

forall a. exists q. a = a * q

Structural proof guide

Every natural number is a multiple of itself.

Direct prerequisites: mul_one. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT000A mul_one

Direct dependents

BT002L is_gcd_zero_right BT002U gcd_exists_up_to BT0039 gauss_coprime_cancel BT003K prime_divisor_exists_up_to BT004K beta_moduli_coprime_of_gap_dvd BT011B nonzero_remainder_not_multiple

Formal native tactic body

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

  1. 0001intro a
  2. 0002exists 1
  3. 0003symm
  4. 0004apply mul_one