BT0118

nonprime_has_small_prime_divisor_below_square

Alpha body-checked · checked-use disabled

Every composite below (B+1)^2 has a prime divisor at most B.

Exact expanded PA statement

forall B n. ~(n = 0) -> ~(n = 1) -> (exists bpr_gap_bb8npsp_square. bpr_gap_bb8npsp_square + S (n) = S B * S B) -> ~((~(n = 1) /\ forall bpr_left_bb8npsp_source bpr_right_bb8npsp_source. n = bpr_left_bb8npsp_source * bpr_right_bb8npsp_source -> bpr_left_bb8npsp_source = 1 \/ bpr_right_bb8npsp_source = 1)) -> (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)))

Structural proof guide

Every composite below (B+1)^2 has a prime divisor at most B.

Direct prerequisites: prime_or_composite, factor_pair_has_small_member_below_square, mul_zero_left, prime_divisor_exists, divisor_le_nonzero, le_trans, multiple_trans, mul_comm. The authored body proceeds by case analysis (10), intermediate claims (9), equality transport (2).

Proof neighborhood

Direct dependencies

BT003F prime_or_composite BT0117 factor_pair_has_small_member_below_square BT0004 mul_zero_left BT003L prime_divisor_exists BT002D divisor_le_nonzero BT000F le_trans BT002C multiple_trans BT0006 mul_comm

Direct dependents

BT0119 prime_of_no_small_prime_divisor_below_square

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 hbound
  6. 0006intro hnotprime
  7. 0007specialize prime_or_composite n
  8. 0008have hkind : ((~(n = 1) /\ forall a b. n = a * b -> a = 1 \/ b = 1) \/ exists c d. ((~(c = 1) /\ ~(d = 1)) /\ n = c * d))
  9. 0009apply prime_or_composite
  10. 0010exact hn0
  11. 0011exact hn1
  12. 0012cases hkind
  13. 0013exfalso
  14. 0014apply hnotprime
  15. 0015exact hkind_left
  16. 0016cases hkind_right
  17. 0017cases hkind_right_witness
  18. 0018cases hkind_right_witness_witness
  19. 0019cases hkind_right_witness_witness_left
  20. 0020have hsmall : (exists k. k + x = B) \/ (exists k. k + x1 = B)
  21. 0021specialize factor_pair_has_small_member_below_square B
  22. 0022specialize factor_pair_has_small_member_below_square n
  23. 0023specialize factor_pair_has_small_member_below_square x
  24. 0024specialize factor_pair_has_small_member_below_square x1
  25. 0025apply factor_pair_has_small_member_below_square
  26. 0026exact hkind_right_witness_witness_right
  27. 0027exact hbound
  28. 0028cases hsmall
  29. 0029have hx0 : ~(x = 0)
  30. 0030intro hx0_source
  31. 0031apply hn0
  32. 0032trans x * x1
  33. 0033exact hkind_right_witness_witness_right
  34. 0034rewrite hx0_source
  35. 0035apply mul_zero_left
  36. 0036have hp : exists p. ((~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) /\ exists q. x = p * q)
  37. 0037specialize prime_divisor_exists x
  38. 0038apply prime_divisor_exists
  39. 0039exact hx0
  40. 0040exact hkind_right_witness_witness_left_left
  41. 0041cases hp
  42. 0042cases hp_witness
  43. 0043exists x2
  44. 0044split
  45. 0045exact hp_witness_left
  46. 0046split
  47. 0047have hpx : exists k. k + x2 = x
  48. 0048specialize divisor_le_nonzero x2
  49. 0049specialize divisor_le_nonzero x
  50. 0050apply divisor_le_nonzero
  51. 0051exact hx0
  52. 0052exact hp_witness_right
  53. 0053specialize le_trans x2
  54. 0054specialize le_trans x
  55. 0055specialize le_trans B
  56. 0056apply le_trans
  57. 0057exact hpx
  58. 0058exact hsmall_left
  59. 0059specialize multiple_trans x
  60. 0060specialize multiple_trans x2
  61. 0061specialize multiple_trans n
  62. 0062apply multiple_trans
  63. 0063exists x1
  64. 0064exact hkind_right_witness_witness_right
  65. 0065exact hp_witness_right
  66. 0066have hswap : n = x1 * x
  67. 0067trans x * x1
  68. 0068exact hkind_right_witness_witness_right
  69. 0069apply mul_comm
  70. 0070have hx10 : ~(x1 = 0)
  71. 0071intro hx10_source
  72. 0072apply hn0
  73. 0073trans x1 * x
  74. 0074exact hswap
  75. 0075rewrite hx10_source
  76. 0076apply mul_zero_left
  77. 0077have hp : exists p. ((~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) /\ exists q. x1 = p * q)
  78. 0078specialize prime_divisor_exists x1
  79. 0079apply prime_divisor_exists
  80. 0080exact hx10
  81. 0081exact hkind_right_witness_witness_left_right
  82. 0082cases hp
  83. 0083cases hp_witness
  84. 0084exists x2
  85. 0085split
  86. 0086exact hp_witness_left
  87. 0087split
  88. 0088have hpx : exists k. k + x2 = x1
  89. 0089specialize divisor_le_nonzero x2
  90. 0090specialize divisor_le_nonzero x1
  91. 0091apply divisor_le_nonzero
  92. 0092exact hx10
  93. 0093exact hp_witness_right
  94. 0094specialize le_trans x2
  95. 0095specialize le_trans x1
  96. 0096specialize le_trans B
  97. 0097apply le_trans
  98. 0098exact hpx
  99. 0099exact hsmall_right
  100. 0100specialize multiple_trans x1
  101. 0101specialize multiple_trans x2
  102. 0102specialize multiple_trans n
  103. 0103apply multiple_trans
  104. 0104exists x
  105. 0105exact hswap
  106. 0106exact hp_witness_right