PC001F

central_binom_prime_count_power_bound

The actual central binomial coefficient is at most (2n)^pi(N) whenever 2n is at most N; all factors and prime counts are constructed.

Alpha v34 checked-use · first admitted v27 · 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.

These are the exact finite integer inequalities with constant 8, for every N≥2. The proof uses constructive binomial and primorial infrastructure; it does not assume logarithms, asymptotic estimates, the prime number theorem, or a factorization oracle.

Exact theorem in conservative defined notation

∀ n. ∀ N. ∀ k. ∀ C. ∀ Q. Lt(0,n) → Le(n + n,N) → PrimeCount(N,k) → CentralBinom(n,C) → Pow(n + n,k,Q) → Le(C,Q)

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

Definition DAG

PrimeCount(x,z) · 1Le(a,b) · 5Lt(a,b) · 2Prime(p) · 2BetaAt(b,c,i,x) · 1Product(b,c,l,z) · 1Pow(a,e,z) · 4CentralBinom(n,z) · 1

Actual proof prerequisites

central_binom_positive · checked external prerequisiteprime_contribution_complete_exists · checked external prerequisitecentral_binom_prime_divisor_le_double · checked external prerequisitele_trans · checked external prerequisitebeta_product_bit_weighted_upper_powercentral_binom_prime_mask_weighted_upper
Original expanded first-order statement 
forall n N k C Q. (exists pc_le_central_count_positive. pc_le_central_count_positive + (1) = (n)) -> (exists pc_le_central_count_range. pc_le_central_count_range + (n + n) = (N)) -> (exists pc_code_central_count_count pc_scale_central_count_count. (forall pc_index_central_count_count_mask. (exists pc_lt_central_count_count_mask_bound. pc_lt_central_count_count_mask_bound + S (pc_index_central_count_count_mask) = (N)) -> exists pc_bit_central_count_count_mask. (((exists fs_h_pc_central_count_count_mask_entry. fs_h_pc_central_count_count_mask_entry + S (pc_bit_central_count_count_mask) = S ((S (pc_index_central_count_count_mask)) * pc_scale_central_count_count)) /\ exists fs_q_pc_central_count_count_mask_entry. pc_code_central_count_count = fs_q_pc_central_count_count_mask_entry * S ((S (pc_index_central_count_count_mask)) * pc_scale_central_count_count) + (pc_bit_central_count_count_mask))) /\ (((((~(S (pc_index_central_count_count_mask) = 1) /\ forall bpr_left_pc_central_count_count_mask_choice_prime bpr_right_pc_central_count_count_mask_choice_prime. S (pc_index_central_count_count_mask) = bpr_left_pc_central_count_count_mask_choice_prime * bpr_right_pc_central_count_count_mask_choice_prime -> bpr_left_pc_central_count_count_mask_choice_prime = 1 \/ bpr_right_pc_central_count_count_mask_choice_prime = 1)) /\ pc_bit_central_count_count_mask = 1) \/ (~((~(S (pc_index_central_count_count_mask) = 1) /\ forall bpr_left_pc_central_count_count_mask_choice_prime bpr_right_pc_central_count_count_mask_choice_prime. S (pc_index_central_count_count_mask) = bpr_left_pc_central_count_count_mask_choice_prime * bpr_right_pc_central_count_count_mask_choice_prime -> bpr_left_pc_central_count_count_mask_choice_prime = 1 \/ bpr_right_pc_central_count_count_mask_choice_prime = 1)) /\ pc_bit_central_count_count_mask = 0)))) /\ (exists fs_u_pc_central_count_count_sum fs_v_pc_central_count_count_sum. ((((exists fs_h_pc_central_count_count_sum_body_start. fs_h_pc_central_count_count_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_central_count_count_sum)) /\ exists fs_q_pc_central_count_count_sum_body_start. fs_u_pc_central_count_count_sum = fs_q_pc_central_count_count_sum_body_start * S ((S (0)) * fs_v_pc_central_count_count_sum) + (0))) /\ ((((exists fs_h_pc_central_count_count_sum_body_terminal. fs_h_pc_central_count_count_sum_body_terminal + S (k) = S ((S (N)) * fs_v_pc_central_count_count_sum)) /\ exists fs_q_pc_central_count_count_sum_body_terminal. fs_u_pc_central_count_count_sum = fs_q_pc_central_count_count_sum_body_terminal * S ((S (N)) * fs_v_pc_central_count_count_sum) + (k))) /\ forall fs_i_pc_central_count_count_sum_body_steps. (exists fs_lt_pc_central_count_count_sum_body_steps_bound. fs_lt_pc_central_count_count_sum_body_steps_bound + S fs_i_pc_central_count_count_sum_body_steps = N) -> exists fs_a_pc_central_count_count_sum_body_steps fs_r_pc_central_count_count_sum_body_steps fs_s_pc_central_count_count_sum_body_steps. ((((exists fs_h_pc_central_count_count_sum_body_steps_summand. fs_h_pc_central_count_count_sum_body_steps_summand + S (fs_a_pc_central_count_count_sum_body_steps) = S ((S (fs_i_pc_central_count_count_sum_body_steps)) * pc_scale_central_count_count)) /\ exists fs_q_pc_central_count_count_sum_body_steps_summand. pc_code_central_count_count = fs_q_pc_central_count_count_sum_body_steps_summand * S ((S (fs_i_pc_central_count_count_sum_body_steps)) * pc_scale_central_count_count) + (fs_a_pc_central_count_count_sum_body_steps))) /\ ((((exists fs_h_pc_central_count_count_sum_body_steps_partial. fs_h_pc_central_count_count_sum_body_steps_partial + S (fs_r_pc_central_count_count_sum_body_steps) = S ((S (fs_i_pc_central_count_count_sum_body_steps)) * fs_v_pc_central_count_count_sum)) /\ exists fs_q_pc_central_count_count_sum_body_steps_partial. fs_u_pc_central_count_count_sum = fs_q_pc_central_count_count_sum_body_steps_partial * S ((S (fs_i_pc_central_count_count_sum_body_steps)) * fs_v_pc_central_count_count_sum) + (fs_r_pc_central_count_count_sum_body_steps))) /\ ((((exists fs_h_pc_central_count_count_sum_body_steps_successor. fs_h_pc_central_count_count_sum_body_steps_successor + S (fs_s_pc_central_count_count_sum_body_steps) = S ((S (S fs_i_pc_central_count_count_sum_body_steps)) * fs_v_pc_central_count_count_sum)) /\ exists fs_q_pc_central_count_count_sum_body_steps_successor. fs_u_pc_central_count_count_sum = fs_q_pc_central_count_count_sum_body_steps_successor * S ((S (S fs_i_pc_central_count_count_sum_body_steps)) * fs_v_pc_central_count_count_sum) + (fs_s_pc_central_count_count_sum_body_steps))) /\ fs_s_pc_central_count_count_sum_body_steps = fs_r_pc_central_count_count_sum_body_steps + fs_a_pc_central_count_count_sum_body_steps))))))) -> (((exists bcf_lt_gap_pc_central_count_value_out_of_range. bcf_lt_gap_pc_central_count_value_out_of_range + S (n + n) = n) /\ C = 0) \/ ((exists bcf_le_gap_pc_central_count_value_in_range. bcf_le_gap_pc_central_count_value_in_range + (n) = n + n) /\ (exists bcf_row_code_code_pc_central_count_value bcf_row_code_scale_pc_central_count_value bcf_row_scale_code_pc_central_count_value bcf_row_scale_scale_pc_central_count_value bcf_row_code_pc_central_count_value bcf_row_scale_pc_central_count_value. ((forall bcf_row_index_pc_central_count_value_table. (exists bcf_lt_gap_pc_central_count_value_table_row_bound. bcf_lt_gap_pc_central_count_value_table_row_bound + S (bcf_row_index_pc_central_count_value_table) = S (n + n)) -> exists bcf_row_code_pc_central_count_value_table bcf_row_scale_pc_central_count_value_table. ((((exists bcf_height_pc_central_count_value_table_decoded_row_code. bcf_height_pc_central_count_value_table_decoded_row_code + S (bcf_row_code_pc_central_count_value_table) = S ((S (bcf_row_index_pc_central_count_value_table)) * bcf_row_code_scale_pc_central_count_value)) /\ exists bcf_quotient_pc_central_count_value_table_decoded_row_code. bcf_row_code_code_pc_central_count_value = bcf_quotient_pc_central_count_value_table_decoded_row_code * S ((S (bcf_row_index_pc_central_count_value_table)) * bcf_row_code_scale_pc_central_count_value) + (bcf_row_code_pc_central_count_value_table))) /\ ((((exists bcf_height_pc_central_count_value_table_decoded_row_scale. bcf_height_pc_central_count_value_table_decoded_row_scale + S (bcf_row_scale_pc_central_count_value_table) = S ((S (bcf_row_index_pc_central_count_value_table)) * bcf_row_scale_scale_pc_central_count_value)) /\ exists bcf_quotient_pc_central_count_value_table_decoded_row_scale. bcf_row_scale_code_pc_central_count_value = bcf_quotient_pc_central_count_value_table_decoded_row_scale * S ((S (bcf_row_index_pc_central_count_value_table)) * bcf_row_scale_scale_pc_central_count_value) + (bcf_row_scale_pc_central_count_value_table))) /\ ((bcf_row_index_pc_central_count_value_table = 0 /\ (forall bcf_index_pc_central_count_value_table_zero_row. (exists bcf_lt_gap_pc_central_count_value_table_zero_row_bound. bcf_lt_gap_pc_central_count_value_table_zero_row_bound + S (bcf_index_pc_central_count_value_table_zero_row) = S (n + n)) -> exists bcf_value_pc_central_count_value_table_zero_row. ((((exists bcf_height_pc_central_count_value_table_zero_row_entry. bcf_height_pc_central_count_value_table_zero_row_entry + S (bcf_value_pc_central_count_value_table_zero_row) = S ((S (bcf_index_pc_central_count_value_table_zero_row)) * bcf_row_scale_pc_central_count_value_table)) /\ exists bcf_quotient_pc_central_count_value_table_zero_row_entry. bcf_row_code_pc_central_count_value_table = bcf_quotient_pc_central_count_value_table_zero_row_entry * S ((S (bcf_index_pc_central_count_value_table_zero_row)) * bcf_row_scale_pc_central_count_value_table) + (bcf_value_pc_central_count_value_table_zero_row))) /\ ((bcf_index_pc_central_count_value_table_zero_row = 0 /\ bcf_value_pc_central_count_value_table_zero_row = 1) \/ exists bcf_predecessor_pc_central_count_value_table_zero_row. bcf_index_pc_central_count_value_table_zero_row = S bcf_predecessor_pc_central_count_value_table_zero_row /\ bcf_value_pc_central_count_value_table_zero_row = 0)))) \/ exists bcf_predecessor_pc_central_count_value_table bcf_previous_code_pc_central_count_value_table bcf_previous_scale_pc_central_count_value_table. bcf_row_index_pc_central_count_value_table = S bcf_predecessor_pc_central_count_value_table /\ ((((exists bcf_height_pc_central_count_value_table_decoded_previous_code. bcf_height_pc_central_count_value_table_decoded_previous_code + S (bcf_previous_code_pc_central_count_value_table) = S ((S (bcf_predecessor_pc_central_count_value_table)) * bcf_row_code_scale_pc_central_count_value)) /\ exists bcf_quotient_pc_central_count_value_table_decoded_previous_code. bcf_row_code_code_pc_central_count_value = bcf_quotient_pc_central_count_value_table_decoded_previous_code * S ((S (bcf_predecessor_pc_central_count_value_table)) * bcf_row_code_scale_pc_central_count_value) + (bcf_previous_code_pc_central_count_value_table))) /\ ((((exists bcf_height_pc_central_count_value_table_decoded_previous_scale. bcf_height_pc_central_count_value_table_decoded_previous_scale + S (bcf_previous_scale_pc_central_count_value_table) = S ((S (bcf_predecessor_pc_central_count_value_table)) * bcf_row_scale_scale_pc_central_count_value)) /\ exists bcf_quotient_pc_central_count_value_table_decoded_previous_scale. bcf_row_scale_code_pc_central_count_value = bcf_quotient_pc_central_count_value_table_decoded_previous_scale * S ((S (bcf_predecessor_pc_central_count_value_table)) * bcf_row_scale_scale_pc_central_count_value) + (bcf_previous_scale_pc_central_count_value_table))) /\ (forall bcf_index_pc_central_count_value_table_row_step. (exists bcf_lt_gap_pc_central_count_value_table_row_step_bound. bcf_lt_gap_pc_central_count_value_table_row_step_bound + S (bcf_index_pc_central_count_value_table_row_step) = S (n + n)) -> exists bcf_value_pc_central_count_value_table_row_step. ((((exists bcf_height_pc_central_count_value_table_row_step_entry. bcf_height_pc_central_count_value_table_row_step_entry + S (bcf_value_pc_central_count_value_table_row_step) = S ((S (bcf_index_pc_central_count_value_table_row_step)) * bcf_row_scale_pc_central_count_value_table)) /\ exists bcf_quotient_pc_central_count_value_table_row_step_entry. bcf_row_code_pc_central_count_value_table = bcf_quotient_pc_central_count_value_table_row_step_entry * S ((S (bcf_index_pc_central_count_value_table_row_step)) * bcf_row_scale_pc_central_count_value_table) + (bcf_value_pc_central_count_value_table_row_step))) /\ ((bcf_index_pc_central_count_value_table_row_step = 0 /\ bcf_value_pc_central_count_value_table_row_step = 1) \/ exists bcf_predecessor_pc_central_count_value_table_row_step bcf_left_pc_central_count_value_table_row_step bcf_right_pc_central_count_value_table_row_step. bcf_index_pc_central_count_value_table_row_step = S bcf_predecessor_pc_central_count_value_table_row_step /\ ((((exists bcf_height_pc_central_count_value_table_row_step_previous_left. bcf_height_pc_central_count_value_table_row_step_previous_left + S (bcf_left_pc_central_count_value_table_row_step) = S ((S (bcf_predecessor_pc_central_count_value_table_row_step)) * bcf_previous_scale_pc_central_count_value_table)) /\ exists bcf_quotient_pc_central_count_value_table_row_step_previous_left. bcf_previous_code_pc_central_count_value_table = bcf_quotient_pc_central_count_value_table_row_step_previous_left * S ((S (bcf_predecessor_pc_central_count_value_table_row_step)) * bcf_previous_scale_pc_central_count_value_table) + (bcf_left_pc_central_count_value_table_row_step))) /\ ((((exists bcf_height_pc_central_count_value_table_row_step_previous_right. bcf_height_pc_central_count_value_table_row_step_previous_right + S (bcf_right_pc_central_count_value_table_row_step) = S ((S (S (bcf_predecessor_pc_central_count_value_table_row_step))) * bcf_previous_scale_pc_central_count_value_table)) /\ exists bcf_quotient_pc_central_count_value_table_row_step_previous_right. bcf_previous_code_pc_central_count_value_table = bcf_quotient_pc_central_count_value_table_row_step_previous_right * S ((S (S (bcf_predecessor_pc_central_count_value_table_row_step))) * bcf_previous_scale_pc_central_count_value_table) + (bcf_right_pc_central_count_value_table_row_step))) /\ bcf_value_pc_central_count_value_table_row_step = bcf_left_pc_central_count_value_table_row_step + bcf_right_pc_central_count_value_table_row_step))))))))))) /\ ((((exists bcf_height_pc_central_count_value_decoded_row_code. bcf_height_pc_central_count_value_decoded_row_code + S (bcf_row_code_pc_central_count_value) = S ((S (n + n)) * bcf_row_code_scale_pc_central_count_value)) /\ exists bcf_quotient_pc_central_count_value_decoded_row_code. bcf_row_code_code_pc_central_count_value = bcf_quotient_pc_central_count_value_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_pc_central_count_value) + (bcf_row_code_pc_central_count_value))) /\ ((((exists bcf_height_pc_central_count_value_decoded_row_scale. bcf_height_pc_central_count_value_decoded_row_scale + S (bcf_row_scale_pc_central_count_value) = S ((S (n + n)) * bcf_row_scale_scale_pc_central_count_value)) /\ exists bcf_quotient_pc_central_count_value_decoded_row_scale. bcf_row_scale_code_pc_central_count_value = bcf_quotient_pc_central_count_value_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_pc_central_count_value) + (bcf_row_scale_pc_central_count_value))) /\ (((exists bcf_height_pc_central_count_value_decoded_value. bcf_height_pc_central_count_value_decoded_value + S (C) = S ((S (n)) * bcf_row_scale_pc_central_count_value)) /\ exists bcf_quotient_pc_central_count_value_decoded_value. bcf_row_code_pc_central_count_value = bcf_quotient_pc_central_count_value_decoded_value * S ((S (n)) * bcf_row_scale_pc_central_count_value) + (C))))))))) -> (exists pa_b_pc_central_count_power pa_c_pc_central_count_power. ((forall pa_i_pc_central_count_power_repeat. (exists pa_lt_pc_central_count_power_repeat_bound. pa_lt_pc_central_count_power_repeat_bound + S pa_i_pc_central_count_power_repeat = k) -> (((exists pa_h_pc_central_count_power_repeat_decoded. pa_h_pc_central_count_power_repeat_decoded + S (n + n) = S ((S (pa_i_pc_central_count_power_repeat)) * pa_c_pc_central_count_power)) /\ exists pa_q_pc_central_count_power_repeat_decoded. pa_b_pc_central_count_power = pa_q_pc_central_count_power_repeat_decoded * S ((S (pa_i_pc_central_count_power_repeat)) * pa_c_pc_central_count_power) + (n + n)))) /\ (exists pa_u_pc_central_count_power_product pa_v_pc_central_count_power_product. ((((exists pa_h_pc_central_count_power_product_start. pa_h_pc_central_count_power_product_start + S (1) = S ((S (0)) * pa_v_pc_central_count_power_product)) /\ exists pa_q_pc_central_count_power_product_start. pa_u_pc_central_count_power_product = pa_q_pc_central_count_power_product_start * S ((S (0)) * pa_v_pc_central_count_power_product) + (1))) /\ ((((exists pa_h_pc_central_count_power_product_terminal. pa_h_pc_central_count_power_product_terminal + S (Q) = S ((S (k)) * pa_v_pc_central_count_power_product)) /\ exists pa_q_pc_central_count_power_product_terminal. pa_u_pc_central_count_power_product = pa_q_pc_central_count_power_product_terminal * S ((S (k)) * pa_v_pc_central_count_power_product) + (Q))) /\ forall pa_i_pc_central_count_power_product. (exists pa_lt_pc_central_count_power_product_bound. pa_lt_pc_central_count_power_product_bound + S pa_i_pc_central_count_power_product = k) -> exists pa_p_pc_central_count_power_product pa_r_pc_central_count_power_product pa_s_pc_central_count_power_product. ((((exists pa_h_pc_central_count_power_product_factor. pa_h_pc_central_count_power_product_factor + S (pa_p_pc_central_count_power_product) = S ((S (pa_i_pc_central_count_power_product)) * pa_c_pc_central_count_power)) /\ exists pa_q_pc_central_count_power_product_factor. pa_b_pc_central_count_power = pa_q_pc_central_count_power_product_factor * S ((S (pa_i_pc_central_count_power_product)) * pa_c_pc_central_count_power) + (pa_p_pc_central_count_power_product))) /\ ((((exists pa_h_pc_central_count_power_product_partial. pa_h_pc_central_count_power_product_partial + S (pa_r_pc_central_count_power_product) = S ((S (pa_i_pc_central_count_power_product)) * pa_v_pc_central_count_power_product)) /\ exists pa_q_pc_central_count_power_product_partial. pa_u_pc_central_count_power_product = pa_q_pc_central_count_power_product_partial * S ((S (pa_i_pc_central_count_power_product)) * pa_v_pc_central_count_power_product) + (pa_r_pc_central_count_power_product))) /\ ((((exists pa_h_pc_central_count_power_product_successor. pa_h_pc_central_count_power_product_successor + S (pa_s_pc_central_count_power_product) = S ((S (S pa_i_pc_central_count_power_product)) * pa_v_pc_central_count_power_product)) /\ exists pa_q_pc_central_count_power_product_successor. pa_u_pc_central_count_power_product = pa_q_pc_central_count_power_product_successor * S ((S (S pa_i_pc_central_count_power_product)) * pa_v_pc_central_count_power_product) + (pa_s_pc_central_count_power_product))) /\ pa_s_pc_central_count_power_product = pa_r_pc_central_count_power_product * pa_p_pc_central_count_power_product)))))))) -> (exists pc_le_central_count_result. pc_le_central_count_result + (C) = (Q))

Complete tactic proof in conservative notation

All 75 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

75 script commands · 16 reading checkpoints · 2 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 (2)
beta product bit weighted upper powercentral binom prime mask weighted upper
01Fix variables and assumptionsL1–10

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

  1. L1
    intro n
  2. L2
    intro N
  3. L3
    intro k
  4. L4
    intro C
  5. L5
    intro Q
  6. L6
    intro hn
  7. L7
    intro hN
  8. L8
    intro hk
  9. L9
    intro hC
  10. L10
    intro hQ
02Separate the logical casesL11–13

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

  1. L11
    cases hk
  2. L12
    cases hk_witness
  3. L13
    cases hk_witness_witness
03Establish hcompleteL14–18

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

  1. L14
    have hcomplete : ∃ z. (∃ x. ∃ y. (∀ n. Lt(n,N) → ∃ m. BetaAt(x,y,n,m) ∧ (Prime(S n) ∧ (∃ k. Le(k,C) ∧ (∃ i. Pow(S n,k,i) ∧ (∃ j. C = i · j)) ∧ (∀ i. Le(i,C) → (∃ j. Pow(S n,i,j) ∧ (∃ u. C = j · u)) → Le(i,k)) ∧ Pow(S n,k,m)) ∨ ¬Prime(S n) ∧ m = 1)) ∧ Product(x,y,N,z)) ∧ C = zDefinitions: Lt(n,N)BetaAt(x,y,n,m)Prime(S n)Le(k,C)Pow(S n,k,i)Le(i,C)Pow(S n,i,j)Le(i,k)Pow(S n,k,m)Product(x,y,N,z)Original native command in the exact edition
  2. L15
    specialize prime_contribution_complete_exists C
  3. L16
    specialize prime_contribution_complete_exists N
  4. L17
    apply prime_contribution_complete_exists
  5. L18
    intro hz
04Establish hpL19–23

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

  1. L19
    have hp : exists r. C = S r
  2. L20
    specialize central_binom_positive n
  3. L21
    specialize central_binom_positive C
  4. L22
    apply central_binom_positive
  5. L23
    exact hC
05Separate the logical casesL24–24

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

  1. L24
    cases hp
06Use earlier factsL25–25

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

  1. L25
    apply PA1
07Calculate and transport equalitiesL26–27

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

  1. L26
    trans C
  2. L27
    symm
08Use earlier factsL28–29

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

  1. L28
    exact hp_witness
  2. L29
    exact hz
09Fix variables and assumptionsL30–32

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

  1. L30
    intro p
  2. L31
    intro hp
  3. L32
    intro hd
10Use earlier factsL33–42

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

  1. L33
    specialize le_trans p
  2. L34
    specialize le_trans (n + n)
  3. L35
    specialize le_trans N
  4. L36
    apply le_trans
  5. L37
    specialize central_binom_prime_divisor_le_double n
  6. L38
    specialize central_binom_prime_divisor_le_double C
  7. L39
    specialize central_binom_prime_divisor_le_double p
  8. L40
    apply central_binom_prime_divisor_le_double
  9. L41
    exact hp
  10. L42
    exact hC
11Use earlier factsL43–44

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

  1. L43
    exact hd
  2. L44
    exact hN
12Separate the logical casesL45–49

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

  1. L45
    cases hcomplete
  2. L46
    cases hcomplete_witness
  3. L47
    cases hcomplete_witness_left
  4. L48
    cases hcomplete_witness_left_witness
  5. L49
    cases hcomplete_witness_left_witness_witness
13Calculate and transport equalitiesL50–50

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

  1. L50
    rewrite hcomplete_witness_right
14Use earlier factsL51–60

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

  1. L51
    specialize beta_product_bit_weighted_upper_power x3
  2. L52
    specialize beta_product_bit_weighted_upper_power x4
  3. L53
    specialize beta_product_bit_weighted_upper_power x
  4. L54
    specialize beta_product_bit_weighted_upper_power x1
  5. L55
    specialize beta_product_bit_weighted_upper_power (n + n)
  6. L56
    specialize beta_product_bit_weighted_upper_power N
  7. L57
    specialize beta_product_bit_weighted_upper_power x2
  8. L58
    specialize beta_product_bit_weighted_upper_power k
  9. L59
    specialize beta_product_bit_weighted_upper_power Q
  10. L60
    apply beta_product_bit_weighted_upper_power
15Use earlier factsL61–70

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

  1. L61
    specialize central_binom_prime_mask_weighted_upper n
  2. L62
    specialize central_binom_prime_mask_weighted_upper C
  3. L63
    specialize central_binom_prime_mask_weighted_upper x3
  4. L64
    specialize central_binom_prime_mask_weighted_upper x4
  5. L65
    specialize central_binom_prime_mask_weighted_upper x
  6. L66
    specialize central_binom_prime_mask_weighted_upper x1
  7. L67
    specialize central_binom_prime_mask_weighted_upper N
  8. L68
    apply central_binom_prime_mask_weighted_upper
  9. L69
    exact hn
  10. L70
    exact hC
16Use earlier factsL71–75

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

  1. L71
    exact hcomplete_witness_left_witness_witness_left
  2. L72
    exact hk_witness_witness_left
  3. L73
    exact hcomplete_witness_left_witness_witness_right
  4. L74
    exact hk_witness_witness_right
  5. L75
    exact hQ

Library-wide reading audit

Original defined command ledger · 75 lines
  1. 0001intro n
  2. 0002intro N
  3. 0003intro k
  4. 0004intro C
  5. 0005intro Q
  6. 0006intro hn
  7. 0007intro hN
  8. 0008intro hk
  9. 0009intro hC
  10. 0010intro hQ
  11. 0011cases hk
  12. 0012cases hk_witness
  13. 0013cases hk_witness_witness
  14. 0014have hcomplete : ∃ z. (∃ x. ∃ y. (∀ n. Lt(n,N) → ∃ m. BetaAt(x,y,n,m) ∧ (Prime(S n) ∧ (∃ k. Le(k,C) ∧ (∃ i. Pow(S n,k,i) ∧ (∃ j. C = i · j)) ∧ (∀ i. Le(i,C) → (∃ j. Pow(S n,i,j) ∧ (∃ u. C = j · u)) → Le(i,k)) ∧ Pow(S n,k,m)) ∨ ¬Prime(S n) ∧ m = 1)) ∧ Product(x,y,N,z)) ∧ C = z
  15. 0015specialize prime_contribution_complete_exists C
  16. 0016specialize prime_contribution_complete_exists N
  17. 0017apply prime_contribution_complete_exists
  18. 0018intro hz
  19. 0019have hp : exists r. C = S r
  20. 0020specialize central_binom_positive n
  21. 0021specialize central_binom_positive C
  22. 0022apply central_binom_positive
  23. 0023exact hC
  24. 0024cases hp
  25. 0025apply PA1
  26. 0026trans C
  27. 0027symm
  28. 0028exact hp_witness
  29. 0029exact hz
  30. 0030intro p
  31. 0031intro hp
  32. 0032intro hd
  33. 0033specialize le_trans p
  34. 0034specialize le_trans (n + n)
  35. 0035specialize le_trans N
  36. 0036apply le_trans
  37. 0037specialize central_binom_prime_divisor_le_double n
  38. 0038specialize central_binom_prime_divisor_le_double C
  39. 0039specialize central_binom_prime_divisor_le_double p
  40. 0040apply central_binom_prime_divisor_le_double
  41. 0041exact hp
  42. 0042exact hC
  43. 0043exact hd
  44. 0044exact hN
  45. 0045cases hcomplete
  46. 0046cases hcomplete_witness
  47. 0047cases hcomplete_witness_left
  48. 0048cases hcomplete_witness_left_witness
  49. 0049cases hcomplete_witness_left_witness_witness
  50. 0050rewrite hcomplete_witness_right
  51. 0051specialize beta_product_bit_weighted_upper_power x3
  52. 0052specialize beta_product_bit_weighted_upper_power x4
  53. 0053specialize beta_product_bit_weighted_upper_power x
  54. 0054specialize beta_product_bit_weighted_upper_power x1
  55. 0055specialize beta_product_bit_weighted_upper_power (n + n)
  56. 0056specialize beta_product_bit_weighted_upper_power N
  57. 0057specialize beta_product_bit_weighted_upper_power x2
  58. 0058specialize beta_product_bit_weighted_upper_power k
  59. 0059specialize beta_product_bit_weighted_upper_power Q
  60. 0060apply beta_product_bit_weighted_upper_power
  61. 0061specialize central_binom_prime_mask_weighted_upper n
  62. 0062specialize central_binom_prime_mask_weighted_upper C
  63. 0063specialize central_binom_prime_mask_weighted_upper x3
  64. 0064specialize central_binom_prime_mask_weighted_upper x4
  65. 0065specialize central_binom_prime_mask_weighted_upper x
  66. 0066specialize central_binom_prime_mask_weighted_upper x1
  67. 0067specialize central_binom_prime_mask_weighted_upper N
  68. 0068apply central_binom_prime_mask_weighted_upper
  69. 0069exact hn
  70. 0070exact hC
  71. 0071exact hcomplete_witness_left_witness_witness_left
  72. 0072exact hk_witness_witness_left
  73. 0073exact hcomplete_witness_left_witness_witness_right
  74. 0074exact hk_witness_witness_right
  75. 0075exact hQ