BP0004

bertrand_window_central_valuation_nonzero

A Bertrand-window prime divides the positive central coefficient nontrivially.

Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not Stable

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.

Exact theorem in conservative defined notation

∀ n. ∀ p. ∀ C. ∀ e. Prime(p) → Lt(n,p) → Lt(p,n + n) → Lt(n + n,n) ∧ C = 0 ∨ Le(n,n + n) ∧ (∃ x. ∃ y. ∃ z. ∃ m. ∃ k. ∃ i. (∀ j. Lt(j,S (n + n)) → ∃ u. ∃ v. Beta(x,y,j,u) ∧ (Beta(z,m,j,v) ∧ (j = 0 ∧ (∀ w. Lt(w,S (n + n)) → ∃ x0. Beta(u,v,w,x0) ∧ (w = 0 ∧ x0 = 1 ∨ (∃ x1. w = S x1 ∧ x0 = 0))) ∨ (∃ w. ∃ x0. ∃ x1. j = S w ∧ (Beta(x,y,w,x0) ∧ (Beta(z,m,w,x1) ∧ (∀ x2. Lt(x2,S (n + n)) → ∃ x3. Beta(u,v,x2,x3) ∧ (x2 = 0 ∧ x3 = 1 ∨ (∃ x4. ∃ x5. ∃ x6. x2 = S x4 ∧ (Beta(x0,x1,x4,x5) ∧ (Beta(x0,x1,S x4,x6) ∧ x3 = x5 + x6))))))))))) ∧ (Beta(x,y,n + n,k) ∧ (Beta(z,m,n + n,i) ∧ Beta(k,i,n,C)))) → BoundedPowerValuation(p,C,C,e) → ¬e = 0

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Beta(b,c,i,x) · 11Le(a,b) · 1Lt(a,b) · 6Prime(p) · 1BoundedPowerValuation(p,n,b,e) · 1

Actual proof prerequisites

central_binom_positive · checked external prerequisitebertrand_window_prime_divides_central_binomprime_divisor_power_valuation_nonzero · checked external prerequisite
Original expanded first-order statement 
forall n p C e. ((~(p = 1) /\ forall frm_prime_left_bpc_prime frm_prime_right_bpc_prime. p = frm_prime_left_bpc_prime * frm_prime_right_bpc_prime -> frm_prime_left_bpc_prime = 1 \/ frm_prime_right_bpc_prime = 1)) -> (exists bcf_lt_gap_bpc_lower. bcf_lt_gap_bpc_lower + S (n) = p) -> (exists bcf_lt_gap_bpc_upper. bcf_lt_gap_bpc_upper + S (p) = n + n) -> (((exists bcf_lt_gap_bpc_central_out_of_range. bcf_lt_gap_bpc_central_out_of_range + S (n + n) = n) /\ C = 0) \/ ((exists bcf_le_gap_bpc_central_in_range. bcf_le_gap_bpc_central_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bpc_central bcf_row_code_scale_bpc_central bcf_row_scale_code_bpc_central bcf_row_scale_scale_bpc_central bcf_row_code_bpc_central bcf_row_scale_bpc_central. ((forall bcf_row_index_bpc_central_table. (exists bcf_lt_gap_bpc_central_table_row_bound. bcf_lt_gap_bpc_central_table_row_bound + S (bcf_row_index_bpc_central_table) = S (n + n)) -> exists bcf_row_code_bpc_central_table bcf_row_scale_bpc_central_table. ((((exists bcf_height_bpc_central_table_decoded_row_code. bcf_height_bpc_central_table_decoded_row_code + S (bcf_row_code_bpc_central_table) = S ((S (bcf_row_index_bpc_central_table)) * bcf_row_code_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_row_code. bcf_row_code_code_bpc_central = bcf_quotient_bpc_central_table_decoded_row_code * S ((S (bcf_row_index_bpc_central_table)) * bcf_row_code_scale_bpc_central) + (bcf_row_code_bpc_central_table))) /\ ((((exists bcf_height_bpc_central_table_decoded_row_scale. bcf_height_bpc_central_table_decoded_row_scale + S (bcf_row_scale_bpc_central_table) = S ((S (bcf_row_index_bpc_central_table)) * bcf_row_scale_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_row_scale. bcf_row_scale_code_bpc_central = bcf_quotient_bpc_central_table_decoded_row_scale * S ((S (bcf_row_index_bpc_central_table)) * bcf_row_scale_scale_bpc_central) + (bcf_row_scale_bpc_central_table))) /\ ((bcf_row_index_bpc_central_table = 0 /\ (forall bcf_index_bpc_central_table_zero_row. (exists bcf_lt_gap_bpc_central_table_zero_row_bound. bcf_lt_gap_bpc_central_table_zero_row_bound + S (bcf_index_bpc_central_table_zero_row) = S (n + n)) -> exists bcf_value_bpc_central_table_zero_row. ((((exists bcf_height_bpc_central_table_zero_row_entry. bcf_height_bpc_central_table_zero_row_entry + S (bcf_value_bpc_central_table_zero_row) = S ((S (bcf_index_bpc_central_table_zero_row)) * bcf_row_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_zero_row_entry. bcf_row_code_bpc_central_table = bcf_quotient_bpc_central_table_zero_row_entry * S ((S (bcf_index_bpc_central_table_zero_row)) * bcf_row_scale_bpc_central_table) + (bcf_value_bpc_central_table_zero_row))) /\ ((bcf_index_bpc_central_table_zero_row = 0 /\ bcf_value_bpc_central_table_zero_row = 1) \/ exists bcf_predecessor_bpc_central_table_zero_row. bcf_index_bpc_central_table_zero_row = S bcf_predecessor_bpc_central_table_zero_row /\ bcf_value_bpc_central_table_zero_row = 0)))) \/ exists bcf_predecessor_bpc_central_table bcf_previous_code_bpc_central_table bcf_previous_scale_bpc_central_table. bcf_row_index_bpc_central_table = S bcf_predecessor_bpc_central_table /\ ((((exists bcf_height_bpc_central_table_decoded_previous_code. bcf_height_bpc_central_table_decoded_previous_code + S (bcf_previous_code_bpc_central_table) = S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_code_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_previous_code. bcf_row_code_code_bpc_central = bcf_quotient_bpc_central_table_decoded_previous_code * S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_code_scale_bpc_central) + (bcf_previous_code_bpc_central_table))) /\ ((((exists bcf_height_bpc_central_table_decoded_previous_scale. bcf_height_bpc_central_table_decoded_previous_scale + S (bcf_previous_scale_bpc_central_table) = S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_scale_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_previous_scale. bcf_row_scale_code_bpc_central = bcf_quotient_bpc_central_table_decoded_previous_scale * S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_scale_scale_bpc_central) + (bcf_previous_scale_bpc_central_table))) /\ (forall bcf_index_bpc_central_table_row_step. (exists bcf_lt_gap_bpc_central_table_row_step_bound. bcf_lt_gap_bpc_central_table_row_step_bound + S (bcf_index_bpc_central_table_row_step) = S (n + n)) -> exists bcf_value_bpc_central_table_row_step. ((((exists bcf_height_bpc_central_table_row_step_entry. bcf_height_bpc_central_table_row_step_entry + S (bcf_value_bpc_central_table_row_step) = S ((S (bcf_index_bpc_central_table_row_step)) * bcf_row_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_row_step_entry. bcf_row_code_bpc_central_table = bcf_quotient_bpc_central_table_row_step_entry * S ((S (bcf_index_bpc_central_table_row_step)) * bcf_row_scale_bpc_central_table) + (bcf_value_bpc_central_table_row_step))) /\ ((bcf_index_bpc_central_table_row_step = 0 /\ bcf_value_bpc_central_table_row_step = 1) \/ exists bcf_predecessor_bpc_central_table_row_step bcf_left_bpc_central_table_row_step bcf_right_bpc_central_table_row_step. bcf_index_bpc_central_table_row_step = S bcf_predecessor_bpc_central_table_row_step /\ ((((exists bcf_height_bpc_central_table_row_step_previous_left. bcf_height_bpc_central_table_row_step_previous_left + S (bcf_left_bpc_central_table_row_step) = S ((S (bcf_predecessor_bpc_central_table_row_step)) * bcf_previous_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_row_step_previous_left. bcf_previous_code_bpc_central_table = bcf_quotient_bpc_central_table_row_step_previous_left * S ((S (bcf_predecessor_bpc_central_table_row_step)) * bcf_previous_scale_bpc_central_table) + (bcf_left_bpc_central_table_row_step))) /\ ((((exists bcf_height_bpc_central_table_row_step_previous_right. bcf_height_bpc_central_table_row_step_previous_right + S (bcf_right_bpc_central_table_row_step) = S ((S (S (bcf_predecessor_bpc_central_table_row_step))) * bcf_previous_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_row_step_previous_right. bcf_previous_code_bpc_central_table = bcf_quotient_bpc_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_bpc_central_table_row_step))) * bcf_previous_scale_bpc_central_table) + (bcf_right_bpc_central_table_row_step))) /\ bcf_value_bpc_central_table_row_step = bcf_left_bpc_central_table_row_step + bcf_right_bpc_central_table_row_step))))))))))) /\ ((((exists bcf_height_bpc_central_decoded_row_code. bcf_height_bpc_central_decoded_row_code + S (bcf_row_code_bpc_central) = S ((S (n + n)) * bcf_row_code_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_decoded_row_code. bcf_row_code_code_bpc_central = bcf_quotient_bpc_central_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bpc_central) + (bcf_row_code_bpc_central))) /\ ((((exists bcf_height_bpc_central_decoded_row_scale. bcf_height_bpc_central_decoded_row_scale + S (bcf_row_scale_bpc_central) = S ((S (n + n)) * bcf_row_scale_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_decoded_row_scale. bcf_row_scale_code_bpc_central = bcf_quotient_bpc_central_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bpc_central) + (bcf_row_scale_bpc_central))) /\ (((exists bcf_height_bpc_central_decoded_value. bcf_height_bpc_central_decoded_value + S (C) = S ((S (n)) * bcf_row_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_decoded_value. bcf_row_code_bpc_central = bcf_quotient_bpc_central_decoded_value * S ((S (n)) * bcf_row_scale_bpc_central) + (C))))))))) -> (((exists bpv_gap_bpc_value_exponent_bound. bpv_gap_bpc_value_exponent_bound + e = C) /\ (exists bpv_result_bpc_value_selected. ((exists ff_b_bpc_value_selected_power ff_c_bpc_value_selected_power. ((forall ff_i_bpc_value_selected_power_repeat. (exists ff_lt_bpc_value_selected_power_repeat_bound. ff_lt_bpc_value_selected_power_repeat_bound + S ff_i_bpc_value_selected_power_repeat = e) -> (((exists ff_h_bpc_value_selected_power_repeat_decoded. ff_h_bpc_value_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bpc_value_selected_power_repeat)) * ff_c_bpc_value_selected_power)) /\ exists ff_q_bpc_value_selected_power_repeat_decoded. ff_b_bpc_value_selected_power = ff_q_bpc_value_selected_power_repeat_decoded * S ((S (ff_i_bpc_value_selected_power_repeat)) * ff_c_bpc_value_selected_power) + (p)))) /\ (exists ff_u_bpc_value_selected_power_product ff_v_bpc_value_selected_power_product. ((((exists ff_h_bpc_value_selected_power_product_start. ff_h_bpc_value_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpc_value_selected_power_product)) /\ exists ff_q_bpc_value_selected_power_product_start. ff_u_bpc_value_selected_power_product = ff_q_bpc_value_selected_power_product_start * S ((S (0)) * ff_v_bpc_value_selected_power_product) + (1))) /\ ((((exists ff_h_bpc_value_selected_power_product_terminal. ff_h_bpc_value_selected_power_product_terminal + S (bpv_result_bpc_value_selected) = S ((S (e)) * ff_v_bpc_value_selected_power_product)) /\ exists ff_q_bpc_value_selected_power_product_terminal. ff_u_bpc_value_selected_power_product = ff_q_bpc_value_selected_power_product_terminal * S ((S (e)) * ff_v_bpc_value_selected_power_product) + (bpv_result_bpc_value_selected))) /\ forall ff_i_bpc_value_selected_power_product. (exists ff_lt_bpc_value_selected_power_product_bound. ff_lt_bpc_value_selected_power_product_bound + S ff_i_bpc_value_selected_power_product = e) -> exists ff_p_bpc_value_selected_power_product ff_r_bpc_value_selected_power_product ff_s_bpc_value_selected_power_product. ((((exists ff_h_bpc_value_selected_power_product_factor. ff_h_bpc_value_selected_power_product_factor + S (ff_p_bpc_value_selected_power_product) = S ((S (ff_i_bpc_value_selected_power_product)) * ff_c_bpc_value_selected_power)) /\ exists ff_q_bpc_value_selected_power_product_factor. ff_b_bpc_value_selected_power = ff_q_bpc_value_selected_power_product_factor * S ((S (ff_i_bpc_value_selected_power_product)) * ff_c_bpc_value_selected_power) + (ff_p_bpc_value_selected_power_product))) /\ ((((exists ff_h_bpc_value_selected_power_product_partial. ff_h_bpc_value_selected_power_product_partial + S (ff_r_bpc_value_selected_power_product) = S ((S (ff_i_bpc_value_selected_power_product)) * ff_v_bpc_value_selected_power_product)) /\ exists ff_q_bpc_value_selected_power_product_partial. ff_u_bpc_value_selected_power_product = ff_q_bpc_value_selected_power_product_partial * S ((S (ff_i_bpc_value_selected_power_product)) * ff_v_bpc_value_selected_power_product) + (ff_r_bpc_value_selected_power_product))) /\ ((((exists ff_h_bpc_value_selected_power_product_successor. ff_h_bpc_value_selected_power_product_successor + S (ff_s_bpc_value_selected_power_product) = S ((S (S ff_i_bpc_value_selected_power_product)) * ff_v_bpc_value_selected_power_product)) /\ exists ff_q_bpc_value_selected_power_product_successor. ff_u_bpc_value_selected_power_product = ff_q_bpc_value_selected_power_product_successor * S ((S (S ff_i_bpc_value_selected_power_product)) * ff_v_bpc_value_selected_power_product) + (ff_s_bpc_value_selected_power_product))) /\ ff_s_bpc_value_selected_power_product = ff_r_bpc_value_selected_power_product * ff_p_bpc_value_selected_power_product)))))))) /\ (exists bpv_factor_bpc_value_selected_divides. C = bpv_result_bpc_value_selected * bpv_factor_bpc_value_selected_divides)))) /\ forall bpv_candidate_bpc_value. (exists bpv_gap_bpc_value_candidate_bound. bpv_gap_bpc_value_candidate_bound + bpv_candidate_bpc_value = C) -> (exists bpv_result_bpc_value_candidate. ((exists ff_b_bpc_value_candidate_power ff_c_bpc_value_candidate_power. ((forall ff_i_bpc_value_candidate_power_repeat. (exists ff_lt_bpc_value_candidate_power_repeat_bound. ff_lt_bpc_value_candidate_power_repeat_bound + S ff_i_bpc_value_candidate_power_repeat = bpv_candidate_bpc_value) -> (((exists ff_h_bpc_value_candidate_power_repeat_decoded. ff_h_bpc_value_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bpc_value_candidate_power_repeat)) * ff_c_bpc_value_candidate_power)) /\ exists ff_q_bpc_value_candidate_power_repeat_decoded. ff_b_bpc_value_candidate_power = ff_q_bpc_value_candidate_power_repeat_decoded * S ((S (ff_i_bpc_value_candidate_power_repeat)) * ff_c_bpc_value_candidate_power) + (p)))) /\ (exists ff_u_bpc_value_candidate_power_product ff_v_bpc_value_candidate_power_product. ((((exists ff_h_bpc_value_candidate_power_product_start. ff_h_bpc_value_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpc_value_candidate_power_product)) /\ exists ff_q_bpc_value_candidate_power_product_start. ff_u_bpc_value_candidate_power_product = ff_q_bpc_value_candidate_power_product_start * S ((S (0)) * ff_v_bpc_value_candidate_power_product) + (1))) /\ ((((exists ff_h_bpc_value_candidate_power_product_terminal. ff_h_bpc_value_candidate_power_product_terminal + S (bpv_result_bpc_value_candidate) = S ((S (bpv_candidate_bpc_value)) * ff_v_bpc_value_candidate_power_product)) /\ exists ff_q_bpc_value_candidate_power_product_terminal. ff_u_bpc_value_candidate_power_product = ff_q_bpc_value_candidate_power_product_terminal * S ((S (bpv_candidate_bpc_value)) * ff_v_bpc_value_candidate_power_product) + (bpv_result_bpc_value_candidate))) /\ forall ff_i_bpc_value_candidate_power_product. (exists ff_lt_bpc_value_candidate_power_product_bound. ff_lt_bpc_value_candidate_power_product_bound + S ff_i_bpc_value_candidate_power_product = bpv_candidate_bpc_value) -> exists ff_p_bpc_value_candidate_power_product ff_r_bpc_value_candidate_power_product ff_s_bpc_value_candidate_power_product. ((((exists ff_h_bpc_value_candidate_power_product_factor. ff_h_bpc_value_candidate_power_product_factor + S (ff_p_bpc_value_candidate_power_product) = S ((S (ff_i_bpc_value_candidate_power_product)) * ff_c_bpc_value_candidate_power)) /\ exists ff_q_bpc_value_candidate_power_product_factor. ff_b_bpc_value_candidate_power = ff_q_bpc_value_candidate_power_product_factor * S ((S (ff_i_bpc_value_candidate_power_product)) * ff_c_bpc_value_candidate_power) + (ff_p_bpc_value_candidate_power_product))) /\ ((((exists ff_h_bpc_value_candidate_power_product_partial. ff_h_bpc_value_candidate_power_product_partial + S (ff_r_bpc_value_candidate_power_product) = S ((S (ff_i_bpc_value_candidate_power_product)) * ff_v_bpc_value_candidate_power_product)) /\ exists ff_q_bpc_value_candidate_power_product_partial. ff_u_bpc_value_candidate_power_product = ff_q_bpc_value_candidate_power_product_partial * S ((S (ff_i_bpc_value_candidate_power_product)) * ff_v_bpc_value_candidate_power_product) + (ff_r_bpc_value_candidate_power_product))) /\ ((((exists ff_h_bpc_value_candidate_power_product_successor. ff_h_bpc_value_candidate_power_product_successor + S (ff_s_bpc_value_candidate_power_product) = S ((S (S ff_i_bpc_value_candidate_power_product)) * ff_v_bpc_value_candidate_power_product)) /\ exists ff_q_bpc_value_candidate_power_product_successor. ff_u_bpc_value_candidate_power_product = ff_q_bpc_value_candidate_power_product_successor * S ((S (S ff_i_bpc_value_candidate_power_product)) * ff_v_bpc_value_candidate_power_product) + (ff_s_bpc_value_candidate_power_product))) /\ ff_s_bpc_value_candidate_power_product = ff_r_bpc_value_candidate_power_product * ff_p_bpc_value_candidate_power_product)))))))) /\ (exists bpv_factor_bpc_value_candidate_divides. C = bpv_result_bpc_value_candidate * bpv_factor_bpc_value_candidate_divides))) -> (exists bpv_gap_bpc_value_maximal. bpv_gap_bpc_value_maximal + bpv_candidate_bpc_value = e)) -> ~(e = 0)

Complete unchanged native tactic proof

All 39 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

39 script commands · 6 reading checkpoints · 3 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 (1)
bertrand window prime divides central binom
01Fix variables and assumptionsL1–9

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

  1. L1
    intro n
  2. L2
    intro p
  3. L3
    intro C
  4. L4
    intro e
  5. L5
    intro hprime
  6. L6
    intro hlower
  7. L7
    intro hupper
  8. L8
    intro hcentral
  9. L9
    intro hvaluation
02Establish hpositiveL10–14

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

  1. L10
    have hpositive : exists a. C = S a
  2. L11
    specialize central_binom_positive n
  3. L12
    specialize central_binom_positive C
  4. L13
    apply central_binom_positive
  5. L14
    exact hcentral
03Separate the logical casesL15–15

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

  1. L15
    cases hpositive
04Establish hnonzeroL16–20

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

  1. L16
    have hnonzero : ~(C = 0)
  2. L17
    intro hzero
  3. L18
    rewrite hpositive_witness at hzero
  4. L19
    apply PA1
  5. L20
    exact hzero
05Establish hdividesL21–30

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

  1. L21
    have hdivides : exists bcf_quotient_bpc_bpc_central_factor. C = p * bcf_quotient_bpc_bpc_central_factor
  2. L22
    specialize bertrand_window_prime_divides_central_binom n
  3. L23
    specialize bertrand_window_prime_divides_central_binom p
  4. L24
    specialize bertrand_window_prime_divides_central_binom C
  5. L25
    apply bertrand_window_prime_divides_central_binom
  6. L26
    exact hprime
  7. L27
    exact hlower
  8. L28
    exact hupper
  9. L29
    exact hcentral
  10. L30
    intro hexponent_zero
06Use earlier factsL31–39

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

  1. L31
    specialize prime_divisor_power_valuation_nonzero p
  2. L32
    specialize prime_divisor_power_valuation_nonzero C
  3. L33
    specialize prime_divisor_power_valuation_nonzero e
  4. L34
    apply prime_divisor_power_valuation_nonzero
  5. L35
    exact hprime
  6. L36
    exact hnonzero
  7. L37
    exact hvaluation
  8. L38
    exact hdivides
  9. L39
    exact hexponent_zero

Library-wide reading audit

Original defined command ledger · 39 lines
  1. 0001intro n
  2. 0002intro p
  3. 0003intro C
  4. 0004intro e
  5. 0005intro hprime
  6. 0006intro hlower
  7. 0007intro hupper
  8. 0008intro hcentral
  9. 0009intro hvaluation
  10. 0010have hpositive : exists a. C = S a
  11. 0011specialize central_binom_positive n
  12. 0012specialize central_binom_positive C
  13. 0013apply central_binom_positive
  14. 0014exact hcentral
  15. 0015cases hpositive
  16. 0016have hnonzero : ~(C = 0)
  17. 0017intro hzero
  18. 0018rewrite hpositive_witness at hzero
  19. 0019apply PA1
  20. 0020exact hzero
  21. 0021have hdivides : exists bcf_quotient_bpc_bpc_central_factor. C = p * bcf_quotient_bpc_bpc_central_factor
  22. 0022specialize bertrand_window_prime_divides_central_binom n
  23. 0023specialize bertrand_window_prime_divides_central_binom p
  24. 0024specialize bertrand_window_prime_divides_central_binom C
  25. 0025apply bertrand_window_prime_divides_central_binom
  26. 0026exact hprime
  27. 0027exact hlower
  28. 0028exact hupper
  29. 0029exact hcentral
  30. 0030intro hexponent_zero
  31. 0031specialize prime_divisor_power_valuation_nonzero p
  32. 0032specialize prime_divisor_power_valuation_nonzero C
  33. 0033specialize prime_divisor_power_valuation_nonzero e
  34. 0034apply prime_divisor_power_valuation_nonzero
  35. 0035exact hprime
  36. 0036exact hnonzero
  37. 0037exact hvaluation
  38. 0038exact hdivides
  39. 0039exact hexponent_zero