BT00VC · Bertrand theorem

choose_prime_divides_between

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

A prime between both denominator indices and the row 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

∀ n. ∀ k. ∀ j. ∀ p. ∀ c. k + j = n → Prime(p) → Lt(k,p) → Lt(j,p) → Le(p,n) → Choose(n,k,c) → Dvd(p,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 PD0003 Dvd PD0004 Prime PD0041 Choose

6 occurrences

In local proof propositions

PD0001 Le PD0003 Dvd PD0023 Factorial

10 occurrences

Exact expanded native-PA statement
forall n k j p c. k + j = n -> ((~(p = 1) /\ forall bpr_left_bcpdb_prime bpr_right_bcpdb_prime. p = bpr_left_bcpdb_prime * bpr_right_bcpdb_prime -> bpr_left_bcpdb_prime = 1 \/ bpr_right_bcpdb_prime = 1)) -> (exists bpr_gap_bcpdb_left_bound. bpr_gap_bcpdb_left_bound + S (k) = p) -> (exists bpr_gap_bcpdb_right_bound. bpr_gap_bcpdb_right_bound + S (j) = p) -> (exists bpr_le_gap_bcpdb_upper_bound. bpr_le_gap_bcpdb_upper_bound + (p) = (n)) -> (((exists bcf_lt_gap_bcpdb_source_out_of_range. bcf_lt_gap_bcpdb_source_out_of_range + S (n) = k) /\ c = 0) \/ ((exists bcf_le_gap_bcpdb_source_in_range. bcf_le_gap_bcpdb_source_in_range + (k) = n) /\ (exists bcf_row_code_code_bcpdb_source bcf_row_code_scale_bcpdb_source bcf_row_scale_code_bcpdb_source bcf_row_scale_scale_bcpdb_source bcf_row_code_bcpdb_source bcf_row_scale_bcpdb_source. ((forall bcf_row_index_bcpdb_source_table. (exists bcf_lt_gap_bcpdb_source_table_row_bound. bcf_lt_gap_bcpdb_source_table_row_bound + S (bcf_row_index_bcpdb_source_table) = S (n)) -> exists bcf_row_code_bcpdb_source_table bcf_row_scale_bcpdb_source_table. ((((exists bcf_height_bcpdb_source_table_decoded_row_code. bcf_height_bcpdb_source_table_decoded_row_code + S (bcf_row_code_bcpdb_source_table) = S ((S (bcf_row_index_bcpdb_source_table)) * bcf_row_code_scale_bcpdb_source)) /\ exists bcf_quotient_bcpdb_source_table_decoded_row_code. bcf_row_code_code_bcpdb_source = bcf_quotient_bcpdb_source_table_decoded_row_code * S ((S (bcf_row_index_bcpdb_source_table)) * bcf_row_code_scale_bcpdb_source) + (bcf_row_code_bcpdb_source_table))) /\ ((((exists bcf_height_bcpdb_source_table_decoded_row_scale. bcf_height_bcpdb_source_table_decoded_row_scale + S (bcf_row_scale_bcpdb_source_table) = S ((S (bcf_row_index_bcpdb_source_table)) * bcf_row_scale_scale_bcpdb_source)) /\ exists bcf_quotient_bcpdb_source_table_decoded_row_scale. bcf_row_scale_code_bcpdb_source = bcf_quotient_bcpdb_source_table_decoded_row_scale * S ((S (bcf_row_index_bcpdb_source_table)) * bcf_row_scale_scale_bcpdb_source) + (bcf_row_scale_bcpdb_source_table))) /\ ((bcf_row_index_bcpdb_source_table = 0 /\ (forall bcf_index_bcpdb_source_table_zero_row. (exists bcf_lt_gap_bcpdb_source_table_zero_row_bound. bcf_lt_gap_bcpdb_source_table_zero_row_bound + S (bcf_index_bcpdb_source_table_zero_row) = S (n)) -> exists bcf_value_bcpdb_source_table_zero_row. ((((exists bcf_height_bcpdb_source_table_zero_row_entry. bcf_height_bcpdb_source_table_zero_row_entry + S (bcf_value_bcpdb_source_table_zero_row) = S ((S (bcf_index_bcpdb_source_table_zero_row)) * bcf_row_scale_bcpdb_source_table)) /\ exists bcf_quotient_bcpdb_source_table_zero_row_entry. bcf_row_code_bcpdb_source_table = bcf_quotient_bcpdb_source_table_zero_row_entry * S ((S (bcf_index_bcpdb_source_table_zero_row)) * bcf_row_scale_bcpdb_source_table) + (bcf_value_bcpdb_source_table_zero_row))) /\ ((bcf_index_bcpdb_source_table_zero_row = 0 /\ bcf_value_bcpdb_source_table_zero_row = 1) \/ exists bcf_predecessor_bcpdb_source_table_zero_row. bcf_index_bcpdb_source_table_zero_row = S bcf_predecessor_bcpdb_source_table_zero_row /\ bcf_value_bcpdb_source_table_zero_row = 0)))) \/ exists bcf_predecessor_bcpdb_source_table bcf_previous_code_bcpdb_source_table bcf_previous_scale_bcpdb_source_table. bcf_row_index_bcpdb_source_table = S bcf_predecessor_bcpdb_source_table /\ ((((exists bcf_height_bcpdb_source_table_decoded_previous_code. bcf_height_bcpdb_source_table_decoded_previous_code + S (bcf_previous_code_bcpdb_source_table) = S ((S (bcf_predecessor_bcpdb_source_table)) * bcf_row_code_scale_bcpdb_source)) /\ exists bcf_quotient_bcpdb_source_table_decoded_previous_code. bcf_row_code_code_bcpdb_source = bcf_quotient_bcpdb_source_table_decoded_previous_code * S ((S (bcf_predecessor_bcpdb_source_table)) * bcf_row_code_scale_bcpdb_source) + (bcf_previous_code_bcpdb_source_table))) /\ ((((exists bcf_height_bcpdb_source_table_decoded_previous_scale. bcf_height_bcpdb_source_table_decoded_previous_scale + S (bcf_previous_scale_bcpdb_source_table) = S ((S (bcf_predecessor_bcpdb_source_table)) * bcf_row_scale_scale_bcpdb_source)) /\ exists bcf_quotient_bcpdb_source_table_decoded_previous_scale. bcf_row_scale_code_bcpdb_source = bcf_quotient_bcpdb_source_table_decoded_previous_scale * S ((S (bcf_predecessor_bcpdb_source_table)) * bcf_row_scale_scale_bcpdb_source) + (bcf_previous_scale_bcpdb_source_table))) /\ (forall bcf_index_bcpdb_source_table_row_step. (exists bcf_lt_gap_bcpdb_source_table_row_step_bound. bcf_lt_gap_bcpdb_source_table_row_step_bound + S (bcf_index_bcpdb_source_table_row_step) = S (n)) -> exists bcf_value_bcpdb_source_table_row_step. ((((exists bcf_height_bcpdb_source_table_row_step_entry. bcf_height_bcpdb_source_table_row_step_entry + S (bcf_value_bcpdb_source_table_row_step) = S ((S (bcf_index_bcpdb_source_table_row_step)) * bcf_row_scale_bcpdb_source_table)) /\ exists bcf_quotient_bcpdb_source_table_row_step_entry. bcf_row_code_bcpdb_source_table = bcf_quotient_bcpdb_source_table_row_step_entry * S ((S (bcf_index_bcpdb_source_table_row_step)) * bcf_row_scale_bcpdb_source_table) + (bcf_value_bcpdb_source_table_row_step))) /\ ((bcf_index_bcpdb_source_table_row_step = 0 /\ bcf_value_bcpdb_source_table_row_step = 1) \/ exists bcf_predecessor_bcpdb_source_table_row_step bcf_left_bcpdb_source_table_row_step bcf_right_bcpdb_source_table_row_step. bcf_index_bcpdb_source_table_row_step = S bcf_predecessor_bcpdb_source_table_row_step /\ ((((exists bcf_height_bcpdb_source_table_row_step_previous_left. bcf_height_bcpdb_source_table_row_step_previous_left + S (bcf_left_bcpdb_source_table_row_step) = S ((S (bcf_predecessor_bcpdb_source_table_row_step)) * bcf_previous_scale_bcpdb_source_table)) /\ exists bcf_quotient_bcpdb_source_table_row_step_previous_left. bcf_previous_code_bcpdb_source_table = bcf_quotient_bcpdb_source_table_row_step_previous_left * S ((S (bcf_predecessor_bcpdb_source_table_row_step)) * bcf_previous_scale_bcpdb_source_table) + (bcf_left_bcpdb_source_table_row_step))) /\ ((((exists bcf_height_bcpdb_source_table_row_step_previous_right. bcf_height_bcpdb_source_table_row_step_previous_right + S (bcf_right_bcpdb_source_table_row_step) = S ((S (S (bcf_predecessor_bcpdb_source_table_row_step))) * bcf_previous_scale_bcpdb_source_table)) /\ exists bcf_quotient_bcpdb_source_table_row_step_previous_right. bcf_previous_code_bcpdb_source_table = bcf_quotient_bcpdb_source_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcpdb_source_table_row_step))) * bcf_previous_scale_bcpdb_source_table) + (bcf_right_bcpdb_source_table_row_step))) /\ bcf_value_bcpdb_source_table_row_step = bcf_left_bcpdb_source_table_row_step + bcf_right_bcpdb_source_table_row_step))))))))))) /\ ((((exists bcf_height_bcpdb_source_decoded_row_code. bcf_height_bcpdb_source_decoded_row_code + S (bcf_row_code_bcpdb_source) = S ((S (n)) * bcf_row_code_scale_bcpdb_source)) /\ exists bcf_quotient_bcpdb_source_decoded_row_code. bcf_row_code_code_bcpdb_source = bcf_quotient_bcpdb_source_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcpdb_source) + (bcf_row_code_bcpdb_source))) /\ ((((exists bcf_height_bcpdb_source_decoded_row_scale. bcf_height_bcpdb_source_decoded_row_scale + S (bcf_row_scale_bcpdb_source) = S ((S (n)) * bcf_row_scale_scale_bcpdb_source)) /\ exists bcf_quotient_bcpdb_source_decoded_row_scale. bcf_row_scale_code_bcpdb_source = bcf_quotient_bcpdb_source_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcpdb_source) + (bcf_row_scale_bcpdb_source))) /\ (((exists bcf_height_bcpdb_source_decoded_value. bcf_height_bcpdb_source_decoded_value + S (c) = S ((S (k)) * bcf_row_scale_bcpdb_source)) /\ exists bcf_quotient_bcpdb_source_decoded_value. bcf_row_code_bcpdb_source = bcf_quotient_bcpdb_source_decoded_value * S ((S (k)) * bcf_row_scale_bcpdb_source) + (c))))))))) -> (exists bpr_quotient_bcpdb_result. c = (p) * bpr_quotient_bcpdb_result)

Proof neighborhood

Direct theorem prerequisites

BT008Y factorial_exists BT00TX choose_factorial_bridge BT00VA factorial_prime_divides_of_le BT003N euclid_prime_dvd_product BT00VB factorial_prime_le_of_divides BT001I lt_not_le

Direct theorem dependents

BT00VF primorial_interval_divides_choose_between

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 · 21 reading checkpoints · 9 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)
factorial existschoose factorial bridgefactorial prime divides of leeuclid prime dvd productfactorial prime le of divideslt not le
01Fix variables and assumptionsL1–10

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

  1. L1
    intro n
  2. L2
    intro k
  3. L3
    intro j
  4. L4
    intro p
  5. L5
    intro c
  6. L6
    intro hsum
  7. L7
    intro hp
  8. L8
    intro hk
  9. L9
    intro hj
  10. L10
    intro hpn
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hchoose
03Establish hFL12–13

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

  1. L12
    have hF : ∃ F. Factorial(n,F)Definitions: Factorial(n,F)Original native command in the exact edition
  2. L13
    apply factorial_exists
04Separate the logical casesL14–14

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

  1. L14
    cases hF
05Establish hKL15–16

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

  1. L15
    have hK : ∃ K. Factorial(k,K)Definitions: Factorial(k,K)Original native command in the exact edition
  2. L16
    apply factorial_exists
06Separate the logical casesL17–17

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

  1. L17
    cases hK
07Establish hJL18–19

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

  1. L18
    have hJ : ∃ J. Factorial(j,J)Definitions: Factorial(j,J)Original native command in the exact edition
  2. L19
    apply factorial_exists
08Separate the logical casesL20–20

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

  1. L20
    cases hJ
09Establish hbridgeL21–30

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

  1. L21
    have hbridge : x = (x1 * x2) * c
  2. L22
    specialize choose_factorial_bridge n
  3. L23
    specialize choose_factorial_bridge k
  4. L24
    specialize choose_factorial_bridge j
  5. L25
    specialize choose_factorial_bridge c
  6. L26
    specialize choose_factorial_bridge x
  7. L27
    specialize choose_factorial_bridge x1
  8. L28
    specialize choose_factorial_bridge x2
  9. L29
    apply choose_factorial_bridge
  10. L30
    exact hsum
10Use earlier factsL31–34

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

  1. L31
    exact hchoose
  2. L32
    exact hF_witness
  3. L33
    exact hK_witness
  4. L34
    exact hJ_witness
11Establish htotalL35–43

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

  1. L35
    have htotal : Dvd(p,x)Definitions: Dvd(p,x)Original native command in the exact edition
  2. L36
    specialize factorial_prime_divides_of_le p
  3. L37
    specialize factorial_prime_divides_of_le n
  4. L38
    specialize factorial_prime_divides_of_le x
  5. L39
    apply factorial_prime_divides_of_le
  6. L40
    exact hp
  7. L41
    exact hpn
  8. L42
    exact hF_witness
  9. L43
    rewrite hbridge at htotal
12Establish houterL44–50

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

  1. L44
    have houter : Dvd(p,x1 · x2) ∨ Dvd(p,c)Definitions: Dvd(p,x1 · x2)Dvd(p,c)Original native command in the exact edition
  2. L45
    specialize euclid_prime_dvd_product p
  3. L46
    specialize euclid_prime_dvd_product (x1 * x2)
  4. L47
    specialize euclid_prime_dvd_product c
  5. L48
    apply euclid_prime_dvd_product
  6. L49
    exact hp
  7. L50
    exact htotal
13Separate the logical casesL51–51

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

  1. L51
    cases houter
14Establish hinnerL52–58

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

  1. L52
    have hinner : Dvd(p,x1) ∨ Dvd(p,x2)Definitions: Dvd(p,x1)Dvd(p,x2)Original native command in the exact edition
  2. L53
    specialize euclid_prime_dvd_product p
  3. L54
    specialize euclid_prime_dvd_product x1
  4. L55
    specialize euclid_prime_dvd_product x2
  5. L56
    apply euclid_prime_dvd_product
  6. L57
    exact hp
  7. L58
    exact houter_left
15Separate the logical casesL59–59

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

  1. L59
    cases hinner
16Establish hpkL60–67

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

  1. L60
  2. L61
    specialize factorial_prime_le_of_divides p
  3. L62
    specialize factorial_prime_le_of_divides k
  4. L63
    specialize factorial_prime_le_of_divides x1
  5. L64
    apply factorial_prime_le_of_divides
  6. L65
    exact hp
  7. L66
    exact hK_witness
  8. L67
    exact hinner_left
17Separate the logical casesL68–68

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

  1. L68
    exfalso
18Use earlier factsL69–73

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

  1. L69
    specialize lt_not_le k
  2. L70
    specialize lt_not_le p
  3. L71
    apply lt_not_le
  4. L72
    exact hk
  5. L73
    exact hpk
19Establish hpjL74–81

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

  1. L74
  2. L75
    specialize factorial_prime_le_of_divides p
  3. L76
    specialize factorial_prime_le_of_divides j
  4. L77
    specialize factorial_prime_le_of_divides x2
  5. L78
    apply factorial_prime_le_of_divides
  6. L79
    exact hp
  7. L80
    exact hJ_witness
  8. L81
    exact hinner_right
20Separate the logical casesL82–82

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

  1. L82
    exfalso
21Use earlier factsL83–88

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

  1. L83
    specialize lt_not_le j
  2. L84
    specialize lt_not_le p
  3. L85
    apply lt_not_le
  4. L86
    exact hj
  5. L87
    exact hpj
  6. L88
    exact houter_right

Library-wide reading audit

Original defined command ledger · 88 lines
  1. 0001intro n
  2. 0002intro k
  3. 0003intro j
  4. 0004intro p
  5. 0005intro c
  6. 0006intro hsum
  7. 0007intro hp
  8. 0008intro hk
  9. 0009intro hj
  10. 0010intro hpn
  11. 0011intro hchoose
  12. 0012have hF : ∃ F. Factorial(n,F)
    Exact native replay linehave hF : exists F. (exists ff_b_bcpdb_total_factorial ff_c_bcpdb_total_factorial. ((forall ff_i_bcpdb_total_factorial_range. (exists ff_lt_bcpdb_total_factorial_range_bound. ff_lt_bcpdb_total_factorial_range_bound + S ff_i_bcpdb_total_factorial_range = n) -> (((exists ff_h_bcpdb_total_factorial_range_decoded. ff_h_bcpdb_total_factorial_range_decoded + S (1 + ff_i_bcpdb_total_factorial_range) = S ((S (ff_i_bcpdb_total_factorial_range)) * ff_c_bcpdb_total_factorial)) /\ exists ff_q_bcpdb_total_factorial_range_decoded. ff_b_bcpdb_total_factorial = ff_q_bcpdb_total_factorial_range_decoded * S ((S (ff_i_bcpdb_total_factorial_range)) * ff_c_bcpdb_total_factorial) + (1 + ff_i_bcpdb_total_factorial_range)))) /\ (exists ff_u_bcpdb_total_factorial_product ff_v_bcpdb_total_factorial_product. ((((exists ff_h_bcpdb_total_factorial_product_start. ff_h_bcpdb_total_factorial_product_start + S (1) = S ((S (0)) * ff_v_bcpdb_total_factorial_product)) /\ exists ff_q_bcpdb_total_factorial_product_start. ff_u_bcpdb_total_factorial_product = ff_q_bcpdb_total_factorial_product_start * S ((S (0)) * ff_v_bcpdb_total_factorial_product) + (1))) /\ ((((exists ff_h_bcpdb_total_factorial_product_terminal. ff_h_bcpdb_total_factorial_product_terminal + S (F) = S ((S (n)) * ff_v_bcpdb_total_factorial_product)) /\ exists ff_q_bcpdb_total_factorial_product_terminal. ff_u_bcpdb_total_factorial_product = ff_q_bcpdb_total_factorial_product_terminal * S ((S (n)) * ff_v_bcpdb_total_factorial_product) + (F))) /\ forall ff_i_bcpdb_total_factorial_product. (exists ff_lt_bcpdb_total_factorial_product_bound. ff_lt_bcpdb_total_factorial_product_bound + S ff_i_bcpdb_total_factorial_product = n) -> exists ff_p_bcpdb_total_factorial_product ff_r_bcpdb_total_factorial_product ff_s_bcpdb_total_factorial_product. ((((exists ff_h_bcpdb_total_factorial_product_factor. ff_h_bcpdb_total_factorial_product_factor + S (ff_p_bcpdb_total_factorial_product) = S ((S (ff_i_bcpdb_total_factorial_product)) * ff_c_bcpdb_total_factorial)) /\ exists ff_q_bcpdb_total_factorial_product_factor. ff_b_bcpdb_total_factorial = ff_q_bcpdb_total_factorial_product_factor * S ((S (ff_i_bcpdb_total_factorial_product)) * ff_c_bcpdb_total_factorial) + (ff_p_bcpdb_total_factorial_product))) /\ ((((exists ff_h_bcpdb_total_factorial_product_partial. ff_h_bcpdb_total_factorial_product_partial + S (ff_r_bcpdb_total_factorial_product) = S ((S (ff_i_bcpdb_total_factorial_product)) * ff_v_bcpdb_total_factorial_product)) /\ exists ff_q_bcpdb_total_factorial_product_partial. ff_u_bcpdb_total_factorial_product = ff_q_bcpdb_total_factorial_product_partial * S ((S (ff_i_bcpdb_total_factorial_product)) * ff_v_bcpdb_total_factorial_product) + (ff_r_bcpdb_total_factorial_product))) /\ ((((exists ff_h_bcpdb_total_factorial_product_successor. ff_h_bcpdb_total_factorial_product_successor + S (ff_s_bcpdb_total_factorial_product) = S ((S (S ff_i_bcpdb_total_factorial_product)) * ff_v_bcpdb_total_factorial_product)) /\ exists ff_q_bcpdb_total_factorial_product_successor. ff_u_bcpdb_total_factorial_product = ff_q_bcpdb_total_factorial_product_successor * S ((S (S ff_i_bcpdb_total_factorial_product)) * ff_v_bcpdb_total_factorial_product) + (ff_s_bcpdb_total_factorial_product))) /\ ff_s_bcpdb_total_factorial_product = ff_r_bcpdb_total_factorial_product * ff_p_bcpdb_total_factorial_product))))))))
  13. 0013apply factorial_exists
  14. 0014cases hF
  15. 0015have hK : ∃ K. Factorial(k,K)
    Exact native replay linehave hK : exists K. (exists ff_b_bcpdb_left_factorial ff_c_bcpdb_left_factorial. ((forall ff_i_bcpdb_left_factorial_range. (exists ff_lt_bcpdb_left_factorial_range_bound. ff_lt_bcpdb_left_factorial_range_bound + S ff_i_bcpdb_left_factorial_range = k) -> (((exists ff_h_bcpdb_left_factorial_range_decoded. ff_h_bcpdb_left_factorial_range_decoded + S (1 + ff_i_bcpdb_left_factorial_range) = S ((S (ff_i_bcpdb_left_factorial_range)) * ff_c_bcpdb_left_factorial)) /\ exists ff_q_bcpdb_left_factorial_range_decoded. ff_b_bcpdb_left_factorial = ff_q_bcpdb_left_factorial_range_decoded * S ((S (ff_i_bcpdb_left_factorial_range)) * ff_c_bcpdb_left_factorial) + (1 + ff_i_bcpdb_left_factorial_range)))) /\ (exists ff_u_bcpdb_left_factorial_product ff_v_bcpdb_left_factorial_product. ((((exists ff_h_bcpdb_left_factorial_product_start. ff_h_bcpdb_left_factorial_product_start + S (1) = S ((S (0)) * ff_v_bcpdb_left_factorial_product)) /\ exists ff_q_bcpdb_left_factorial_product_start. ff_u_bcpdb_left_factorial_product = ff_q_bcpdb_left_factorial_product_start * S ((S (0)) * ff_v_bcpdb_left_factorial_product) + (1))) /\ ((((exists ff_h_bcpdb_left_factorial_product_terminal. ff_h_bcpdb_left_factorial_product_terminal + S (K) = S ((S (k)) * ff_v_bcpdb_left_factorial_product)) /\ exists ff_q_bcpdb_left_factorial_product_terminal. ff_u_bcpdb_left_factorial_product = ff_q_bcpdb_left_factorial_product_terminal * S ((S (k)) * ff_v_bcpdb_left_factorial_product) + (K))) /\ forall ff_i_bcpdb_left_factorial_product. (exists ff_lt_bcpdb_left_factorial_product_bound. ff_lt_bcpdb_left_factorial_product_bound + S ff_i_bcpdb_left_factorial_product = k) -> exists ff_p_bcpdb_left_factorial_product ff_r_bcpdb_left_factorial_product ff_s_bcpdb_left_factorial_product. ((((exists ff_h_bcpdb_left_factorial_product_factor. ff_h_bcpdb_left_factorial_product_factor + S (ff_p_bcpdb_left_factorial_product) = S ((S (ff_i_bcpdb_left_factorial_product)) * ff_c_bcpdb_left_factorial)) /\ exists ff_q_bcpdb_left_factorial_product_factor. ff_b_bcpdb_left_factorial = ff_q_bcpdb_left_factorial_product_factor * S ((S (ff_i_bcpdb_left_factorial_product)) * ff_c_bcpdb_left_factorial) + (ff_p_bcpdb_left_factorial_product))) /\ ((((exists ff_h_bcpdb_left_factorial_product_partial. ff_h_bcpdb_left_factorial_product_partial + S (ff_r_bcpdb_left_factorial_product) = S ((S (ff_i_bcpdb_left_factorial_product)) * ff_v_bcpdb_left_factorial_product)) /\ exists ff_q_bcpdb_left_factorial_product_partial. ff_u_bcpdb_left_factorial_product = ff_q_bcpdb_left_factorial_product_partial * S ((S (ff_i_bcpdb_left_factorial_product)) * ff_v_bcpdb_left_factorial_product) + (ff_r_bcpdb_left_factorial_product))) /\ ((((exists ff_h_bcpdb_left_factorial_product_successor. ff_h_bcpdb_left_factorial_product_successor + S (ff_s_bcpdb_left_factorial_product) = S ((S (S ff_i_bcpdb_left_factorial_product)) * ff_v_bcpdb_left_factorial_product)) /\ exists ff_q_bcpdb_left_factorial_product_successor. ff_u_bcpdb_left_factorial_product = ff_q_bcpdb_left_factorial_product_successor * S ((S (S ff_i_bcpdb_left_factorial_product)) * ff_v_bcpdb_left_factorial_product) + (ff_s_bcpdb_left_factorial_product))) /\ ff_s_bcpdb_left_factorial_product = ff_r_bcpdb_left_factorial_product * ff_p_bcpdb_left_factorial_product))))))))
  16. 0016apply factorial_exists
  17. 0017cases hK
  18. 0018have hJ : ∃ J. Factorial(j,J)
    Exact native replay linehave hJ : exists J. (exists ff_b_bcpdb_right_factorial ff_c_bcpdb_right_factorial. ((forall ff_i_bcpdb_right_factorial_range. (exists ff_lt_bcpdb_right_factorial_range_bound. ff_lt_bcpdb_right_factorial_range_bound + S ff_i_bcpdb_right_factorial_range = j) -> (((exists ff_h_bcpdb_right_factorial_range_decoded. ff_h_bcpdb_right_factorial_range_decoded + S (1 + ff_i_bcpdb_right_factorial_range) = S ((S (ff_i_bcpdb_right_factorial_range)) * ff_c_bcpdb_right_factorial)) /\ exists ff_q_bcpdb_right_factorial_range_decoded. ff_b_bcpdb_right_factorial = ff_q_bcpdb_right_factorial_range_decoded * S ((S (ff_i_bcpdb_right_factorial_range)) * ff_c_bcpdb_right_factorial) + (1 + ff_i_bcpdb_right_factorial_range)))) /\ (exists ff_u_bcpdb_right_factorial_product ff_v_bcpdb_right_factorial_product. ((((exists ff_h_bcpdb_right_factorial_product_start. ff_h_bcpdb_right_factorial_product_start + S (1) = S ((S (0)) * ff_v_bcpdb_right_factorial_product)) /\ exists ff_q_bcpdb_right_factorial_product_start. ff_u_bcpdb_right_factorial_product = ff_q_bcpdb_right_factorial_product_start * S ((S (0)) * ff_v_bcpdb_right_factorial_product) + (1))) /\ ((((exists ff_h_bcpdb_right_factorial_product_terminal. ff_h_bcpdb_right_factorial_product_terminal + S (J) = S ((S (j)) * ff_v_bcpdb_right_factorial_product)) /\ exists ff_q_bcpdb_right_factorial_product_terminal. ff_u_bcpdb_right_factorial_product = ff_q_bcpdb_right_factorial_product_terminal * S ((S (j)) * ff_v_bcpdb_right_factorial_product) + (J))) /\ forall ff_i_bcpdb_right_factorial_product. (exists ff_lt_bcpdb_right_factorial_product_bound. ff_lt_bcpdb_right_factorial_product_bound + S ff_i_bcpdb_right_factorial_product = j) -> exists ff_p_bcpdb_right_factorial_product ff_r_bcpdb_right_factorial_product ff_s_bcpdb_right_factorial_product. ((((exists ff_h_bcpdb_right_factorial_product_factor. ff_h_bcpdb_right_factorial_product_factor + S (ff_p_bcpdb_right_factorial_product) = S ((S (ff_i_bcpdb_right_factorial_product)) * ff_c_bcpdb_right_factorial)) /\ exists ff_q_bcpdb_right_factorial_product_factor. ff_b_bcpdb_right_factorial = ff_q_bcpdb_right_factorial_product_factor * S ((S (ff_i_bcpdb_right_factorial_product)) * ff_c_bcpdb_right_factorial) + (ff_p_bcpdb_right_factorial_product))) /\ ((((exists ff_h_bcpdb_right_factorial_product_partial. ff_h_bcpdb_right_factorial_product_partial + S (ff_r_bcpdb_right_factorial_product) = S ((S (ff_i_bcpdb_right_factorial_product)) * ff_v_bcpdb_right_factorial_product)) /\ exists ff_q_bcpdb_right_factorial_product_partial. ff_u_bcpdb_right_factorial_product = ff_q_bcpdb_right_factorial_product_partial * S ((S (ff_i_bcpdb_right_factorial_product)) * ff_v_bcpdb_right_factorial_product) + (ff_r_bcpdb_right_factorial_product))) /\ ((((exists ff_h_bcpdb_right_factorial_product_successor. ff_h_bcpdb_right_factorial_product_successor + S (ff_s_bcpdb_right_factorial_product) = S ((S (S ff_i_bcpdb_right_factorial_product)) * ff_v_bcpdb_right_factorial_product)) /\ exists ff_q_bcpdb_right_factorial_product_successor. ff_u_bcpdb_right_factorial_product = ff_q_bcpdb_right_factorial_product_successor * S ((S (S ff_i_bcpdb_right_factorial_product)) * ff_v_bcpdb_right_factorial_product) + (ff_s_bcpdb_right_factorial_product))) /\ ff_s_bcpdb_right_factorial_product = ff_r_bcpdb_right_factorial_product * ff_p_bcpdb_right_factorial_product))))))))
  19. 0019apply factorial_exists
  20. 0020cases hJ
  21. 0021have hbridge : x = (x1 * x2) * c
  22. 0022specialize choose_factorial_bridge n
  23. 0023specialize choose_factorial_bridge k
  24. 0024specialize choose_factorial_bridge j
  25. 0025specialize choose_factorial_bridge c
  26. 0026specialize choose_factorial_bridge x
  27. 0027specialize choose_factorial_bridge x1
  28. 0028specialize choose_factorial_bridge x2
  29. 0029apply choose_factorial_bridge
  30. 0030exact hsum
  31. 0031exact hchoose
  32. 0032exact hF_witness
  33. 0033exact hK_witness
  34. 0034exact hJ_witness
  35. 0035have htotal : Dvd(p,x)
    Exact native replay linehave htotal : exists bpr_quotient_bcpdb_total_divides. x = (p) * bpr_quotient_bcpdb_total_divides
  36. 0036specialize factorial_prime_divides_of_le p
  37. 0037specialize factorial_prime_divides_of_le n
  38. 0038specialize factorial_prime_divides_of_le x
  39. 0039apply factorial_prime_divides_of_le
  40. 0040exact hp
  41. 0041exact hpn
  42. 0042exact hF_witness
  43. 0043rewrite hbridge at htotal
  44. 0044have houter : Dvd(p,x1 · x2) ∨ Dvd(p,c)
    Exact native replay linehave houter : (exists bpr_quotient_bcpdb_outer_left. x1 * x2 = (p) * bpr_quotient_bcpdb_outer_left) \/ (exists bpr_quotient_bcpdb_outer_right. c = (p) * bpr_quotient_bcpdb_outer_right)
  45. 0045specialize euclid_prime_dvd_product p
  46. 0046specialize euclid_prime_dvd_product (x1 * x2)
  47. 0047specialize euclid_prime_dvd_product c
  48. 0048apply euclid_prime_dvd_product
  49. 0049exact hp
  50. 0050exact htotal
  51. 0051cases houter
  52. 0052have hinner : Dvd(p,x1) ∨ Dvd(p,x2)
    Exact native replay linehave hinner : (exists bpr_quotient_bcpdb_inner_left. x1 = (p) * bpr_quotient_bcpdb_inner_left) \/ (exists bpr_quotient_bcpdb_inner_right. x2 = (p) * bpr_quotient_bcpdb_inner_right)
  53. 0053specialize euclid_prime_dvd_product p
  54. 0054specialize euclid_prime_dvd_product x1
  55. 0055specialize euclid_prime_dvd_product x2
  56. 0056apply euclid_prime_dvd_product
  57. 0057exact hp
  58. 0058exact houter_left
  59. 0059cases hinner
  60. 0060have hpk : Le(p,k)
    Exact native replay linehave hpk : exists g. g + p = k
  61. 0061specialize factorial_prime_le_of_divides p
  62. 0062specialize factorial_prime_le_of_divides k
  63. 0063specialize factorial_prime_le_of_divides x1
  64. 0064apply factorial_prime_le_of_divides
  65. 0065exact hp
  66. 0066exact hK_witness
  67. 0067exact hinner_left
  68. 0068exfalso
  69. 0069specialize lt_not_le k
  70. 0070specialize lt_not_le p
  71. 0071apply lt_not_le
  72. 0072exact hk
  73. 0073exact hpk
  74. 0074have hpj : Le(p,j)
    Exact native replay linehave hpj : exists g. g + p = j
  75. 0075specialize factorial_prime_le_of_divides p
  76. 0076specialize factorial_prime_le_of_divides j
  77. 0077specialize factorial_prime_le_of_divides x2
  78. 0078apply factorial_prime_le_of_divides
  79. 0079exact hp
  80. 0080exact hJ_witness
  81. 0081exact hinner_right
  82. 0082exfalso
  83. 0083specialize lt_not_le j
  84. 0084specialize lt_not_le p
  85. 0085apply lt_not_le
  86. 0086exact hj
  87. 0087exact hpj
  88. 0088exact houter_right