BT00YE · Bertrand theorem

central_binom_prime_valuation_zero_two_thirds_range

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

Primes in the open two-thirds range contribute zero valuation.

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

∀ p. ∀ n. ∀ C. ∀ v. Prime(p) → Lt(2,n) → Le(p,n) → Lt(n + n,p + p + p) → CentralBinom(n,C) → PowerValuation(p,C,v) → v = 0

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 PD0042 CentralBinom PD0046 PowerValuation

6 occurrences

In local proof propositions

PD0002 Lt PD0007 DivRem PD0020 Pow

6 occurrences

Exact expanded native-PA statement
forall p n C v. ((~(p = 1) /\ forall frm_prime_left_bcpvztt_prime frm_prime_right_bcpvztt_prime. p = frm_prime_left_bcpvztt_prime * frm_prime_right_bcpvztt_prime -> frm_prime_left_bcpvztt_prime = 1 \/ frm_prime_right_bcpvztt_prime = 1)) -> (exists bcf_lt_gap_bcpvztt_positive. bcf_lt_gap_bcpvztt_positive + S (2) = n) -> (exists bcf_le_gap_bcpvztt_lower. bcf_le_gap_bcpvztt_lower + (p) = n) -> (exists bcf_lt_gap_bcpvztt_scaled. bcf_lt_gap_bcpvztt_scaled + S (n + n) = (p + p) + p) -> (((exists bcf_lt_gap_bcpvztt_central_out_of_range. bcf_lt_gap_bcpvztt_central_out_of_range + S (n + n) = n) /\ C = 0) \/ ((exists bcf_le_gap_bcpvztt_central_in_range. bcf_le_gap_bcpvztt_central_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bcpvztt_central bcf_row_code_scale_bcpvztt_central bcf_row_scale_code_bcpvztt_central bcf_row_scale_scale_bcpvztt_central bcf_row_code_bcpvztt_central bcf_row_scale_bcpvztt_central. ((forall bcf_row_index_bcpvztt_central_table. (exists bcf_lt_gap_bcpvztt_central_table_row_bound. bcf_lt_gap_bcpvztt_central_table_row_bound + S (bcf_row_index_bcpvztt_central_table) = S (n + n)) -> exists bcf_row_code_bcpvztt_central_table bcf_row_scale_bcpvztt_central_table. ((((exists bcf_height_bcpvztt_central_table_decoded_row_code. bcf_height_bcpvztt_central_table_decoded_row_code + S (bcf_row_code_bcpvztt_central_table) = S ((S (bcf_row_index_bcpvztt_central_table)) * bcf_row_code_scale_bcpvztt_central)) /\ exists bcf_quotient_bcpvztt_central_table_decoded_row_code. bcf_row_code_code_bcpvztt_central = bcf_quotient_bcpvztt_central_table_decoded_row_code * S ((S (bcf_row_index_bcpvztt_central_table)) * bcf_row_code_scale_bcpvztt_central) + (bcf_row_code_bcpvztt_central_table))) /\ ((((exists bcf_height_bcpvztt_central_table_decoded_row_scale. bcf_height_bcpvztt_central_table_decoded_row_scale + S (bcf_row_scale_bcpvztt_central_table) = S ((S (bcf_row_index_bcpvztt_central_table)) * bcf_row_scale_scale_bcpvztt_central)) /\ exists bcf_quotient_bcpvztt_central_table_decoded_row_scale. bcf_row_scale_code_bcpvztt_central = bcf_quotient_bcpvztt_central_table_decoded_row_scale * S ((S (bcf_row_index_bcpvztt_central_table)) * bcf_row_scale_scale_bcpvztt_central) + (bcf_row_scale_bcpvztt_central_table))) /\ ((bcf_row_index_bcpvztt_central_table = 0 /\ (forall bcf_index_bcpvztt_central_table_zero_row. (exists bcf_lt_gap_bcpvztt_central_table_zero_row_bound. bcf_lt_gap_bcpvztt_central_table_zero_row_bound + S (bcf_index_bcpvztt_central_table_zero_row) = S (n + n)) -> exists bcf_value_bcpvztt_central_table_zero_row. ((((exists bcf_height_bcpvztt_central_table_zero_row_entry. bcf_height_bcpvztt_central_table_zero_row_entry + S (bcf_value_bcpvztt_central_table_zero_row) = S ((S (bcf_index_bcpvztt_central_table_zero_row)) * bcf_row_scale_bcpvztt_central_table)) /\ exists bcf_quotient_bcpvztt_central_table_zero_row_entry. bcf_row_code_bcpvztt_central_table = bcf_quotient_bcpvztt_central_table_zero_row_entry * S ((S (bcf_index_bcpvztt_central_table_zero_row)) * bcf_row_scale_bcpvztt_central_table) + (bcf_value_bcpvztt_central_table_zero_row))) /\ ((bcf_index_bcpvztt_central_table_zero_row = 0 /\ bcf_value_bcpvztt_central_table_zero_row = 1) \/ exists bcf_predecessor_bcpvztt_central_table_zero_row. bcf_index_bcpvztt_central_table_zero_row = S bcf_predecessor_bcpvztt_central_table_zero_row /\ bcf_value_bcpvztt_central_table_zero_row = 0)))) \/ exists bcf_predecessor_bcpvztt_central_table bcf_previous_code_bcpvztt_central_table bcf_previous_scale_bcpvztt_central_table. bcf_row_index_bcpvztt_central_table = S bcf_predecessor_bcpvztt_central_table /\ ((((exists bcf_height_bcpvztt_central_table_decoded_previous_code. bcf_height_bcpvztt_central_table_decoded_previous_code + S (bcf_previous_code_bcpvztt_central_table) = S ((S (bcf_predecessor_bcpvztt_central_table)) * bcf_row_code_scale_bcpvztt_central)) /\ exists bcf_quotient_bcpvztt_central_table_decoded_previous_code. bcf_row_code_code_bcpvztt_central = bcf_quotient_bcpvztt_central_table_decoded_previous_code * S ((S (bcf_predecessor_bcpvztt_central_table)) * bcf_row_code_scale_bcpvztt_central) + (bcf_previous_code_bcpvztt_central_table))) /\ ((((exists bcf_height_bcpvztt_central_table_decoded_previous_scale. bcf_height_bcpvztt_central_table_decoded_previous_scale + S (bcf_previous_scale_bcpvztt_central_table) = S ((S (bcf_predecessor_bcpvztt_central_table)) * bcf_row_scale_scale_bcpvztt_central)) /\ exists bcf_quotient_bcpvztt_central_table_decoded_previous_scale. bcf_row_scale_code_bcpvztt_central = bcf_quotient_bcpvztt_central_table_decoded_previous_scale * S ((S (bcf_predecessor_bcpvztt_central_table)) * bcf_row_scale_scale_bcpvztt_central) + (bcf_previous_scale_bcpvztt_central_table))) /\ (forall bcf_index_bcpvztt_central_table_row_step. (exists bcf_lt_gap_bcpvztt_central_table_row_step_bound. bcf_lt_gap_bcpvztt_central_table_row_step_bound + S (bcf_index_bcpvztt_central_table_row_step) = S (n + n)) -> exists bcf_value_bcpvztt_central_table_row_step. ((((exists bcf_height_bcpvztt_central_table_row_step_entry. bcf_height_bcpvztt_central_table_row_step_entry + S (bcf_value_bcpvztt_central_table_row_step) = S ((S (bcf_index_bcpvztt_central_table_row_step)) * bcf_row_scale_bcpvztt_central_table)) /\ exists bcf_quotient_bcpvztt_central_table_row_step_entry. bcf_row_code_bcpvztt_central_table = bcf_quotient_bcpvztt_central_table_row_step_entry * S ((S (bcf_index_bcpvztt_central_table_row_step)) * bcf_row_scale_bcpvztt_central_table) + (bcf_value_bcpvztt_central_table_row_step))) /\ ((bcf_index_bcpvztt_central_table_row_step = 0 /\ bcf_value_bcpvztt_central_table_row_step = 1) \/ exists bcf_predecessor_bcpvztt_central_table_row_step bcf_left_bcpvztt_central_table_row_step bcf_right_bcpvztt_central_table_row_step. bcf_index_bcpvztt_central_table_row_step = S bcf_predecessor_bcpvztt_central_table_row_step /\ ((((exists bcf_height_bcpvztt_central_table_row_step_previous_left. bcf_height_bcpvztt_central_table_row_step_previous_left + S (bcf_left_bcpvztt_central_table_row_step) = S ((S (bcf_predecessor_bcpvztt_central_table_row_step)) * bcf_previous_scale_bcpvztt_central_table)) /\ exists bcf_quotient_bcpvztt_central_table_row_step_previous_left. bcf_previous_code_bcpvztt_central_table = bcf_quotient_bcpvztt_central_table_row_step_previous_left * S ((S (bcf_predecessor_bcpvztt_central_table_row_step)) * bcf_previous_scale_bcpvztt_central_table) + (bcf_left_bcpvztt_central_table_row_step))) /\ ((((exists bcf_height_bcpvztt_central_table_row_step_previous_right. bcf_height_bcpvztt_central_table_row_step_previous_right + S (bcf_right_bcpvztt_central_table_row_step) = S ((S (S (bcf_predecessor_bcpvztt_central_table_row_step))) * bcf_previous_scale_bcpvztt_central_table)) /\ exists bcf_quotient_bcpvztt_central_table_row_step_previous_right. bcf_previous_code_bcpvztt_central_table = bcf_quotient_bcpvztt_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcpvztt_central_table_row_step))) * bcf_previous_scale_bcpvztt_central_table) + (bcf_right_bcpvztt_central_table_row_step))) /\ bcf_value_bcpvztt_central_table_row_step = bcf_left_bcpvztt_central_table_row_step + bcf_right_bcpvztt_central_table_row_step))))))))))) /\ ((((exists bcf_height_bcpvztt_central_decoded_row_code. bcf_height_bcpvztt_central_decoded_row_code + S (bcf_row_code_bcpvztt_central) = S ((S (n + n)) * bcf_row_code_scale_bcpvztt_central)) /\ exists bcf_quotient_bcpvztt_central_decoded_row_code. bcf_row_code_code_bcpvztt_central = bcf_quotient_bcpvztt_central_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bcpvztt_central) + (bcf_row_code_bcpvztt_central))) /\ ((((exists bcf_height_bcpvztt_central_decoded_row_scale. bcf_height_bcpvztt_central_decoded_row_scale + S (bcf_row_scale_bcpvztt_central) = S ((S (n + n)) * bcf_row_scale_scale_bcpvztt_central)) /\ exists bcf_quotient_bcpvztt_central_decoded_row_scale. bcf_row_scale_code_bcpvztt_central = bcf_quotient_bcpvztt_central_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bcpvztt_central) + (bcf_row_scale_bcpvztt_central))) /\ (((exists bcf_height_bcpvztt_central_decoded_value. bcf_height_bcpvztt_central_decoded_value + S (C) = S ((S (n)) * bcf_row_scale_bcpvztt_central)) /\ exists bcf_quotient_bcpvztt_central_decoded_value. bcf_row_code_bcpvztt_central = bcf_quotient_bcpvztt_central_decoded_value * S ((S (n)) * bcf_row_scale_bcpvztt_central) + (C))))))))) -> (((exists bpv_gap_bcpvztt_valuation_exponent_bound. bpv_gap_bcpvztt_valuation_exponent_bound + v = C) /\ (exists bpv_result_bcpvztt_valuation_selected. ((exists ff_b_bcpvztt_valuation_selected_power ff_c_bcpvztt_valuation_selected_power. ((forall ff_i_bcpvztt_valuation_selected_power_repeat. (exists ff_lt_bcpvztt_valuation_selected_power_repeat_bound. ff_lt_bcpvztt_valuation_selected_power_repeat_bound + S ff_i_bcpvztt_valuation_selected_power_repeat = v) -> (((exists ff_h_bcpvztt_valuation_selected_power_repeat_decoded. ff_h_bcpvztt_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bcpvztt_valuation_selected_power_repeat)) * ff_c_bcpvztt_valuation_selected_power)) /\ exists ff_q_bcpvztt_valuation_selected_power_repeat_decoded. ff_b_bcpvztt_valuation_selected_power = ff_q_bcpvztt_valuation_selected_power_repeat_decoded * S ((S (ff_i_bcpvztt_valuation_selected_power_repeat)) * ff_c_bcpvztt_valuation_selected_power) + (p)))) /\ (exists ff_u_bcpvztt_valuation_selected_power_product ff_v_bcpvztt_valuation_selected_power_product. ((((exists ff_h_bcpvztt_valuation_selected_power_product_start. ff_h_bcpvztt_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bcpvztt_valuation_selected_power_product)) /\ exists ff_q_bcpvztt_valuation_selected_power_product_start. ff_u_bcpvztt_valuation_selected_power_product = ff_q_bcpvztt_valuation_selected_power_product_start * S ((S (0)) * ff_v_bcpvztt_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bcpvztt_valuation_selected_power_product_terminal. ff_h_bcpvztt_valuation_selected_power_product_terminal + S (bpv_result_bcpvztt_valuation_selected) = S ((S (v)) * ff_v_bcpvztt_valuation_selected_power_product)) /\ exists ff_q_bcpvztt_valuation_selected_power_product_terminal. ff_u_bcpvztt_valuation_selected_power_product = ff_q_bcpvztt_valuation_selected_power_product_terminal * S ((S (v)) * ff_v_bcpvztt_valuation_selected_power_product) + (bpv_result_bcpvztt_valuation_selected))) /\ forall ff_i_bcpvztt_valuation_selected_power_product. (exists ff_lt_bcpvztt_valuation_selected_power_product_bound. ff_lt_bcpvztt_valuation_selected_power_product_bound + S ff_i_bcpvztt_valuation_selected_power_product = v) -> exists ff_p_bcpvztt_valuation_selected_power_product ff_r_bcpvztt_valuation_selected_power_product ff_s_bcpvztt_valuation_selected_power_product. ((((exists ff_h_bcpvztt_valuation_selected_power_product_factor. ff_h_bcpvztt_valuation_selected_power_product_factor + S (ff_p_bcpvztt_valuation_selected_power_product) = S ((S (ff_i_bcpvztt_valuation_selected_power_product)) * ff_c_bcpvztt_valuation_selected_power)) /\ exists ff_q_bcpvztt_valuation_selected_power_product_factor. ff_b_bcpvztt_valuation_selected_power = ff_q_bcpvztt_valuation_selected_power_product_factor * S ((S (ff_i_bcpvztt_valuation_selected_power_product)) * ff_c_bcpvztt_valuation_selected_power) + (ff_p_bcpvztt_valuation_selected_power_product))) /\ ((((exists ff_h_bcpvztt_valuation_selected_power_product_partial. ff_h_bcpvztt_valuation_selected_power_product_partial + S (ff_r_bcpvztt_valuation_selected_power_product) = S ((S (ff_i_bcpvztt_valuation_selected_power_product)) * ff_v_bcpvztt_valuation_selected_power_product)) /\ exists ff_q_bcpvztt_valuation_selected_power_product_partial. ff_u_bcpvztt_valuation_selected_power_product = ff_q_bcpvztt_valuation_selected_power_product_partial * S ((S (ff_i_bcpvztt_valuation_selected_power_product)) * ff_v_bcpvztt_valuation_selected_power_product) + (ff_r_bcpvztt_valuation_selected_power_product))) /\ ((((exists ff_h_bcpvztt_valuation_selected_power_product_successor. ff_h_bcpvztt_valuation_selected_power_product_successor + S (ff_s_bcpvztt_valuation_selected_power_product) = S ((S (S ff_i_bcpvztt_valuation_selected_power_product)) * ff_v_bcpvztt_valuation_selected_power_product)) /\ exists ff_q_bcpvztt_valuation_selected_power_product_successor. ff_u_bcpvztt_valuation_selected_power_product = ff_q_bcpvztt_valuation_selected_power_product_successor * S ((S (S ff_i_bcpvztt_valuation_selected_power_product)) * ff_v_bcpvztt_valuation_selected_power_product) + (ff_s_bcpvztt_valuation_selected_power_product))) /\ ff_s_bcpvztt_valuation_selected_power_product = ff_r_bcpvztt_valuation_selected_power_product * ff_p_bcpvztt_valuation_selected_power_product)))))))) /\ (exists bpv_factor_bcpvztt_valuation_selected_divides. C = bpv_result_bcpvztt_valuation_selected * bpv_factor_bcpvztt_valuation_selected_divides)))) /\ forall bpv_candidate_bcpvztt_valuation. (exists bpv_gap_bcpvztt_valuation_candidate_bound. bpv_gap_bcpvztt_valuation_candidate_bound + bpv_candidate_bcpvztt_valuation = C) -> (exists bpv_result_bcpvztt_valuation_candidate. ((exists ff_b_bcpvztt_valuation_candidate_power ff_c_bcpvztt_valuation_candidate_power. ((forall ff_i_bcpvztt_valuation_candidate_power_repeat. (exists ff_lt_bcpvztt_valuation_candidate_power_repeat_bound. ff_lt_bcpvztt_valuation_candidate_power_repeat_bound + S ff_i_bcpvztt_valuation_candidate_power_repeat = bpv_candidate_bcpvztt_valuation) -> (((exists ff_h_bcpvztt_valuation_candidate_power_repeat_decoded. ff_h_bcpvztt_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bcpvztt_valuation_candidate_power_repeat)) * ff_c_bcpvztt_valuation_candidate_power)) /\ exists ff_q_bcpvztt_valuation_candidate_power_repeat_decoded. ff_b_bcpvztt_valuation_candidate_power = ff_q_bcpvztt_valuation_candidate_power_repeat_decoded * S ((S (ff_i_bcpvztt_valuation_candidate_power_repeat)) * ff_c_bcpvztt_valuation_candidate_power) + (p)))) /\ (exists ff_u_bcpvztt_valuation_candidate_power_product ff_v_bcpvztt_valuation_candidate_power_product. ((((exists ff_h_bcpvztt_valuation_candidate_power_product_start. ff_h_bcpvztt_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bcpvztt_valuation_candidate_power_product)) /\ exists ff_q_bcpvztt_valuation_candidate_power_product_start. ff_u_bcpvztt_valuation_candidate_power_product = ff_q_bcpvztt_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bcpvztt_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bcpvztt_valuation_candidate_power_product_terminal. ff_h_bcpvztt_valuation_candidate_power_product_terminal + S (bpv_result_bcpvztt_valuation_candidate) = S ((S (bpv_candidate_bcpvztt_valuation)) * ff_v_bcpvztt_valuation_candidate_power_product)) /\ exists ff_q_bcpvztt_valuation_candidate_power_product_terminal. ff_u_bcpvztt_valuation_candidate_power_product = ff_q_bcpvztt_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_bcpvztt_valuation)) * ff_v_bcpvztt_valuation_candidate_power_product) + (bpv_result_bcpvztt_valuation_candidate))) /\ forall ff_i_bcpvztt_valuation_candidate_power_product. (exists ff_lt_bcpvztt_valuation_candidate_power_product_bound. ff_lt_bcpvztt_valuation_candidate_power_product_bound + S ff_i_bcpvztt_valuation_candidate_power_product = bpv_candidate_bcpvztt_valuation) -> exists ff_p_bcpvztt_valuation_candidate_power_product ff_r_bcpvztt_valuation_candidate_power_product ff_s_bcpvztt_valuation_candidate_power_product. ((((exists ff_h_bcpvztt_valuation_candidate_power_product_factor. ff_h_bcpvztt_valuation_candidate_power_product_factor + S (ff_p_bcpvztt_valuation_candidate_power_product) = S ((S (ff_i_bcpvztt_valuation_candidate_power_product)) * ff_c_bcpvztt_valuation_candidate_power)) /\ exists ff_q_bcpvztt_valuation_candidate_power_product_factor. ff_b_bcpvztt_valuation_candidate_power = ff_q_bcpvztt_valuation_candidate_power_product_factor * S ((S (ff_i_bcpvztt_valuation_candidate_power_product)) * ff_c_bcpvztt_valuation_candidate_power) + (ff_p_bcpvztt_valuation_candidate_power_product))) /\ ((((exists ff_h_bcpvztt_valuation_candidate_power_product_partial. ff_h_bcpvztt_valuation_candidate_power_product_partial + S (ff_r_bcpvztt_valuation_candidate_power_product) = S ((S (ff_i_bcpvztt_valuation_candidate_power_product)) * ff_v_bcpvztt_valuation_candidate_power_product)) /\ exists ff_q_bcpvztt_valuation_candidate_power_product_partial. ff_u_bcpvztt_valuation_candidate_power_product = ff_q_bcpvztt_valuation_candidate_power_product_partial * S ((S (ff_i_bcpvztt_valuation_candidate_power_product)) * ff_v_bcpvztt_valuation_candidate_power_product) + (ff_r_bcpvztt_valuation_candidate_power_product))) /\ ((((exists ff_h_bcpvztt_valuation_candidate_power_product_successor. ff_h_bcpvztt_valuation_candidate_power_product_successor + S (ff_s_bcpvztt_valuation_candidate_power_product) = S ((S (S ff_i_bcpvztt_valuation_candidate_power_product)) * ff_v_bcpvztt_valuation_candidate_power_product)) /\ exists ff_q_bcpvztt_valuation_candidate_power_product_successor. ff_u_bcpvztt_valuation_candidate_power_product = ff_q_bcpvztt_valuation_candidate_power_product_successor * S ((S (S ff_i_bcpvztt_valuation_candidate_power_product)) * ff_v_bcpvztt_valuation_candidate_power_product) + (ff_s_bcpvztt_valuation_candidate_power_product))) /\ ff_s_bcpvztt_valuation_candidate_power_product = ff_r_bcpvztt_valuation_candidate_power_product * ff_p_bcpvztt_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_bcpvztt_valuation_candidate_divides. C = bpv_result_bcpvztt_valuation_candidate * bpv_factor_bcpvztt_valuation_candidate_divides))) -> (exists bpv_gap_bcpvztt_valuation_maximal. bpv_gap_bcpvztt_valuation_maximal + bpv_candidate_bcpvztt_valuation = v)) -> v = 0

Proof neighborhood

Direct theorem prerequisites

BT0080 pow_exists BT00YA prime_square_tail_of_two_three_range BT00YB division_first_two_of_two_three_range BT003G prime_nonzero BT0010 one_le_of_ne_zero BT00YD central_binom_prime_valuation_zero_of_exact_double_quotients

Direct theorem dependents

BT00YG central_binom_prime_valuation_zero_above_third_quotient

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

65 script commands · 12 reading checkpoints · 7 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 (6)
pow existsprime square tail of two three rangedivision first two of two three rangeprime nonzeroone le of ne zerocentral binom prime valuation zero of exact double quotients
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro C
  4. L4
    intro v
  5. L5
    intro hp
  6. L6
    intro hpositive
  7. L7
    intro hlower
  8. L8
    intro hscaled
  9. L9
    intro hcentral
  10. L10
    intro hvaluation
02Establish hsquareL11–14

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

  1. L11
    have hsquare : ∃ s. Pow(p,2,s)Definitions: Pow(p,2,s)Original native command in the exact edition
  2. L12
    specialize pow_exists p
  3. L13
    specialize pow_exists 2
  4. L14
    exact pow_exists
03Separate the logical casesL15–15

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

  1. L15
    cases hsquare
04Establish hstrictL16–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime square tail of two three range.

  1. L16
    have hstrict : Lt(n + n,x)Definitions: Lt(n + n,x)Original native command in the exact edition
  2. L17
    specialize prime_square_tail_of_two_three_range p
  3. L18
    specialize prime_square_tail_of_two_three_range n
  4. L19
    specialize prime_square_tail_of_two_three_range x
  5. L20
    apply prime_square_tail_of_two_three_range
  6. L21
    exact hp
  7. L22
    exact hpositive
  8. L23
    exact hscaled
  9. L24
    exact hsquare_witness
05Establish hquotientsL25–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division first two of two three range.

  1. L25
    have hquotients : ∃ r. ∃ R. DivRem(n,p,1,r) ∧ DivRem(n + n,p,2,R)Definitions: DivRem(n,p,1,r)DivRem(n + n,p,2,R)Original native command in the exact edition
  2. L26
    specialize division_first_two_of_two_three_range p
  3. L27
    specialize division_first_two_of_two_three_range n
  4. L28
    apply division_first_two_of_two_three_range
  5. L29
    exact hlower
  6. L30
    exact hscaled
06Separate the logical casesL31–33

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

  1. L31
    cases hquotients
  2. L32
    cases hquotients_witness
  3. L33
    cases hquotients_witness_witness
07Establish hp_nonzeroL34–39

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

  1. L34
    have hp_nonzero : ~(p = 0)
  2. L35
    intro hpzero
  3. L36
    specialize prime_nonzero p
  4. L37
    apply prime_nonzero
  5. L38
    exact hp
  6. L39
    exact hpzero
08Establish hbaseL40–43

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

  1. L40
  2. L41
    specialize one_le_of_ne_zero p
  3. L42
    apply one_le_of_ne_zero
  4. L43
    exact hp_nonzero
09Establish hdouble_alignedL44–44

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

  1. L44
    have hdouble_aligned : DivRem(n + n,p,1 + 1,x2)Definitions: DivRem(n + n,p,1 + 1,x2)Original native command in the exact edition
10Establish htwoL45–54

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

  1. L45
    have htwo : 2 = 1 + 1
  2. L46
    norm_num
  3. L47
    rewrite <- htwo
  4. L48
    exact hquotients_witness_witness_right
  5. L49
    specialize central_binom_prime_valuation_zero_of_exact_double_quotients p
  6. L50
    specialize central_binom_prime_valuation_zero_of_exact_double_quotients n
  7. L51
    specialize central_binom_prime_valuation_zero_of_exact_double_quotients C
  8. L52
    specialize central_binom_prime_valuation_zero_of_exact_double_quotients v
  9. L53
    specialize central_binom_prime_valuation_zero_of_exact_double_quotients 1
  10. L54
    specialize central_binom_prime_valuation_zero_of_exact_double_quotients x1
11Use earlier factsL55–64

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

  1. L55
    specialize central_binom_prime_valuation_zero_of_exact_double_quotients x2
  2. L56
    specialize central_binom_prime_valuation_zero_of_exact_double_quotients x
  3. L57
    apply central_binom_prime_valuation_zero_of_exact_double_quotients
  4. L58
    exact hp
  5. L59
    exact hcentral
  6. L60
    exact hvaluation
  7. L61
    exact hbase
  8. L62
    exact hsquare_witness
  9. L63
    exact hstrict
  10. L64
    exact hquotients_witness_witness_left
12Use earlier factsL65–65

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

  1. L65
    exact hdouble_aligned

Library-wide reading audit

Original defined command ledger · 65 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro C
  4. 0004intro v
  5. 0005intro hp
  6. 0006intro hpositive
  7. 0007intro hlower
  8. 0008intro hscaled
  9. 0009intro hcentral
  10. 0010intro hvaluation
  11. 0011have hsquare : ∃ s. Pow(p,2,s)
    Exact native replay linehave hsquare : exists s. exists bpvi_b_bcpvztt_square bpvi_c_bcpvztt_square. ((forall bpvi_i_bcpvztt_square. (exists bpvi_repeat_gap_bcpvztt_square. bpvi_repeat_gap_bcpvztt_square + S bpvi_i_bcpvztt_square = 2) -> (((exists bpvi_h_bcpvztt_square_repeat. bpvi_h_bcpvztt_square_repeat + S (p) = S ((S (bpvi_i_bcpvztt_square)) * bpvi_c_bcpvztt_square)) /\ exists bpvi_q_bcpvztt_square_repeat. bpvi_b_bcpvztt_square = bpvi_q_bcpvztt_square_repeat * S ((S (bpvi_i_bcpvztt_square)) * bpvi_c_bcpvztt_square) + (p)))) /\ (exists bpvi_u_bcpvztt_square bpvi_v_bcpvztt_square. ((((exists bpvi_h_bcpvztt_square_start. bpvi_h_bcpvztt_square_start + S (1) = S ((S (0)) * bpvi_v_bcpvztt_square)) /\ exists bpvi_q_bcpvztt_square_start. bpvi_u_bcpvztt_square = bpvi_q_bcpvztt_square_start * S ((S (0)) * bpvi_v_bcpvztt_square) + (1))) /\ ((((exists bpvi_h_bcpvztt_square_terminal. bpvi_h_bcpvztt_square_terminal + S (s) = S ((S (2)) * bpvi_v_bcpvztt_square)) /\ exists bpvi_q_bcpvztt_square_terminal. bpvi_u_bcpvztt_square = bpvi_q_bcpvztt_square_terminal * S ((S (2)) * bpvi_v_bcpvztt_square) + (s))) /\ forall bpvi_j_bcpvztt_square. (exists bpvi_product_gap_bcpvztt_square. bpvi_product_gap_bcpvztt_square + S bpvi_j_bcpvztt_square = 2) -> exists bpvi_factor_bcpvztt_square bpvi_partial_bcpvztt_square bpvi_successor_bcpvztt_square. ((((exists bpvi_h_bcpvztt_square_factor. bpvi_h_bcpvztt_square_factor + S (bpvi_factor_bcpvztt_square) = S ((S (bpvi_j_bcpvztt_square)) * bpvi_c_bcpvztt_square)) /\ exists bpvi_q_bcpvztt_square_factor. bpvi_b_bcpvztt_square = bpvi_q_bcpvztt_square_factor * S ((S (bpvi_j_bcpvztt_square)) * bpvi_c_bcpvztt_square) + (bpvi_factor_bcpvztt_square))) /\ ((((exists bpvi_h_bcpvztt_square_partial. bpvi_h_bcpvztt_square_partial + S (bpvi_partial_bcpvztt_square) = S ((S (bpvi_j_bcpvztt_square)) * bpvi_v_bcpvztt_square)) /\ exists bpvi_q_bcpvztt_square_partial. bpvi_u_bcpvztt_square = bpvi_q_bcpvztt_square_partial * S ((S (bpvi_j_bcpvztt_square)) * bpvi_v_bcpvztt_square) + (bpvi_partial_bcpvztt_square))) /\ ((((exists bpvi_h_bcpvztt_square_successor. bpvi_h_bcpvztt_square_successor + S (bpvi_successor_bcpvztt_square) = S ((S (S bpvi_j_bcpvztt_square)) * bpvi_v_bcpvztt_square)) /\ exists bpvi_q_bcpvztt_square_successor. bpvi_u_bcpvztt_square = bpvi_q_bcpvztt_square_successor * S ((S (S bpvi_j_bcpvztt_square)) * bpvi_v_bcpvztt_square) + (bpvi_successor_bcpvztt_square))) /\ bpvi_successor_bcpvztt_square = bpvi_partial_bcpvztt_square * bpvi_factor_bcpvztt_square)))))))
  12. 0012specialize pow_exists p
  13. 0013specialize pow_exists 2
  14. 0014exact pow_exists
  15. 0015cases hsquare
  16. 0016have hstrict : Lt(n + n,x)
    Exact native replay linehave hstrict : exists bcf_lt_gap_bcpvztt_square_strict. bcf_lt_gap_bcpvztt_square_strict + S (n + n) = x
  17. 0017specialize prime_square_tail_of_two_three_range p
  18. 0018specialize prime_square_tail_of_two_three_range n
  19. 0019specialize prime_square_tail_of_two_three_range x
  20. 0020apply prime_square_tail_of_two_three_range
  21. 0021exact hp
  22. 0022exact hpositive
  23. 0023exact hscaled
  24. 0024exact hsquare_witness
  25. 0025have hquotients : ∃ r. ∃ R. DivRem(n,p,1,r) ∧ DivRem(n + n,p,2,R)
    Exact native replay linehave hquotients : exists r R. (((n) = (p) * (1) + (r) /\ (exists bcf_lt_gap_bdftt_left_bound. bcf_lt_gap_bdftt_left_bound + S (r) = p))) /\ (((n + n) = (p) * (2) + (R) /\ (exists bcf_lt_gap_bdftt_right_bound. bcf_lt_gap_bdftt_right_bound + S (R) = p)))
  26. 0026specialize division_first_two_of_two_three_range p
  27. 0027specialize division_first_two_of_two_three_range n
  28. 0028apply division_first_two_of_two_three_range
  29. 0029exact hlower
  30. 0030exact hscaled
  31. 0031cases hquotients
  32. 0032cases hquotients_witness
  33. 0033cases hquotients_witness_witness
  34. 0034have hp_nonzero : ~(p = 0)
  35. 0035intro hpzero
  36. 0036specialize prime_nonzero p
  37. 0037apply prime_nonzero
  38. 0038exact hp
  39. 0039exact hpzero
  40. 0040have hbase : Lt(0,p)
    Exact native replay linehave hbase : exists bcf_le_gap_bcpvzeq_base. bcf_le_gap_bcpvzeq_base + (1) = p
  41. 0041specialize one_le_of_ne_zero p
  42. 0042apply one_le_of_ne_zero
  43. 0043exact hp_nonzero
  44. 0044have hdouble_aligned : DivRem(n + n,p,1 + 1,x2)
    Exact native replay linehave hdouble_aligned : ((n + n) = (p) * (1 + 1) + (x2) /\ (exists bcf_lt_gap_bcpvztt_double_aligned_bound. bcf_lt_gap_bcpvztt_double_aligned_bound + S (x2) = p))
  45. 0045have htwo : 2 = 1 + 1
  46. 0046norm_num
  47. 0047rewrite <- htwo
  48. 0048exact hquotients_witness_witness_right
  49. 0049specialize central_binom_prime_valuation_zero_of_exact_double_quotients p
  50. 0050specialize central_binom_prime_valuation_zero_of_exact_double_quotients n
  51. 0051specialize central_binom_prime_valuation_zero_of_exact_double_quotients C
  52. 0052specialize central_binom_prime_valuation_zero_of_exact_double_quotients v
  53. 0053specialize central_binom_prime_valuation_zero_of_exact_double_quotients 1
  54. 0054specialize central_binom_prime_valuation_zero_of_exact_double_quotients x1
  55. 0055specialize central_binom_prime_valuation_zero_of_exact_double_quotients x2
  56. 0056specialize central_binom_prime_valuation_zero_of_exact_double_quotients x
  57. 0057apply central_binom_prime_valuation_zero_of_exact_double_quotients
  58. 0058exact hp
  59. 0059exact hcentral
  60. 0060exact hvaluation
  61. 0061exact hbase
  62. 0062exact hsquare_witness
  63. 0063exact hstrict
  64. 0064exact hquotients_witness_witness_left
  65. 0065exact hdouble_aligned