BT010F

floor_sqrt_le_third_quotient

Alpha body-checked · checked-use disabled

The floor root is at most the quotient of the doubled input by three.

Exact expanded PA statement

forall n s q r. (exists bcf_lt_gap_b5rbfsltq_positive. bcf_lt_gap_b5rbfsltq_positive + S (2) = n) -> (((exists bcs_sqrt_lower_gap_b5rbfsltq_floor. bcs_sqrt_lower_gap_b5rbfsltq_floor + (s) * (s) = (n + n)) /\ exists bcs_sqrt_upper_gap_b5rbfsltq_floor. bcs_sqrt_upper_gap_b5rbfsltq_floor + S (n + n) = S (s) * S (s))) -> (((n + n) = (3) * (q) + (r) /\ (exists bcf_lt_gap_b5rbfsltq_division_bound. bcf_lt_gap_b5rbfsltq_division_bound + S (r) = 3))) -> (exists bcf_le_gap_b5rbfsltq_result. bcf_le_gap_b5rbfsltq_result + (s) = q)

Structural proof guide

The floor root is at most the quotient of the doubled input by three.

Direct prerequisites: floor_sqrt_three_mul_le_double, division_quotient_lower_of_scaled_le. The authored body proceeds by intermediate claims (1).

Proof neighborhood

Direct dependencies

BT010D floor_sqrt_three_mul_le_double BT010E division_quotient_lower_of_scaled_le

Direct dependents

BT010G floor_sqrt_third_quotient_gap_exists BT010X no_bertrand_high_contribution_choice_eq_one

Formal native tactic body

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

  1. 0001intro n
  2. 0002intro s
  3. 0003intro q
  4. 0004intro r
  5. 0005intro hpositive
  6. 0006intro hfloor
  7. 0007intro hdivision
  8. 0008have hscaled : exists bcf_le_gap_b5rbfsltq_scaled. bcf_le_gap_b5rbfsltq_scaled + (3 * s) = n + n
  9. 0009specialize floor_sqrt_three_mul_le_double n
  10. 0010specialize floor_sqrt_three_mul_le_double s
  11. 0011apply floor_sqrt_three_mul_le_double
  12. 0012exact hpositive
  13. 0013exact hfloor
  14. 0014specialize division_quotient_lower_of_scaled_le 3
  15. 0015specialize division_quotient_lower_of_scaled_le (n + n)
  16. 0016specialize division_quotient_lower_of_scaled_le q
  17. 0017specialize division_quotient_lower_of_scaled_le r
  18. 0018specialize division_quotient_lower_of_scaled_le s
  19. 0019apply division_quotient_lower_of_scaled_le
  20. 0020exact hdivision
  21. 0021exact hscaled