BT0115 · Bertrand theorem

bertrand_eventually_closed_upper

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Every n at least 16*32 has a prime in the constructive open-closed Bertrand interval.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ n. Le(16 · 32,n) → ∃ x. Prime(x) ∧ (Lt(n,x) ∧ Le(x,n + n))

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0002 Lt PD0004 Prime

4 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0004 Prime PD0007 DivRem PD0020 Pow PD0042 CentralBinom PD0051 FloorSqrt

25 occurrences

Exact expanded native-PA statement
forall n. (exists bcf_le_gap_b7_threshold. bcf_le_gap_b7_threshold + (16 * 32) = n) -> (exists b7_prime. ((~(b7_prime = 1) /\ forall bpr_left_b7_result_prime bpr_right_b7_result_prime. b7_prime = bpr_left_b7_result_prime * bpr_right_b7_result_prime -> bpr_left_b7_result_prime = 1 \/ bpr_right_b7_result_prime = 1)) /\ ((exists bcf_lt_gap_b7_result_lower. bcf_lt_gap_b7_result_lower + S (n) = b7_prime) /\ (exists bcf_le_gap_b7_result_upper. bcf_le_gap_b7_result_upper + (b7_prime) = n + n)))

Proof neighborhood

Direct theorem prerequisites

BT00PS bounded_prime_interval_search BT00PW le_mul_of_one_le_right BT000F le_trans BT001D lt_of_lt_of_le BT00RA floor_sqrt_total BT001P division_remainder_exists BT00TN central_binom_exists BT0080 pow_exists BT00U4 four_pow_lt_mul_central_binom BT0114 central_binom_le_of_no_bertrand_prime BT001L mul_le_mul_left BT0008 mul_assoc BT00X8 bertrand_main_inequality_nat BT001I lt_not_le

Direct theorem dependents

BT0125 bertrand_closed_upper

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

139 script commands · 39 reading checkpoints · 20 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (14)
bounded prime interval searchle mul of one le rightle translt of lt of lefloor sqrt totaldivision remainder existscentral binom existspow existsfour pow lt mul central binomcentral binom le of no bertrand primemul le mul leftmul assocbertrand main inequality natlt not le
01Fix variables and assumptionsL1–2

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
  2. L2
    intro hthreshold
02Establish hsearchL3–6

Establish this local claim before using it. It is not an additional assumption.

  1. L3
    have hsearch : (∃ x. Prime(x) ∧ (Lt(n,x) ∧ Le(x,n + n))) ∨ (∀ x. Lt(n,x) ∧ Le(x,n + n) → ¬Prime(x))Definitions: Prime(x)Lt(n,x)Le(x,n + n)Original native command in the exact edition
  2. L4
    specialize bounded_prime_interval_search n
  3. L5
    specialize bounded_prime_interval_search (n + n)
  4. L6
    exact bounded_prime_interval_search
03Separate the logical casesL7–7

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L7
    cases hsearch
04Use earlier factsL8–8

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L8
    exact hsearch_left
05Separate the logical casesL9–9

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L9
    exfalso
06Establish hone_thirty_twoL10–10

Establish this local claim before using it. It is not an additional assumption.

  1. L10
    have hone_thirty_two : Lt(0,32)Definitions: Lt(0,32)Original native command in the exact edition
07Construct an explicit witnessL11–11

Supply the displayed value, then prove that it has the required property.

  1. L11
    exists 31
08Calculate and transport equalitiesL12–12

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L12
    norm_num
09Establish hsixteen_thresholdL13–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le mul of one le right.

  1. L13
    have hsixteen_threshold : Lt(15,16 · 32)Definitions: Lt(15,16 · 32)Original native command in the exact edition
  2. L14
    specialize le_mul_of_one_le_right 16
  3. L15
    specialize le_mul_of_one_le_right 32
  4. L16
    apply le_mul_of_one_le_right
  5. L17
    exact hone_thirty_two
10Establish hfour_sixteenL18–18

Establish this local claim before using it. It is not an additional assumption.

  1. L18
    have hfour_sixteen : Lt(3,16)Definitions: Lt(3,16)Original native command in the exact edition
11Construct an explicit witnessL19–19

Supply the displayed value, then prove that it has the required property.

  1. L19
    exists 12
12Calculate and transport equalitiesL20–20

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L20
    norm_num
13Establish hfour_thresholdL21–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.

  1. L21
    have hfour_threshold : Lt(3,16 · 32)Definitions: Lt(3,16 · 32)Original native command in the exact edition
  2. L22
    specialize le_trans 4
  3. L23
    specialize le_trans 16
  4. L24
    specialize le_trans (16 * 32)
  5. L25
    apply le_trans
  6. L26
    exact hfour_sixteen
  7. L27
    exact hsixteen_threshold
14Establish hfour_nL28–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.

  1. L28
    have hfour_n : Lt(3,n)Definitions: Lt(3,n)Original native command in the exact edition
  2. L29
    specialize le_trans 4
  3. L30
    specialize le_trans (16 * 32)
  4. L31
    specialize le_trans n
  5. L32
    apply le_trans
  6. L33
    exact hfour_threshold
  7. L34
    exact hthreshold
15Establish htwo_fourL35–35

Establish this local claim before using it. It is not an additional assumption.

  1. L35
    have htwo_four : Lt(2,4)Definitions: Lt(2,4)Original native command in the exact edition
16Construct an explicit witnessL36–36

Supply the displayed value, then prove that it has the required property.

  1. L36
    exists 1
17Calculate and transport equalitiesL37–37

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L37
    norm_num
18Establish htwo_nL38–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt of lt of le.

  1. L38
    have htwo_n : Lt(2,n)Definitions: Lt(2,n)Original native command in the exact edition
  2. L39
    specialize lt_of_lt_of_le 2
  3. L40
    specialize lt_of_lt_of_le 4
  4. L41
    specialize lt_of_lt_of_le n
  5. L42
    apply lt_of_lt_of_le
  6. L43
    exact htwo_four
  7. L44
    exact hfour_n
19Establish hfloor_existsL45–47

Establish this local claim before using it. It is not an additional assumption.

  1. L45
    have hfloor_exists : ∃ s. FloorSqrt(n + n,s)Definitions: FloorSqrt(n + n,s)Original native command in the exact edition
  2. L46
    specialize floor_sqrt_total (n + n)
  3. L47
    exact floor_sqrt_total
20Separate the logical casesL48–48

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L48
    cases hfloor_exists
21Establish hdivision_existsL49–55

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division remainder exists.

  1. L49
    have hdivision_exists : ∃ q. ∃ r. DivRem(n + n,3,q,r)Definitions: DivRem(n + n,3,q,r)Original native command in the exact edition
  2. L50
    specialize division_remainder_exists 3
  3. L51
    specialize division_remainder_exists (n + n)
  4. L52
    apply division_remainder_exists
  5. L53
    intro hthree_zero
  6. L54
    apply PA1
  7. L55
    exact hthree_zero
22Separate the logical casesL56–57

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L56
    cases hdivision_exists
  2. L57
    cases hdivision_exists_witness
23Establish hcentral_existsL58–60

Establish this local claim before using it. It is not an additional assumption.

  1. L58
    have hcentral_exists : ∃ C. CentralBinom(n,C)Definitions: CentralBinom(n,C)Original native command in the exact edition
  2. L59
    specialize central_binom_exists n
  3. L60
    exact central_binom_exists
24Separate the logical casesL61–61

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L61
    cases hcentral_exists
25Establish hpower_a_existsL62–65

Establish this local claim before using it. It is not an additional assumption.

  1. L62
    have hpower_a_exists : ∃ A. Pow(n + n,x,A)Definitions: Pow(n + n,x,A)Original native command in the exact edition
  2. L63
    specialize pow_exists (n + n)
  3. L64
    specialize pow_exists x
  4. L65
    exact pow_exists
26Separate the logical casesL66–66

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L66
    cases hpower_a_exists
27Establish hpower_b_existsL67–70

Establish this local claim before using it. It is not an additional assumption.

  1. L67
    have hpower_b_exists : ∃ B. Pow(4,x1,B)Definitions: Pow(4,x1,B)Original native command in the exact edition
  2. L68
    specialize pow_exists 4
  3. L69
    specialize pow_exists x1
  4. L70
    exact pow_exists
28Separate the logical casesL71–71

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L71
    cases hpower_b_exists
29Establish hpower_f_existsL72–75

Establish this local claim before using it. It is not an additional assumption.

  1. L72
    have hpower_f_exists : ∃ F. Pow(4,n,F)Definitions: Pow(4,n,F)Original native command in the exact edition
  2. L73
    specialize pow_exists 4
  3. L74
    specialize pow_exists n
  4. L75
    exact pow_exists
30Separate the logical casesL76–76

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L76
    cases hpower_f_exists
31Establish hlowerL77–84

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four pow lt mul central binom.

  1. L77
    have hlower : Lt(x6,n · x3)Definitions: Lt(x6,n · x3)Original native command in the exact edition
  2. L78
    specialize four_pow_lt_mul_central_binom n
  3. L79
    specialize four_pow_lt_mul_central_binom x6
  4. L80
    specialize four_pow_lt_mul_central_binom x3
  5. L81
    apply four_pow_lt_mul_central_binom
  6. L82
    exact hfour_n
  7. L83
    exact hpower_f_exists_witness
  8. L84
    exact hcentral_exists_witness
32Establish hcentral_upperL85–94

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply central binom le of no bertrand prime.

  1. L85
    have hcentral_upper : Le(x3,x4 · x5)Definitions: Le(x3,x4 · x5)Original native command in the exact edition
  2. L86
    specialize central_binom_le_of_no_bertrand_prime n
  3. L87
    specialize central_binom_le_of_no_bertrand_prime x
  4. L88
    specialize central_binom_le_of_no_bertrand_prime x1
  5. L89
    specialize central_binom_le_of_no_bertrand_prime x2
  6. L90
    specialize central_binom_le_of_no_bertrand_prime x3
  7. L91
    specialize central_binom_le_of_no_bertrand_prime x4
  8. L92
    specialize central_binom_le_of_no_bertrand_prime x5
  9. L93
    apply central_binom_le_of_no_bertrand_prime
  10. L94
    exact hsearch_right
33Use earlier factsL95–100

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L95
    exact htwo_n
  2. L96
    exact hfloor_exists_witness
  3. L97
    exact hdivision_exists_witness_witness
  4. L98
    exact hcentral_exists_witness
  5. L99
    exact hpower_a_exists_witness
  6. L100
    exact hpower_b_exists_witness
34Establish hscaled_upperL101–106

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul left.

  1. L101
    have hscaled_upper : Le(n · x3,n · (x4 · x5))Definitions: Le(n · x3,n · (x4 · x5))Original native command in the exact edition
  2. L102
    specialize mul_le_mul_left x3
  3. L103
    specialize mul_le_mul_left (x4 * x5)
  4. L104
    specialize mul_le_mul_left n
  5. L105
    apply mul_le_mul_left
  6. L106
    exact hcentral_upper
35Establish hassociated_upperL107–112

Establish this local claim before using it. It is not an additional assumption.

  1. L107
    have hassociated_upper : Le(n · x3,n · x4 · x5)Definitions: Le(n · x3,n · x4 · x5)Original native command in the exact edition
  2. L108
    specialize mul_assoc n
  3. L109
    specialize mul_assoc x4
  4. L110
    specialize mul_assoc x5
  5. L111
    rewrite <- mul_assoc at hscaled_upper
  6. L112
    exact hscaled_upper
36Establish hmainL113–122

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand main inequality nat.

  1. L113
    have hmain : Le(n · x4 · x5,x6)Definitions: Le(n · x4 · x5,x6)Original native command in the exact edition
  2. L114
    specialize bertrand_main_inequality_nat n
  3. L115
    specialize bertrand_main_inequality_nat x
  4. L116
    specialize bertrand_main_inequality_nat x1
  5. L117
    specialize bertrand_main_inequality_nat x2
  6. L118
    specialize bertrand_main_inequality_nat x4
  7. L119
    specialize bertrand_main_inequality_nat x5
  8. L120
    specialize bertrand_main_inequality_nat x6
  9. L121
    apply bertrand_main_inequality_nat
  10. L122
    exact hthreshold
37Use earlier factsL123–127

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L123
    exact hfloor_exists_witness
  2. L124
    exact hdivision_exists_witness_witness
  3. L125
    exact hpower_a_exists_witness
  4. L126
    exact hpower_b_exists_witness
  5. L127
    exact hpower_f_exists_witness
38Establish hcontradiction_upperL128–137

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.

  1. L128
    have hcontradiction_upper : Le(n · x3,x6)Definitions: Le(n · x3,x6)Original native command in the exact edition
  2. L129
    specialize le_trans (n * x3)
  3. L130
    specialize le_trans (n * x4 * x5)
  4. L131
    specialize le_trans x6
  5. L132
    apply le_trans
  6. L133
    exact hassociated_upper
  7. L134
    exact hmain
  8. L135
    specialize lt_not_le x6
  9. L136
    specialize lt_not_le (n * x3)
  10. L137
    apply lt_not_le
39Use earlier factsL138–139

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L138
    exact hlower
  2. L139
    exact hcontradiction_upper

Library-wide reading audit

Original defined command ledger · 139 lines
  1. 0001intro n
  2. 0002intro hthreshold
  3. 0003have hsearch : (∃ x. Prime(x) ∧ (Lt(n,x) ∧ Le(x,n + n))) ∨ (∀ x. Lt(n,x) ∧ Le(x,n + n) → ¬Prime(x))
    Exact native replay linehave hsearch : (exists b7_prime. ((~(b7_prime = 1) /\ forall bpr_left_b7_result_prime bpr_right_b7_result_prime. b7_prime = bpr_left_b7_result_prime * bpr_right_b7_result_prime -> bpr_left_b7_result_prime = 1 \/ bpr_right_b7_result_prime = 1)) /\ ((exists bcf_lt_gap_b7_result_lower. bcf_lt_gap_b7_result_lower + S (n) = b7_prime) /\ (exists bcf_le_gap_b7_result_upper. bcf_le_gap_b7_result_upper + (b7_prime) = n + n))) \/ (forall bpr_prime_candidate_b7_exclusion. ((exists bpr_gap_b7_exclusion_lower. bpr_gap_b7_exclusion_lower + S (n) = bpr_prime_candidate_b7_exclusion) /\ (exists bpr_le_gap_b7_exclusion_upper. bpr_le_gap_b7_exclusion_upper + (bpr_prime_candidate_b7_exclusion) = (n + n))) -> ~((~(bpr_prime_candidate_b7_exclusion = 1) /\ forall bpr_left_b7_exclusion_prime bpr_right_b7_exclusion_prime. bpr_prime_candidate_b7_exclusion = bpr_left_b7_exclusion_prime * bpr_right_b7_exclusion_prime -> bpr_left_b7_exclusion_prime = 1 \/ bpr_right_b7_exclusion_prime = 1)))
  4. 0004specialize bounded_prime_interval_search n
  5. 0005specialize bounded_prime_interval_search (n + n)
  6. 0006exact bounded_prime_interval_search
  7. 0007cases hsearch
  8. 0008exact hsearch_left
  9. 0009exfalso
  10. 0010have hone_thirty_two : Lt(0,32)
    Exact native replay linehave hone_thirty_two : exists bcf_le_gap_b7_one_thirty_two. bcf_le_gap_b7_one_thirty_two + (1) = 32
  11. 0011exists 31
  12. 0012norm_num
  13. 0013have hsixteen_threshold : Lt(15,16 · 32)
    Exact native replay linehave hsixteen_threshold : exists bcf_le_gap_b7_sixteen_threshold. bcf_le_gap_b7_sixteen_threshold + (16) = 16 * 32
  14. 0014specialize le_mul_of_one_le_right 16
  15. 0015specialize le_mul_of_one_le_right 32
  16. 0016apply le_mul_of_one_le_right
  17. 0017exact hone_thirty_two
  18. 0018have hfour_sixteen : Lt(3,16)
    Exact native replay linehave hfour_sixteen : exists bcf_le_gap_b7_four_sixteen. bcf_le_gap_b7_four_sixteen + (4) = 16
  19. 0019exists 12
  20. 0020norm_num
  21. 0021have hfour_threshold : Lt(3,16 · 32)
    Exact native replay linehave hfour_threshold : exists bcf_le_gap_b7_four_threshold. bcf_le_gap_b7_four_threshold + (4) = 16 * 32
  22. 0022specialize le_trans 4
  23. 0023specialize le_trans 16
  24. 0024specialize le_trans (16 * 32)
  25. 0025apply le_trans
  26. 0026exact hfour_sixteen
  27. 0027exact hsixteen_threshold
  28. 0028have hfour_n : Lt(3,n)
    Exact native replay linehave hfour_n : exists bcf_le_gap_b7_four_n. bcf_le_gap_b7_four_n + (4) = n
  29. 0029specialize le_trans 4
  30. 0030specialize le_trans (16 * 32)
  31. 0031specialize le_trans n
  32. 0032apply le_trans
  33. 0033exact hfour_threshold
  34. 0034exact hthreshold
  35. 0035have htwo_four : Lt(2,4)
    Exact native replay linehave htwo_four : exists bcf_lt_gap_b7_two_four. bcf_lt_gap_b7_two_four + S (2) = 4
  36. 0036exists 1
  37. 0037norm_num
  38. 0038have htwo_n : Lt(2,n)
    Exact native replay linehave htwo_n : exists bcf_lt_gap_b7_two_n. bcf_lt_gap_b7_two_n + S (2) = n
  39. 0039specialize lt_of_lt_of_le 2
  40. 0040specialize lt_of_lt_of_le 4
  41. 0041specialize lt_of_lt_of_le n
  42. 0042apply lt_of_lt_of_le
  43. 0043exact htwo_four
  44. 0044exact hfour_n
  45. 0045have hfloor_exists : ∃ s. FloorSqrt(n + n,s)
    Exact native replay linehave hfloor_exists : exists s. (((exists bcs_sqrt_lower_gap_b7_floor. bcs_sqrt_lower_gap_b7_floor + (s) * (s) = (n + n)) /\ exists bcs_sqrt_upper_gap_b7_floor. bcs_sqrt_upper_gap_b7_floor + S (n + n) = S (s) * S (s)))
  46. 0046specialize floor_sqrt_total (n + n)
  47. 0047exact floor_sqrt_total
  48. 0048cases hfloor_exists
  49. 0049have hdivision_exists : ∃ q. ∃ r. DivRem(n + n,3,q,r)
    Exact native replay linehave hdivision_exists : exists q r. (((n + n) = (3) * (q) + (r) /\ (exists bcf_lt_gap_b7_division_bound. bcf_lt_gap_b7_division_bound + S (r) = 3)))
  50. 0050specialize division_remainder_exists 3
  51. 0051specialize division_remainder_exists (n + n)
  52. 0052apply division_remainder_exists
  53. 0053intro hthree_zero
  54. 0054apply PA1
  55. 0055exact hthree_zero
  56. 0056cases hdivision_exists
  57. 0057cases hdivision_exists_witness
  58. 0058have hcentral_exists : ∃ C. CentralBinom(n,C)
    Exact native replay linehave hcentral_exists : exists C. (((exists bcf_lt_gap_b7_central_out_of_range. bcf_lt_gap_b7_central_out_of_range + S (n + n) = n) /\ C = 0) \/ ((exists bcf_le_gap_b7_central_in_range. bcf_le_gap_b7_central_in_range + (n) = n + n) /\ (exists bcf_row_code_code_b7_central bcf_row_code_scale_b7_central bcf_row_scale_code_b7_central bcf_row_scale_scale_b7_central bcf_row_code_b7_central bcf_row_scale_b7_central. ((forall bcf_row_index_b7_central_table. (exists bcf_lt_gap_b7_central_table_row_bound. bcf_lt_gap_b7_central_table_row_bound + S (bcf_row_index_b7_central_table) = S (n + n)) -> exists bcf_row_code_b7_central_table bcf_row_scale_b7_central_table. ((((exists bcf_height_b7_central_table_decoded_row_code. bcf_height_b7_central_table_decoded_row_code + S (bcf_row_code_b7_central_table) = S ((S (bcf_row_index_b7_central_table)) * bcf_row_code_scale_b7_central)) /\ exists bcf_quotient_b7_central_table_decoded_row_code. bcf_row_code_code_b7_central = bcf_quotient_b7_central_table_decoded_row_code * S ((S (bcf_row_index_b7_central_table)) * bcf_row_code_scale_b7_central) + (bcf_row_code_b7_central_table))) /\ ((((exists bcf_height_b7_central_table_decoded_row_scale. bcf_height_b7_central_table_decoded_row_scale + S (bcf_row_scale_b7_central_table) = S ((S (bcf_row_index_b7_central_table)) * bcf_row_scale_scale_b7_central)) /\ exists bcf_quotient_b7_central_table_decoded_row_scale. bcf_row_scale_code_b7_central = bcf_quotient_b7_central_table_decoded_row_scale * S ((S (bcf_row_index_b7_central_table)) * bcf_row_scale_scale_b7_central) + (bcf_row_scale_b7_central_table))) /\ ((bcf_row_index_b7_central_table = 0 /\ (forall bcf_index_b7_central_table_zero_row. (exists bcf_lt_gap_b7_central_table_zero_row_bound. bcf_lt_gap_b7_central_table_zero_row_bound + S (bcf_index_b7_central_table_zero_row) = S (n + n)) -> exists bcf_value_b7_central_table_zero_row. ((((exists bcf_height_b7_central_table_zero_row_entry. bcf_height_b7_central_table_zero_row_entry + S (bcf_value_b7_central_table_zero_row) = S ((S (bcf_index_b7_central_table_zero_row)) * bcf_row_scale_b7_central_table)) /\ exists bcf_quotient_b7_central_table_zero_row_entry. bcf_row_code_b7_central_table = bcf_quotient_b7_central_table_zero_row_entry * S ((S (bcf_index_b7_central_table_zero_row)) * bcf_row_scale_b7_central_table) + (bcf_value_b7_central_table_zero_row))) /\ ((bcf_index_b7_central_table_zero_row = 0 /\ bcf_value_b7_central_table_zero_row = 1) \/ exists bcf_predecessor_b7_central_table_zero_row. bcf_index_b7_central_table_zero_row = S bcf_predecessor_b7_central_table_zero_row /\ bcf_value_b7_central_table_zero_row = 0)))) \/ exists bcf_predecessor_b7_central_table bcf_previous_code_b7_central_table bcf_previous_scale_b7_central_table. bcf_row_index_b7_central_table = S bcf_predecessor_b7_central_table /\ ((((exists bcf_height_b7_central_table_decoded_previous_code. bcf_height_b7_central_table_decoded_previous_code + S (bcf_previous_code_b7_central_table) = S ((S (bcf_predecessor_b7_central_table)) * bcf_row_code_scale_b7_central)) /\ exists bcf_quotient_b7_central_table_decoded_previous_code. bcf_row_code_code_b7_central = bcf_quotient_b7_central_table_decoded_previous_code * S ((S (bcf_predecessor_b7_central_table)) * bcf_row_code_scale_b7_central) + (bcf_previous_code_b7_central_table))) /\ ((((exists bcf_height_b7_central_table_decoded_previous_scale. bcf_height_b7_central_table_decoded_previous_scale + S (bcf_previous_scale_b7_central_table) = S ((S (bcf_predecessor_b7_central_table)) * bcf_row_scale_scale_b7_central)) /\ exists bcf_quotient_b7_central_table_decoded_previous_scale. bcf_row_scale_code_b7_central = bcf_quotient_b7_central_table_decoded_previous_scale * S ((S (bcf_predecessor_b7_central_table)) * bcf_row_scale_scale_b7_central) + (bcf_previous_scale_b7_central_table))) /\ (forall bcf_index_b7_central_table_row_step. (exists bcf_lt_gap_b7_central_table_row_step_bound. bcf_lt_gap_b7_central_table_row_step_bound + S (bcf_index_b7_central_table_row_step) = S (n + n)) -> exists bcf_value_b7_central_table_row_step. ((((exists bcf_height_b7_central_table_row_step_entry. bcf_height_b7_central_table_row_step_entry + S (bcf_value_b7_central_table_row_step) = S ((S (bcf_index_b7_central_table_row_step)) * bcf_row_scale_b7_central_table)) /\ exists bcf_quotient_b7_central_table_row_step_entry. bcf_row_code_b7_central_table = bcf_quotient_b7_central_table_row_step_entry * S ((S (bcf_index_b7_central_table_row_step)) * bcf_row_scale_b7_central_table) + (bcf_value_b7_central_table_row_step))) /\ ((bcf_index_b7_central_table_row_step = 0 /\ bcf_value_b7_central_table_row_step = 1) \/ exists bcf_predecessor_b7_central_table_row_step bcf_left_b7_central_table_row_step bcf_right_b7_central_table_row_step. bcf_index_b7_central_table_row_step = S bcf_predecessor_b7_central_table_row_step /\ ((((exists bcf_height_b7_central_table_row_step_previous_left. bcf_height_b7_central_table_row_step_previous_left + S (bcf_left_b7_central_table_row_step) = S ((S (bcf_predecessor_b7_central_table_row_step)) * bcf_previous_scale_b7_central_table)) /\ exists bcf_quotient_b7_central_table_row_step_previous_left. bcf_previous_code_b7_central_table = bcf_quotient_b7_central_table_row_step_previous_left * S ((S (bcf_predecessor_b7_central_table_row_step)) * bcf_previous_scale_b7_central_table) + (bcf_left_b7_central_table_row_step))) /\ ((((exists bcf_height_b7_central_table_row_step_previous_right. bcf_height_b7_central_table_row_step_previous_right + S (bcf_right_b7_central_table_row_step) = S ((S (S (bcf_predecessor_b7_central_table_row_step))) * bcf_previous_scale_b7_central_table)) /\ exists bcf_quotient_b7_central_table_row_step_previous_right. bcf_previous_code_b7_central_table = bcf_quotient_b7_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_b7_central_table_row_step))) * bcf_previous_scale_b7_central_table) + (bcf_right_b7_central_table_row_step))) /\ bcf_value_b7_central_table_row_step = bcf_left_b7_central_table_row_step + bcf_right_b7_central_table_row_step))))))))))) /\ ((((exists bcf_height_b7_central_decoded_row_code. bcf_height_b7_central_decoded_row_code + S (bcf_row_code_b7_central) = S ((S (n + n)) * bcf_row_code_scale_b7_central)) /\ exists bcf_quotient_b7_central_decoded_row_code. bcf_row_code_code_b7_central = bcf_quotient_b7_central_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_b7_central) + (bcf_row_code_b7_central))) /\ ((((exists bcf_height_b7_central_decoded_row_scale. bcf_height_b7_central_decoded_row_scale + S (bcf_row_scale_b7_central) = S ((S (n + n)) * bcf_row_scale_scale_b7_central)) /\ exists bcf_quotient_b7_central_decoded_row_scale. bcf_row_scale_code_b7_central = bcf_quotient_b7_central_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_b7_central) + (bcf_row_scale_b7_central))) /\ (((exists bcf_height_b7_central_decoded_value. bcf_height_b7_central_decoded_value + S (C) = S ((S (n)) * bcf_row_scale_b7_central)) /\ exists bcf_quotient_b7_central_decoded_value. bcf_row_code_b7_central = bcf_quotient_b7_central_decoded_value * S ((S (n)) * bcf_row_scale_b7_central) + (C)))))))))
  59. 0059specialize central_binom_exists n
  60. 0060exact central_binom_exists
  61. 0061cases hcentral_exists
  62. 0062have hpower_a_exists : ∃ A. Pow(n + n,x,A)
    Exact native replay linehave hpower_a_exists : exists A. (exists pa_b_b7_power_a pa_c_b7_power_a. ((forall pa_i_b7_power_a_repeat. (exists pa_lt_b7_power_a_repeat_bound. pa_lt_b7_power_a_repeat_bound + S pa_i_b7_power_a_repeat = x) -> (((exists pa_h_b7_power_a_repeat_decoded. pa_h_b7_power_a_repeat_decoded + S (n + n) = S ((S (pa_i_b7_power_a_repeat)) * pa_c_b7_power_a)) /\ exists pa_q_b7_power_a_repeat_decoded. pa_b_b7_power_a = pa_q_b7_power_a_repeat_decoded * S ((S (pa_i_b7_power_a_repeat)) * pa_c_b7_power_a) + (n + n)))) /\ (exists pa_u_b7_power_a_product pa_v_b7_power_a_product. ((((exists pa_h_b7_power_a_product_start. pa_h_b7_power_a_product_start + S (1) = S ((S (0)) * pa_v_b7_power_a_product)) /\ exists pa_q_b7_power_a_product_start. pa_u_b7_power_a_product = pa_q_b7_power_a_product_start * S ((S (0)) * pa_v_b7_power_a_product) + (1))) /\ ((((exists pa_h_b7_power_a_product_terminal. pa_h_b7_power_a_product_terminal + S (A) = S ((S (x)) * pa_v_b7_power_a_product)) /\ exists pa_q_b7_power_a_product_terminal. pa_u_b7_power_a_product = pa_q_b7_power_a_product_terminal * S ((S (x)) * pa_v_b7_power_a_product) + (A))) /\ forall pa_i_b7_power_a_product. (exists pa_lt_b7_power_a_product_bound. pa_lt_b7_power_a_product_bound + S pa_i_b7_power_a_product = x) -> exists pa_p_b7_power_a_product pa_r_b7_power_a_product pa_s_b7_power_a_product. ((((exists pa_h_b7_power_a_product_factor. pa_h_b7_power_a_product_factor + S (pa_p_b7_power_a_product) = S ((S (pa_i_b7_power_a_product)) * pa_c_b7_power_a)) /\ exists pa_q_b7_power_a_product_factor. pa_b_b7_power_a = pa_q_b7_power_a_product_factor * S ((S (pa_i_b7_power_a_product)) * pa_c_b7_power_a) + (pa_p_b7_power_a_product))) /\ ((((exists pa_h_b7_power_a_product_partial. pa_h_b7_power_a_product_partial + S (pa_r_b7_power_a_product) = S ((S (pa_i_b7_power_a_product)) * pa_v_b7_power_a_product)) /\ exists pa_q_b7_power_a_product_partial. pa_u_b7_power_a_product = pa_q_b7_power_a_product_partial * S ((S (pa_i_b7_power_a_product)) * pa_v_b7_power_a_product) + (pa_r_b7_power_a_product))) /\ ((((exists pa_h_b7_power_a_product_successor. pa_h_b7_power_a_product_successor + S (pa_s_b7_power_a_product) = S ((S (S pa_i_b7_power_a_product)) * pa_v_b7_power_a_product)) /\ exists pa_q_b7_power_a_product_successor. pa_u_b7_power_a_product = pa_q_b7_power_a_product_successor * S ((S (S pa_i_b7_power_a_product)) * pa_v_b7_power_a_product) + (pa_s_b7_power_a_product))) /\ pa_s_b7_power_a_product = pa_r_b7_power_a_product * pa_p_b7_power_a_product))))))))
  63. 0063specialize pow_exists (n + n)
  64. 0064specialize pow_exists x
  65. 0065exact pow_exists
  66. 0066cases hpower_a_exists
  67. 0067have hpower_b_exists : ∃ B. Pow(4,x1,B)
    Exact native replay linehave hpower_b_exists : exists B. (exists pa_b_b7_power_b pa_c_b7_power_b. ((forall pa_i_b7_power_b_repeat. (exists pa_lt_b7_power_b_repeat_bound. pa_lt_b7_power_b_repeat_bound + S pa_i_b7_power_b_repeat = x1) -> (((exists pa_h_b7_power_b_repeat_decoded. pa_h_b7_power_b_repeat_decoded + S (4) = S ((S (pa_i_b7_power_b_repeat)) * pa_c_b7_power_b)) /\ exists pa_q_b7_power_b_repeat_decoded. pa_b_b7_power_b = pa_q_b7_power_b_repeat_decoded * S ((S (pa_i_b7_power_b_repeat)) * pa_c_b7_power_b) + (4)))) /\ (exists pa_u_b7_power_b_product pa_v_b7_power_b_product. ((((exists pa_h_b7_power_b_product_start. pa_h_b7_power_b_product_start + S (1) = S ((S (0)) * pa_v_b7_power_b_product)) /\ exists pa_q_b7_power_b_product_start. pa_u_b7_power_b_product = pa_q_b7_power_b_product_start * S ((S (0)) * pa_v_b7_power_b_product) + (1))) /\ ((((exists pa_h_b7_power_b_product_terminal. pa_h_b7_power_b_product_terminal + S (B) = S ((S (x1)) * pa_v_b7_power_b_product)) /\ exists pa_q_b7_power_b_product_terminal. pa_u_b7_power_b_product = pa_q_b7_power_b_product_terminal * S ((S (x1)) * pa_v_b7_power_b_product) + (B))) /\ forall pa_i_b7_power_b_product. (exists pa_lt_b7_power_b_product_bound. pa_lt_b7_power_b_product_bound + S pa_i_b7_power_b_product = x1) -> exists pa_p_b7_power_b_product pa_r_b7_power_b_product pa_s_b7_power_b_product. ((((exists pa_h_b7_power_b_product_factor. pa_h_b7_power_b_product_factor + S (pa_p_b7_power_b_product) = S ((S (pa_i_b7_power_b_product)) * pa_c_b7_power_b)) /\ exists pa_q_b7_power_b_product_factor. pa_b_b7_power_b = pa_q_b7_power_b_product_factor * S ((S (pa_i_b7_power_b_product)) * pa_c_b7_power_b) + (pa_p_b7_power_b_product))) /\ ((((exists pa_h_b7_power_b_product_partial. pa_h_b7_power_b_product_partial + S (pa_r_b7_power_b_product) = S ((S (pa_i_b7_power_b_product)) * pa_v_b7_power_b_product)) /\ exists pa_q_b7_power_b_product_partial. pa_u_b7_power_b_product = pa_q_b7_power_b_product_partial * S ((S (pa_i_b7_power_b_product)) * pa_v_b7_power_b_product) + (pa_r_b7_power_b_product))) /\ ((((exists pa_h_b7_power_b_product_successor. pa_h_b7_power_b_product_successor + S (pa_s_b7_power_b_product) = S ((S (S pa_i_b7_power_b_product)) * pa_v_b7_power_b_product)) /\ exists pa_q_b7_power_b_product_successor. pa_u_b7_power_b_product = pa_q_b7_power_b_product_successor * S ((S (S pa_i_b7_power_b_product)) * pa_v_b7_power_b_product) + (pa_s_b7_power_b_product))) /\ pa_s_b7_power_b_product = pa_r_b7_power_b_product * pa_p_b7_power_b_product))))))))
  68. 0068specialize pow_exists 4
  69. 0069specialize pow_exists x1
  70. 0070exact pow_exists
  71. 0071cases hpower_b_exists
  72. 0072have hpower_f_exists : ∃ F. Pow(4,n,F)
    Exact native replay linehave hpower_f_exists : exists F. (exists pa_b_b7_power_f pa_c_b7_power_f. ((forall pa_i_b7_power_f_repeat. (exists pa_lt_b7_power_f_repeat_bound. pa_lt_b7_power_f_repeat_bound + S pa_i_b7_power_f_repeat = n) -> (((exists pa_h_b7_power_f_repeat_decoded. pa_h_b7_power_f_repeat_decoded + S (4) = S ((S (pa_i_b7_power_f_repeat)) * pa_c_b7_power_f)) /\ exists pa_q_b7_power_f_repeat_decoded. pa_b_b7_power_f = pa_q_b7_power_f_repeat_decoded * S ((S (pa_i_b7_power_f_repeat)) * pa_c_b7_power_f) + (4)))) /\ (exists pa_u_b7_power_f_product pa_v_b7_power_f_product. ((((exists pa_h_b7_power_f_product_start. pa_h_b7_power_f_product_start + S (1) = S ((S (0)) * pa_v_b7_power_f_product)) /\ exists pa_q_b7_power_f_product_start. pa_u_b7_power_f_product = pa_q_b7_power_f_product_start * S ((S (0)) * pa_v_b7_power_f_product) + (1))) /\ ((((exists pa_h_b7_power_f_product_terminal. pa_h_b7_power_f_product_terminal + S (F) = S ((S (n)) * pa_v_b7_power_f_product)) /\ exists pa_q_b7_power_f_product_terminal. pa_u_b7_power_f_product = pa_q_b7_power_f_product_terminal * S ((S (n)) * pa_v_b7_power_f_product) + (F))) /\ forall pa_i_b7_power_f_product. (exists pa_lt_b7_power_f_product_bound. pa_lt_b7_power_f_product_bound + S pa_i_b7_power_f_product = n) -> exists pa_p_b7_power_f_product pa_r_b7_power_f_product pa_s_b7_power_f_product. ((((exists pa_h_b7_power_f_product_factor. pa_h_b7_power_f_product_factor + S (pa_p_b7_power_f_product) = S ((S (pa_i_b7_power_f_product)) * pa_c_b7_power_f)) /\ exists pa_q_b7_power_f_product_factor. pa_b_b7_power_f = pa_q_b7_power_f_product_factor * S ((S (pa_i_b7_power_f_product)) * pa_c_b7_power_f) + (pa_p_b7_power_f_product))) /\ ((((exists pa_h_b7_power_f_product_partial. pa_h_b7_power_f_product_partial + S (pa_r_b7_power_f_product) = S ((S (pa_i_b7_power_f_product)) * pa_v_b7_power_f_product)) /\ exists pa_q_b7_power_f_product_partial. pa_u_b7_power_f_product = pa_q_b7_power_f_product_partial * S ((S (pa_i_b7_power_f_product)) * pa_v_b7_power_f_product) + (pa_r_b7_power_f_product))) /\ ((((exists pa_h_b7_power_f_product_successor. pa_h_b7_power_f_product_successor + S (pa_s_b7_power_f_product) = S ((S (S pa_i_b7_power_f_product)) * pa_v_b7_power_f_product)) /\ exists pa_q_b7_power_f_product_successor. pa_u_b7_power_f_product = pa_q_b7_power_f_product_successor * S ((S (S pa_i_b7_power_f_product)) * pa_v_b7_power_f_product) + (pa_s_b7_power_f_product))) /\ pa_s_b7_power_f_product = pa_r_b7_power_f_product * pa_p_b7_power_f_product))))))))
  73. 0073specialize pow_exists 4
  74. 0074specialize pow_exists n
  75. 0075exact pow_exists
  76. 0076cases hpower_f_exists
  77. 0077have hlower : Lt(x6,n · x3)
    Exact native replay linehave hlower : exists bcf_lt_gap_b7_lower. bcf_lt_gap_b7_lower + S (x6) = n * x3
  78. 0078specialize four_pow_lt_mul_central_binom n
  79. 0079specialize four_pow_lt_mul_central_binom x6
  80. 0080specialize four_pow_lt_mul_central_binom x3
  81. 0081apply four_pow_lt_mul_central_binom
  82. 0082exact hfour_n
  83. 0083exact hpower_f_exists_witness
  84. 0084exact hcentral_exists_witness
  85. 0085have hcentral_upper : Le(x3,x4 · x5)
    Exact native replay linehave hcentral_upper : exists bcf_le_gap_b7_central_upper. bcf_le_gap_b7_central_upper + (x3) = x4 * x5
  86. 0086specialize central_binom_le_of_no_bertrand_prime n
  87. 0087specialize central_binom_le_of_no_bertrand_prime x
  88. 0088specialize central_binom_le_of_no_bertrand_prime x1
  89. 0089specialize central_binom_le_of_no_bertrand_prime x2
  90. 0090specialize central_binom_le_of_no_bertrand_prime x3
  91. 0091specialize central_binom_le_of_no_bertrand_prime x4
  92. 0092specialize central_binom_le_of_no_bertrand_prime x5
  93. 0093apply central_binom_le_of_no_bertrand_prime
  94. 0094exact hsearch_right
  95. 0095exact htwo_n
  96. 0096exact hfloor_exists_witness
  97. 0097exact hdivision_exists_witness_witness
  98. 0098exact hcentral_exists_witness
  99. 0099exact hpower_a_exists_witness
  100. 0100exact hpower_b_exists_witness
  101. 0101have hscaled_upper : Le(n · x3,n · (x4 · x5))
    Exact native replay linehave hscaled_upper : exists bcf_le_gap_b7_scaled_upper. bcf_le_gap_b7_scaled_upper + (n * x3) = n * (x4 * x5)
  102. 0102specialize mul_le_mul_left x3
  103. 0103specialize mul_le_mul_left (x4 * x5)
  104. 0104specialize mul_le_mul_left n
  105. 0105apply mul_le_mul_left
  106. 0106exact hcentral_upper
  107. 0107have hassociated_upper : Le(n · x3,n · x4 · x5)
    Exact native replay linehave hassociated_upper : exists bcf_le_gap_b7_associated_upper. bcf_le_gap_b7_associated_upper + (n * x3) = n * x4 * x5
  108. 0108specialize mul_assoc n
  109. 0109specialize mul_assoc x4
  110. 0110specialize mul_assoc x5
  111. 0111rewrite <- mul_assoc at hscaled_upper
  112. 0112exact hscaled_upper
  113. 0113have hmain : Le(n · x4 · x5,x6)
    Exact native replay linehave hmain : exists bcf_le_gap_b7_main. bcf_le_gap_b7_main + (n * x4 * x5) = x6
  114. 0114specialize bertrand_main_inequality_nat n
  115. 0115specialize bertrand_main_inequality_nat x
  116. 0116specialize bertrand_main_inequality_nat x1
  117. 0117specialize bertrand_main_inequality_nat x2
  118. 0118specialize bertrand_main_inequality_nat x4
  119. 0119specialize bertrand_main_inequality_nat x5
  120. 0120specialize bertrand_main_inequality_nat x6
  121. 0121apply bertrand_main_inequality_nat
  122. 0122exact hthreshold
  123. 0123exact hfloor_exists_witness
  124. 0124exact hdivision_exists_witness_witness
  125. 0125exact hpower_a_exists_witness
  126. 0126exact hpower_b_exists_witness
  127. 0127exact hpower_f_exists_witness
  128. 0128have hcontradiction_upper : Le(n · x3,x6)
    Exact native replay linehave hcontradiction_upper : exists bcf_le_gap_b7_contradiction_upper. bcf_le_gap_b7_contradiction_upper + (n * x3) = x6
  129. 0129specialize le_trans (n * x3)
  130. 0130specialize le_trans (n * x4 * x5)
  131. 0131specialize le_trans x6
  132. 0132apply le_trans
  133. 0133exact hassociated_upper
  134. 0134exact hmain
  135. 0135specialize lt_not_le x6
  136. 0136specialize lt_not_le (n * x3)
  137. 0137apply lt_not_le
  138. 0138exact hlower
  139. 0139exact hcontradiction_upper