PV000B

prime_exponent_entries_prime_divides

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Every decoded support entry is a prime that genuinely divides the supported value.

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.

Exact expanded first-order arithmetic statement

forall n pb pc eb ec vb vc l i q. (forall pvs_index_divisor_entries. (exists pvs_gap_divisor_entriesindex. pvs_gap_divisor_entriesindex + S (pvs_index_divisor_entries) = (l)) -> exists pvs_prime_divisor_entries pvs_exponent_divisor_entries pvs_power_divisor_entries. (((((exists ff_h_pvs_divisor_entriesprime. ff_h_pvs_divisor_entriesprime + S (pvs_prime_divisor_entries) = S ((S (pvs_index_divisor_entries)) * pc)) /\ exists ff_q_pvs_divisor_entriesprime. pb = ff_q_pvs_divisor_entriesprime * S ((S (pvs_index_divisor_entries)) * pc) + (pvs_prime_divisor_entries))) /\ (((((exists ff_h_pvs_divisor_entriesexponent. ff_h_pvs_divisor_entriesexponent + S (pvs_exponent_divisor_entries) = S ((S (pvs_index_divisor_entries)) * ec)) /\ exists ff_q_pvs_divisor_entriesexponent. eb = ff_q_pvs_divisor_entriesexponent * S ((S (pvs_index_divisor_entries)) * ec) + (pvs_exponent_divisor_entries))) /\ (((((exists ff_h_pvs_divisor_entriespower. ff_h_pvs_divisor_entriespower + S (pvs_power_divisor_entries) = S ((S (pvs_index_divisor_entries)) * vc)) /\ exists ff_q_pvs_divisor_entriespower. vb = ff_q_pvs_divisor_entriespower * S ((S (pvs_index_divisor_entries)) * vc) + (pvs_power_divisor_entries))) /\ (((~((pvs_prime_divisor_entries) = 1) /\ forall pvs_left_divisor_entriesdomain pvs_right_divisor_entriesdomain. (pvs_prime_divisor_entries) = pvs_left_divisor_entriesdomain * pvs_right_divisor_entriesdomain -> pvs_left_divisor_entriesdomain = 1 \/ pvs_right_divisor_entriesdomain = 1) /\ (((~(pvs_exponent_divisor_entries = 0)) /\ (((((exists bpd_gap_pvs_divisor_entriesvaluation_selected_bound. bpd_gap_pvs_divisor_entriesvaluation_selected_bound + (pvs_exponent_divisor_entries) = (n)) /\ (exists bpvi_result_pvs_divisor_entriesvaluation_selected. ((exists bpvi_b_pvs_divisor_entriesvaluation_selected_power bpvi_c_pvs_divisor_entriesvaluation_selected_power. ((forall bpvi_i_pvs_divisor_entriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_divisor_entriesvaluation_selected_power. bpvi_repeat_gap_pvs_divisor_entriesvaluation_selected_power + S bpvi_i_pvs_divisor_entriesvaluation_selected_power = pvs_exponent_divisor_entries) -> (((exists bpvi_h_pvs_divisor_entriesvaluation_selected_power_repeat. bpvi_h_pvs_divisor_entriesvaluation_selected_power_repeat + S (pvs_prime_divisor_entries) = S ((S (bpvi_i_pvs_divisor_entriesvaluation_selected_power)) * bpvi_c_pvs_divisor_entriesvaluation_selected_power)) /\ exists bpvi_q_pvs_divisor_entriesvaluation_selected_power_repeat. bpvi_b_pvs_divisor_entriesvaluation_selected_power = bpvi_q_pvs_divisor_entriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_divisor_entriesvaluation_selected_power)) * bpvi_c_pvs_divisor_entriesvaluation_selected_power) + (pvs_prime_divisor_entries)))) /\ (exists bpvi_u_pvs_divisor_entriesvaluation_selected_power bpvi_v_pvs_divisor_entriesvaluation_selected_power. ((((exists bpvi_h_pvs_divisor_entriesvaluation_selected_power_start. bpvi_h_pvs_divisor_entriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_divisor_entriesvaluation_selected_power)) /\ exists bpvi_q_pvs_divisor_entriesvaluation_selected_power_start. bpvi_u_pvs_divisor_entriesvaluation_selected_power = bpvi_q_pvs_divisor_entriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_divisor_entriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_divisor_entriesvaluation_selected_power_terminal. bpvi_h_pvs_divisor_entriesvaluation_selected_power_terminal + S (bpvi_result_pvs_divisor_entriesvaluation_selected) = S ((S (pvs_exponent_divisor_entries)) * bpvi_v_pvs_divisor_entriesvaluation_selected_power)) /\ exists bpvi_q_pvs_divisor_entriesvaluation_selected_power_terminal. bpvi_u_pvs_divisor_entriesvaluation_selected_power = bpvi_q_pvs_divisor_entriesvaluation_selected_power_terminal * S ((S (pvs_exponent_divisor_entries)) * bpvi_v_pvs_divisor_entriesvaluation_selected_power) + (bpvi_result_pvs_divisor_entriesvaluation_selected))) /\ forall bpvi_j_pvs_divisor_entriesvaluation_selected_power. (exists bpvi_product_gap_pvs_divisor_entriesvaluation_selected_power. bpvi_product_gap_pvs_divisor_entriesvaluation_selected_power + S bpvi_j_pvs_divisor_entriesvaluation_selected_power = pvs_exponent_divisor_entries) -> exists bpvi_factor_pvs_divisor_entriesvaluation_selected_power bpvi_partial_pvs_divisor_entriesvaluation_selected_power bpvi_successor_pvs_divisor_entriesvaluation_selected_power. ((((exists bpvi_h_pvs_divisor_entriesvaluation_selected_power_factor. bpvi_h_pvs_divisor_entriesvaluation_selected_power_factor + S (bpvi_factor_pvs_divisor_entriesvaluation_selected_power) = S ((S (bpvi_j_pvs_divisor_entriesvaluation_selected_power)) * bpvi_c_pvs_divisor_entriesvaluation_selected_power)) /\ exists bpvi_q_pvs_divisor_entriesvaluation_selected_power_factor. bpvi_b_pvs_divisor_entriesvaluation_selected_power = bpvi_q_pvs_divisor_entriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_divisor_entriesvaluation_selected_power)) * bpvi_c_pvs_divisor_entriesvaluation_selected_power) + (bpvi_factor_pvs_divisor_entriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_divisor_entriesvaluation_selected_power_partial. bpvi_h_pvs_divisor_entriesvaluation_selected_power_partial + S (bpvi_partial_pvs_divisor_entriesvaluation_selected_power) = S ((S (bpvi_j_pvs_divisor_entriesvaluation_selected_power)) * bpvi_v_pvs_divisor_entriesvaluation_selected_power)) /\ exists bpvi_q_pvs_divisor_entriesvaluation_selected_power_partial. bpvi_u_pvs_divisor_entriesvaluation_selected_power = bpvi_q_pvs_divisor_entriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_divisor_entriesvaluation_selected_power)) * bpvi_v_pvs_divisor_entriesvaluation_selected_power) + (bpvi_partial_pvs_divisor_entriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_divisor_entriesvaluation_selected_power_successor. bpvi_h_pvs_divisor_entriesvaluation_selected_power_successor + S (bpvi_successor_pvs_divisor_entriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_divisor_entriesvaluation_selected_power)) * bpvi_v_pvs_divisor_entriesvaluation_selected_power)) /\ exists bpvi_q_pvs_divisor_entriesvaluation_selected_power_successor. bpvi_u_pvs_divisor_entriesvaluation_selected_power = bpvi_q_pvs_divisor_entriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_divisor_entriesvaluation_selected_power)) * bpvi_v_pvs_divisor_entriesvaluation_selected_power) + (bpvi_successor_pvs_divisor_entriesvaluation_selected_power))) /\ bpvi_successor_pvs_divisor_entriesvaluation_selected_power = bpvi_partial_pvs_divisor_entriesvaluation_selected_power * bpvi_factor_pvs_divisor_entriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_divisor_entriesvaluation_selected. n = bpvi_result_pvs_divisor_entriesvaluation_selected * bpvi_divisor_factor_pvs_divisor_entriesvaluation_selected))) /\ forall bpd_candidate_pvs_divisor_entriesvaluation. (exists bpd_gap_pvs_divisor_entriesvaluation_candidate_bound. bpd_gap_pvs_divisor_entriesvaluation_candidate_bound + (bpd_candidate_pvs_divisor_entriesvaluation) = (n)) -> (exists bpvi_result_pvs_divisor_entriesvaluation_candidate. ((exists bpvi_b_pvs_divisor_entriesvaluation_candidate_power bpvi_c_pvs_divisor_entriesvaluation_candidate_power. ((forall bpvi_i_pvs_divisor_entriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_divisor_entriesvaluation_candidate_power. bpvi_repeat_gap_pvs_divisor_entriesvaluation_candidate_power + S bpvi_i_pvs_divisor_entriesvaluation_candidate_power = bpd_candidate_pvs_divisor_entriesvaluation) -> (((exists bpvi_h_pvs_divisor_entriesvaluation_candidate_power_repeat. bpvi_h_pvs_divisor_entriesvaluation_candidate_power_repeat + S (pvs_prime_divisor_entries) = S ((S (bpvi_i_pvs_divisor_entriesvaluation_candidate_power)) * bpvi_c_pvs_divisor_entriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_divisor_entriesvaluation_candidate_power_repeat. bpvi_b_pvs_divisor_entriesvaluation_candidate_power = bpvi_q_pvs_divisor_entriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_divisor_entriesvaluation_candidate_power)) * bpvi_c_pvs_divisor_entriesvaluation_candidate_power) + (pvs_prime_divisor_entries)))) /\ (exists bpvi_u_pvs_divisor_entriesvaluation_candidate_power bpvi_v_pvs_divisor_entriesvaluation_candidate_power. ((((exists bpvi_h_pvs_divisor_entriesvaluation_candidate_power_start. bpvi_h_pvs_divisor_entriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_divisor_entriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_divisor_entriesvaluation_candidate_power_start. bpvi_u_pvs_divisor_entriesvaluation_candidate_power = bpvi_q_pvs_divisor_entriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_divisor_entriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_divisor_entriesvaluation_candidate_power_terminal. bpvi_h_pvs_divisor_entriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_divisor_entriesvaluation_candidate) = S ((S (bpd_candidate_pvs_divisor_entriesvaluation)) * bpvi_v_pvs_divisor_entriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_divisor_entriesvaluation_candidate_power_terminal. bpvi_u_pvs_divisor_entriesvaluation_candidate_power = bpvi_q_pvs_divisor_entriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_divisor_entriesvaluation)) * bpvi_v_pvs_divisor_entriesvaluation_candidate_power) + (bpvi_result_pvs_divisor_entriesvaluation_candidate))) /\ forall bpvi_j_pvs_divisor_entriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_divisor_entriesvaluation_candidate_power. bpvi_product_gap_pvs_divisor_entriesvaluation_candidate_power + S bpvi_j_pvs_divisor_entriesvaluation_candidate_power = bpd_candidate_pvs_divisor_entriesvaluation) -> exists bpvi_factor_pvs_divisor_entriesvaluation_candidate_power bpvi_partial_pvs_divisor_entriesvaluation_candidate_power bpvi_successor_pvs_divisor_entriesvaluation_candidate_power. ((((exists bpvi_h_pvs_divisor_entriesvaluation_candidate_power_factor. bpvi_h_pvs_divisor_entriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_divisor_entriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_divisor_entriesvaluation_candidate_power)) * bpvi_c_pvs_divisor_entriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_divisor_entriesvaluation_candidate_power_factor. bpvi_b_pvs_divisor_entriesvaluation_candidate_power = bpvi_q_pvs_divisor_entriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_divisor_entriesvaluation_candidate_power)) * bpvi_c_pvs_divisor_entriesvaluation_candidate_power) + (bpvi_factor_pvs_divisor_entriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_divisor_entriesvaluation_candidate_power_partial. bpvi_h_pvs_divisor_entriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_divisor_entriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_divisor_entriesvaluation_candidate_power)) * bpvi_v_pvs_divisor_entriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_divisor_entriesvaluation_candidate_power_partial. bpvi_u_pvs_divisor_entriesvaluation_candidate_power = bpvi_q_pvs_divisor_entriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_divisor_entriesvaluation_candidate_power)) * bpvi_v_pvs_divisor_entriesvaluation_candidate_power) + (bpvi_partial_pvs_divisor_entriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_divisor_entriesvaluation_candidate_power_successor. bpvi_h_pvs_divisor_entriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_divisor_entriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_divisor_entriesvaluation_candidate_power)) * bpvi_v_pvs_divisor_entriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_divisor_entriesvaluation_candidate_power_successor. bpvi_u_pvs_divisor_entriesvaluation_candidate_power = bpvi_q_pvs_divisor_entriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_divisor_entriesvaluation_candidate_power)) * bpvi_v_pvs_divisor_entriesvaluation_candidate_power) + (bpvi_successor_pvs_divisor_entriesvaluation_candidate_power))) /\ bpvi_successor_pvs_divisor_entriesvaluation_candidate_power = bpvi_partial_pvs_divisor_entriesvaluation_candidate_power * bpvi_factor_pvs_divisor_entriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_divisor_entriesvaluation_candidate. n = bpvi_result_pvs_divisor_entriesvaluation_candidate * bpvi_divisor_factor_pvs_divisor_entriesvaluation_candidate)) -> (exists bpd_gap_pvs_divisor_entriesvaluation_maximal. bpd_gap_pvs_divisor_entriesvaluation_maximal + (bpd_candidate_pvs_divisor_entriesvaluation) = (pvs_exponent_divisor_entries))) /\ (exists pa_b_pvs_divisor_entriesvalue pa_c_pvs_divisor_entriesvalue. ((forall pa_i_pvs_divisor_entriesvalue_repeat. (exists pa_lt_pvs_divisor_entriesvalue_repeat_bound. pa_lt_pvs_divisor_entriesvalue_repeat_bound + S pa_i_pvs_divisor_entriesvalue_repeat = pvs_exponent_divisor_entries) -> (((exists pa_h_pvs_divisor_entriesvalue_repeat_decoded. pa_h_pvs_divisor_entriesvalue_repeat_decoded + S (pvs_prime_divisor_entries) = S ((S (pa_i_pvs_divisor_entriesvalue_repeat)) * pa_c_pvs_divisor_entriesvalue)) /\ exists pa_q_pvs_divisor_entriesvalue_repeat_decoded. pa_b_pvs_divisor_entriesvalue = pa_q_pvs_divisor_entriesvalue_repeat_decoded * S ((S (pa_i_pvs_divisor_entriesvalue_repeat)) * pa_c_pvs_divisor_entriesvalue) + (pvs_prime_divisor_entries)))) /\ (exists pa_u_pvs_divisor_entriesvalue_product pa_v_pvs_divisor_entriesvalue_product. ((((exists pa_h_pvs_divisor_entriesvalue_product_start. pa_h_pvs_divisor_entriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_divisor_entriesvalue_product)) /\ exists pa_q_pvs_divisor_entriesvalue_product_start. pa_u_pvs_divisor_entriesvalue_product = pa_q_pvs_divisor_entriesvalue_product_start * S ((S (0)) * pa_v_pvs_divisor_entriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_divisor_entriesvalue_product_terminal. pa_h_pvs_divisor_entriesvalue_product_terminal + S (pvs_power_divisor_entries) = S ((S (pvs_exponent_divisor_entries)) * pa_v_pvs_divisor_entriesvalue_product)) /\ exists pa_q_pvs_divisor_entriesvalue_product_terminal. pa_u_pvs_divisor_entriesvalue_product = pa_q_pvs_divisor_entriesvalue_product_terminal * S ((S (pvs_exponent_divisor_entries)) * pa_v_pvs_divisor_entriesvalue_product) + (pvs_power_divisor_entries))) /\ forall pa_i_pvs_divisor_entriesvalue_product. (exists pa_lt_pvs_divisor_entriesvalue_product_bound. pa_lt_pvs_divisor_entriesvalue_product_bound + S pa_i_pvs_divisor_entriesvalue_product = pvs_exponent_divisor_entries) -> exists pa_p_pvs_divisor_entriesvalue_product pa_r_pvs_divisor_entriesvalue_product pa_s_pvs_divisor_entriesvalue_product. ((((exists pa_h_pvs_divisor_entriesvalue_product_factor. pa_h_pvs_divisor_entriesvalue_product_factor + S (pa_p_pvs_divisor_entriesvalue_product) = S ((S (pa_i_pvs_divisor_entriesvalue_product)) * pa_c_pvs_divisor_entriesvalue)) /\ exists pa_q_pvs_divisor_entriesvalue_product_factor. pa_b_pvs_divisor_entriesvalue = pa_q_pvs_divisor_entriesvalue_product_factor * S ((S (pa_i_pvs_divisor_entriesvalue_product)) * pa_c_pvs_divisor_entriesvalue) + (pa_p_pvs_divisor_entriesvalue_product))) /\ ((((exists pa_h_pvs_divisor_entriesvalue_product_partial. pa_h_pvs_divisor_entriesvalue_product_partial + S (pa_r_pvs_divisor_entriesvalue_product) = S ((S (pa_i_pvs_divisor_entriesvalue_product)) * pa_v_pvs_divisor_entriesvalue_product)) /\ exists pa_q_pvs_divisor_entriesvalue_product_partial. pa_u_pvs_divisor_entriesvalue_product = pa_q_pvs_divisor_entriesvalue_product_partial * S ((S (pa_i_pvs_divisor_entriesvalue_product)) * pa_v_pvs_divisor_entriesvalue_product) + (pa_r_pvs_divisor_entriesvalue_product))) /\ ((((exists pa_h_pvs_divisor_entriesvalue_product_successor. pa_h_pvs_divisor_entriesvalue_product_successor + S (pa_s_pvs_divisor_entriesvalue_product) = S ((S (S pa_i_pvs_divisor_entriesvalue_product)) * pa_v_pvs_divisor_entriesvalue_product)) /\ exists pa_q_pvs_divisor_entriesvalue_product_successor. pa_u_pvs_divisor_entriesvalue_product = pa_q_pvs_divisor_entriesvalue_product_successor * S ((S (S pa_i_pvs_divisor_entriesvalue_product)) * pa_v_pvs_divisor_entriesvalue_product) + (pa_s_pvs_divisor_entriesvalue_product))) /\ pa_s_pvs_divisor_entriesvalue_product = pa_r_pvs_divisor_entriesvalue_product * pa_p_pvs_divisor_entriesvalue_product))))))))))))))))))))) -> (exists pvs_gap_divisor_index. pvs_gap_divisor_index + S (i) = (l)) -> (((exists ff_h_pvs_divisor_at. ff_h_pvs_divisor_at + S (q) = S ((S (i)) * pc)) /\ exists ff_q_pvs_divisor_at. pb = ff_q_pvs_divisor_at * S ((S (i)) * pc) + (q))) -> (~((q) = 1) /\ forall pvs_left_entry_prime pvs_right_entry_prime. (q) = pvs_left_entry_prime * pvs_right_entry_prime -> pvs_left_entry_prime = 1 \/ pvs_right_entry_prime = 1) /\ (exists pvs_factor_entry_divisor. (n) = (q) * pvs_factor_entry_divisor)

Constructive proof overview

Generated structural guide

Every decoded support entry is a prime that genuinely divides the supported value.

The unchanged tactic script uses 2 declared prerequisites and contains 46 exact native proof lines.

Alpha v34 checked-use · first admitted v29 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

beta_at_unique Stable theorem; checked-use authorized power_valuation_nonzero_exponent_divides_base Alpha theorem; checked-use authorized

Direct dependents

PV0012 prime_valuation_support_append_full_power

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

46 script commands · 10 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro n
  2. L2
    intro pb
  3. L3
    intro pc
  4. L4
    intro eb
  5. L5
    intro ec
  6. L6
    intro vb
  7. L7
    intro vc
  8. L8
    intro l
  9. L9
    intro i
  10. L10
    intro q
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hentries
  2. L12
    intro hi
  3. L13
    intro hat
03Establish hrowL14–17

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

  1. L14
    have hrow : ∃ p. ∃ e. ∃ v. BetaAt(pb,pc,i,p) ∧ (BetaAt(eb,ec,i,e) ∧ (BetaAt(vb,vc,i,v) ∧ (Prime(p) ∧ (¬e = 0 ∧ (BoundedPowerValuation(p,n,n,e) ∧ Pow(p,e,v))))))Definitions: PrimeBetaAtPowBoundedPowerValuation
  2. L15
    specialize hentries (i)
  3. L16
    apply hentries
  4. L17
    exact hi
04Separate the logical casesL18–26

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

  1. L18
    cases hrow
  2. L19
    cases hrow_witness
  3. L20
    cases hrow_witness_witness
  4. L21
    cases hrow_witness_witness_witness
  5. L22
    cases hrow_witness_witness_witness_right
  6. L23
    cases hrow_witness_witness_witness_right_right
  7. L24
    cases hrow_witness_witness_witness_right_right_right
  8. L25
    cases hrow_witness_witness_witness_right_right_right_right
  9. L26
    cases hrow_witness_witness_witness_right_right_right_right_right
05Establish heqL27–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 heq : q = x
  2. L28
    specialize beta_at_unique (pb)
  3. L29
    specialize beta_at_unique (pc)
  4. L30
    specialize beta_at_unique (i)
  5. L31
    specialize beta_at_unique (q)
  6. L32
    specialize beta_at_unique (x)
  7. L33
    apply beta_at_unique
  8. L34
    exact hat
  9. L35
    exact hrow_witness_witness_witness_left
06Separate the logical casesL36–36

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

  1. L36
    split
07Calculate and transport equalitiesL37–38

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

  1. L37
    rewrite heq
  2. L38
    rewrite heq
08Use earlier factsL39–39

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

  1. L39
    exact hrow_witness_witness_witness_right_right_right_left
09Calculate and transport equalitiesL40–40

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

  1. L40
    rewrite heq
10Use earlier factsL41–46

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

  1. L41
    specialize power_valuation_nonzero_exponent_divides_base (x)
  2. L42
    specialize power_valuation_nonzero_exponent_divides_base (n)
  3. L43
    specialize power_valuation_nonzero_exponent_divides_base (x1)
  4. L44
    apply power_valuation_nonzero_exponent_divides_base
  5. L45
    exact hrow_witness_witness_witness_right_right_right_right_right_left
  6. L46
    exact hrow_witness_witness_witness_right_right_right_right_left

Library-wide reading audit

Original exact command ledger · 46 lines
  1. 0001intro n
  2. 0002intro pb
  3. 0003intro pc
  4. 0004intro eb
  5. 0005intro ec
  6. 0006intro vb
  7. 0007intro vc
  8. 0008intro l
  9. 0009intro i
  10. 0010intro q
  11. 0011intro hentries
  12. 0012intro hi
  13. 0013intro hat
  14. 0014have hrow : exists p e v. (((((exists ff_h_pvs_chosenprime. ff_h_pvs_chosenprime + S (p) = S ((S (i)) * pc)) /\ exists ff_q_pvs_chosenprime. pb = ff_q_pvs_chosenprime * S ((S (i)) * pc) + (p))) /\ (((((exists ff_h_pvs_chosenexponent. ff_h_pvs_chosenexponent + S (e) = S ((S (i)) * ec)) /\ exists ff_q_pvs_chosenexponent. eb = ff_q_pvs_chosenexponent * S ((S (i)) * ec) + (e))) /\ (((((exists ff_h_pvs_chosenpower. ff_h_pvs_chosenpower + S (v) = S ((S (i)) * vc)) /\ exists ff_q_pvs_chosenpower. vb = ff_q_pvs_chosenpower * S ((S (i)) * vc) + (v))) /\ (((~((p) = 1) /\ forall pvs_left_chosendomain pvs_right_chosendomain. (p) = pvs_left_chosendomain * pvs_right_chosendomain -> pvs_left_chosendomain = 1 \/ pvs_right_chosendomain = 1) /\ (((~(e = 0)) /\ (((((exists bpd_gap_pvs_chosenvaluation_selected_bound. bpd_gap_pvs_chosenvaluation_selected_bound + (e) = (n)) /\ (exists bpvi_result_pvs_chosenvaluation_selected. ((exists bpvi_b_pvs_chosenvaluation_selected_power bpvi_c_pvs_chosenvaluation_selected_power. ((forall bpvi_i_pvs_chosenvaluation_selected_power. (exists bpvi_repeat_gap_pvs_chosenvaluation_selected_power. bpvi_repeat_gap_pvs_chosenvaluation_selected_power + S bpvi_i_pvs_chosenvaluation_selected_power = e) -> (((exists bpvi_h_pvs_chosenvaluation_selected_power_repeat. bpvi_h_pvs_chosenvaluation_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_chosenvaluation_selected_power)) * bpvi_c_pvs_chosenvaluation_selected_power)) /\ exists bpvi_q_pvs_chosenvaluation_selected_power_repeat. bpvi_b_pvs_chosenvaluation_selected_power = bpvi_q_pvs_chosenvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_chosenvaluation_selected_power)) * bpvi_c_pvs_chosenvaluation_selected_power) + (p)))) /\ (exists bpvi_u_pvs_chosenvaluation_selected_power bpvi_v_pvs_chosenvaluation_selected_power. ((((exists bpvi_h_pvs_chosenvaluation_selected_power_start. bpvi_h_pvs_chosenvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_chosenvaluation_selected_power)) /\ exists bpvi_q_pvs_chosenvaluation_selected_power_start. bpvi_u_pvs_chosenvaluation_selected_power = bpvi_q_pvs_chosenvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_chosenvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_chosenvaluation_selected_power_terminal. bpvi_h_pvs_chosenvaluation_selected_power_terminal + S (bpvi_result_pvs_chosenvaluation_selected) = S ((S (e)) * bpvi_v_pvs_chosenvaluation_selected_power)) /\ exists bpvi_q_pvs_chosenvaluation_selected_power_terminal. bpvi_u_pvs_chosenvaluation_selected_power = bpvi_q_pvs_chosenvaluation_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_chosenvaluation_selected_power) + (bpvi_result_pvs_chosenvaluation_selected))) /\ forall bpvi_j_pvs_chosenvaluation_selected_power. (exists bpvi_product_gap_pvs_chosenvaluation_selected_power. bpvi_product_gap_pvs_chosenvaluation_selected_power + S bpvi_j_pvs_chosenvaluation_selected_power = e) -> exists bpvi_factor_pvs_chosenvaluation_selected_power bpvi_partial_pvs_chosenvaluation_selected_power bpvi_successor_pvs_chosenvaluation_selected_power. ((((exists bpvi_h_pvs_chosenvaluation_selected_power_factor. bpvi_h_pvs_chosenvaluation_selected_power_factor + S (bpvi_factor_pvs_chosenvaluation_selected_power) = S ((S (bpvi_j_pvs_chosenvaluation_selected_power)) * bpvi_c_pvs_chosenvaluation_selected_power)) /\ exists bpvi_q_pvs_chosenvaluation_selected_power_factor. bpvi_b_pvs_chosenvaluation_selected_power = bpvi_q_pvs_chosenvaluation_selected_power_factor * S ((S (bpvi_j_pvs_chosenvaluation_selected_power)) * bpvi_c_pvs_chosenvaluation_selected_power) + (bpvi_factor_pvs_chosenvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_chosenvaluation_selected_power_partial. bpvi_h_pvs_chosenvaluation_selected_power_partial + S (bpvi_partial_pvs_chosenvaluation_selected_power) = S ((S (bpvi_j_pvs_chosenvaluation_selected_power)) * bpvi_v_pvs_chosenvaluation_selected_power)) /\ exists bpvi_q_pvs_chosenvaluation_selected_power_partial. bpvi_u_pvs_chosenvaluation_selected_power = bpvi_q_pvs_chosenvaluation_selected_power_partial * S ((S (bpvi_j_pvs_chosenvaluation_selected_power)) * bpvi_v_pvs_chosenvaluation_selected_power) + (bpvi_partial_pvs_chosenvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_chosenvaluation_selected_power_successor. bpvi_h_pvs_chosenvaluation_selected_power_successor + S (bpvi_successor_pvs_chosenvaluation_selected_power) = S ((S (S bpvi_j_pvs_chosenvaluation_selected_power)) * bpvi_v_pvs_chosenvaluation_selected_power)) /\ exists bpvi_q_pvs_chosenvaluation_selected_power_successor. bpvi_u_pvs_chosenvaluation_selected_power = bpvi_q_pvs_chosenvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_chosenvaluation_selected_power)) * bpvi_v_pvs_chosenvaluation_selected_power) + (bpvi_successor_pvs_chosenvaluation_selected_power))) /\ bpvi_successor_pvs_chosenvaluation_selected_power = bpvi_partial_pvs_chosenvaluation_selected_power * bpvi_factor_pvs_chosenvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_chosenvaluation_selected. n = bpvi_result_pvs_chosenvaluation_selected * bpvi_divisor_factor_pvs_chosenvaluation_selected))) /\ forall bpd_candidate_pvs_chosenvaluation. (exists bpd_gap_pvs_chosenvaluation_candidate_bound. bpd_gap_pvs_chosenvaluation_candidate_bound + (bpd_candidate_pvs_chosenvaluation) = (n)) -> (exists bpvi_result_pvs_chosenvaluation_candidate. ((exists bpvi_b_pvs_chosenvaluation_candidate_power bpvi_c_pvs_chosenvaluation_candidate_power. ((forall bpvi_i_pvs_chosenvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_chosenvaluation_candidate_power. bpvi_repeat_gap_pvs_chosenvaluation_candidate_power + S bpvi_i_pvs_chosenvaluation_candidate_power = bpd_candidate_pvs_chosenvaluation) -> (((exists bpvi_h_pvs_chosenvaluation_candidate_power_repeat. bpvi_h_pvs_chosenvaluation_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_chosenvaluation_candidate_power)) * bpvi_c_pvs_chosenvaluation_candidate_power)) /\ exists bpvi_q_pvs_chosenvaluation_candidate_power_repeat. bpvi_b_pvs_chosenvaluation_candidate_power = bpvi_q_pvs_chosenvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_chosenvaluation_candidate_power)) * bpvi_c_pvs_chosenvaluation_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_chosenvaluation_candidate_power bpvi_v_pvs_chosenvaluation_candidate_power. ((((exists bpvi_h_pvs_chosenvaluation_candidate_power_start. bpvi_h_pvs_chosenvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_chosenvaluation_candidate_power)) /\ exists bpvi_q_pvs_chosenvaluation_candidate_power_start. bpvi_u_pvs_chosenvaluation_candidate_power = bpvi_q_pvs_chosenvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_chosenvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_chosenvaluation_candidate_power_terminal. bpvi_h_pvs_chosenvaluation_candidate_power_terminal + S (bpvi_result_pvs_chosenvaluation_candidate) = S ((S (bpd_candidate_pvs_chosenvaluation)) * bpvi_v_pvs_chosenvaluation_candidate_power)) /\ exists bpvi_q_pvs_chosenvaluation_candidate_power_terminal. bpvi_u_pvs_chosenvaluation_candidate_power = bpvi_q_pvs_chosenvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_chosenvaluation)) * bpvi_v_pvs_chosenvaluation_candidate_power) + (bpvi_result_pvs_chosenvaluation_candidate))) /\ forall bpvi_j_pvs_chosenvaluation_candidate_power. (exists bpvi_product_gap_pvs_chosenvaluation_candidate_power. bpvi_product_gap_pvs_chosenvaluation_candidate_power + S bpvi_j_pvs_chosenvaluation_candidate_power = bpd_candidate_pvs_chosenvaluation) -> exists bpvi_factor_pvs_chosenvaluation_candidate_power bpvi_partial_pvs_chosenvaluation_candidate_power bpvi_successor_pvs_chosenvaluation_candidate_power. ((((exists bpvi_h_pvs_chosenvaluation_candidate_power_factor. bpvi_h_pvs_chosenvaluation_candidate_power_factor + S (bpvi_factor_pvs_chosenvaluation_candidate_power) = S ((S (bpvi_j_pvs_chosenvaluation_candidate_power)) * bpvi_c_pvs_chosenvaluation_candidate_power)) /\ exists bpvi_q_pvs_chosenvaluation_candidate_power_factor. bpvi_b_pvs_chosenvaluation_candidate_power = bpvi_q_pvs_chosenvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_chosenvaluation_candidate_power)) * bpvi_c_pvs_chosenvaluation_candidate_power) + (bpvi_factor_pvs_chosenvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_chosenvaluation_candidate_power_partial. bpvi_h_pvs_chosenvaluation_candidate_power_partial + S (bpvi_partial_pvs_chosenvaluation_candidate_power) = S ((S (bpvi_j_pvs_chosenvaluation_candidate_power)) * bpvi_v_pvs_chosenvaluation_candidate_power)) /\ exists bpvi_q_pvs_chosenvaluation_candidate_power_partial. bpvi_u_pvs_chosenvaluation_candidate_power = bpvi_q_pvs_chosenvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_chosenvaluation_candidate_power)) * bpvi_v_pvs_chosenvaluation_candidate_power) + (bpvi_partial_pvs_chosenvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_chosenvaluation_candidate_power_successor. bpvi_h_pvs_chosenvaluation_candidate_power_successor + S (bpvi_successor_pvs_chosenvaluation_candidate_power) = S ((S (S bpvi_j_pvs_chosenvaluation_candidate_power)) * bpvi_v_pvs_chosenvaluation_candidate_power)) /\ exists bpvi_q_pvs_chosenvaluation_candidate_power_successor. bpvi_u_pvs_chosenvaluation_candidate_power = bpvi_q_pvs_chosenvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_chosenvaluation_candidate_power)) * bpvi_v_pvs_chosenvaluation_candidate_power) + (bpvi_successor_pvs_chosenvaluation_candidate_power))) /\ bpvi_successor_pvs_chosenvaluation_candidate_power = bpvi_partial_pvs_chosenvaluation_candidate_power * bpvi_factor_pvs_chosenvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_chosenvaluation_candidate. n = bpvi_result_pvs_chosenvaluation_candidate * bpvi_divisor_factor_pvs_chosenvaluation_candidate)) -> (exists bpd_gap_pvs_chosenvaluation_maximal. bpd_gap_pvs_chosenvaluation_maximal + (bpd_candidate_pvs_chosenvaluation) = (e))) /\ (exists pa_b_pvs_chosenvalue pa_c_pvs_chosenvalue. ((forall pa_i_pvs_chosenvalue_repeat. (exists pa_lt_pvs_chosenvalue_repeat_bound. pa_lt_pvs_chosenvalue_repeat_bound + S pa_i_pvs_chosenvalue_repeat = e) -> (((exists pa_h_pvs_chosenvalue_repeat_decoded. pa_h_pvs_chosenvalue_repeat_decoded + S (p) = S ((S (pa_i_pvs_chosenvalue_repeat)) * pa_c_pvs_chosenvalue)) /\ exists pa_q_pvs_chosenvalue_repeat_decoded. pa_b_pvs_chosenvalue = pa_q_pvs_chosenvalue_repeat_decoded * S ((S (pa_i_pvs_chosenvalue_repeat)) * pa_c_pvs_chosenvalue) + (p)))) /\ (exists pa_u_pvs_chosenvalue_product pa_v_pvs_chosenvalue_product. ((((exists pa_h_pvs_chosenvalue_product_start. pa_h_pvs_chosenvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_chosenvalue_product)) /\ exists pa_q_pvs_chosenvalue_product_start. pa_u_pvs_chosenvalue_product = pa_q_pvs_chosenvalue_product_start * S ((S (0)) * pa_v_pvs_chosenvalue_product) + (1))) /\ ((((exists pa_h_pvs_chosenvalue_product_terminal. pa_h_pvs_chosenvalue_product_terminal + S (v) = S ((S (e)) * pa_v_pvs_chosenvalue_product)) /\ exists pa_q_pvs_chosenvalue_product_terminal. pa_u_pvs_chosenvalue_product = pa_q_pvs_chosenvalue_product_terminal * S ((S (e)) * pa_v_pvs_chosenvalue_product) + (v))) /\ forall pa_i_pvs_chosenvalue_product. (exists pa_lt_pvs_chosenvalue_product_bound. pa_lt_pvs_chosenvalue_product_bound + S pa_i_pvs_chosenvalue_product = e) -> exists pa_p_pvs_chosenvalue_product pa_r_pvs_chosenvalue_product pa_s_pvs_chosenvalue_product. ((((exists pa_h_pvs_chosenvalue_product_factor. pa_h_pvs_chosenvalue_product_factor + S (pa_p_pvs_chosenvalue_product) = S ((S (pa_i_pvs_chosenvalue_product)) * pa_c_pvs_chosenvalue)) /\ exists pa_q_pvs_chosenvalue_product_factor. pa_b_pvs_chosenvalue = pa_q_pvs_chosenvalue_product_factor * S ((S (pa_i_pvs_chosenvalue_product)) * pa_c_pvs_chosenvalue) + (pa_p_pvs_chosenvalue_product))) /\ ((((exists pa_h_pvs_chosenvalue_product_partial. pa_h_pvs_chosenvalue_product_partial + S (pa_r_pvs_chosenvalue_product) = S ((S (pa_i_pvs_chosenvalue_product)) * pa_v_pvs_chosenvalue_product)) /\ exists pa_q_pvs_chosenvalue_product_partial. pa_u_pvs_chosenvalue_product = pa_q_pvs_chosenvalue_product_partial * S ((S (pa_i_pvs_chosenvalue_product)) * pa_v_pvs_chosenvalue_product) + (pa_r_pvs_chosenvalue_product))) /\ ((((exists pa_h_pvs_chosenvalue_product_successor. pa_h_pvs_chosenvalue_product_successor + S (pa_s_pvs_chosenvalue_product) = S ((S (S pa_i_pvs_chosenvalue_product)) * pa_v_pvs_chosenvalue_product)) /\ exists pa_q_pvs_chosenvalue_product_successor. pa_u_pvs_chosenvalue_product = pa_q_pvs_chosenvalue_product_successor * S ((S (S pa_i_pvs_chosenvalue_product)) * pa_v_pvs_chosenvalue_product) + (pa_s_pvs_chosenvalue_product))) /\ pa_s_pvs_chosenvalue_product = pa_r_pvs_chosenvalue_product * pa_p_pvs_chosenvalue_product))))))))))))))))))))
  15. 0015specialize hentries (i)
  16. 0016apply hentries
  17. 0017exact hi
  18. 0018cases hrow
  19. 0019cases hrow_witness
  20. 0020cases hrow_witness_witness
  21. 0021cases hrow_witness_witness_witness
  22. 0022cases hrow_witness_witness_witness_right
  23. 0023cases hrow_witness_witness_witness_right_right
  24. 0024cases hrow_witness_witness_witness_right_right_right
  25. 0025cases hrow_witness_witness_witness_right_right_right_right
  26. 0026cases hrow_witness_witness_witness_right_right_right_right_right
  27. 0027have heq : q = x
  28. 0028specialize beta_at_unique (pb)
  29. 0029specialize beta_at_unique (pc)
  30. 0030specialize beta_at_unique (i)
  31. 0031specialize beta_at_unique (q)
  32. 0032specialize beta_at_unique (x)
  33. 0033apply beta_at_unique
  34. 0034exact hat
  35. 0035exact hrow_witness_witness_witness_left
  36. 0036split
  37. 0037rewrite heq
  38. 0038rewrite heq
  39. 0039exact hrow_witness_witness_witness_right_right_right_left
  40. 0040rewrite heq
  41. 0041specialize power_valuation_nonzero_exponent_divides_base (x)
  42. 0042specialize power_valuation_nonzero_exponent_divides_base (n)
  43. 0043specialize power_valuation_nonzero_exponent_divides_base (x1)
  44. 0044apply power_valuation_nonzero_exponent_divides_base
  45. 0045exact hrow_witness_witness_witness_right_right_right_right_right_left
  46. 0046exact hrow_witness_witness_witness_right_right_right_right_left