BT010C

three_mul_le_square_of_three_le

Alpha body-checked · checked-use disabled

Every natural at least three dominates three times itself by its square.

Exact expanded PA statement

forall s. (exists bcf_le_gap_b5rbtmsts_source. bcf_le_gap_b5rbtmsts_source + (3) = s) -> (exists bcf_le_gap_b5rbtmsts_result. bcf_le_gap_b5rbtmsts_result + (3 * s) = s * s)

Structural proof guide

Every natural at least three dominates three times itself by its square.

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

Proof neighborhood

Direct dependencies

BT001M mul_le_mul_right

Direct dependents

BT010D floor_sqrt_three_mul_le_double

Formal native tactic body

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

  1. 0001intro s
  2. 0002intro hthree
  3. 0003specialize mul_le_mul_right 3
  4. 0004specialize mul_le_mul_right s
  5. 0005specialize mul_le_mul_right s
  6. 0006apply mul_le_mul_right
  7. 0007exact hthree