BT00VI · Bertrand theorem

primorial_even_interval_le_central

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

The even Primorial interval is bounded by the central coefficient.

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

Statement with defined notation

∀ n. ∀ z. ∀ c. (∃ x. ∃ y. (∀ m. Lt(m,n) → ∃ k. BetaAt(x,y,m,k) ∧ (Prime(S (n + m)) ∧ k = S (n + m) ∨ ¬Prime(S (n + m)) ∧ k = 1)) ∧ Product(x,y,n,z)) → CentralBinom(n,c) → Le(z,c)

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 PD0013 BetaAt PD0014 Product PD0042 CentralBinom

7 occurrences

In local proof propositions

PD0003 Dvd

1 occurrences

Exact expanded native-PA statement
forall n z c. (exists bpr_code_bpeidc_interval bpr_scale_bpeidc_interval. ((forall bpr_index_bpeidc_interval_mask. (exists bpr_gap_bpeidc_interval_mask_bound. bpr_gap_bpeidc_interval_mask_bound + S (bpr_index_bpeidc_interval_mask) = n) -> exists bpr_value_bpeidc_interval_mask. ((((exists bpr_height_bpeidc_interval_mask_decoded. bpr_height_bpeidc_interval_mask_decoded + S (bpr_value_bpeidc_interval_mask) = S ((S (bpr_index_bpeidc_interval_mask)) * bpr_scale_bpeidc_interval)) /\ exists bpr_quotient_bpeidc_interval_mask_decoded. bpr_code_bpeidc_interval = bpr_quotient_bpeidc_interval_mask_decoded * S ((S (bpr_index_bpeidc_interval_mask)) * bpr_scale_bpeidc_interval) + (bpr_value_bpeidc_interval_mask))) /\ (((((~(S (n + bpr_index_bpeidc_interval_mask) = 1) /\ forall bpr_left_bpeidc_interval_mask_choice_prime bpr_right_bpeidc_interval_mask_choice_prime. S (n + bpr_index_bpeidc_interval_mask) = bpr_left_bpeidc_interval_mask_choice_prime * bpr_right_bpeidc_interval_mask_choice_prime -> bpr_left_bpeidc_interval_mask_choice_prime = 1 \/ bpr_right_bpeidc_interval_mask_choice_prime = 1)) /\ bpr_value_bpeidc_interval_mask = S (n + bpr_index_bpeidc_interval_mask)) \/ (~((~(S (n + bpr_index_bpeidc_interval_mask) = 1) /\ forall bpr_left_bpeidc_interval_mask_choice_prime bpr_right_bpeidc_interval_mask_choice_prime. S (n + bpr_index_bpeidc_interval_mask) = bpr_left_bpeidc_interval_mask_choice_prime * bpr_right_bpeidc_interval_mask_choice_prime -> bpr_left_bpeidc_interval_mask_choice_prime = 1 \/ bpr_right_bpeidc_interval_mask_choice_prime = 1)) /\ bpr_value_bpeidc_interval_mask = 1))))) /\ (exists ff_u_bpeidc_interval_product ff_v_bpeidc_interval_product. ((((exists ff_h_bpeidc_interval_product_start. ff_h_bpeidc_interval_product_start + S (1) = S ((S (0)) * ff_v_bpeidc_interval_product)) /\ exists ff_q_bpeidc_interval_product_start. ff_u_bpeidc_interval_product = ff_q_bpeidc_interval_product_start * S ((S (0)) * ff_v_bpeidc_interval_product) + (1))) /\ ((((exists ff_h_bpeidc_interval_product_terminal. ff_h_bpeidc_interval_product_terminal + S (z) = S ((S (n)) * ff_v_bpeidc_interval_product)) /\ exists ff_q_bpeidc_interval_product_terminal. ff_u_bpeidc_interval_product = ff_q_bpeidc_interval_product_terminal * S ((S (n)) * ff_v_bpeidc_interval_product) + (z))) /\ forall ff_i_bpeidc_interval_product. (exists ff_lt_bpeidc_interval_product_bound. ff_lt_bpeidc_interval_product_bound + S ff_i_bpeidc_interval_product = n) -> exists ff_p_bpeidc_interval_product ff_r_bpeidc_interval_product ff_s_bpeidc_interval_product. ((((exists ff_h_bpeidc_interval_product_factor. ff_h_bpeidc_interval_product_factor + S (ff_p_bpeidc_interval_product) = S ((S (ff_i_bpeidc_interval_product)) * bpr_scale_bpeidc_interval)) /\ exists ff_q_bpeidc_interval_product_factor. bpr_code_bpeidc_interval = ff_q_bpeidc_interval_product_factor * S ((S (ff_i_bpeidc_interval_product)) * bpr_scale_bpeidc_interval) + (ff_p_bpeidc_interval_product))) /\ ((((exists ff_h_bpeidc_interval_product_partial. ff_h_bpeidc_interval_product_partial + S (ff_r_bpeidc_interval_product) = S ((S (ff_i_bpeidc_interval_product)) * ff_v_bpeidc_interval_product)) /\ exists ff_q_bpeidc_interval_product_partial. ff_u_bpeidc_interval_product = ff_q_bpeidc_interval_product_partial * S ((S (ff_i_bpeidc_interval_product)) * ff_v_bpeidc_interval_product) + (ff_r_bpeidc_interval_product))) /\ ((((exists ff_h_bpeidc_interval_product_successor. ff_h_bpeidc_interval_product_successor + S (ff_s_bpeidc_interval_product) = S ((S (S ff_i_bpeidc_interval_product)) * ff_v_bpeidc_interval_product)) /\ exists ff_q_bpeidc_interval_product_successor. ff_u_bpeidc_interval_product = ff_q_bpeidc_interval_product_successor * S ((S (S ff_i_bpeidc_interval_product)) * ff_v_bpeidc_interval_product) + (ff_s_bpeidc_interval_product))) /\ ff_s_bpeidc_interval_product = ff_r_bpeidc_interval_product * ff_p_bpeidc_interval_product)))))))) -> (((exists bcf_lt_gap_bpeidc_central_out_of_range. bcf_lt_gap_bpeidc_central_out_of_range + S (n + n) = n) /\ c = 0) \/ ((exists bcf_le_gap_bpeidc_central_in_range. bcf_le_gap_bpeidc_central_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bpeidc_central bcf_row_code_scale_bpeidc_central bcf_row_scale_code_bpeidc_central bcf_row_scale_scale_bpeidc_central bcf_row_code_bpeidc_central bcf_row_scale_bpeidc_central. ((forall bcf_row_index_bpeidc_central_table. (exists bcf_lt_gap_bpeidc_central_table_row_bound. bcf_lt_gap_bpeidc_central_table_row_bound + S (bcf_row_index_bpeidc_central_table) = S (n + n)) -> exists bcf_row_code_bpeidc_central_table bcf_row_scale_bpeidc_central_table. ((((exists bcf_height_bpeidc_central_table_decoded_row_code. bcf_height_bpeidc_central_table_decoded_row_code + S (bcf_row_code_bpeidc_central_table) = S ((S (bcf_row_index_bpeidc_central_table)) * bcf_row_code_scale_bpeidc_central)) /\ exists bcf_quotient_bpeidc_central_table_decoded_row_code. bcf_row_code_code_bpeidc_central = bcf_quotient_bpeidc_central_table_decoded_row_code * S ((S (bcf_row_index_bpeidc_central_table)) * bcf_row_code_scale_bpeidc_central) + (bcf_row_code_bpeidc_central_table))) /\ ((((exists bcf_height_bpeidc_central_table_decoded_row_scale. bcf_height_bpeidc_central_table_decoded_row_scale + S (bcf_row_scale_bpeidc_central_table) = S ((S (bcf_row_index_bpeidc_central_table)) * bcf_row_scale_scale_bpeidc_central)) /\ exists bcf_quotient_bpeidc_central_table_decoded_row_scale. bcf_row_scale_code_bpeidc_central = bcf_quotient_bpeidc_central_table_decoded_row_scale * S ((S (bcf_row_index_bpeidc_central_table)) * bcf_row_scale_scale_bpeidc_central) + (bcf_row_scale_bpeidc_central_table))) /\ ((bcf_row_index_bpeidc_central_table = 0 /\ (forall bcf_index_bpeidc_central_table_zero_row. (exists bcf_lt_gap_bpeidc_central_table_zero_row_bound. bcf_lt_gap_bpeidc_central_table_zero_row_bound + S (bcf_index_bpeidc_central_table_zero_row) = S (n + n)) -> exists bcf_value_bpeidc_central_table_zero_row. ((((exists bcf_height_bpeidc_central_table_zero_row_entry. bcf_height_bpeidc_central_table_zero_row_entry + S (bcf_value_bpeidc_central_table_zero_row) = S ((S (bcf_index_bpeidc_central_table_zero_row)) * bcf_row_scale_bpeidc_central_table)) /\ exists bcf_quotient_bpeidc_central_table_zero_row_entry. bcf_row_code_bpeidc_central_table = bcf_quotient_bpeidc_central_table_zero_row_entry * S ((S (bcf_index_bpeidc_central_table_zero_row)) * bcf_row_scale_bpeidc_central_table) + (bcf_value_bpeidc_central_table_zero_row))) /\ ((bcf_index_bpeidc_central_table_zero_row = 0 /\ bcf_value_bpeidc_central_table_zero_row = 1) \/ exists bcf_predecessor_bpeidc_central_table_zero_row. bcf_index_bpeidc_central_table_zero_row = S bcf_predecessor_bpeidc_central_table_zero_row /\ bcf_value_bpeidc_central_table_zero_row = 0)))) \/ exists bcf_predecessor_bpeidc_central_table bcf_previous_code_bpeidc_central_table bcf_previous_scale_bpeidc_central_table. bcf_row_index_bpeidc_central_table = S bcf_predecessor_bpeidc_central_table /\ ((((exists bcf_height_bpeidc_central_table_decoded_previous_code. bcf_height_bpeidc_central_table_decoded_previous_code + S (bcf_previous_code_bpeidc_central_table) = S ((S (bcf_predecessor_bpeidc_central_table)) * bcf_row_code_scale_bpeidc_central)) /\ exists bcf_quotient_bpeidc_central_table_decoded_previous_code. bcf_row_code_code_bpeidc_central = bcf_quotient_bpeidc_central_table_decoded_previous_code * S ((S (bcf_predecessor_bpeidc_central_table)) * bcf_row_code_scale_bpeidc_central) + (bcf_previous_code_bpeidc_central_table))) /\ ((((exists bcf_height_bpeidc_central_table_decoded_previous_scale. bcf_height_bpeidc_central_table_decoded_previous_scale + S (bcf_previous_scale_bpeidc_central_table) = S ((S (bcf_predecessor_bpeidc_central_table)) * bcf_row_scale_scale_bpeidc_central)) /\ exists bcf_quotient_bpeidc_central_table_decoded_previous_scale. bcf_row_scale_code_bpeidc_central = bcf_quotient_bpeidc_central_table_decoded_previous_scale * S ((S (bcf_predecessor_bpeidc_central_table)) * bcf_row_scale_scale_bpeidc_central) + (bcf_previous_scale_bpeidc_central_table))) /\ (forall bcf_index_bpeidc_central_table_row_step. (exists bcf_lt_gap_bpeidc_central_table_row_step_bound. bcf_lt_gap_bpeidc_central_table_row_step_bound + S (bcf_index_bpeidc_central_table_row_step) = S (n + n)) -> exists bcf_value_bpeidc_central_table_row_step. ((((exists bcf_height_bpeidc_central_table_row_step_entry. bcf_height_bpeidc_central_table_row_step_entry + S (bcf_value_bpeidc_central_table_row_step) = S ((S (bcf_index_bpeidc_central_table_row_step)) * bcf_row_scale_bpeidc_central_table)) /\ exists bcf_quotient_bpeidc_central_table_row_step_entry. bcf_row_code_bpeidc_central_table = bcf_quotient_bpeidc_central_table_row_step_entry * S ((S (bcf_index_bpeidc_central_table_row_step)) * bcf_row_scale_bpeidc_central_table) + (bcf_value_bpeidc_central_table_row_step))) /\ ((bcf_index_bpeidc_central_table_row_step = 0 /\ bcf_value_bpeidc_central_table_row_step = 1) \/ exists bcf_predecessor_bpeidc_central_table_row_step bcf_left_bpeidc_central_table_row_step bcf_right_bpeidc_central_table_row_step. bcf_index_bpeidc_central_table_row_step = S bcf_predecessor_bpeidc_central_table_row_step /\ ((((exists bcf_height_bpeidc_central_table_row_step_previous_left. bcf_height_bpeidc_central_table_row_step_previous_left + S (bcf_left_bpeidc_central_table_row_step) = S ((S (bcf_predecessor_bpeidc_central_table_row_step)) * bcf_previous_scale_bpeidc_central_table)) /\ exists bcf_quotient_bpeidc_central_table_row_step_previous_left. bcf_previous_code_bpeidc_central_table = bcf_quotient_bpeidc_central_table_row_step_previous_left * S ((S (bcf_predecessor_bpeidc_central_table_row_step)) * bcf_previous_scale_bpeidc_central_table) + (bcf_left_bpeidc_central_table_row_step))) /\ ((((exists bcf_height_bpeidc_central_table_row_step_previous_right. bcf_height_bpeidc_central_table_row_step_previous_right + S (bcf_right_bpeidc_central_table_row_step) = S ((S (S (bcf_predecessor_bpeidc_central_table_row_step))) * bcf_previous_scale_bpeidc_central_table)) /\ exists bcf_quotient_bpeidc_central_table_row_step_previous_right. bcf_previous_code_bpeidc_central_table = bcf_quotient_bpeidc_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_bpeidc_central_table_row_step))) * bcf_previous_scale_bpeidc_central_table) + (bcf_right_bpeidc_central_table_row_step))) /\ bcf_value_bpeidc_central_table_row_step = bcf_left_bpeidc_central_table_row_step + bcf_right_bpeidc_central_table_row_step))))))))))) /\ ((((exists bcf_height_bpeidc_central_decoded_row_code. bcf_height_bpeidc_central_decoded_row_code + S (bcf_row_code_bpeidc_central) = S ((S (n + n)) * bcf_row_code_scale_bpeidc_central)) /\ exists bcf_quotient_bpeidc_central_decoded_row_code. bcf_row_code_code_bpeidc_central = bcf_quotient_bpeidc_central_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bpeidc_central) + (bcf_row_code_bpeidc_central))) /\ ((((exists bcf_height_bpeidc_central_decoded_row_scale. bcf_height_bpeidc_central_decoded_row_scale + S (bcf_row_scale_bpeidc_central) = S ((S (n + n)) * bcf_row_scale_scale_bpeidc_central)) /\ exists bcf_quotient_bpeidc_central_decoded_row_scale. bcf_row_scale_code_bpeidc_central = bcf_quotient_bpeidc_central_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bpeidc_central) + (bcf_row_scale_bpeidc_central))) /\ (((exists bcf_height_bpeidc_central_decoded_value. bcf_height_bpeidc_central_decoded_value + S (c) = S ((S (n)) * bcf_row_scale_bpeidc_central)) /\ exists bcf_quotient_bpeidc_central_decoded_value. bcf_row_code_bpeidc_central = bcf_quotient_bpeidc_central_decoded_value * S ((S (n)) * bcf_row_scale_bpeidc_central) + (c))))))))) -> (exists bpr_le_gap_bpeilc_result. bpr_le_gap_bpeilc_result + (z) = (c))

Proof neighborhood

Direct theorem prerequisites

BT00VG primorial_even_interval_divides_central BT00TP central_binom_positive BT002D divisor_le_nonzero

Direct theorem dependents

BT00VU primorial_four_power_support_package

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

24 script commands · 7 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 (3)
primorial even interval divides centralcentral binom positivedivisor le nonzero
01Fix variables and assumptionsL1–5

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

  1. L1
    intro n
  2. L2
    intro z
  3. L3
    intro c
  4. L4
    intro hinterval
  5. L5
    intro hcentral
02Establish hdividesL6–9

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply primorial even interval divides central.

  1. L6
    have hdivides : Dvd(z,c)Definitions: Dvd(z,c)Original native command in the exact edition
  2. L7
    apply primorial_even_interval_divides_central
  3. L8
    exact hinterval
  4. L9
    exact hcentral
03Establish hpositiveL10–19

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 r. c = S r
  2. L11
    specialize central_binom_positive n
  3. L12
    specialize central_binom_positive c
  4. L13
    apply central_binom_positive
  5. L14
    exact hcentral
  6. L15
    specialize divisor_le_nonzero z
  7. L16
    specialize divisor_le_nonzero c
  8. L17
    apply divisor_le_nonzero
  9. L18
    intro hc
  10. L19
    rewrite hc at hpositive
04Separate the logical casesL20–20

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

  1. L20
    cases hpositive
05Use earlier factsL21–21

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

  1. L21
    apply PA1
06Calculate and transport equalitiesL22–22

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

  1. L22
    symm
07Use earlier factsL23–24

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

  1. L23
    exact hpositive_witness
  2. L24
    exact hdivides

Library-wide reading audit

Original defined command ledger · 24 lines
  1. 0001intro n
  2. 0002intro z
  3. 0003intro c
  4. 0004intro hinterval
  5. 0005intro hcentral
  6. 0006have hdivides : Dvd(z,c)
    Exact native replay linehave hdivides : exists q. c = z * q
  7. 0007apply primorial_even_interval_divides_central
  8. 0008exact hinterval
  9. 0009exact hcentral
  10. 0010have hpositive : exists r. c = S r
  11. 0011specialize central_binom_positive n
  12. 0012specialize central_binom_positive c
  13. 0013apply central_binom_positive
  14. 0014exact hcentral
  15. 0015specialize divisor_le_nonzero z
  16. 0016specialize divisor_le_nonzero c
  17. 0017apply divisor_le_nonzero
  18. 0018intro hc
  19. 0019rewrite hc at hpositive
  20. 0020cases hpositive
  21. 0021apply PA1
  22. 0022symm
  23. 0023exact hpositive_witness
  24. 0024exact hdivides