BT00YA

prime_square_tail_of_two_three_range

Alpha body-checked · checked-use disabled

The scaled two-thirds range places the prime square above 2*n.

Exact expanded PA statement

forall p n s. ((~(p = 1) /\ forall frm_prime_left_bpstt_prime frm_prime_right_bpstt_prime. p = frm_prime_left_bpstt_prime * frm_prime_right_bpstt_prime -> frm_prime_left_bpstt_prime = 1 \/ frm_prime_right_bpstt_prime = 1)) -> (exists bcf_lt_gap_bpstt_positive. bcf_lt_gap_bpstt_positive + S (2) = n) -> (exists bcf_lt_gap_bpstt_scaled. bcf_lt_gap_bpstt_scaled + S (n + n) = (p + p) + p) -> (exists bpvi_b_bpstt_power bpvi_c_bpstt_power. ((forall bpvi_i_bpstt_power. (exists bpvi_repeat_gap_bpstt_power. bpvi_repeat_gap_bpstt_power + S bpvi_i_bpstt_power = 2) -> (((exists bpvi_h_bpstt_power_repeat. bpvi_h_bpstt_power_repeat + S (p) = S ((S (bpvi_i_bpstt_power)) * bpvi_c_bpstt_power)) /\ exists bpvi_q_bpstt_power_repeat. bpvi_b_bpstt_power = bpvi_q_bpstt_power_repeat * S ((S (bpvi_i_bpstt_power)) * bpvi_c_bpstt_power) + (p)))) /\ (exists bpvi_u_bpstt_power bpvi_v_bpstt_power. ((((exists bpvi_h_bpstt_power_start. bpvi_h_bpstt_power_start + S (1) = S ((S (0)) * bpvi_v_bpstt_power)) /\ exists bpvi_q_bpstt_power_start. bpvi_u_bpstt_power = bpvi_q_bpstt_power_start * S ((S (0)) * bpvi_v_bpstt_power) + (1))) /\ ((((exists bpvi_h_bpstt_power_terminal. bpvi_h_bpstt_power_terminal + S (s) = S ((S (2)) * bpvi_v_bpstt_power)) /\ exists bpvi_q_bpstt_power_terminal. bpvi_u_bpstt_power = bpvi_q_bpstt_power_terminal * S ((S (2)) * bpvi_v_bpstt_power) + (s))) /\ forall bpvi_j_bpstt_power. (exists bpvi_product_gap_bpstt_power. bpvi_product_gap_bpstt_power + S bpvi_j_bpstt_power = 2) -> exists bpvi_factor_bpstt_power bpvi_partial_bpstt_power bpvi_successor_bpstt_power. ((((exists bpvi_h_bpstt_power_factor. bpvi_h_bpstt_power_factor + S (bpvi_factor_bpstt_power) = S ((S (bpvi_j_bpstt_power)) * bpvi_c_bpstt_power)) /\ exists bpvi_q_bpstt_power_factor. bpvi_b_bpstt_power = bpvi_q_bpstt_power_factor * S ((S (bpvi_j_bpstt_power)) * bpvi_c_bpstt_power) + (bpvi_factor_bpstt_power))) /\ ((((exists bpvi_h_bpstt_power_partial. bpvi_h_bpstt_power_partial + S (bpvi_partial_bpstt_power) = S ((S (bpvi_j_bpstt_power)) * bpvi_v_bpstt_power)) /\ exists bpvi_q_bpstt_power_partial. bpvi_u_bpstt_power = bpvi_q_bpstt_power_partial * S ((S (bpvi_j_bpstt_power)) * bpvi_v_bpstt_power) + (bpvi_partial_bpstt_power))) /\ ((((exists bpvi_h_bpstt_power_successor. bpvi_h_bpstt_power_successor + S (bpvi_successor_bpstt_power) = S ((S (S bpvi_j_bpstt_power)) * bpvi_v_bpstt_power)) /\ exists bpvi_q_bpstt_power_successor. bpvi_u_bpstt_power = bpvi_q_bpstt_power_successor * S ((S (S bpvi_j_bpstt_power)) * bpvi_v_bpstt_power) + (bpvi_successor_bpstt_power))) /\ bpvi_successor_bpstt_power = bpvi_partial_bpstt_power * bpvi_factor_bpstt_power)))))))) -> (exists bcf_lt_gap_bpstt_result. bcf_lt_gap_bpstt_result + S (n + n) = s)

Structural proof guide

The scaled two-thirds range places the prime square above 2*n.

Direct prerequisites: prime_is_succ_succ, zero_or_succ, add_le_add_right, add_le_add_left, le_trans, lt_not_le, mul_le_mul_left, mul_one, lt_of_lt_of_le, pow_two. The authored body proceeds by case analysis (3), intermediate claims (12), equality transport (12), closed numeral normalization (1).

Proof neighborhood

Direct dependencies

BT00AW prime_is_succ_succ BT000Q zero_or_succ BT0014 add_le_add_right BT0015 add_le_add_left BT000F le_trans BT001I lt_not_le BT001L mul_le_mul_left BT000A mul_one BT001D lt_of_lt_of_le BT009W pow_two

Direct dependents

BT00YE central_binom_prime_valuation_zero_two_thirds_range

Formal native tactic body

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

  1. 0001intro p
  2. 0002intro n
  3. 0003intro s
  4. 0004intro hp
  5. 0005intro hpositive
  6. 0006intro hscaled
  7. 0007intro hsquare
  8. 0008have hshape : exists k. p = S (S k)
  9. 0009specialize prime_is_succ_succ p
  10. 0010apply prime_is_succ_succ
  11. 0011exact hp
  12. 0012cases hshape
  13. 0013specialize zero_or_succ x
  14. 0014cases zero_or_succ
  15. 0015have hn_lower : exists bcf_le_gap_bpstt_three_lower. bcf_le_gap_bpstt_three_lower + (3) = n
  16. 0016exact hpositive
  17. 0017have hdouble_lower : exists bcf_le_gap_bpstt_six_lower. bcf_le_gap_bpstt_six_lower + (3 + 3) = n + n
  18. 0018have hfirst_add : exists bcf_le_gap_bpstt_first_add. bcf_le_gap_bpstt_first_add + (3 + 3) = n + 3
  19. 0019specialize add_le_add_right 3
  20. 0020specialize add_le_add_right n
  21. 0021specialize add_le_add_right 3
  22. 0022apply add_le_add_right
  23. 0023exact hn_lower
  24. 0024have hsecond_add : exists bcf_le_gap_bpstt_second_add. bcf_le_gap_bpstt_second_add + (n + 3) = n + n
  25. 0025specialize add_le_add_left 3
  26. 0026specialize add_le_add_left n
  27. 0027specialize add_le_add_left n
  28. 0028apply add_le_add_left
  29. 0029exact hn_lower
  30. 0030specialize le_trans (3 + 3)
  31. 0031specialize le_trans (n + 3)
  32. 0032specialize le_trans (n + n)
  33. 0033apply le_trans
  34. 0034exact hfirst_add
  35. 0035exact hsecond_add
  36. 0036rewrite zero_or_succ_left at hshape_witness
  37. 0037rewrite hshape_witness at hscaled
  38. 0038rewrite hshape_witness at hscaled
  39. 0039rewrite hshape_witness at hscaled
  40. 0040exfalso
  41. 0041specialize lt_not_le (n + n)
  42. 0042specialize lt_not_le ((2 + 2) + 2)
  43. 0043apply lt_not_le
  44. 0044exact hscaled
  45. 0045have hsmall : (2 + 2) + 2 = 3 + 3
  46. 0046norm_num
  47. 0047rewrite hsmall
  48. 0048exact hdouble_lower
  49. 0049cases zero_or_succ_right
  50. 0050have hp_lower : exists bcf_le_gap_bpstt_prime_lower. bcf_le_gap_bpstt_prime_lower + (3) = p
  51. 0051exists x1
  52. 0052rewrite hshape_witness
  53. 0053rewrite zero_or_succ_right_witness
  54. 0054simp
  55. 0055have hproduct_lower : exists bcf_le_gap_bpstt_product_lower. bcf_le_gap_bpstt_product_lower + ((p + p) + p) = p * p
  56. 0056have hraw_product_lower : exists bcf_le_gap_bpstt_raw_product_lower. bcf_le_gap_bpstt_raw_product_lower + (p * 3) = p * p
  57. 0057specialize mul_le_mul_left 3
  58. 0058specialize mul_le_mul_left p
  59. 0059specialize mul_le_mul_left p
  60. 0060apply mul_le_mul_left
  61. 0061exact hp_lower
  62. 0062have htriple : p * 3 = (p + p) + p
  63. 0063rewrite PA6
  64. 0064rewrite PA6
  65. 0065specialize mul_one p
  66. 0066rewrite mul_one
  67. 0067refl
  68. 0068rewrite htriple at hraw_product_lower
  69. 0069exact hraw_product_lower
  70. 0070have hstrict_product : exists bcf_lt_gap_bpstt_strict_product. bcf_lt_gap_bpstt_strict_product + S (n + n) = p * p
  71. 0071specialize lt_of_lt_of_le (n + n)
  72. 0072specialize lt_of_lt_of_le ((p + p) + p)
  73. 0073specialize lt_of_lt_of_le (p * p)
  74. 0074apply lt_of_lt_of_le
  75. 0075exact hscaled
  76. 0076exact hproduct_lower
  77. 0077have hsquare_value : s = p * p
  78. 0078specialize pow_two p
  79. 0079specialize pow_two 2
  80. 0080specialize pow_two s
  81. 0081apply pow_two
  82. 0082refl
  83. 0083exact hsquare
  84. 0084rewrite hsquare_value
  85. 0085exact hstrict_product