BT00UF · Bertrand theorem

primorial_index_eq_transport

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

Equal indices transport the expanded Primorial relation.

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. ∀ m. ∀ z. n = m → Primorial(n,z) → Primorial(m,z)

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

PD0043 Primorial

2 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall n m z. n = m -> (exists bpr_code_bpmit_source bpr_scale_bpmit_source. ((forall bpr_index_bpmit_source_mask. (exists bpr_gap_bpmit_source_mask_bound. bpr_gap_bpmit_source_mask_bound + S (bpr_index_bpmit_source_mask) = n) -> exists bpr_value_bpmit_source_mask. ((((exists bpr_height_bpmit_source_mask_decoded. bpr_height_bpmit_source_mask_decoded + S (bpr_value_bpmit_source_mask) = S ((S (bpr_index_bpmit_source_mask)) * bpr_scale_bpmit_source)) /\ exists bpr_quotient_bpmit_source_mask_decoded. bpr_code_bpmit_source = bpr_quotient_bpmit_source_mask_decoded * S ((S (bpr_index_bpmit_source_mask)) * bpr_scale_bpmit_source) + (bpr_value_bpmit_source_mask))) /\ (((((~(S (bpr_index_bpmit_source_mask) = 1) /\ forall bpr_left_bpmit_source_mask_choice_prime bpr_right_bpmit_source_mask_choice_prime. S (bpr_index_bpmit_source_mask) = bpr_left_bpmit_source_mask_choice_prime * bpr_right_bpmit_source_mask_choice_prime -> bpr_left_bpmit_source_mask_choice_prime = 1 \/ bpr_right_bpmit_source_mask_choice_prime = 1)) /\ bpr_value_bpmit_source_mask = S (bpr_index_bpmit_source_mask)) \/ (~((~(S (bpr_index_bpmit_source_mask) = 1) /\ forall bpr_left_bpmit_source_mask_choice_prime bpr_right_bpmit_source_mask_choice_prime. S (bpr_index_bpmit_source_mask) = bpr_left_bpmit_source_mask_choice_prime * bpr_right_bpmit_source_mask_choice_prime -> bpr_left_bpmit_source_mask_choice_prime = 1 \/ bpr_right_bpmit_source_mask_choice_prime = 1)) /\ bpr_value_bpmit_source_mask = 1))))) /\ (exists ff_u_bpmit_source_product ff_v_bpmit_source_product. ((((exists ff_h_bpmit_source_product_start. ff_h_bpmit_source_product_start + S (1) = S ((S (0)) * ff_v_bpmit_source_product)) /\ exists ff_q_bpmit_source_product_start. ff_u_bpmit_source_product = ff_q_bpmit_source_product_start * S ((S (0)) * ff_v_bpmit_source_product) + (1))) /\ ((((exists ff_h_bpmit_source_product_terminal. ff_h_bpmit_source_product_terminal + S (z) = S ((S (n)) * ff_v_bpmit_source_product)) /\ exists ff_q_bpmit_source_product_terminal. ff_u_bpmit_source_product = ff_q_bpmit_source_product_terminal * S ((S (n)) * ff_v_bpmit_source_product) + (z))) /\ forall ff_i_bpmit_source_product. (exists ff_lt_bpmit_source_product_bound. ff_lt_bpmit_source_product_bound + S ff_i_bpmit_source_product = n) -> exists ff_p_bpmit_source_product ff_r_bpmit_source_product ff_s_bpmit_source_product. ((((exists ff_h_bpmit_source_product_factor. ff_h_bpmit_source_product_factor + S (ff_p_bpmit_source_product) = S ((S (ff_i_bpmit_source_product)) * bpr_scale_bpmit_source)) /\ exists ff_q_bpmit_source_product_factor. bpr_code_bpmit_source = ff_q_bpmit_source_product_factor * S ((S (ff_i_bpmit_source_product)) * bpr_scale_bpmit_source) + (ff_p_bpmit_source_product))) /\ ((((exists ff_h_bpmit_source_product_partial. ff_h_bpmit_source_product_partial + S (ff_r_bpmit_source_product) = S ((S (ff_i_bpmit_source_product)) * ff_v_bpmit_source_product)) /\ exists ff_q_bpmit_source_product_partial. ff_u_bpmit_source_product = ff_q_bpmit_source_product_partial * S ((S (ff_i_bpmit_source_product)) * ff_v_bpmit_source_product) + (ff_r_bpmit_source_product))) /\ ((((exists ff_h_bpmit_source_product_successor. ff_h_bpmit_source_product_successor + S (ff_s_bpmit_source_product) = S ((S (S ff_i_bpmit_source_product)) * ff_v_bpmit_source_product)) /\ exists ff_q_bpmit_source_product_successor. ff_u_bpmit_source_product = ff_q_bpmit_source_product_successor * S ((S (S ff_i_bpmit_source_product)) * ff_v_bpmit_source_product) + (ff_s_bpmit_source_product))) /\ ff_s_bpmit_source_product = ff_r_bpmit_source_product * ff_p_bpmit_source_product)))))))) -> (exists bpr_code_bpmit_target bpr_scale_bpmit_target. ((forall bpr_index_bpmit_target_mask. (exists bpr_gap_bpmit_target_mask_bound. bpr_gap_bpmit_target_mask_bound + S (bpr_index_bpmit_target_mask) = m) -> exists bpr_value_bpmit_target_mask. ((((exists bpr_height_bpmit_target_mask_decoded. bpr_height_bpmit_target_mask_decoded + S (bpr_value_bpmit_target_mask) = S ((S (bpr_index_bpmit_target_mask)) * bpr_scale_bpmit_target)) /\ exists bpr_quotient_bpmit_target_mask_decoded. bpr_code_bpmit_target = bpr_quotient_bpmit_target_mask_decoded * S ((S (bpr_index_bpmit_target_mask)) * bpr_scale_bpmit_target) + (bpr_value_bpmit_target_mask))) /\ (((((~(S (bpr_index_bpmit_target_mask) = 1) /\ forall bpr_left_bpmit_target_mask_choice_prime bpr_right_bpmit_target_mask_choice_prime. S (bpr_index_bpmit_target_mask) = bpr_left_bpmit_target_mask_choice_prime * bpr_right_bpmit_target_mask_choice_prime -> bpr_left_bpmit_target_mask_choice_prime = 1 \/ bpr_right_bpmit_target_mask_choice_prime = 1)) /\ bpr_value_bpmit_target_mask = S (bpr_index_bpmit_target_mask)) \/ (~((~(S (bpr_index_bpmit_target_mask) = 1) /\ forall bpr_left_bpmit_target_mask_choice_prime bpr_right_bpmit_target_mask_choice_prime. S (bpr_index_bpmit_target_mask) = bpr_left_bpmit_target_mask_choice_prime * bpr_right_bpmit_target_mask_choice_prime -> bpr_left_bpmit_target_mask_choice_prime = 1 \/ bpr_right_bpmit_target_mask_choice_prime = 1)) /\ bpr_value_bpmit_target_mask = 1))))) /\ (exists ff_u_bpmit_target_product ff_v_bpmit_target_product. ((((exists ff_h_bpmit_target_product_start. ff_h_bpmit_target_product_start + S (1) = S ((S (0)) * ff_v_bpmit_target_product)) /\ exists ff_q_bpmit_target_product_start. ff_u_bpmit_target_product = ff_q_bpmit_target_product_start * S ((S (0)) * ff_v_bpmit_target_product) + (1))) /\ ((((exists ff_h_bpmit_target_product_terminal. ff_h_bpmit_target_product_terminal + S (z) = S ((S (m)) * ff_v_bpmit_target_product)) /\ exists ff_q_bpmit_target_product_terminal. ff_u_bpmit_target_product = ff_q_bpmit_target_product_terminal * S ((S (m)) * ff_v_bpmit_target_product) + (z))) /\ forall ff_i_bpmit_target_product. (exists ff_lt_bpmit_target_product_bound. ff_lt_bpmit_target_product_bound + S ff_i_bpmit_target_product = m) -> exists ff_p_bpmit_target_product ff_r_bpmit_target_product ff_s_bpmit_target_product. ((((exists ff_h_bpmit_target_product_factor. ff_h_bpmit_target_product_factor + S (ff_p_bpmit_target_product) = S ((S (ff_i_bpmit_target_product)) * bpr_scale_bpmit_target)) /\ exists ff_q_bpmit_target_product_factor. bpr_code_bpmit_target = ff_q_bpmit_target_product_factor * S ((S (ff_i_bpmit_target_product)) * bpr_scale_bpmit_target) + (ff_p_bpmit_target_product))) /\ ((((exists ff_h_bpmit_target_product_partial. ff_h_bpmit_target_product_partial + S (ff_r_bpmit_target_product) = S ((S (ff_i_bpmit_target_product)) * ff_v_bpmit_target_product)) /\ exists ff_q_bpmit_target_product_partial. ff_u_bpmit_target_product = ff_q_bpmit_target_product_partial * S ((S (ff_i_bpmit_target_product)) * ff_v_bpmit_target_product) + (ff_r_bpmit_target_product))) /\ ((((exists ff_h_bpmit_target_product_successor. ff_h_bpmit_target_product_successor + S (ff_s_bpmit_target_product) = S ((S (S ff_i_bpmit_target_product)) * ff_v_bpmit_target_product)) /\ exists ff_q_bpmit_target_product_successor. ff_u_bpmit_target_product = ff_q_bpmit_target_product_successor * S ((S (S ff_i_bpmit_target_product)) * ff_v_bpmit_target_product) + (ff_s_bpmit_target_product))) /\ ff_s_bpmit_target_product = ff_r_bpmit_target_product * ff_p_bpmit_target_product))))))))

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

BT00VV primorial_le_four_pow_bounded BT0111 no_bertrand_middle_contribution_interval_le_four_pow

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

10 script commands · 3 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–5

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

  1. L1
    intro n
  2. L2
    intro m
  3. L3
    intro z
  4. L4
    intro hindex
  5. L5
    intro hsource
02Calculate and transport equalitiesL6–9

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

  1. L6
    rewrite hindex at hsource
  2. L7
    rewrite hindex at hsource
  3. L8
    rewrite hindex at hsource
  4. L9
    rewrite hindex at hsource
03Use earlier factsL10–10

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

  1. L10
    exact hsource

Library-wide reading audit

Original defined command ledger · 10 lines
  1. 0001intro n
  2. 0002intro m
  3. 0003intro z
  4. 0004intro hindex
  5. 0005intro hsource
  6. 0006rewrite hindex at hsource
  7. 0007rewrite hindex at hsource
  8. 0008rewrite hindex at hsource
  9. 0009rewrite hindex at hsource
  10. 0010exact hsource