bertrand_eventually_closed_upper

Proof neighborhood

Direct dependencies

Direct dependents

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 hthreshold
3. 0003have 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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