TS0032 · theorem body

even_valuation_sorted_terminal_prime_has_equal_predecessor

dependency-curried kernel-checked candidate body; not enrolled in Alpha or Stable

In a sorted all-prime beta factorization, a terminal prime with positive even valuation has the identical immediately preceding factor.

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

∀ b. ∀ c. ∀ l. ∀ n. ∀ p. ∀ e. ∀ h. Prime(p) → AllPrime(b,c,S S l) → Sorted(b,c,S S l) → Product(b,c,S S l,n) → BetaAt(b,c,S l,p) → ¬n = 0 → PowerValuation(p,n,e) → e = h + h → BetaAt(b,c,l,p)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0004 Prime PD0013 BetaAt PD0014 Product PD0028 AllPrime PD0029 Sorted PD0046 PowerValuation

In local proof propositions

PD0001 Le PD0003 Dvd PD0013 BetaAt PD0014 Product PD0028 AllPrime PD0029 Sorted
Exact expanded first-order statement
forall b c l n p e h. ((~(p = 1) /\ forall frm_prime_left_ftsp_p frm_prime_right_ftsp_p. p = frm_prime_left_ftsp_p * frm_prime_right_ftsp_p -> frm_prime_left_ftsp_p = 1 \/ frm_prime_right_ftsp_p = 1)) -> (forall ftsf_index_ftsp_full. (exists ftsf_gap_ftsp_full_bound. ftsf_gap_ftsp_full_bound + S ftsf_index_ftsp_full = (S (S l))) -> exists ftsf_factor_ftsp_full. ((((exists ff_h_ftsf_ftsp_full_entry. ff_h_ftsf_ftsp_full_entry + S (ftsf_factor_ftsp_full) = S ((S (ftsf_index_ftsp_full)) * c)) /\ exists ff_q_ftsf_ftsp_full_entry. b = ff_q_ftsf_ftsp_full_entry * S ((S (ftsf_index_ftsp_full)) * c) + (ftsf_factor_ftsp_full))) /\ ((~(ftsf_factor_ftsp_full = 1) /\ forall frm_prime_left_ftsf_ftsp_full_prime frm_prime_right_ftsf_ftsp_full_prime. ftsf_factor_ftsp_full = frm_prime_left_ftsf_ftsp_full_prime * frm_prime_right_ftsf_ftsp_full_prime -> frm_prime_left_ftsf_ftsp_full_prime = 1 \/ frm_prime_right_ftsf_ftsp_full_prime = 1)))) -> (forall ftsp_index_full. (exists ftsp_bound_full. ftsp_bound_full + S (S ftsp_index_full) = (S (S l))) -> exists ftsp_left_full ftsp_right_full. ((((exists ff_h_ftsp_full_left. ff_h_ftsp_full_left + S (ftsp_left_full) = S ((S (ftsp_index_full)) * c)) /\ exists ff_q_ftsp_full_left. b = ff_q_ftsp_full_left * S ((S (ftsp_index_full)) * c) + (ftsp_left_full))) /\ ((((exists ff_h_ftsp_full_right. ff_h_ftsp_full_right + S (ftsp_right_full) = S ((S (S ftsp_index_full)) * c)) /\ exists ff_q_ftsp_full_right. b = ff_q_ftsp_full_right * S ((S (S ftsp_index_full)) * c) + (ftsp_right_full))) /\ (exists ftsp_order_full. ftsp_order_full + ftsp_left_full = ftsp_right_full)))) -> (exists ff_u_ftsp_full ff_v_ftsp_full. ((((exists ff_h_ftsp_full_start. ff_h_ftsp_full_start + S (1) = S ((S (0)) * ff_v_ftsp_full)) /\ exists ff_q_ftsp_full_start. ff_u_ftsp_full = ff_q_ftsp_full_start * S ((S (0)) * ff_v_ftsp_full) + (1))) /\ ((((exists ff_h_ftsp_full_terminal. ff_h_ftsp_full_terminal + S (n) = S ((S (S (S l))) * ff_v_ftsp_full)) /\ exists ff_q_ftsp_full_terminal. ff_u_ftsp_full = ff_q_ftsp_full_terminal * S ((S (S (S l))) * ff_v_ftsp_full) + (n))) /\ forall ff_i_ftsp_full. (exists ff_lt_ftsp_full_bound. ff_lt_ftsp_full_bound + S ff_i_ftsp_full = S (S l)) -> exists ff_p_ftsp_full ff_r_ftsp_full ff_s_ftsp_full. ((((exists ff_h_ftsp_full_factor. ff_h_ftsp_full_factor + S (ff_p_ftsp_full) = S ((S (ff_i_ftsp_full)) * c)) /\ exists ff_q_ftsp_full_factor. b = ff_q_ftsp_full_factor * S ((S (ff_i_ftsp_full)) * c) + (ff_p_ftsp_full))) /\ ((((exists ff_h_ftsp_full_partial. ff_h_ftsp_full_partial + S (ff_r_ftsp_full) = S ((S (ff_i_ftsp_full)) * ff_v_ftsp_full)) /\ exists ff_q_ftsp_full_partial. ff_u_ftsp_full = ff_q_ftsp_full_partial * S ((S (ff_i_ftsp_full)) * ff_v_ftsp_full) + (ff_r_ftsp_full))) /\ ((((exists ff_h_ftsp_full_successor. ff_h_ftsp_full_successor + S (ff_s_ftsp_full) = S ((S (S ff_i_ftsp_full)) * ff_v_ftsp_full)) /\ exists ff_q_ftsp_full_successor. ff_u_ftsp_full = ff_q_ftsp_full_successor * S ((S (S ff_i_ftsp_full)) * ff_v_ftsp_full) + (ff_s_ftsp_full))) /\ ff_s_ftsp_full = ff_r_ftsp_full * ff_p_ftsp_full)))))) -> (((exists ff_h_ftsp_terminal. ff_h_ftsp_terminal + S (p) = S ((S (S l)) * c)) /\ exists ff_q_ftsp_terminal. b = ff_q_ftsp_terminal * S ((S (S l)) * c) + (p))) -> ~(n = 0) -> (((exists bpv_gap_ftsp_source_exponent_bound. bpv_gap_ftsp_source_exponent_bound + e = n) /\ (exists bpv_result_ftsp_source_selected. ((exists ff_b_ftsp_source_selected_power ff_c_ftsp_source_selected_power. ((forall ff_i_ftsp_source_selected_power_repeat. (exists ff_lt_ftsp_source_selected_power_repeat_bound. ff_lt_ftsp_source_selected_power_repeat_bound + S ff_i_ftsp_source_selected_power_repeat = e) -> (((exists ff_h_ftsp_source_selected_power_repeat_decoded. ff_h_ftsp_source_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_source_selected_power_repeat)) * ff_c_ftsp_source_selected_power)) /\ exists ff_q_ftsp_source_selected_power_repeat_decoded. ff_b_ftsp_source_selected_power = ff_q_ftsp_source_selected_power_repeat_decoded * S ((S (ff_i_ftsp_source_selected_power_repeat)) * ff_c_ftsp_source_selected_power) + (p)))) /\ (exists ff_u_ftsp_source_selected_power_product ff_v_ftsp_source_selected_power_product. ((((exists ff_h_ftsp_source_selected_power_product_start. ff_h_ftsp_source_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_source_selected_power_product)) /\ exists ff_q_ftsp_source_selected_power_product_start. ff_u_ftsp_source_selected_power_product = ff_q_ftsp_source_selected_power_product_start * S ((S (0)) * ff_v_ftsp_source_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_source_selected_power_product_terminal. ff_h_ftsp_source_selected_power_product_terminal + S (bpv_result_ftsp_source_selected) = S ((S (e)) * ff_v_ftsp_source_selected_power_product)) /\ exists ff_q_ftsp_source_selected_power_product_terminal. ff_u_ftsp_source_selected_power_product = ff_q_ftsp_source_selected_power_product_terminal * S ((S (e)) * ff_v_ftsp_source_selected_power_product) + (bpv_result_ftsp_source_selected))) /\ forall ff_i_ftsp_source_selected_power_product. (exists ff_lt_ftsp_source_selected_power_product_bound. ff_lt_ftsp_source_selected_power_product_bound + S ff_i_ftsp_source_selected_power_product = e) -> exists ff_p_ftsp_source_selected_power_product ff_r_ftsp_source_selected_power_product ff_s_ftsp_source_selected_power_product. ((((exists ff_h_ftsp_source_selected_power_product_factor. ff_h_ftsp_source_selected_power_product_factor + S (ff_p_ftsp_source_selected_power_product) = S ((S (ff_i_ftsp_source_selected_power_product)) * ff_c_ftsp_source_selected_power)) /\ exists ff_q_ftsp_source_selected_power_product_factor. ff_b_ftsp_source_selected_power = ff_q_ftsp_source_selected_power_product_factor * S ((S (ff_i_ftsp_source_selected_power_product)) * ff_c_ftsp_source_selected_power) + (ff_p_ftsp_source_selected_power_product))) /\ ((((exists ff_h_ftsp_source_selected_power_product_partial. ff_h_ftsp_source_selected_power_product_partial + S (ff_r_ftsp_source_selected_power_product) = S ((S (ff_i_ftsp_source_selected_power_product)) * ff_v_ftsp_source_selected_power_product)) /\ exists ff_q_ftsp_source_selected_power_product_partial. ff_u_ftsp_source_selected_power_product = ff_q_ftsp_source_selected_power_product_partial * S ((S (ff_i_ftsp_source_selected_power_product)) * ff_v_ftsp_source_selected_power_product) + (ff_r_ftsp_source_selected_power_product))) /\ ((((exists ff_h_ftsp_source_selected_power_product_successor. ff_h_ftsp_source_selected_power_product_successor + S (ff_s_ftsp_source_selected_power_product) = S ((S (S ff_i_ftsp_source_selected_power_product)) * ff_v_ftsp_source_selected_power_product)) /\ exists ff_q_ftsp_source_selected_power_product_successor. ff_u_ftsp_source_selected_power_product = ff_q_ftsp_source_selected_power_product_successor * S ((S (S ff_i_ftsp_source_selected_power_product)) * ff_v_ftsp_source_selected_power_product) + (ff_s_ftsp_source_selected_power_product))) /\ ff_s_ftsp_source_selected_power_product = ff_r_ftsp_source_selected_power_product * ff_p_ftsp_source_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_source_selected_divides. n = bpv_result_ftsp_source_selected * bpv_factor_ftsp_source_selected_divides)))) /\ forall bpv_candidate_ftsp_source. (exists bpv_gap_ftsp_source_candidate_bound. bpv_gap_ftsp_source_candidate_bound + bpv_candidate_ftsp_source = n) -> (exists bpv_result_ftsp_source_candidate. ((exists ff_b_ftsp_source_candidate_power ff_c_ftsp_source_candidate_power. ((forall ff_i_ftsp_source_candidate_power_repeat. (exists ff_lt_ftsp_source_candidate_power_repeat_bound. ff_lt_ftsp_source_candidate_power_repeat_bound + S ff_i_ftsp_source_candidate_power_repeat = bpv_candidate_ftsp_source) -> (((exists ff_h_ftsp_source_candidate_power_repeat_decoded. ff_h_ftsp_source_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_source_candidate_power_repeat)) * ff_c_ftsp_source_candidate_power)) /\ exists ff_q_ftsp_source_candidate_power_repeat_decoded. ff_b_ftsp_source_candidate_power = ff_q_ftsp_source_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_source_candidate_power_repeat)) * ff_c_ftsp_source_candidate_power) + (p)))) /\ (exists ff_u_ftsp_source_candidate_power_product ff_v_ftsp_source_candidate_power_product. ((((exists ff_h_ftsp_source_candidate_power_product_start. ff_h_ftsp_source_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_source_candidate_power_product)) /\ exists ff_q_ftsp_source_candidate_power_product_start. ff_u_ftsp_source_candidate_power_product = ff_q_ftsp_source_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_source_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_source_candidate_power_product_terminal. ff_h_ftsp_source_candidate_power_product_terminal + S (bpv_result_ftsp_source_candidate) = S ((S (bpv_candidate_ftsp_source)) * ff_v_ftsp_source_candidate_power_product)) /\ exists ff_q_ftsp_source_candidate_power_product_terminal. ff_u_ftsp_source_candidate_power_product = ff_q_ftsp_source_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_source)) * ff_v_ftsp_source_candidate_power_product) + (bpv_result_ftsp_source_candidate))) /\ forall ff_i_ftsp_source_candidate_power_product. (exists ff_lt_ftsp_source_candidate_power_product_bound. ff_lt_ftsp_source_candidate_power_product_bound + S ff_i_ftsp_source_candidate_power_product = bpv_candidate_ftsp_source) -> exists ff_p_ftsp_source_candidate_power_product ff_r_ftsp_source_candidate_power_product ff_s_ftsp_source_candidate_power_product. ((((exists ff_h_ftsp_source_candidate_power_product_factor. ff_h_ftsp_source_candidate_power_product_factor + S (ff_p_ftsp_source_candidate_power_product) = S ((S (ff_i_ftsp_source_candidate_power_product)) * ff_c_ftsp_source_candidate_power)) /\ exists ff_q_ftsp_source_candidate_power_product_factor. ff_b_ftsp_source_candidate_power = ff_q_ftsp_source_candidate_power_product_factor * S ((S (ff_i_ftsp_source_candidate_power_product)) * ff_c_ftsp_source_candidate_power) + (ff_p_ftsp_source_candidate_power_product))) /\ ((((exists ff_h_ftsp_source_candidate_power_product_partial. ff_h_ftsp_source_candidate_power_product_partial + S (ff_r_ftsp_source_candidate_power_product) = S ((S (ff_i_ftsp_source_candidate_power_product)) * ff_v_ftsp_source_candidate_power_product)) /\ exists ff_q_ftsp_source_candidate_power_product_partial. ff_u_ftsp_source_candidate_power_product = ff_q_ftsp_source_candidate_power_product_partial * S ((S (ff_i_ftsp_source_candidate_power_product)) * ff_v_ftsp_source_candidate_power_product) + (ff_r_ftsp_source_candidate_power_product))) /\ ((((exists ff_h_ftsp_source_candidate_power_product_successor. ff_h_ftsp_source_candidate_power_product_successor + S (ff_s_ftsp_source_candidate_power_product) = S ((S (S ff_i_ftsp_source_candidate_power_product)) * ff_v_ftsp_source_candidate_power_product)) /\ exists ff_q_ftsp_source_candidate_power_product_successor. ff_u_ftsp_source_candidate_power_product = ff_q_ftsp_source_candidate_power_product_successor * S ((S (S ff_i_ftsp_source_candidate_power_product)) * ff_v_ftsp_source_candidate_power_product) + (ff_s_ftsp_source_candidate_power_product))) /\ ff_s_ftsp_source_candidate_power_product = ff_r_ftsp_source_candidate_power_product * ff_p_ftsp_source_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_source_candidate_divides. n = bpv_result_ftsp_source_candidate * bpv_factor_ftsp_source_candidate_divides))) -> (exists bpv_gap_ftsp_source_maximal. bpv_gap_ftsp_source_maximal + bpv_candidate_ftsp_source = e)) -> e = h + h -> (((exists ff_h_ftsp_predecessor. ff_h_ftsp_predecessor + S (p) = S ((S (l)) * c)) /\ exists ff_q_ftsp_predecessor. b = ff_q_ftsp_predecessor * S ((S (l)) * c) + (p)))

Proof neighborhood

Direct theorem prerequisites

beta_product_succ_decompose · Stable closed beta_at_unique · Stable closed mul_comm · Stable closed TS002Z even_positive_prime_valuation_has_square_divisor TS0030 prime_square_divisibility_forces_suffix_prime_divisor all_prime_succ_elim_prefix · Stable closed sorted_succ_elim_prefix · Stable closed sorted_succ_elim_last · Stable closed TS0031 beta_sorted_prime_prefix_divisor_equals_bounded_last

Direct theorem dependents

none

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

117 script commands · 23 reading checkpoints · 12 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)
even positive prime valuation has square divisorprime square divisibility forces suffix prime divisorbeta sorted prime prefix divisor equals bounded last
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro n
  5. L5
    intro p
  6. L6
    intro e
  7. L7
    intro h
  8. L8
    intro hprime
  9. L9
    intro hallprime
  10. L10
    intro hsorted
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hproduct
  2. L12
    intro hterminal
  3. L13
    intro hnonzero
  4. L14
    intro hvaluation
  5. L15
    intro heven
03Establish hdecompositionL16–22

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

  1. L16
    have hdecomposition : ∃ t. ∃ r. BetaAt(b,c,S l,t) ∧ (Product(b,c,S l,r) ∧ n = r · t)Definitions: BetaAt(b,c,S l,t)Product(b,c,S l,r)Original native command in the exact edition
  2. L17
    specialize beta_product_succ_decompose b
  3. L18
    specialize beta_product_succ_decompose c
  4. L19
    specialize beta_product_succ_decompose (S l)
  5. L20
    specialize beta_product_succ_decompose n
  6. L21
    apply beta_product_succ_decompose
  7. L22
    exact hproduct
04Separate the logical casesL23–26

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

  1. L23
    cases hdecomposition
  2. L24
    cases hdecomposition_witness
  3. L25
    cases hdecomposition_witness_witness
  4. L26
    cases hdecomposition_witness_witness_right
05Establish hlast_equalL27–35

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

  1. L27
    have hlast_equal : x = p
  2. L28
    specialize beta_at_unique b
  3. L29
    specialize beta_at_unique c
  4. L30
    specialize beta_at_unique (S l)
  5. L31
    specialize beta_at_unique x
  6. L32
    specialize beta_at_unique p
  7. L33
    apply beta_at_unique
  8. L34
    exact hdecomposition_witness_witness_left
  9. L35
    exact hterminal
06Establish hfactorizationL36–41

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

  1. L36
    have hfactorization : n = x1 * p
  2. L37
    trans x1 * x
  3. L38
    exact hdecomposition_witness_witness_right_right
  4. L39
    congr
  5. L40
    refl
  6. L41
    exact hlast_equal
07Establish hprime_dividesL42–42

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

  1. L42
    have hprime_divides : Dvd(p,n)Definitions: Dvd(p,n)Original native command in the exact edition
08Construct an explicit witnessL43–43

Supply the displayed value, then prove that it has the required property.

  1. L43
    exists x1
09Calculate and transport equalitiesL44–44

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

  1. L44
    trans x1 * p
10Use earlier factsL45–46

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

  1. L45
    exact hfactorization
  2. L46
    apply mul_comm
11Establish hsquare_dividesL47–56

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply even positive prime valuation has square divisor.

  1. L47
    have hsquare_divides : Dvd(p · p,n)Definitions: Dvd(p · p,n)Original native command in the exact edition
  2. L48
    specialize even_positive_prime_valuation_has_square_divisor p
  3. L49
    specialize even_positive_prime_valuation_has_square_divisor n
  4. L50
    specialize even_positive_prime_valuation_has_square_divisor e
  5. L51
    specialize even_positive_prime_valuation_has_square_divisor h
  6. L52
    apply even_positive_prime_valuation_has_square_divisor
  7. L53
    exact hprime
  8. L54
    exact hnonzero
  9. L55
    exact hvaluation
  10. L56
    exact hprime_divides
12Use earlier factsL57–57

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

  1. L57
    exact heven
13Establish hprefix_dividesL58–65

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime square divisibility forces suffix prime divisor.

  1. L58
    have hprefix_divides : Dvd(p,x1)Definitions: Dvd(p,x1)Original native command in the exact edition
  2. L59
    specialize prime_square_divisibility_forces_suffix_prime_divisor p
  3. L60
    specialize prime_square_divisibility_forces_suffix_prime_divisor x1
  4. L61
    specialize prime_square_divisibility_forces_suffix_prime_divisor n
  5. L62
    apply prime_square_divisibility_forces_suffix_prime_divisor
  6. L63
    exact hprime
  7. L64
    exact hfactorization
  8. L65
    exact hsquare_divides
14Establish hprefix_primeL66–71

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

  1. L66
    have hprefix_prime : AllPrime(b,c,S l)Definitions: AllPrime(b,c,S l)Original native command in the exact edition
  2. L67
    specialize all_prime_succ_elim_prefix b
  3. L68
    specialize all_prime_succ_elim_prefix c
  4. L69
    specialize all_prime_succ_elim_prefix (S l)
  5. L70
    apply all_prime_succ_elim_prefix
  6. L71
    exact hallprime
15Establish hprefix_sortedL72–77

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply sorted succ elim prefix.

  1. L72
    have hprefix_sorted : Sorted(b,c,S l)Definitions: Sorted(b,c,S l)Original native command in the exact edition
  2. L73
    specialize sorted_succ_elim_prefix b
  3. L74
    specialize sorted_succ_elim_prefix c
  4. L75
    specialize sorted_succ_elim_prefix (S l)
  5. L76
    apply sorted_succ_elim_prefix
  6. L77
    exact hsorted
16Establish hlast_pairL78–83

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply sorted succ elim last.

  1. L78
    have hlast_pair : ∃ u. ∃ v. BetaAt(b,c,l,u) ∧ (BetaAt(b,c,S l,v) ∧ Le(u,v))Definitions: BetaAt(b,c,l,u)BetaAt(b,c,S l,v)Le(u,v)Original native command in the exact edition
  2. L79
    specialize sorted_succ_elim_last b
  3. L80
    specialize sorted_succ_elim_last c
  4. L81
    specialize sorted_succ_elim_last l
  5. L82
    apply sorted_succ_elim_last
  6. L83
    exact hsorted
17Separate the logical casesL84–87

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

  1. L84
    cases hlast_pair
  2. L85
    cases hlast_pair_witness
  3. L86
    cases hlast_pair_witness_witness
  4. L87
    cases hlast_pair_witness_witness_right
18Establish hright_equalL88–96

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

  1. L88
    have hright_equal : x3 = p
  2. L89
    specialize beta_at_unique b
  3. L90
    specialize beta_at_unique c
  4. L91
    specialize beta_at_unique (S l)
  5. L92
    specialize beta_at_unique x3
  6. L93
    specialize beta_at_unique p
  7. L94
    apply beta_at_unique
  8. L95
    exact hlast_pair_witness_witness_right_left
  9. L96
    exact hterminal
19Establish hupperL97–99

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

  1. L97
    have hupper : Le(x2,p)Definitions: Le(x2,p)Original native command in the exact edition
  2. L98
    rewrite hright_equal at hlast_pair_witness_witness_right_right
  3. L99
    exact hlast_pair_witness_witness_right_right
20Establish hpredecessor_equalL100–109

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sorted prime prefix divisor equals bounded last.

  1. L100
    have hpredecessor_equal : x2 = p
  2. L101
    specialize beta_sorted_prime_prefix_divisor_equals_bounded_last b
  3. L102
    specialize beta_sorted_prime_prefix_divisor_equals_bounded_last c
  4. L103
    specialize beta_sorted_prime_prefix_divisor_equals_bounded_last l
  5. L104
    specialize beta_sorted_prime_prefix_divisor_equals_bounded_last x1
  6. L105
    specialize beta_sorted_prime_prefix_divisor_equals_bounded_last p
  7. L106
    specialize beta_sorted_prime_prefix_divisor_equals_bounded_last x2
  8. L107
    apply beta_sorted_prime_prefix_divisor_equals_bounded_last
  9. L108
    exact hprime
  10. L109
    exact hprefix_prime
21Use earlier factsL110–114

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

  1. L110
    exact hprefix_sorted
  2. L111
    exact hdecomposition_witness_witness_right_left
  3. L112
    exact hlast_pair_witness_witness_left
  4. L113
    exact hprefix_divides
  5. L114
    exact hupper
22Calculate and transport equalitiesL115–116

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

  1. L115
    rewrite hpredecessor_equal at hlast_pair_witness_witness_left
  2. L116
    rewrite hpredecessor_equal at hlast_pair_witness_witness_left
23Use earlier factsL117–117

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

  1. L117
    exact hlast_pair_witness_witness_left

Library-wide reading audit

Original defined command ledger · 117 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro n
  5. 0005intro p
  6. 0006intro e
  7. 0007intro h
  8. 0008intro hprime
  9. 0009intro hallprime
  10. 0010intro hsorted
  11. 0011intro hproduct
  12. 0012intro hterminal
  13. 0013intro hnonzero
  14. 0014intro hvaluation
  15. 0015intro heven
  16. 0016have hdecomposition : ∃ t. ∃ r. BetaAt(b,c,S l,t) ∧ (Product(b,c,S l,r) ∧ n = r · t)
    Exact native replay linehave hdecomposition : exists t r. ((((exists ff_h_ftsp_decomposition_entry. ff_h_ftsp_decomposition_entry + S (t) = S ((S (S l)) * c)) /\ exists ff_q_ftsp_decomposition_entry. b = ff_q_ftsp_decomposition_entry * S ((S (S l)) * c) + (t))) /\ ((exists ff_u_ftsp_decomposition ff_v_ftsp_decomposition. ((((exists ff_h_ftsp_decomposition_start. ff_h_ftsp_decomposition_start + S (1) = S ((S (0)) * ff_v_ftsp_decomposition)) /\ exists ff_q_ftsp_decomposition_start. ff_u_ftsp_decomposition = ff_q_ftsp_decomposition_start * S ((S (0)) * ff_v_ftsp_decomposition) + (1))) /\ ((((exists ff_h_ftsp_decomposition_terminal. ff_h_ftsp_decomposition_terminal + S (r) = S ((S (S l)) * ff_v_ftsp_decomposition)) /\ exists ff_q_ftsp_decomposition_terminal. ff_u_ftsp_decomposition = ff_q_ftsp_decomposition_terminal * S ((S (S l)) * ff_v_ftsp_decomposition) + (r))) /\ forall ff_i_ftsp_decomposition. (exists ff_lt_ftsp_decomposition_bound. ff_lt_ftsp_decomposition_bound + S ff_i_ftsp_decomposition = S l) -> exists ff_p_ftsp_decomposition ff_r_ftsp_decomposition ff_s_ftsp_decomposition. ((((exists ff_h_ftsp_decomposition_factor. ff_h_ftsp_decomposition_factor + S (ff_p_ftsp_decomposition) = S ((S (ff_i_ftsp_decomposition)) * c)) /\ exists ff_q_ftsp_decomposition_factor. b = ff_q_ftsp_decomposition_factor * S ((S (ff_i_ftsp_decomposition)) * c) + (ff_p_ftsp_decomposition))) /\ ((((exists ff_h_ftsp_decomposition_partial. ff_h_ftsp_decomposition_partial + S (ff_r_ftsp_decomposition) = S ((S (ff_i_ftsp_decomposition)) * ff_v_ftsp_decomposition)) /\ exists ff_q_ftsp_decomposition_partial. ff_u_ftsp_decomposition = ff_q_ftsp_decomposition_partial * S ((S (ff_i_ftsp_decomposition)) * ff_v_ftsp_decomposition) + (ff_r_ftsp_decomposition))) /\ ((((exists ff_h_ftsp_decomposition_successor. ff_h_ftsp_decomposition_successor + S (ff_s_ftsp_decomposition) = S ((S (S ff_i_ftsp_decomposition)) * ff_v_ftsp_decomposition)) /\ exists ff_q_ftsp_decomposition_successor. ff_u_ftsp_decomposition = ff_q_ftsp_decomposition_successor * S ((S (S ff_i_ftsp_decomposition)) * ff_v_ftsp_decomposition) + (ff_s_ftsp_decomposition))) /\ ff_s_ftsp_decomposition = ff_r_ftsp_decomposition * ff_p_ftsp_decomposition)))))) /\ n = r * t))
  17. 0017specialize beta_product_succ_decompose b
  18. 0018specialize beta_product_succ_decompose c
  19. 0019specialize beta_product_succ_decompose (S l)
  20. 0020specialize beta_product_succ_decompose n
  21. 0021apply beta_product_succ_decompose
  22. 0022exact hproduct
  23. 0023cases hdecomposition
  24. 0024cases hdecomposition_witness
  25. 0025cases hdecomposition_witness_witness
  26. 0026cases hdecomposition_witness_witness_right
  27. 0027have hlast_equal : x = p
  28. 0028specialize beta_at_unique b
  29. 0029specialize beta_at_unique c
  30. 0030specialize beta_at_unique (S l)
  31. 0031specialize beta_at_unique x
  32. 0032specialize beta_at_unique p
  33. 0033apply beta_at_unique
  34. 0034exact hdecomposition_witness_witness_left
  35. 0035exact hterminal
  36. 0036have hfactorization : n = x1 * p
  37. 0037trans x1 * x
  38. 0038exact hdecomposition_witness_witness_right_right
  39. 0039congr
  40. 0040refl
  41. 0041exact hlast_equal
  42. 0042have hprime_divides : Dvd(p,n)
    Exact native replay linehave hprime_divides : exists ftcn_factor_ftsp_value. (n) = (p) * ftcn_factor_ftsp_value
  43. 0043exists x1
  44. 0044trans x1 * p
  45. 0045exact hfactorization
  46. 0046apply mul_comm
  47. 0047have hsquare_divides : Dvd(p · p,n)
    Exact native replay linehave hsquare_divides : exists ftcn_factor_ftsp_square. (n) = (p * p) * ftcn_factor_ftsp_square
  48. 0048specialize even_positive_prime_valuation_has_square_divisor p
  49. 0049specialize even_positive_prime_valuation_has_square_divisor n
  50. 0050specialize even_positive_prime_valuation_has_square_divisor e
  51. 0051specialize even_positive_prime_valuation_has_square_divisor h
  52. 0052apply even_positive_prime_valuation_has_square_divisor
  53. 0053exact hprime
  54. 0054exact hnonzero
  55. 0055exact hvaluation
  56. 0056exact hprime_divides
  57. 0057exact heven
  58. 0058have hprefix_divides : Dvd(p,x1)
    Exact native replay linehave hprefix_divides : exists ftcn_factor_ftsp_terminal_prefix_divides. (x1) = (p) * ftcn_factor_ftsp_terminal_prefix_divides
  59. 0059specialize prime_square_divisibility_forces_suffix_prime_divisor p
  60. 0060specialize prime_square_divisibility_forces_suffix_prime_divisor x1
  61. 0061specialize prime_square_divisibility_forces_suffix_prime_divisor n
  62. 0062apply prime_square_divisibility_forces_suffix_prime_divisor
  63. 0063exact hprime
  64. 0064exact hfactorization
  65. 0065exact hsquare_divides
  66. 0066have hprefix_prime : AllPrime(b,c,S l)
    Exact native replay linehave hprefix_prime : forall ftsf_index_ftsp_prefix. (exists ftsf_gap_ftsp_prefix_bound. ftsf_gap_ftsp_prefix_bound + S ftsf_index_ftsp_prefix = (S l)) -> exists ftsf_factor_ftsp_prefix. ((((exists ff_h_ftsf_ftsp_prefix_entry. ff_h_ftsf_ftsp_prefix_entry + S (ftsf_factor_ftsp_prefix) = S ((S (ftsf_index_ftsp_prefix)) * c)) /\ exists ff_q_ftsf_ftsp_prefix_entry. b = ff_q_ftsf_ftsp_prefix_entry * S ((S (ftsf_index_ftsp_prefix)) * c) + (ftsf_factor_ftsp_prefix))) /\ ((~(ftsf_factor_ftsp_prefix = 1) /\ forall frm_prime_left_ftsf_ftsp_prefix_prime frm_prime_right_ftsf_ftsp_prefix_prime. ftsf_factor_ftsp_prefix = frm_prime_left_ftsf_ftsp_prefix_prime * frm_prime_right_ftsf_ftsp_prefix_prime -> frm_prime_left_ftsf_ftsp_prefix_prime = 1 \/ frm_prime_right_ftsf_ftsp_prefix_prime = 1)))
  67. 0067specialize all_prime_succ_elim_prefix b
  68. 0068specialize all_prime_succ_elim_prefix c
  69. 0069specialize all_prime_succ_elim_prefix (S l)
  70. 0070apply all_prime_succ_elim_prefix
  71. 0071exact hallprime
  72. 0072have hprefix_sorted : Sorted(b,c,S l)
    Exact native replay linehave hprefix_sorted : forall ftsp_index_prefix. (exists ftsp_bound_prefix. ftsp_bound_prefix + S (S ftsp_index_prefix) = (S l)) -> exists ftsp_left_prefix ftsp_right_prefix. ((((exists ff_h_ftsp_prefix_left. ff_h_ftsp_prefix_left + S (ftsp_left_prefix) = S ((S (ftsp_index_prefix)) * c)) /\ exists ff_q_ftsp_prefix_left. b = ff_q_ftsp_prefix_left * S ((S (ftsp_index_prefix)) * c) + (ftsp_left_prefix))) /\ ((((exists ff_h_ftsp_prefix_right. ff_h_ftsp_prefix_right + S (ftsp_right_prefix) = S ((S (S ftsp_index_prefix)) * c)) /\ exists ff_q_ftsp_prefix_right. b = ff_q_ftsp_prefix_right * S ((S (S ftsp_index_prefix)) * c) + (ftsp_right_prefix))) /\ (exists ftsp_order_prefix. ftsp_order_prefix + ftsp_left_prefix = ftsp_right_prefix)))
  73. 0073specialize sorted_succ_elim_prefix b
  74. 0074specialize sorted_succ_elim_prefix c
  75. 0075specialize sorted_succ_elim_prefix (S l)
  76. 0076apply sorted_succ_elim_prefix
  77. 0077exact hsorted
  78. 0078have hlast_pair : ∃ u. ∃ v. BetaAt(b,c,l,u) ∧ (BetaAt(b,c,S l,v) ∧ Le(u,v))
    Exact native replay linehave hlast_pair : exists u v. ((((exists ff_h_ftsp_sorted_left. ff_h_ftsp_sorted_left + S (u) = S ((S (l)) * c)) /\ exists ff_q_ftsp_sorted_left. b = ff_q_ftsp_sorted_left * S ((S (l)) * c) + (u))) /\ ((((exists ff_h_ftsp_sorted_right. ff_h_ftsp_sorted_right + S (v) = S ((S (S l)) * c)) /\ exists ff_q_ftsp_sorted_right. b = ff_q_ftsp_sorted_right * S ((S (S l)) * c) + (v))) /\ (exists k. k + u = v)))
  79. 0079specialize sorted_succ_elim_last b
  80. 0080specialize sorted_succ_elim_last c
  81. 0081specialize sorted_succ_elim_last l
  82. 0082apply sorted_succ_elim_last
  83. 0083exact hsorted
  84. 0084cases hlast_pair
  85. 0085cases hlast_pair_witness
  86. 0086cases hlast_pair_witness_witness
  87. 0087cases hlast_pair_witness_witness_right
  88. 0088have hright_equal : x3 = p
  89. 0089specialize beta_at_unique b
  90. 0090specialize beta_at_unique c
  91. 0091specialize beta_at_unique (S l)
  92. 0092specialize beta_at_unique x3
  93. 0093specialize beta_at_unique p
  94. 0094apply beta_at_unique
  95. 0095exact hlast_pair_witness_witness_right_left
  96. 0096exact hterminal
  97. 0097have hupper : Le(x2,p)
    Exact native replay linehave hupper : exists k. k + x2 = p
  98. 0098rewrite hright_equal at hlast_pair_witness_witness_right_right
  99. 0099exact hlast_pair_witness_witness_right_right
  100. 0100have hpredecessor_equal : x2 = p
  101. 0101specialize beta_sorted_prime_prefix_divisor_equals_bounded_last b
  102. 0102specialize beta_sorted_prime_prefix_divisor_equals_bounded_last c
  103. 0103specialize beta_sorted_prime_prefix_divisor_equals_bounded_last l
  104. 0104specialize beta_sorted_prime_prefix_divisor_equals_bounded_last x1
  105. 0105specialize beta_sorted_prime_prefix_divisor_equals_bounded_last p
  106. 0106specialize beta_sorted_prime_prefix_divisor_equals_bounded_last x2
  107. 0107apply beta_sorted_prime_prefix_divisor_equals_bounded_last
  108. 0108exact hprime
  109. 0109exact hprefix_prime
  110. 0110exact hprefix_sorted
  111. 0111exact hdecomposition_witness_witness_right_left
  112. 0112exact hlast_pair_witness_witness_left
  113. 0113exact hprefix_divides
  114. 0114exact hupper
  115. 0115rewrite hpredecessor_equal at hlast_pair_witness_witness_left
  116. 0116rewrite hpredecessor_equal at hlast_pair_witness_witness_left
  117. 0117exact hlast_pair_witness_witness_left