BT00VF · Bertrand theorem

primorial_interval_divides_choose_between

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

A selector interval between both denominator indices divides Choose.

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

∀ a. ∀ l. ∀ n. ∀ k. ∀ j. ∀ c. ∀ z. k + j = n → Choose(n,k,c) → (∃ x. ∃ y. (∀ m. Lt(m,l) → ∃ i. BetaAt(x,y,m,i) ∧ (Prime(S (a + m)) ∧ i = S (a + m) ∨ ¬Prime(S (a + m)) ∧ i = 1)) ∧ Product(x,y,l,z)) → (∀ x. Lt(x,l) → Lt(k,S (a + x)) ∧ (Lt(j,S (a + x)) ∧ Lt(a + x,n))) → Dvd(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

PD0002 Lt PD0003 Dvd PD0004 Prime PD0013 BetaAt PD0014 Product PD0041 Choose

11 occurrences

In local proof propositions

PD0002 Lt PD0003 Dvd PD0004 Prime PD0005 Coprime PD0013 BetaAt

14 occurrences

Exact expanded native-PA statement
forall a l n k j c z. k + j = n -> (((exists bcf_lt_gap_bpidcb_choose_out_of_range. bcf_lt_gap_bpidcb_choose_out_of_range + S (n) = k) /\ c = 0) \/ ((exists bcf_le_gap_bpidcb_choose_in_range. bcf_le_gap_bpidcb_choose_in_range + (k) = n) /\ (exists bcf_row_code_code_bpidcb_choose bcf_row_code_scale_bpidcb_choose bcf_row_scale_code_bpidcb_choose bcf_row_scale_scale_bpidcb_choose bcf_row_code_bpidcb_choose bcf_row_scale_bpidcb_choose. ((forall bcf_row_index_bpidcb_choose_table. (exists bcf_lt_gap_bpidcb_choose_table_row_bound. bcf_lt_gap_bpidcb_choose_table_row_bound + S (bcf_row_index_bpidcb_choose_table) = S (n)) -> exists bcf_row_code_bpidcb_choose_table bcf_row_scale_bpidcb_choose_table. ((((exists bcf_height_bpidcb_choose_table_decoded_row_code. bcf_height_bpidcb_choose_table_decoded_row_code + S (bcf_row_code_bpidcb_choose_table) = S ((S (bcf_row_index_bpidcb_choose_table)) * bcf_row_code_scale_bpidcb_choose)) /\ exists bcf_quotient_bpidcb_choose_table_decoded_row_code. bcf_row_code_code_bpidcb_choose = bcf_quotient_bpidcb_choose_table_decoded_row_code * S ((S (bcf_row_index_bpidcb_choose_table)) * bcf_row_code_scale_bpidcb_choose) + (bcf_row_code_bpidcb_choose_table))) /\ ((((exists bcf_height_bpidcb_choose_table_decoded_row_scale. bcf_height_bpidcb_choose_table_decoded_row_scale + S (bcf_row_scale_bpidcb_choose_table) = S ((S (bcf_row_index_bpidcb_choose_table)) * bcf_row_scale_scale_bpidcb_choose)) /\ exists bcf_quotient_bpidcb_choose_table_decoded_row_scale. bcf_row_scale_code_bpidcb_choose = bcf_quotient_bpidcb_choose_table_decoded_row_scale * S ((S (bcf_row_index_bpidcb_choose_table)) * bcf_row_scale_scale_bpidcb_choose) + (bcf_row_scale_bpidcb_choose_table))) /\ ((bcf_row_index_bpidcb_choose_table = 0 /\ (forall bcf_index_bpidcb_choose_table_zero_row. (exists bcf_lt_gap_bpidcb_choose_table_zero_row_bound. bcf_lt_gap_bpidcb_choose_table_zero_row_bound + S (bcf_index_bpidcb_choose_table_zero_row) = S (n)) -> exists bcf_value_bpidcb_choose_table_zero_row. ((((exists bcf_height_bpidcb_choose_table_zero_row_entry. bcf_height_bpidcb_choose_table_zero_row_entry + S (bcf_value_bpidcb_choose_table_zero_row) = S ((S (bcf_index_bpidcb_choose_table_zero_row)) * bcf_row_scale_bpidcb_choose_table)) /\ exists bcf_quotient_bpidcb_choose_table_zero_row_entry. bcf_row_code_bpidcb_choose_table = bcf_quotient_bpidcb_choose_table_zero_row_entry * S ((S (bcf_index_bpidcb_choose_table_zero_row)) * bcf_row_scale_bpidcb_choose_table) + (bcf_value_bpidcb_choose_table_zero_row))) /\ ((bcf_index_bpidcb_choose_table_zero_row = 0 /\ bcf_value_bpidcb_choose_table_zero_row = 1) \/ exists bcf_predecessor_bpidcb_choose_table_zero_row. bcf_index_bpidcb_choose_table_zero_row = S bcf_predecessor_bpidcb_choose_table_zero_row /\ bcf_value_bpidcb_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_bpidcb_choose_table bcf_previous_code_bpidcb_choose_table bcf_previous_scale_bpidcb_choose_table. bcf_row_index_bpidcb_choose_table = S bcf_predecessor_bpidcb_choose_table /\ ((((exists bcf_height_bpidcb_choose_table_decoded_previous_code. bcf_height_bpidcb_choose_table_decoded_previous_code + S (bcf_previous_code_bpidcb_choose_table) = S ((S (bcf_predecessor_bpidcb_choose_table)) * bcf_row_code_scale_bpidcb_choose)) /\ exists bcf_quotient_bpidcb_choose_table_decoded_previous_code. bcf_row_code_code_bpidcb_choose = bcf_quotient_bpidcb_choose_table_decoded_previous_code * S ((S (bcf_predecessor_bpidcb_choose_table)) * bcf_row_code_scale_bpidcb_choose) + (bcf_previous_code_bpidcb_choose_table))) /\ ((((exists bcf_height_bpidcb_choose_table_decoded_previous_scale. bcf_height_bpidcb_choose_table_decoded_previous_scale + S (bcf_previous_scale_bpidcb_choose_table) = S ((S (bcf_predecessor_bpidcb_choose_table)) * bcf_row_scale_scale_bpidcb_choose)) /\ exists bcf_quotient_bpidcb_choose_table_decoded_previous_scale. bcf_row_scale_code_bpidcb_choose = bcf_quotient_bpidcb_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_bpidcb_choose_table)) * bcf_row_scale_scale_bpidcb_choose) + (bcf_previous_scale_bpidcb_choose_table))) /\ (forall bcf_index_bpidcb_choose_table_row_step. (exists bcf_lt_gap_bpidcb_choose_table_row_step_bound. bcf_lt_gap_bpidcb_choose_table_row_step_bound + S (bcf_index_bpidcb_choose_table_row_step) = S (n)) -> exists bcf_value_bpidcb_choose_table_row_step. ((((exists bcf_height_bpidcb_choose_table_row_step_entry. bcf_height_bpidcb_choose_table_row_step_entry + S (bcf_value_bpidcb_choose_table_row_step) = S ((S (bcf_index_bpidcb_choose_table_row_step)) * bcf_row_scale_bpidcb_choose_table)) /\ exists bcf_quotient_bpidcb_choose_table_row_step_entry. bcf_row_code_bpidcb_choose_table = bcf_quotient_bpidcb_choose_table_row_step_entry * S ((S (bcf_index_bpidcb_choose_table_row_step)) * bcf_row_scale_bpidcb_choose_table) + (bcf_value_bpidcb_choose_table_row_step))) /\ ((bcf_index_bpidcb_choose_table_row_step = 0 /\ bcf_value_bpidcb_choose_table_row_step = 1) \/ exists bcf_predecessor_bpidcb_choose_table_row_step bcf_left_bpidcb_choose_table_row_step bcf_right_bpidcb_choose_table_row_step. bcf_index_bpidcb_choose_table_row_step = S bcf_predecessor_bpidcb_choose_table_row_step /\ ((((exists bcf_height_bpidcb_choose_table_row_step_previous_left. bcf_height_bpidcb_choose_table_row_step_previous_left + S (bcf_left_bpidcb_choose_table_row_step) = S ((S (bcf_predecessor_bpidcb_choose_table_row_step)) * bcf_previous_scale_bpidcb_choose_table)) /\ exists bcf_quotient_bpidcb_choose_table_row_step_previous_left. bcf_previous_code_bpidcb_choose_table = bcf_quotient_bpidcb_choose_table_row_step_previous_left * S ((S (bcf_predecessor_bpidcb_choose_table_row_step)) * bcf_previous_scale_bpidcb_choose_table) + (bcf_left_bpidcb_choose_table_row_step))) /\ ((((exists bcf_height_bpidcb_choose_table_row_step_previous_right. bcf_height_bpidcb_choose_table_row_step_previous_right + S (bcf_right_bpidcb_choose_table_row_step) = S ((S (S (bcf_predecessor_bpidcb_choose_table_row_step))) * bcf_previous_scale_bpidcb_choose_table)) /\ exists bcf_quotient_bpidcb_choose_table_row_step_previous_right. bcf_previous_code_bpidcb_choose_table = bcf_quotient_bpidcb_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_bpidcb_choose_table_row_step))) * bcf_previous_scale_bpidcb_choose_table) + (bcf_right_bpidcb_choose_table_row_step))) /\ bcf_value_bpidcb_choose_table_row_step = bcf_left_bpidcb_choose_table_row_step + bcf_right_bpidcb_choose_table_row_step))))))))))) /\ ((((exists bcf_height_bpidcb_choose_decoded_row_code. bcf_height_bpidcb_choose_decoded_row_code + S (bcf_row_code_bpidcb_choose) = S ((S (n)) * bcf_row_code_scale_bpidcb_choose)) /\ exists bcf_quotient_bpidcb_choose_decoded_row_code. bcf_row_code_code_bpidcb_choose = bcf_quotient_bpidcb_choose_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bpidcb_choose) + (bcf_row_code_bpidcb_choose))) /\ ((((exists bcf_height_bpidcb_choose_decoded_row_scale. bcf_height_bpidcb_choose_decoded_row_scale + S (bcf_row_scale_bpidcb_choose) = S ((S (n)) * bcf_row_scale_scale_bpidcb_choose)) /\ exists bcf_quotient_bpidcb_choose_decoded_row_scale. bcf_row_scale_code_bpidcb_choose = bcf_quotient_bpidcb_choose_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bpidcb_choose) + (bcf_row_scale_bpidcb_choose))) /\ (((exists bcf_height_bpidcb_choose_decoded_value. bcf_height_bpidcb_choose_decoded_value + S (c) = S ((S (k)) * bcf_row_scale_bpidcb_choose)) /\ exists bcf_quotient_bpidcb_choose_decoded_value. bcf_row_code_bpidcb_choose = bcf_quotient_bpidcb_choose_decoded_value * S ((S (k)) * bcf_row_scale_bpidcb_choose) + (c))))))))) -> (exists bpr_code_bpidcb_interval bpr_scale_bpidcb_interval. ((forall bpr_index_bpidcb_interval_mask. (exists bpr_gap_bpidcb_interval_mask_bound. bpr_gap_bpidcb_interval_mask_bound + S (bpr_index_bpidcb_interval_mask) = l) -> exists bpr_value_bpidcb_interval_mask. ((((exists bpr_height_bpidcb_interval_mask_decoded. bpr_height_bpidcb_interval_mask_decoded + S (bpr_value_bpidcb_interval_mask) = S ((S (bpr_index_bpidcb_interval_mask)) * bpr_scale_bpidcb_interval)) /\ exists bpr_quotient_bpidcb_interval_mask_decoded. bpr_code_bpidcb_interval = bpr_quotient_bpidcb_interval_mask_decoded * S ((S (bpr_index_bpidcb_interval_mask)) * bpr_scale_bpidcb_interval) + (bpr_value_bpidcb_interval_mask))) /\ (((((~(S (a + bpr_index_bpidcb_interval_mask) = 1) /\ forall bpr_left_bpidcb_interval_mask_choice_prime bpr_right_bpidcb_interval_mask_choice_prime. S (a + bpr_index_bpidcb_interval_mask) = bpr_left_bpidcb_interval_mask_choice_prime * bpr_right_bpidcb_interval_mask_choice_prime -> bpr_left_bpidcb_interval_mask_choice_prime = 1 \/ bpr_right_bpidcb_interval_mask_choice_prime = 1)) /\ bpr_value_bpidcb_interval_mask = S (a + bpr_index_bpidcb_interval_mask)) \/ (~((~(S (a + bpr_index_bpidcb_interval_mask) = 1) /\ forall bpr_left_bpidcb_interval_mask_choice_prime bpr_right_bpidcb_interval_mask_choice_prime. S (a + bpr_index_bpidcb_interval_mask) = bpr_left_bpidcb_interval_mask_choice_prime * bpr_right_bpidcb_interval_mask_choice_prime -> bpr_left_bpidcb_interval_mask_choice_prime = 1 \/ bpr_right_bpidcb_interval_mask_choice_prime = 1)) /\ bpr_value_bpidcb_interval_mask = 1))))) /\ (exists ff_u_bpidcb_interval_product ff_v_bpidcb_interval_product. ((((exists ff_h_bpidcb_interval_product_start. ff_h_bpidcb_interval_product_start + S (1) = S ((S (0)) * ff_v_bpidcb_interval_product)) /\ exists ff_q_bpidcb_interval_product_start. ff_u_bpidcb_interval_product = ff_q_bpidcb_interval_product_start * S ((S (0)) * ff_v_bpidcb_interval_product) + (1))) /\ ((((exists ff_h_bpidcb_interval_product_terminal. ff_h_bpidcb_interval_product_terminal + S (z) = S ((S (l)) * ff_v_bpidcb_interval_product)) /\ exists ff_q_bpidcb_interval_product_terminal. ff_u_bpidcb_interval_product = ff_q_bpidcb_interval_product_terminal * S ((S (l)) * ff_v_bpidcb_interval_product) + (z))) /\ forall ff_i_bpidcb_interval_product. (exists ff_lt_bpidcb_interval_product_bound. ff_lt_bpidcb_interval_product_bound + S ff_i_bpidcb_interval_product = l) -> exists ff_p_bpidcb_interval_product ff_r_bpidcb_interval_product ff_s_bpidcb_interval_product. ((((exists ff_h_bpidcb_interval_product_factor. ff_h_bpidcb_interval_product_factor + S (ff_p_bpidcb_interval_product) = S ((S (ff_i_bpidcb_interval_product)) * bpr_scale_bpidcb_interval)) /\ exists ff_q_bpidcb_interval_product_factor. bpr_code_bpidcb_interval = ff_q_bpidcb_interval_product_factor * S ((S (ff_i_bpidcb_interval_product)) * bpr_scale_bpidcb_interval) + (ff_p_bpidcb_interval_product))) /\ ((((exists ff_h_bpidcb_interval_product_partial. ff_h_bpidcb_interval_product_partial + S (ff_r_bpidcb_interval_product) = S ((S (ff_i_bpidcb_interval_product)) * ff_v_bpidcb_interval_product)) /\ exists ff_q_bpidcb_interval_product_partial. ff_u_bpidcb_interval_product = ff_q_bpidcb_interval_product_partial * S ((S (ff_i_bpidcb_interval_product)) * ff_v_bpidcb_interval_product) + (ff_r_bpidcb_interval_product))) /\ ((((exists ff_h_bpidcb_interval_product_successor. ff_h_bpidcb_interval_product_successor + S (ff_s_bpidcb_interval_product) = S ((S (S ff_i_bpidcb_interval_product)) * ff_v_bpidcb_interval_product)) /\ exists ff_q_bpidcb_interval_product_successor. ff_u_bpidcb_interval_product = ff_q_bpidcb_interval_product_successor * S ((S (S ff_i_bpidcb_interval_product)) * ff_v_bpidcb_interval_product) + (ff_s_bpidcb_interval_product))) /\ ff_s_bpidcb_interval_product = ff_r_bpidcb_interval_product * ff_p_bpidcb_interval_product)))))))) -> (forall bpr_index_bpidcb_bounds. (exists bpr_gap_bpidcb_bounds_index. bpr_gap_bpidcb_bounds_index + S (bpr_index_bpidcb_bounds) = l) -> ((exists bpr_gap_bpidcb_bounds_left. bpr_gap_bpidcb_bounds_left + S (k) = S (a + bpr_index_bpidcb_bounds)) /\ ((exists bpr_gap_bpidcb_bounds_right. bpr_gap_bpidcb_bounds_right + S (j) = S (a + bpr_index_bpidcb_bounds)) /\ (exists bpr_le_gap_bpidcb_bounds_upper. bpr_le_gap_bpidcb_bounds_upper + (S (a + bpr_index_bpidcb_bounds)) = (n))))) -> (exists bpr_quotient_bpidcb_result. c = (z) * bpr_quotient_bpidcb_result)

Proof neighborhood

Direct theorem prerequisites

BT0042 beta_at_unique BT0027 one_multiple BT00VC choose_prime_divides_between BT00VE primorial_interval_pairwise_coprime BT00VD beta_pairwise_coprime_product_divides_common_multiple

Direct theorem dependents

BT00VG primorial_even_interval_divides_central BT00VH primorial_odd_interval_divides_middle

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

88 script commands · 24 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 (5)
beta at uniqueone multiplechoose prime divides betweenprimorial interval pairwise coprimebeta pairwise coprime product divides common multiple
01Fix variables and assumptionsL1–10

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

  1. L1
    intro a
  2. L2
    intro l
  3. L3
    intro n
  4. L4
    intro k
  5. L5
    intro j
  6. L6
    intro c
  7. L7
    intro z
  8. L8
    intro hsum
  9. L9
    intro hchoose
  10. L10
    intro hinterval
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hbounds
03Separate the logical casesL12–14

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

  1. L12
    cases hinterval
  2. L13
    cases hinterval_witness
  3. L14
    cases hinterval_witness_witness
04Establish hpairwiseL15–21

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

  1. L15
    have hpairwise : ∀ bpr_left_index_bpidcb_pairwise. ∀ bpr_right_index_bpidcb_pairwise. ∀ bpr_left_value_bpidcb_pairwise. ∀ bpr_right_value_bpidcb_pairwise. Lt(bpr_left_index_bpidcb_pairwise,l) → Lt(bpr_right_index_bpidcb_pairwise,l) → BetaAt(x,x1,bpr_left_index_bpidcb_pairwise,bpr_left_value_bpidcb_pairwise) → BetaAt(x,x1,bpr_right_index_bpidcb_pairwise,bpr_right_value_bpidcb_pairwise) → ¬bpr_left_index_bpidcb_pairwise = bpr_right_index_bpidcb_pairwise → Coprime(bpr_left_value_bpidcb_pairwise,bpr_right_value_bpidcb_pairwise)Definitions: Lt(bpr_left_index_bpidcb_pairwise,l)Lt(bpr_right_index_bpidcb_pairwise,l)BetaAt(x,x1,bpr_left_index_bpidcb_pairwise,bpr_left_value_bpidcb_pairwise)BetaAt(x,x1,bpr_right_index_bpidcb_pairwise,bpr_right_value_bpidcb_pairwise)Coprime(bpr_left_value_bpidcb_pairwise,bpr_right_value_bpidcb_pairwise)Original native command in the exact edition
  2. L16
    specialize primorial_interval_pairwise_coprime a
  3. L17
    specialize primorial_interval_pairwise_coprime x
  4. L18
    specialize primorial_interval_pairwise_coprime x1
  5. L19
    specialize primorial_interval_pairwise_coprime l
  6. L20
    apply primorial_interval_pairwise_coprime
  7. L21
    exact hinterval_witness_witness_left
05Establish hpointwiseL22–26

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

  1. L22
    have hpointwise : ∀ bpr_divisor_index_bpidcb_pointwise. ∀ bpr_divisor_value_bpidcb_pointwise. Lt(bpr_divisor_index_bpidcb_pointwise,l) → BetaAt(x,x1,bpr_divisor_index_bpidcb_pointwise,bpr_divisor_value_bpidcb_pointwise) → Dvd(bpr_divisor_value_bpidcb_pointwise,c)Definitions: Lt(bpr_divisor_index_bpidcb_pointwise,l)BetaAt(x,x1,bpr_divisor_index_bpidcb_pointwise,bpr_divisor_value_bpidcb_pointwise)Dvd(bpr_divisor_value_bpidcb_pointwise,c)Original native command in the exact edition
  2. L23
    intro i
  3. L24
    intro p
  4. L25
    intro hi
  5. L26
    intro hp
06Establish hentryL27–29

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

  1. L27
    have hentry : ∃ x2. BetaAt(x,x1,i,x2) ∧ (Prime(S (a + i)) ∧ x2 = S (a + i) ∨ ¬Prime(S (a + i)) ∧ x2 = 1)Definitions: BetaAt(x,x1,i,x2)Prime(S (a + i))Original native command in the exact edition
  2. L28
    apply hinterval_witness_witness_left
  3. L29
    exact hi
07Separate the logical casesL30–31

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

  1. L30
    cases hentry
  2. L31
    cases hentry_witness
08Establish hxpL32–40

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

  1. L32
    have hxp : x2 = p
  2. L33
    specialize beta_at_unique x
  3. L34
    specialize beta_at_unique x1
  4. L35
    specialize beta_at_unique i
  5. L36
    specialize beta_at_unique x2
  6. L37
    specialize beta_at_unique p
  7. L38
    apply beta_at_unique
  8. L39
    exact hentry_witness_left
  9. L40
    exact hp
09Separate the logical casesL41–42

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

  1. L41
    cases hentry_witness_right
  2. L42
    cases hentry_witness_right_left
10Establish hcandidateL43–47

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

  1. L43
    have hcandidate : p = S (a + i)
  2. L44
    trans x2
  3. L45
    symm
  4. L46
    exact hxp
  5. L47
    exact hentry_witness_right_left_right
11Establish hlocal_boundsL48–51

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

  1. L48
    have hlocal_bounds : Lt(k,S (a + i)) ∧ (Lt(j,S (a + i)) ∧ Lt(a + i,n))Definitions: Lt(k,S (a + i))Lt(j,S (a + i))Lt(a + i,n)Original native command in the exact edition
  2. L49
    specialize hbounds i
  3. L50
    apply hbounds
  4. L51
    exact hi
12Separate the logical casesL52–53

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

  1. L52
    cases hlocal_bounds
  2. L53
    cases hlocal_bounds_right
13Use earlier factsL54–60

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

  1. L54
    specialize choose_prime_divides_between n
  2. L55
    specialize choose_prime_divides_between k
  3. L56
    specialize choose_prime_divides_between j
  4. L57
    specialize choose_prime_divides_between p
  5. L58
    specialize choose_prime_divides_between c
  6. L59
    apply choose_prime_divides_between
  7. L60
    exact hsum
14Calculate and transport equalitiesL61–62

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

  1. L61
    rewrite hcandidate
  2. L62
    rewrite hcandidate
15Use earlier factsL63–63

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

  1. L63
    exact hentry_witness_right_left_left
16Calculate and transport equalitiesL64–64

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

  1. L64
    rewrite hcandidate
17Use earlier factsL65–65

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

  1. L65
    exact hlocal_bounds_left
18Calculate and transport equalitiesL66–66

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

  1. L66
    rewrite hcandidate
19Use earlier factsL67–67

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

  1. L67
    exact hlocal_bounds_right_left
20Calculate and transport equalitiesL68–68

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

  1. L68
    rewrite hcandidate
21Use earlier factsL69–70

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

  1. L69
    exact hlocal_bounds_right_right
  2. L70
    exact hchoose
22Separate the logical casesL71–71

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

  1. L71
    cases hentry_witness_right_right
23Establish hp_oneL72–81

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

  1. L72
    have hp_one : p = 1
  2. L73
    trans x2
  3. L74
    symm
  4. L75
    exact hxp
  5. L76
    exact hentry_witness_right_right_right
  6. L77
    rewrite hp_one
  7. L78
    specialize one_multiple c
  8. L79
    exact one_multiple
  9. L80
    specialize beta_pairwise_coprime_product_divides_common_multiple x
  10. L81
    specialize beta_pairwise_coprime_product_divides_common_multiple x1
24Use earlier factsL82–88

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

  1. L82
    specialize beta_pairwise_coprime_product_divides_common_multiple l
  2. L83
    specialize beta_pairwise_coprime_product_divides_common_multiple z
  3. L84
    specialize beta_pairwise_coprime_product_divides_common_multiple c
  4. L85
    apply beta_pairwise_coprime_product_divides_common_multiple
  5. L86
    exact hpairwise
  6. L87
    exact hpointwise
  7. L88
    exact hinterval_witness_witness_right

Library-wide reading audit

Original defined command ledger · 88 lines
  1. 0001intro a
  2. 0002intro l
  3. 0003intro n
  4. 0004intro k
  5. 0005intro j
  6. 0006intro c
  7. 0007intro z
  8. 0008intro hsum
  9. 0009intro hchoose
  10. 0010intro hinterval
  11. 0011intro hbounds
  12. 0012cases hinterval
  13. 0013cases hinterval_witness
  14. 0014cases hinterval_witness_witness
  15. 0015have hpairwise : ∀ bpr_left_index_bpidcb_pairwise. ∀ bpr_right_index_bpidcb_pairwise. ∀ bpr_left_value_bpidcb_pairwise. ∀ bpr_right_value_bpidcb_pairwise. Lt(bpr_left_index_bpidcb_pairwise,l) → Lt(bpr_right_index_bpidcb_pairwise,l) → BetaAt(x,x1,bpr_left_index_bpidcb_pairwise,bpr_left_value_bpidcb_pairwise) → BetaAt(x,x1,bpr_right_index_bpidcb_pairwise,bpr_right_value_bpidcb_pairwise) → ¬bpr_left_index_bpidcb_pairwise = bpr_right_index_bpidcb_pairwise → Coprime(bpr_left_value_bpidcb_pairwise,bpr_right_value_bpidcb_pairwise)
    Exact native replay linehave hpairwise : forall bpr_left_index_bpidcb_pairwise bpr_right_index_bpidcb_pairwise bpr_left_value_bpidcb_pairwise bpr_right_value_bpidcb_pairwise. (exists bpr_gap_bpidcb_pairwise_left_bound. bpr_gap_bpidcb_pairwise_left_bound + S (bpr_left_index_bpidcb_pairwise) = l) -> (exists bpr_gap_bpidcb_pairwise_right_bound. bpr_gap_bpidcb_pairwise_right_bound + S (bpr_right_index_bpidcb_pairwise) = l) -> (((exists bpr_height_bpidcb_pairwise_left_at. bpr_height_bpidcb_pairwise_left_at + S (bpr_left_value_bpidcb_pairwise) = S ((S (bpr_left_index_bpidcb_pairwise)) * x1)) /\ exists bpr_quotient_bpidcb_pairwise_left_at. x = bpr_quotient_bpidcb_pairwise_left_at * S ((S (bpr_left_index_bpidcb_pairwise)) * x1) + (bpr_left_value_bpidcb_pairwise))) -> (((exists bpr_height_bpidcb_pairwise_right_at. bpr_height_bpidcb_pairwise_right_at + S (bpr_right_value_bpidcb_pairwise) = S ((S (bpr_right_index_bpidcb_pairwise)) * x1)) /\ exists bpr_quotient_bpidcb_pairwise_right_at. x = bpr_quotient_bpidcb_pairwise_right_at * S ((S (bpr_right_index_bpidcb_pairwise)) * x1) + (bpr_right_value_bpidcb_pairwise))) -> ~(bpr_left_index_bpidcb_pairwise = bpr_right_index_bpidcb_pairwise) -> (forall bpr_coprime_divisor_bpidcb_pairwise_coprime. (exists bpr_coprime_left_factor_bpidcb_pairwise_coprime. bpr_left_value_bpidcb_pairwise = bpr_coprime_divisor_bpidcb_pairwise_coprime * bpr_coprime_left_factor_bpidcb_pairwise_coprime) -> (exists bpr_coprime_right_factor_bpidcb_pairwise_coprime. bpr_right_value_bpidcb_pairwise = bpr_coprime_divisor_bpidcb_pairwise_coprime * bpr_coprime_right_factor_bpidcb_pairwise_coprime) -> bpr_coprime_divisor_bpidcb_pairwise_coprime = 1)
  16. 0016specialize primorial_interval_pairwise_coprime a
  17. 0017specialize primorial_interval_pairwise_coprime x
  18. 0018specialize primorial_interval_pairwise_coprime x1
  19. 0019specialize primorial_interval_pairwise_coprime l
  20. 0020apply primorial_interval_pairwise_coprime
  21. 0021exact hinterval_witness_witness_left
  22. 0022have hpointwise : ∀ bpr_divisor_index_bpidcb_pointwise. ∀ bpr_divisor_value_bpidcb_pointwise. Lt(bpr_divisor_index_bpidcb_pointwise,l) → BetaAt(x,x1,bpr_divisor_index_bpidcb_pointwise,bpr_divisor_value_bpidcb_pointwise) → Dvd(bpr_divisor_value_bpidcb_pointwise,c)
    Exact native replay linehave hpointwise : forall bpr_divisor_index_bpidcb_pointwise bpr_divisor_value_bpidcb_pointwise. (exists bpr_gap_bpidcb_pointwise_index_bound. bpr_gap_bpidcb_pointwise_index_bound + S (bpr_divisor_index_bpidcb_pointwise) = l) -> (((exists bpr_height_bpidcb_pointwise_decoded. bpr_height_bpidcb_pointwise_decoded + S (bpr_divisor_value_bpidcb_pointwise) = S ((S (bpr_divisor_index_bpidcb_pointwise)) * x1)) /\ exists bpr_quotient_bpidcb_pointwise_decoded. x = bpr_quotient_bpidcb_pointwise_decoded * S ((S (bpr_divisor_index_bpidcb_pointwise)) * x1) + (bpr_divisor_value_bpidcb_pointwise))) -> exists bpr_quotient_bpidcb_pointwise_result. c = bpr_divisor_value_bpidcb_pointwise * bpr_quotient_bpidcb_pointwise_result
  23. 0023intro i
  24. 0024intro p
  25. 0025intro hi
  26. 0026intro hp
  27. 0027have hentry : ∃ x2. BetaAt(x,x1,i,x2) ∧ (Prime(S (a + i)) ∧ x2 = S (a + i) ∨ ¬Prime(S (a + i)) ∧ x2 = 1)
    Exact native replay linehave hentry : exists x2. (((exists bpr_height_bpidcb_local_entry. bpr_height_bpidcb_local_entry + S (x2) = S ((S (i)) * x1)) /\ exists bpr_quotient_bpidcb_local_entry. x = bpr_quotient_bpidcb_local_entry * S ((S (i)) * x1) + (x2))) /\ (((((~(S (a + i) = 1) /\ forall bpr_left_bpidcb_local_choice_prime bpr_right_bpidcb_local_choice_prime. S (a + i) = bpr_left_bpidcb_local_choice_prime * bpr_right_bpidcb_local_choice_prime -> bpr_left_bpidcb_local_choice_prime = 1 \/ bpr_right_bpidcb_local_choice_prime = 1)) /\ x2 = S (a + i)) \/ (~((~(S (a + i) = 1) /\ forall bpr_left_bpidcb_local_choice_prime bpr_right_bpidcb_local_choice_prime. S (a + i) = bpr_left_bpidcb_local_choice_prime * bpr_right_bpidcb_local_choice_prime -> bpr_left_bpidcb_local_choice_prime = 1 \/ bpr_right_bpidcb_local_choice_prime = 1)) /\ x2 = 1)))
  28. 0028apply hinterval_witness_witness_left
  29. 0029exact hi
  30. 0030cases hentry
  31. 0031cases hentry_witness
  32. 0032have hxp : x2 = p
  33. 0033specialize beta_at_unique x
  34. 0034specialize beta_at_unique x1
  35. 0035specialize beta_at_unique i
  36. 0036specialize beta_at_unique x2
  37. 0037specialize beta_at_unique p
  38. 0038apply beta_at_unique
  39. 0039exact hentry_witness_left
  40. 0040exact hp
  41. 0041cases hentry_witness_right
  42. 0042cases hentry_witness_right_left
  43. 0043have hcandidate : p = S (a + i)
  44. 0044trans x2
  45. 0045symm
  46. 0046exact hxp
  47. 0047exact hentry_witness_right_left_right
  48. 0048have hlocal_bounds : Lt(k,S (a + i)) ∧ (Lt(j,S (a + i)) ∧ Lt(a + i,n))
    Exact native replay linehave hlocal_bounds : (exists bpr_gap_bpidcb_local_left. bpr_gap_bpidcb_local_left + S (k) = S (a + i)) /\ ((exists bpr_gap_bpidcb_local_right. bpr_gap_bpidcb_local_right + S (j) = S (a + i)) /\ (exists bpr_le_gap_bpidcb_local_upper. bpr_le_gap_bpidcb_local_upper + (S (a + i)) = (n)))
  49. 0049specialize hbounds i
  50. 0050apply hbounds
  51. 0051exact hi
  52. 0052cases hlocal_bounds
  53. 0053cases hlocal_bounds_right
  54. 0054specialize choose_prime_divides_between n
  55. 0055specialize choose_prime_divides_between k
  56. 0056specialize choose_prime_divides_between j
  57. 0057specialize choose_prime_divides_between p
  58. 0058specialize choose_prime_divides_between c
  59. 0059apply choose_prime_divides_between
  60. 0060exact hsum
  61. 0061rewrite hcandidate
  62. 0062rewrite hcandidate
  63. 0063exact hentry_witness_right_left_left
  64. 0064rewrite hcandidate
  65. 0065exact hlocal_bounds_left
  66. 0066rewrite hcandidate
  67. 0067exact hlocal_bounds_right_left
  68. 0068rewrite hcandidate
  69. 0069exact hlocal_bounds_right_right
  70. 0070exact hchoose
  71. 0071cases hentry_witness_right_right
  72. 0072have hp_one : p = 1
  73. 0073trans x2
  74. 0074symm
  75. 0075exact hxp
  76. 0076exact hentry_witness_right_right_right
  77. 0077rewrite hp_one
  78. 0078specialize one_multiple c
  79. 0079exact one_multiple
  80. 0080specialize beta_pairwise_coprime_product_divides_common_multiple x
  81. 0081specialize beta_pairwise_coprime_product_divides_common_multiple x1
  82. 0082specialize beta_pairwise_coprime_product_divides_common_multiple l
  83. 0083specialize beta_pairwise_coprime_product_divides_common_multiple z
  84. 0084specialize beta_pairwise_coprime_product_divides_common_multiple c
  85. 0085apply beta_pairwise_coprime_product_divides_common_multiple
  86. 0086exact hpairwise
  87. 0087exact hpointwise
  88. 0088exact hinterval_witness_witness_right