SK0017

positive_power_prime_valuations_divisible

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

Every positive k-th power has every actual prime valuation divisible by k, with a constructed quotient valuation of its nonzero base.

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 k r. ~(n = 0) -> ~(k = 0) -> (exists pa_b_pvs_necessary_power pa_c_pvs_necessary_power. ((forall pa_i_pvs_necessary_power_repeat. (exists pa_lt_pvs_necessary_power_repeat_bound. pa_lt_pvs_necessary_power_repeat_bound + S pa_i_pvs_necessary_power_repeat = k) -> (((exists pa_h_pvs_necessary_power_repeat_decoded. pa_h_pvs_necessary_power_repeat_decoded + S (r) = S ((S (pa_i_pvs_necessary_power_repeat)) * pa_c_pvs_necessary_power)) /\ exists pa_q_pvs_necessary_power_repeat_decoded. pa_b_pvs_necessary_power = pa_q_pvs_necessary_power_repeat_decoded * S ((S (pa_i_pvs_necessary_power_repeat)) * pa_c_pvs_necessary_power) + (r)))) /\ (exists pa_u_pvs_necessary_power_product pa_v_pvs_necessary_power_product. ((((exists pa_h_pvs_necessary_power_product_start. pa_h_pvs_necessary_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_necessary_power_product)) /\ exists pa_q_pvs_necessary_power_product_start. pa_u_pvs_necessary_power_product = pa_q_pvs_necessary_power_product_start * S ((S (0)) * pa_v_pvs_necessary_power_product) + (1))) /\ ((((exists pa_h_pvs_necessary_power_product_terminal. pa_h_pvs_necessary_power_product_terminal + S (n) = S ((S (k)) * pa_v_pvs_necessary_power_product)) /\ exists pa_q_pvs_necessary_power_product_terminal. pa_u_pvs_necessary_power_product = pa_q_pvs_necessary_power_product_terminal * S ((S (k)) * pa_v_pvs_necessary_power_product) + (n))) /\ forall pa_i_pvs_necessary_power_product. (exists pa_lt_pvs_necessary_power_product_bound. pa_lt_pvs_necessary_power_product_bound + S pa_i_pvs_necessary_power_product = k) -> exists pa_p_pvs_necessary_power_product pa_r_pvs_necessary_power_product pa_s_pvs_necessary_power_product. ((((exists pa_h_pvs_necessary_power_product_factor. pa_h_pvs_necessary_power_product_factor + S (pa_p_pvs_necessary_power_product) = S ((S (pa_i_pvs_necessary_power_product)) * pa_c_pvs_necessary_power)) /\ exists pa_q_pvs_necessary_power_product_factor. pa_b_pvs_necessary_power = pa_q_pvs_necessary_power_product_factor * S ((S (pa_i_pvs_necessary_power_product)) * pa_c_pvs_necessary_power) + (pa_p_pvs_necessary_power_product))) /\ ((((exists pa_h_pvs_necessary_power_product_partial. pa_h_pvs_necessary_power_product_partial + S (pa_r_pvs_necessary_power_product) = S ((S (pa_i_pvs_necessary_power_product)) * pa_v_pvs_necessary_power_product)) /\ exists pa_q_pvs_necessary_power_product_partial. pa_u_pvs_necessary_power_product = pa_q_pvs_necessary_power_product_partial * S ((S (pa_i_pvs_necessary_power_product)) * pa_v_pvs_necessary_power_product) + (pa_r_pvs_necessary_power_product))) /\ ((((exists pa_h_pvs_necessary_power_product_successor. pa_h_pvs_necessary_power_product_successor + S (pa_s_pvs_necessary_power_product) = S ((S (S pa_i_pvs_necessary_power_product)) * pa_v_pvs_necessary_power_product)) /\ exists pa_q_pvs_necessary_power_product_successor. pa_u_pvs_necessary_power_product = pa_q_pvs_necessary_power_product_successor * S ((S (S pa_i_pvs_necessary_power_product)) * pa_v_pvs_necessary_power_product) + (pa_s_pvs_necessary_power_product))) /\ pa_s_pvs_necessary_power_product = pa_r_pvs_necessary_power_product * pa_p_pvs_necessary_power_product)))))))) -> (forall ppf_prime_necessary_valuations ppf_exponent_necessary_valuations. (~((ppf_prime_necessary_valuations) = 1) /\ forall pvs_left_necessary_valuationsdomain pvs_right_necessary_valuationsdomain. (ppf_prime_necessary_valuations) = pvs_left_necessary_valuationsdomain * pvs_right_necessary_valuationsdomain -> pvs_left_necessary_valuationsdomain = 1 \/ pvs_right_necessary_valuationsdomain = 1) -> (((exists bpd_gap_pvs_necessary_valuationsvaluation_selected_bound. bpd_gap_pvs_necessary_valuationsvaluation_selected_bound + (ppf_exponent_necessary_valuations) = (n)) /\ (exists bpvi_result_pvs_necessary_valuationsvaluation_selected. ((exists bpvi_b_pvs_necessary_valuationsvaluation_selected_power bpvi_c_pvs_necessary_valuationsvaluation_selected_power. ((forall bpvi_i_pvs_necessary_valuationsvaluation_selected_power. (exists bpvi_repeat_gap_pvs_necessary_valuationsvaluation_selected_power. bpvi_repeat_gap_pvs_necessary_valuationsvaluation_selected_power + S bpvi_i_pvs_necessary_valuationsvaluation_selected_power = ppf_exponent_necessary_valuations) -> (((exists bpvi_h_pvs_necessary_valuationsvaluation_selected_power_repeat. bpvi_h_pvs_necessary_valuationsvaluation_selected_power_repeat + S (ppf_prime_necessary_valuations) = S ((S (bpvi_i_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_c_pvs_necessary_valuationsvaluation_selected_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_selected_power_repeat. bpvi_b_pvs_necessary_valuationsvaluation_selected_power = bpvi_q_pvs_necessary_valuationsvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_c_pvs_necessary_valuationsvaluation_selected_power) + (ppf_prime_necessary_valuations)))) /\ (exists bpvi_u_pvs_necessary_valuationsvaluation_selected_power bpvi_v_pvs_necessary_valuationsvaluation_selected_power. ((((exists bpvi_h_pvs_necessary_valuationsvaluation_selected_power_start. bpvi_h_pvs_necessary_valuationsvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_selected_power_start. bpvi_u_pvs_necessary_valuationsvaluation_selected_power = bpvi_q_pvs_necessary_valuationsvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_necessary_valuationsvaluation_selected_power_terminal. bpvi_h_pvs_necessary_valuationsvaluation_selected_power_terminal + S (bpvi_result_pvs_necessary_valuationsvaluation_selected) = S ((S (ppf_exponent_necessary_valuations)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_selected_power_terminal. bpvi_u_pvs_necessary_valuationsvaluation_selected_power = bpvi_q_pvs_necessary_valuationsvaluation_selected_power_terminal * S ((S (ppf_exponent_necessary_valuations)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power) + (bpvi_result_pvs_necessary_valuationsvaluation_selected))) /\ forall bpvi_j_pvs_necessary_valuationsvaluation_selected_power. (exists bpvi_product_gap_pvs_necessary_valuationsvaluation_selected_power. bpvi_product_gap_pvs_necessary_valuationsvaluation_selected_power + S bpvi_j_pvs_necessary_valuationsvaluation_selected_power = ppf_exponent_necessary_valuations) -> exists bpvi_factor_pvs_necessary_valuationsvaluation_selected_power bpvi_partial_pvs_necessary_valuationsvaluation_selected_power bpvi_successor_pvs_necessary_valuationsvaluation_selected_power. ((((exists bpvi_h_pvs_necessary_valuationsvaluation_selected_power_factor. bpvi_h_pvs_necessary_valuationsvaluation_selected_power_factor + S (bpvi_factor_pvs_necessary_valuationsvaluation_selected_power) = S ((S (bpvi_j_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_c_pvs_necessary_valuationsvaluation_selected_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_selected_power_factor. bpvi_b_pvs_necessary_valuationsvaluation_selected_power = bpvi_q_pvs_necessary_valuationsvaluation_selected_power_factor * S ((S (bpvi_j_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_c_pvs_necessary_valuationsvaluation_selected_power) + (bpvi_factor_pvs_necessary_valuationsvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_necessary_valuationsvaluation_selected_power_partial. bpvi_h_pvs_necessary_valuationsvaluation_selected_power_partial + S (bpvi_partial_pvs_necessary_valuationsvaluation_selected_power) = S ((S (bpvi_j_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_selected_power_partial. bpvi_u_pvs_necessary_valuationsvaluation_selected_power = bpvi_q_pvs_necessary_valuationsvaluation_selected_power_partial * S ((S (bpvi_j_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power) + (bpvi_partial_pvs_necessary_valuationsvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_necessary_valuationsvaluation_selected_power_successor. bpvi_h_pvs_necessary_valuationsvaluation_selected_power_successor + S (bpvi_successor_pvs_necessary_valuationsvaluation_selected_power) = S ((S (S bpvi_j_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_selected_power_successor. bpvi_u_pvs_necessary_valuationsvaluation_selected_power = bpvi_q_pvs_necessary_valuationsvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power) + (bpvi_successor_pvs_necessary_valuationsvaluation_selected_power))) /\ bpvi_successor_pvs_necessary_valuationsvaluation_selected_power = bpvi_partial_pvs_necessary_valuationsvaluation_selected_power * bpvi_factor_pvs_necessary_valuationsvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_necessary_valuationsvaluation_selected. n = bpvi_result_pvs_necessary_valuationsvaluation_selected * bpvi_divisor_factor_pvs_necessary_valuationsvaluation_selected))) /\ forall bpd_candidate_pvs_necessary_valuationsvaluation. (exists bpd_gap_pvs_necessary_valuationsvaluation_candidate_bound. bpd_gap_pvs_necessary_valuationsvaluation_candidate_bound + (bpd_candidate_pvs_necessary_valuationsvaluation) = (n)) -> (exists bpvi_result_pvs_necessary_valuationsvaluation_candidate. ((exists bpvi_b_pvs_necessary_valuationsvaluation_candidate_power bpvi_c_pvs_necessary_valuationsvaluation_candidate_power. ((forall bpvi_i_pvs_necessary_valuationsvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_necessary_valuationsvaluation_candidate_power. bpvi_repeat_gap_pvs_necessary_valuationsvaluation_candidate_power + S bpvi_i_pvs_necessary_valuationsvaluation_candidate_power = bpd_candidate_pvs_necessary_valuationsvaluation) -> (((exists bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_repeat. bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_repeat + S (ppf_prime_necessary_valuations) = S ((S (bpvi_i_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_c_pvs_necessary_valuationsvaluation_candidate_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_repeat. bpvi_b_pvs_necessary_valuationsvaluation_candidate_power = bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_c_pvs_necessary_valuationsvaluation_candidate_power) + (ppf_prime_necessary_valuations)))) /\ (exists bpvi_u_pvs_necessary_valuationsvaluation_candidate_power bpvi_v_pvs_necessary_valuationsvaluation_candidate_power. ((((exists bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_start. bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_start. bpvi_u_pvs_necessary_valuationsvaluation_candidate_power = bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_terminal. bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_terminal + S (bpvi_result_pvs_necessary_valuationsvaluation_candidate) = S ((S (bpd_candidate_pvs_necessary_valuationsvaluation)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_terminal. bpvi_u_pvs_necessary_valuationsvaluation_candidate_power = bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_necessary_valuationsvaluation)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power) + (bpvi_result_pvs_necessary_valuationsvaluation_candidate))) /\ forall bpvi_j_pvs_necessary_valuationsvaluation_candidate_power. (exists bpvi_product_gap_pvs_necessary_valuationsvaluation_candidate_power. bpvi_product_gap_pvs_necessary_valuationsvaluation_candidate_power + S bpvi_j_pvs_necessary_valuationsvaluation_candidate_power = bpd_candidate_pvs_necessary_valuationsvaluation) -> exists bpvi_factor_pvs_necessary_valuationsvaluation_candidate_power bpvi_partial_pvs_necessary_valuationsvaluation_candidate_power bpvi_successor_pvs_necessary_valuationsvaluation_candidate_power. ((((exists bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_factor. bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_factor + S (bpvi_factor_pvs_necessary_valuationsvaluation_candidate_power) = S ((S (bpvi_j_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_c_pvs_necessary_valuationsvaluation_candidate_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_factor. bpvi_b_pvs_necessary_valuationsvaluation_candidate_power = bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_c_pvs_necessary_valuationsvaluation_candidate_power) + (bpvi_factor_pvs_necessary_valuationsvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_partial. bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_partial + S (bpvi_partial_pvs_necessary_valuationsvaluation_candidate_power) = S ((S (bpvi_j_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_partial. bpvi_u_pvs_necessary_valuationsvaluation_candidate_power = bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power) + (bpvi_partial_pvs_necessary_valuationsvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_successor. bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_successor + S (bpvi_successor_pvs_necessary_valuationsvaluation_candidate_power) = S ((S (S bpvi_j_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_successor. bpvi_u_pvs_necessary_valuationsvaluation_candidate_power = bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power) + (bpvi_successor_pvs_necessary_valuationsvaluation_candidate_power))) /\ bpvi_successor_pvs_necessary_valuationsvaluation_candidate_power = bpvi_partial_pvs_necessary_valuationsvaluation_candidate_power * bpvi_factor_pvs_necessary_valuationsvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_necessary_valuationsvaluation_candidate. n = bpvi_result_pvs_necessary_valuationsvaluation_candidate * bpvi_divisor_factor_pvs_necessary_valuationsvaluation_candidate)) -> (exists bpd_gap_pvs_necessary_valuationsvaluation_maximal. bpd_gap_pvs_necessary_valuationsvaluation_maximal + (bpd_candidate_pvs_necessary_valuationsvaluation) = (ppf_exponent_necessary_valuations))) -> (exists pvs_factor_necessary_valuationsdivides. (ppf_exponent_necessary_valuations) = (k) * pvs_factor_necessary_valuationsdivides))

Constructive proof overview

Generated structural guide

Every positive k-th power has every actual prime valuation divisible by k, with a constructed quotient valuation of its nonzero base.

The unchanged tactic script uses 3 declared prerequisites and contains 38 exact native proof lines.

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

Proof neighborhood

Direct dependencies

SK0016 positive_power_nonzero_base power_valuation_exists Alpha theorem; checked-use authorized prime_power_valuation_pow_value Alpha theorem; checked-use authorized

Direct dependents

SK0028 prime_support_perfect_power_iff_degree_divides

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

38 script commands · 8 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.

Named ingredients (1)
positive power nonzero base

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–6

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

  1. L1
    intro n
  2. L2
    intro k
  3. L3
    intro r
  4. L4
    intro hn
  5. L5
    intro hk
  6. L6
    intro hpow
02Establish hrL7–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply positive power nonzero base.

  1. L7
    have hr : ~(r = 0)
  2. L8
    intro hz
  3. L9
    specialize positive_power_nonzero_base (n)
  4. L10
    specialize positive_power_nonzero_base (k)
  5. L11
    specialize positive_power_nonzero_base (r)
  6. L12
    apply positive_power_nonzero_base
  7. L13
    exact hn
  8. L14
    exact hk
  9. L15
    exact hpow
  10. L16
    exact hz
03Fix variables and assumptionsL17–20

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

  1. L17
    intro p
  2. L18
    intro e
  3. L19
    intro hp
  4. L20
    intro hval
04Establish hbaseL21–24

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

  1. L21
    have hbase : ∃ f. BoundedPowerValuation(p,r,r,f)Definitions: BoundedPowerValuation
  2. L22
    specialize power_valuation_exists (p)
  3. L23
    specialize power_valuation_exists (r)
  4. L24
    apply power_valuation_exists
05Separate the logical casesL25–25

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

  1. L25
    cases hbase
06Construct an explicit witnessL26–26

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

  1. L26
    exists x
07Use earlier factsL27–36

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

  1. L27
    specialize prime_power_valuation_pow_value (p)
  2. L28
    specialize prime_power_valuation_pow_value (r)
  3. L29
    specialize prime_power_valuation_pow_value (k)
  4. L30
    specialize prime_power_valuation_pow_value (x)
  5. L31
    specialize prime_power_valuation_pow_value (n)
  6. L32
    specialize prime_power_valuation_pow_value (e)
  7. L33
    apply prime_power_valuation_pow_value
  8. L34
    exact hp
  9. L35
    exact hr
  10. L36
    exact hbase_witness
08Use earlier factsL37–38

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

  1. L37
    exact hpow
  2. L38
    exact hval

Library-wide reading audit

Original exact command ledger · 38 lines
  1. 0001intro n
  2. 0002intro k
  3. 0003intro r
  4. 0004intro hn
  5. 0005intro hk
  6. 0006intro hpow
  7. 0007have hr : ~(r = 0)
  8. 0008intro hz
  9. 0009specialize positive_power_nonzero_base (n)
  10. 0010specialize positive_power_nonzero_base (k)
  11. 0011specialize positive_power_nonzero_base (r)
  12. 0012apply positive_power_nonzero_base
  13. 0013exact hn
  14. 0014exact hk
  15. 0015exact hpow
  16. 0016exact hz
  17. 0017intro p
  18. 0018intro e
  19. 0019intro hp
  20. 0020intro hval
  21. 0021have hbase : exists f. (((exists bpd_gap_pvs_necessary_base_selected_bound. bpd_gap_pvs_necessary_base_selected_bound + (f) = (r)) /\ (exists bpvi_result_pvs_necessary_base_selected. ((exists bpvi_b_pvs_necessary_base_selected_power bpvi_c_pvs_necessary_base_selected_power. ((forall bpvi_i_pvs_necessary_base_selected_power. (exists bpvi_repeat_gap_pvs_necessary_base_selected_power. bpvi_repeat_gap_pvs_necessary_base_selected_power + S bpvi_i_pvs_necessary_base_selected_power = f) -> (((exists bpvi_h_pvs_necessary_base_selected_power_repeat. bpvi_h_pvs_necessary_base_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_necessary_base_selected_power)) * bpvi_c_pvs_necessary_base_selected_power)) /\ exists bpvi_q_pvs_necessary_base_selected_power_repeat. bpvi_b_pvs_necessary_base_selected_power = bpvi_q_pvs_necessary_base_selected_power_repeat * S ((S (bpvi_i_pvs_necessary_base_selected_power)) * bpvi_c_pvs_necessary_base_selected_power) + (p)))) /\ (exists bpvi_u_pvs_necessary_base_selected_power bpvi_v_pvs_necessary_base_selected_power. ((((exists bpvi_h_pvs_necessary_base_selected_power_start. bpvi_h_pvs_necessary_base_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_necessary_base_selected_power)) /\ exists bpvi_q_pvs_necessary_base_selected_power_start. bpvi_u_pvs_necessary_base_selected_power = bpvi_q_pvs_necessary_base_selected_power_start * S ((S (0)) * bpvi_v_pvs_necessary_base_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_necessary_base_selected_power_terminal. bpvi_h_pvs_necessary_base_selected_power_terminal + S (bpvi_result_pvs_necessary_base_selected) = S ((S (f)) * bpvi_v_pvs_necessary_base_selected_power)) /\ exists bpvi_q_pvs_necessary_base_selected_power_terminal. bpvi_u_pvs_necessary_base_selected_power = bpvi_q_pvs_necessary_base_selected_power_terminal * S ((S (f)) * bpvi_v_pvs_necessary_base_selected_power) + (bpvi_result_pvs_necessary_base_selected))) /\ forall bpvi_j_pvs_necessary_base_selected_power. (exists bpvi_product_gap_pvs_necessary_base_selected_power. bpvi_product_gap_pvs_necessary_base_selected_power + S bpvi_j_pvs_necessary_base_selected_power = f) -> exists bpvi_factor_pvs_necessary_base_selected_power bpvi_partial_pvs_necessary_base_selected_power bpvi_successor_pvs_necessary_base_selected_power. ((((exists bpvi_h_pvs_necessary_base_selected_power_factor. bpvi_h_pvs_necessary_base_selected_power_factor + S (bpvi_factor_pvs_necessary_base_selected_power) = S ((S (bpvi_j_pvs_necessary_base_selected_power)) * bpvi_c_pvs_necessary_base_selected_power)) /\ exists bpvi_q_pvs_necessary_base_selected_power_factor. bpvi_b_pvs_necessary_base_selected_power = bpvi_q_pvs_necessary_base_selected_power_factor * S ((S (bpvi_j_pvs_necessary_base_selected_power)) * bpvi_c_pvs_necessary_base_selected_power) + (bpvi_factor_pvs_necessary_base_selected_power))) /\ ((((exists bpvi_h_pvs_necessary_base_selected_power_partial. bpvi_h_pvs_necessary_base_selected_power_partial + S (bpvi_partial_pvs_necessary_base_selected_power) = S ((S (bpvi_j_pvs_necessary_base_selected_power)) * bpvi_v_pvs_necessary_base_selected_power)) /\ exists bpvi_q_pvs_necessary_base_selected_power_partial. bpvi_u_pvs_necessary_base_selected_power = bpvi_q_pvs_necessary_base_selected_power_partial * S ((S (bpvi_j_pvs_necessary_base_selected_power)) * bpvi_v_pvs_necessary_base_selected_power) + (bpvi_partial_pvs_necessary_base_selected_power))) /\ ((((exists bpvi_h_pvs_necessary_base_selected_power_successor. bpvi_h_pvs_necessary_base_selected_power_successor + S (bpvi_successor_pvs_necessary_base_selected_power) = S ((S (S bpvi_j_pvs_necessary_base_selected_power)) * bpvi_v_pvs_necessary_base_selected_power)) /\ exists bpvi_q_pvs_necessary_base_selected_power_successor. bpvi_u_pvs_necessary_base_selected_power = bpvi_q_pvs_necessary_base_selected_power_successor * S ((S (S bpvi_j_pvs_necessary_base_selected_power)) * bpvi_v_pvs_necessary_base_selected_power) + (bpvi_successor_pvs_necessary_base_selected_power))) /\ bpvi_successor_pvs_necessary_base_selected_power = bpvi_partial_pvs_necessary_base_selected_power * bpvi_factor_pvs_necessary_base_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_necessary_base_selected. r = bpvi_result_pvs_necessary_base_selected * bpvi_divisor_factor_pvs_necessary_base_selected))) /\ forall bpd_candidate_pvs_necessary_base. (exists bpd_gap_pvs_necessary_base_candidate_bound. bpd_gap_pvs_necessary_base_candidate_bound + (bpd_candidate_pvs_necessary_base) = (r)) -> (exists bpvi_result_pvs_necessary_base_candidate. ((exists bpvi_b_pvs_necessary_base_candidate_power bpvi_c_pvs_necessary_base_candidate_power. ((forall bpvi_i_pvs_necessary_base_candidate_power. (exists bpvi_repeat_gap_pvs_necessary_base_candidate_power. bpvi_repeat_gap_pvs_necessary_base_candidate_power + S bpvi_i_pvs_necessary_base_candidate_power = bpd_candidate_pvs_necessary_base) -> (((exists bpvi_h_pvs_necessary_base_candidate_power_repeat. bpvi_h_pvs_necessary_base_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_necessary_base_candidate_power)) * bpvi_c_pvs_necessary_base_candidate_power)) /\ exists bpvi_q_pvs_necessary_base_candidate_power_repeat. bpvi_b_pvs_necessary_base_candidate_power = bpvi_q_pvs_necessary_base_candidate_power_repeat * S ((S (bpvi_i_pvs_necessary_base_candidate_power)) * bpvi_c_pvs_necessary_base_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_necessary_base_candidate_power bpvi_v_pvs_necessary_base_candidate_power. ((((exists bpvi_h_pvs_necessary_base_candidate_power_start. bpvi_h_pvs_necessary_base_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_necessary_base_candidate_power)) /\ exists bpvi_q_pvs_necessary_base_candidate_power_start. bpvi_u_pvs_necessary_base_candidate_power = bpvi_q_pvs_necessary_base_candidate_power_start * S ((S (0)) * bpvi_v_pvs_necessary_base_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_necessary_base_candidate_power_terminal. bpvi_h_pvs_necessary_base_candidate_power_terminal + S (bpvi_result_pvs_necessary_base_candidate) = S ((S (bpd_candidate_pvs_necessary_base)) * bpvi_v_pvs_necessary_base_candidate_power)) /\ exists bpvi_q_pvs_necessary_base_candidate_power_terminal. bpvi_u_pvs_necessary_base_candidate_power = bpvi_q_pvs_necessary_base_candidate_power_terminal * S ((S (bpd_candidate_pvs_necessary_base)) * bpvi_v_pvs_necessary_base_candidate_power) + (bpvi_result_pvs_necessary_base_candidate))) /\ forall bpvi_j_pvs_necessary_base_candidate_power. (exists bpvi_product_gap_pvs_necessary_base_candidate_power. bpvi_product_gap_pvs_necessary_base_candidate_power + S bpvi_j_pvs_necessary_base_candidate_power = bpd_candidate_pvs_necessary_base) -> exists bpvi_factor_pvs_necessary_base_candidate_power bpvi_partial_pvs_necessary_base_candidate_power bpvi_successor_pvs_necessary_base_candidate_power. ((((exists bpvi_h_pvs_necessary_base_candidate_power_factor. bpvi_h_pvs_necessary_base_candidate_power_factor + S (bpvi_factor_pvs_necessary_base_candidate_power) = S ((S (bpvi_j_pvs_necessary_base_candidate_power)) * bpvi_c_pvs_necessary_base_candidate_power)) /\ exists bpvi_q_pvs_necessary_base_candidate_power_factor. bpvi_b_pvs_necessary_base_candidate_power = bpvi_q_pvs_necessary_base_candidate_power_factor * S ((S (bpvi_j_pvs_necessary_base_candidate_power)) * bpvi_c_pvs_necessary_base_candidate_power) + (bpvi_factor_pvs_necessary_base_candidate_power))) /\ ((((exists bpvi_h_pvs_necessary_base_candidate_power_partial. bpvi_h_pvs_necessary_base_candidate_power_partial + S (bpvi_partial_pvs_necessary_base_candidate_power) = S ((S (bpvi_j_pvs_necessary_base_candidate_power)) * bpvi_v_pvs_necessary_base_candidate_power)) /\ exists bpvi_q_pvs_necessary_base_candidate_power_partial. bpvi_u_pvs_necessary_base_candidate_power = bpvi_q_pvs_necessary_base_candidate_power_partial * S ((S (bpvi_j_pvs_necessary_base_candidate_power)) * bpvi_v_pvs_necessary_base_candidate_power) + (bpvi_partial_pvs_necessary_base_candidate_power))) /\ ((((exists bpvi_h_pvs_necessary_base_candidate_power_successor. bpvi_h_pvs_necessary_base_candidate_power_successor + S (bpvi_successor_pvs_necessary_base_candidate_power) = S ((S (S bpvi_j_pvs_necessary_base_candidate_power)) * bpvi_v_pvs_necessary_base_candidate_power)) /\ exists bpvi_q_pvs_necessary_base_candidate_power_successor. bpvi_u_pvs_necessary_base_candidate_power = bpvi_q_pvs_necessary_base_candidate_power_successor * S ((S (S bpvi_j_pvs_necessary_base_candidate_power)) * bpvi_v_pvs_necessary_base_candidate_power) + (bpvi_successor_pvs_necessary_base_candidate_power))) /\ bpvi_successor_pvs_necessary_base_candidate_power = bpvi_partial_pvs_necessary_base_candidate_power * bpvi_factor_pvs_necessary_base_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_necessary_base_candidate. r = bpvi_result_pvs_necessary_base_candidate * bpvi_divisor_factor_pvs_necessary_base_candidate)) -> (exists bpd_gap_pvs_necessary_base_maximal. bpd_gap_pvs_necessary_base_maximal + (bpd_candidate_pvs_necessary_base) = (f)))
  22. 0022specialize power_valuation_exists (p)
  23. 0023specialize power_valuation_exists (r)
  24. 0024apply power_valuation_exists
  25. 0025cases hbase
  26. 0026exists x
  27. 0027specialize prime_power_valuation_pow_value (p)
  28. 0028specialize prime_power_valuation_pow_value (r)
  29. 0029specialize prime_power_valuation_pow_value (k)
  30. 0030specialize prime_power_valuation_pow_value (x)
  31. 0031specialize prime_power_valuation_pow_value (n)
  32. 0032specialize prime_power_valuation_pow_value (e)
  33. 0033apply prime_power_valuation_pow_value
  34. 0034exact hp
  35. 0035exact hr
  36. 0036exact hbase_witness
  37. 0037exact hpow
  38. 0038exact hval