BT0119

prime_of_no_small_prime_divisor_below_square

Alpha body-checked · checked-use disabled

Trial division by primes through B certifies numbers below (B+1)^2.

Exact expanded PA statement

forall B n. ~(n = 0) -> ~(n = 1) -> (exists bpr_gap_bb8pnsp_square. bpr_gap_bb8pnsp_square + S (n) = S B * S B) -> (forall p. ((~(p = 1) /\ forall bpr_left_bb8pnsp_prime bpr_right_bb8pnsp_prime. p = bpr_left_bb8pnsp_prime * bpr_right_bb8pnsp_prime -> bpr_left_bb8pnsp_prime = 1 \/ bpr_right_bb8pnsp_prime = 1)) -> (exists bpr_le_gap_bb8pnsp_bound. bpr_le_gap_bb8pnsp_bound + (p) = (B)) -> ~(exists bpr_quotient_bb8pnsp_divides. n = (p) * bpr_quotient_bb8pnsp_divides)) -> ((~(n = 1) /\ forall bpr_left_bb8pnsp_result bpr_right_bb8pnsp_result. n = bpr_left_bb8pnsp_result * bpr_right_bb8pnsp_result -> bpr_left_bb8pnsp_result = 1 \/ bpr_right_bb8pnsp_result = 1))

Structural proof guide

Trial division by primes through B certifies numbers below (B+1)^2.

Direct prerequisites: prime_decidable, nonprime_has_small_prime_divisor_below_square. The authored body proceeds by case analysis (4), intermediate claims (1).

Proof neighborhood

Direct dependencies

BT003H prime_decidable BT0118 nonprime_has_small_prime_divisor_below_square

Direct dependents

BT011F prime_five BT011G prime_seven BT011H prime_thirteen BT011I prime_twenty_three BT011J prime_forty_three BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen BT011N prime_five_hundred_twenty_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 B
  2. 0002intro n
  3. 0003intro hn0
  4. 0004intro hn1
  5. 0005intro hsquare
  6. 0006intro hexclude
  7. 0007specialize prime_decidable n
  8. 0008cases prime_decidable
  9. 0009exact prime_decidable_left
  10. 0010exfalso
  11. 0011have hp : exists p. ((~(p = 1) /\ forall bpr_left_bb8npsp_prime bpr_right_bb8npsp_prime. p = bpr_left_bb8npsp_prime * bpr_right_bb8npsp_prime -> bpr_left_bb8npsp_prime = 1 \/ bpr_right_bb8npsp_prime = 1)) /\ ((exists bpr_le_gap_bb8npsp_bound. bpr_le_gap_bb8npsp_bound + (p) = (B)) /\ (exists bpr_quotient_bb8npsp_divides. n = (p) * bpr_quotient_bb8npsp_divides))
  12. 0012specialize nonprime_has_small_prime_divisor_below_square B
  13. 0013specialize nonprime_has_small_prime_divisor_below_square n
  14. 0014apply nonprime_has_small_prime_divisor_below_square
  15. 0015exact hn0
  16. 0016exact hn1
  17. 0017exact hsquare
  18. 0018exact prime_decidable_right
  19. 0019cases hp
  20. 0020cases hp_witness
  21. 0021cases hp_witness_right
  22. 0022specialize hexclude x
  23. 0023apply hexclude
  24. 0024exact hp_witness_left
  25. 0025exact hp_witness_right_left
  26. 0026exact hp_witness_right_right