PV0011

prime_valuation_strict_cofactor_exists

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

Every positive nonunit has an actual full prime-power cofactor strictly smaller than itself; the exponent, power and nondivisibility are all constructed.

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. ~(n = 0) -> ~(n = 1) -> exists p e P u. (((~((p) = 1) /\ forall pvs_left_strict_cofactorprime pvs_right_strict_cofactorprime. (p) = pvs_left_strict_cofactorprime * pvs_right_strict_cofactorprime -> pvs_left_strict_cofactorprime = 1 \/ pvs_right_strict_cofactorprime = 1) /\ (((~(e = 0)) /\ (((((exists bpd_gap_pvs_strict_cofactorvaluation_selected_bound. bpd_gap_pvs_strict_cofactorvaluation_selected_bound + (e) = (n)) /\ (exists bpvi_result_pvs_strict_cofactorvaluation_selected. ((exists bpvi_b_pvs_strict_cofactorvaluation_selected_power bpvi_c_pvs_strict_cofactorvaluation_selected_power. ((forall bpvi_i_pvs_strict_cofactorvaluation_selected_power. (exists bpvi_repeat_gap_pvs_strict_cofactorvaluation_selected_power. bpvi_repeat_gap_pvs_strict_cofactorvaluation_selected_power + S bpvi_i_pvs_strict_cofactorvaluation_selected_power = e) -> (((exists bpvi_h_pvs_strict_cofactorvaluation_selected_power_repeat. bpvi_h_pvs_strict_cofactorvaluation_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_strict_cofactorvaluation_selected_power)) * bpvi_c_pvs_strict_cofactorvaluation_selected_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_selected_power_repeat. bpvi_b_pvs_strict_cofactorvaluation_selected_power = bpvi_q_pvs_strict_cofactorvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_strict_cofactorvaluation_selected_power)) * bpvi_c_pvs_strict_cofactorvaluation_selected_power) + (p)))) /\ (exists bpvi_u_pvs_strict_cofactorvaluation_selected_power bpvi_v_pvs_strict_cofactorvaluation_selected_power. ((((exists bpvi_h_pvs_strict_cofactorvaluation_selected_power_start. bpvi_h_pvs_strict_cofactorvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_selected_power_start. bpvi_u_pvs_strict_cofactorvaluation_selected_power = bpvi_q_pvs_strict_cofactorvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_strict_cofactorvaluation_selected_power_terminal. bpvi_h_pvs_strict_cofactorvaluation_selected_power_terminal + S (bpvi_result_pvs_strict_cofactorvaluation_selected) = S ((S (e)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_selected_power_terminal. bpvi_u_pvs_strict_cofactorvaluation_selected_power = bpvi_q_pvs_strict_cofactorvaluation_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power) + (bpvi_result_pvs_strict_cofactorvaluation_selected))) /\ forall bpvi_j_pvs_strict_cofactorvaluation_selected_power. (exists bpvi_product_gap_pvs_strict_cofactorvaluation_selected_power. bpvi_product_gap_pvs_strict_cofactorvaluation_selected_power + S bpvi_j_pvs_strict_cofactorvaluation_selected_power = e) -> exists bpvi_factor_pvs_strict_cofactorvaluation_selected_power bpvi_partial_pvs_strict_cofactorvaluation_selected_power bpvi_successor_pvs_strict_cofactorvaluation_selected_power. ((((exists bpvi_h_pvs_strict_cofactorvaluation_selected_power_factor. bpvi_h_pvs_strict_cofactorvaluation_selected_power_factor + S (bpvi_factor_pvs_strict_cofactorvaluation_selected_power) = S ((S (bpvi_j_pvs_strict_cofactorvaluation_selected_power)) * bpvi_c_pvs_strict_cofactorvaluation_selected_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_selected_power_factor. bpvi_b_pvs_strict_cofactorvaluation_selected_power = bpvi_q_pvs_strict_cofactorvaluation_selected_power_factor * S ((S (bpvi_j_pvs_strict_cofactorvaluation_selected_power)) * bpvi_c_pvs_strict_cofactorvaluation_selected_power) + (bpvi_factor_pvs_strict_cofactorvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_strict_cofactorvaluation_selected_power_partial. bpvi_h_pvs_strict_cofactorvaluation_selected_power_partial + S (bpvi_partial_pvs_strict_cofactorvaluation_selected_power) = S ((S (bpvi_j_pvs_strict_cofactorvaluation_selected_power)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_selected_power_partial. bpvi_u_pvs_strict_cofactorvaluation_selected_power = bpvi_q_pvs_strict_cofactorvaluation_selected_power_partial * S ((S (bpvi_j_pvs_strict_cofactorvaluation_selected_power)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power) + (bpvi_partial_pvs_strict_cofactorvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_strict_cofactorvaluation_selected_power_successor. bpvi_h_pvs_strict_cofactorvaluation_selected_power_successor + S (bpvi_successor_pvs_strict_cofactorvaluation_selected_power) = S ((S (S bpvi_j_pvs_strict_cofactorvaluation_selected_power)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_selected_power_successor. bpvi_u_pvs_strict_cofactorvaluation_selected_power = bpvi_q_pvs_strict_cofactorvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_strict_cofactorvaluation_selected_power)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power) + (bpvi_successor_pvs_strict_cofactorvaluation_selected_power))) /\ bpvi_successor_pvs_strict_cofactorvaluation_selected_power = bpvi_partial_pvs_strict_cofactorvaluation_selected_power * bpvi_factor_pvs_strict_cofactorvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_strict_cofactorvaluation_selected. n = bpvi_result_pvs_strict_cofactorvaluation_selected * bpvi_divisor_factor_pvs_strict_cofactorvaluation_selected))) /\ forall bpd_candidate_pvs_strict_cofactorvaluation. (exists bpd_gap_pvs_strict_cofactorvaluation_candidate_bound. bpd_gap_pvs_strict_cofactorvaluation_candidate_bound + (bpd_candidate_pvs_strict_cofactorvaluation) = (n)) -> (exists bpvi_result_pvs_strict_cofactorvaluation_candidate. ((exists bpvi_b_pvs_strict_cofactorvaluation_candidate_power bpvi_c_pvs_strict_cofactorvaluation_candidate_power. ((forall bpvi_i_pvs_strict_cofactorvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_strict_cofactorvaluation_candidate_power. bpvi_repeat_gap_pvs_strict_cofactorvaluation_candidate_power + S bpvi_i_pvs_strict_cofactorvaluation_candidate_power = bpd_candidate_pvs_strict_cofactorvaluation) -> (((exists bpvi_h_pvs_strict_cofactorvaluation_candidate_power_repeat. bpvi_h_pvs_strict_cofactorvaluation_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_c_pvs_strict_cofactorvaluation_candidate_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_candidate_power_repeat. bpvi_b_pvs_strict_cofactorvaluation_candidate_power = bpvi_q_pvs_strict_cofactorvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_c_pvs_strict_cofactorvaluation_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_strict_cofactorvaluation_candidate_power bpvi_v_pvs_strict_cofactorvaluation_candidate_power. ((((exists bpvi_h_pvs_strict_cofactorvaluation_candidate_power_start. bpvi_h_pvs_strict_cofactorvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_candidate_power_start. bpvi_u_pvs_strict_cofactorvaluation_candidate_power = bpvi_q_pvs_strict_cofactorvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_strict_cofactorvaluation_candidate_power_terminal. bpvi_h_pvs_strict_cofactorvaluation_candidate_power_terminal + S (bpvi_result_pvs_strict_cofactorvaluation_candidate) = S ((S (bpd_candidate_pvs_strict_cofactorvaluation)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_candidate_power_terminal. bpvi_u_pvs_strict_cofactorvaluation_candidate_power = bpvi_q_pvs_strict_cofactorvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_strict_cofactorvaluation)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power) + (bpvi_result_pvs_strict_cofactorvaluation_candidate))) /\ forall bpvi_j_pvs_strict_cofactorvaluation_candidate_power. (exists bpvi_product_gap_pvs_strict_cofactorvaluation_candidate_power. bpvi_product_gap_pvs_strict_cofactorvaluation_candidate_power + S bpvi_j_pvs_strict_cofactorvaluation_candidate_power = bpd_candidate_pvs_strict_cofactorvaluation) -> exists bpvi_factor_pvs_strict_cofactorvaluation_candidate_power bpvi_partial_pvs_strict_cofactorvaluation_candidate_power bpvi_successor_pvs_strict_cofactorvaluation_candidate_power. ((((exists bpvi_h_pvs_strict_cofactorvaluation_candidate_power_factor. bpvi_h_pvs_strict_cofactorvaluation_candidate_power_factor + S (bpvi_factor_pvs_strict_cofactorvaluation_candidate_power) = S ((S (bpvi_j_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_c_pvs_strict_cofactorvaluation_candidate_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_candidate_power_factor. bpvi_b_pvs_strict_cofactorvaluation_candidate_power = bpvi_q_pvs_strict_cofactorvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_c_pvs_strict_cofactorvaluation_candidate_power) + (bpvi_factor_pvs_strict_cofactorvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_strict_cofactorvaluation_candidate_power_partial. bpvi_h_pvs_strict_cofactorvaluation_candidate_power_partial + S (bpvi_partial_pvs_strict_cofactorvaluation_candidate_power) = S ((S (bpvi_j_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_candidate_power_partial. bpvi_u_pvs_strict_cofactorvaluation_candidate_power = bpvi_q_pvs_strict_cofactorvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power) + (bpvi_partial_pvs_strict_cofactorvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_strict_cofactorvaluation_candidate_power_successor. bpvi_h_pvs_strict_cofactorvaluation_candidate_power_successor + S (bpvi_successor_pvs_strict_cofactorvaluation_candidate_power) = S ((S (S bpvi_j_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_candidate_power_successor. bpvi_u_pvs_strict_cofactorvaluation_candidate_power = bpvi_q_pvs_strict_cofactorvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power) + (bpvi_successor_pvs_strict_cofactorvaluation_candidate_power))) /\ bpvi_successor_pvs_strict_cofactorvaluation_candidate_power = bpvi_partial_pvs_strict_cofactorvaluation_candidate_power * bpvi_factor_pvs_strict_cofactorvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_strict_cofactorvaluation_candidate. n = bpvi_result_pvs_strict_cofactorvaluation_candidate * bpvi_divisor_factor_pvs_strict_cofactorvaluation_candidate)) -> (exists bpd_gap_pvs_strict_cofactorvaluation_maximal. bpd_gap_pvs_strict_cofactorvaluation_maximal + (bpd_candidate_pvs_strict_cofactorvaluation) = (e))) /\ (((exists pa_b_pvs_strict_cofactorpower pa_c_pvs_strict_cofactorpower. ((forall pa_i_pvs_strict_cofactorpower_repeat. (exists pa_lt_pvs_strict_cofactorpower_repeat_bound. pa_lt_pvs_strict_cofactorpower_repeat_bound + S pa_i_pvs_strict_cofactorpower_repeat = e) -> (((exists pa_h_pvs_strict_cofactorpower_repeat_decoded. pa_h_pvs_strict_cofactorpower_repeat_decoded + S (p) = S ((S (pa_i_pvs_strict_cofactorpower_repeat)) * pa_c_pvs_strict_cofactorpower)) /\ exists pa_q_pvs_strict_cofactorpower_repeat_decoded. pa_b_pvs_strict_cofactorpower = pa_q_pvs_strict_cofactorpower_repeat_decoded * S ((S (pa_i_pvs_strict_cofactorpower_repeat)) * pa_c_pvs_strict_cofactorpower) + (p)))) /\ (exists pa_u_pvs_strict_cofactorpower_product pa_v_pvs_strict_cofactorpower_product. ((((exists pa_h_pvs_strict_cofactorpower_product_start. pa_h_pvs_strict_cofactorpower_product_start + S (1) = S ((S (0)) * pa_v_pvs_strict_cofactorpower_product)) /\ exists pa_q_pvs_strict_cofactorpower_product_start. pa_u_pvs_strict_cofactorpower_product = pa_q_pvs_strict_cofactorpower_product_start * S ((S (0)) * pa_v_pvs_strict_cofactorpower_product) + (1))) /\ ((((exists pa_h_pvs_strict_cofactorpower_product_terminal. pa_h_pvs_strict_cofactorpower_product_terminal + S (P) = S ((S (e)) * pa_v_pvs_strict_cofactorpower_product)) /\ exists pa_q_pvs_strict_cofactorpower_product_terminal. pa_u_pvs_strict_cofactorpower_product = pa_q_pvs_strict_cofactorpower_product_terminal * S ((S (e)) * pa_v_pvs_strict_cofactorpower_product) + (P))) /\ forall pa_i_pvs_strict_cofactorpower_product. (exists pa_lt_pvs_strict_cofactorpower_product_bound. pa_lt_pvs_strict_cofactorpower_product_bound + S pa_i_pvs_strict_cofactorpower_product = e) -> exists pa_p_pvs_strict_cofactorpower_product pa_r_pvs_strict_cofactorpower_product pa_s_pvs_strict_cofactorpower_product. ((((exists pa_h_pvs_strict_cofactorpower_product_factor. pa_h_pvs_strict_cofactorpower_product_factor + S (pa_p_pvs_strict_cofactorpower_product) = S ((S (pa_i_pvs_strict_cofactorpower_product)) * pa_c_pvs_strict_cofactorpower)) /\ exists pa_q_pvs_strict_cofactorpower_product_factor. pa_b_pvs_strict_cofactorpower = pa_q_pvs_strict_cofactorpower_product_factor * S ((S (pa_i_pvs_strict_cofactorpower_product)) * pa_c_pvs_strict_cofactorpower) + (pa_p_pvs_strict_cofactorpower_product))) /\ ((((exists pa_h_pvs_strict_cofactorpower_product_partial. pa_h_pvs_strict_cofactorpower_product_partial + S (pa_r_pvs_strict_cofactorpower_product) = S ((S (pa_i_pvs_strict_cofactorpower_product)) * pa_v_pvs_strict_cofactorpower_product)) /\ exists pa_q_pvs_strict_cofactorpower_product_partial. pa_u_pvs_strict_cofactorpower_product = pa_q_pvs_strict_cofactorpower_product_partial * S ((S (pa_i_pvs_strict_cofactorpower_product)) * pa_v_pvs_strict_cofactorpower_product) + (pa_r_pvs_strict_cofactorpower_product))) /\ ((((exists pa_h_pvs_strict_cofactorpower_product_successor. pa_h_pvs_strict_cofactorpower_product_successor + S (pa_s_pvs_strict_cofactorpower_product) = S ((S (S pa_i_pvs_strict_cofactorpower_product)) * pa_v_pvs_strict_cofactorpower_product)) /\ exists pa_q_pvs_strict_cofactorpower_product_successor. pa_u_pvs_strict_cofactorpower_product = pa_q_pvs_strict_cofactorpower_product_successor * S ((S (S pa_i_pvs_strict_cofactorpower_product)) * pa_v_pvs_strict_cofactorpower_product) + (pa_s_pvs_strict_cofactorpower_product))) /\ pa_s_pvs_strict_cofactorpower_product = pa_r_pvs_strict_cofactorpower_product * pa_p_pvs_strict_cofactorpower_product)))))))) /\ ((((n) = (P) * (u)) /\ (((~(u = 0)) /\ (((~(exists pvs_factor_strict_cofactornondivisor. (u) = (p) * pvs_factor_strict_cofactornondivisor)) /\ (exists pvs_gap_strict_cofactordescent. pvs_gap_strict_cofactordescent + S (u) = (n))))))))))))))))

Constructive proof overview

Generated structural guide

Every positive nonunit has an actual full prime-power cofactor strictly smaller than itself; the exponent, power and nondivisibility are all constructed.

The unchanged tactic script uses 8 declared prerequisites and contains 81 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_divisor_exists Stable theorem; checked-use authorized power_valuation_exists Alpha theorem; checked-use authorized prime_divisor_power_valuation_nonzero Alpha theorem; checked-use authorized power_valuation_exact_cofactor Alpha theorem; checked-use authorized PV0006 pow_positive_exponent_base_divides divisor_one Stable theorem; checked-use authorized proper_factor_lt Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized

Direct dependents

PV0013 prime_valuation_support_bounded_exists

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

81 script commands · 30 reading checkpoints · 6 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)
pow positive exponent base divides

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

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

  1. L1
    intro n
  2. L2
    intro hn
  3. L3
    intro hunit
02Establish hpL4–8

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

  1. L4
    have hp : exists p. (~((p) = 1) /\ forall pvs_left_strict_prime pvs_right_strict_prime. (p) = pvs_left_strict_prime * pvs_right_strict_prime -> pvs_left_strict_prime = 1 \/ pvs_right_strict_prime = 1) /\ (exists pvs_factor_strict_divisor. (n) = (p) * pvs_factor_strict_divisor)
  2. L5
    specialize prime_divisor_exists (n)
  3. L6
    apply prime_divisor_exists
  4. L7
    exact hn
  5. L8
    exact hunit
03Separate the logical casesL9–10

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

  1. L9
    cases hp
  2. L10
    cases hp_witness
04Establish heL11–14

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

  1. L11
    have he : ∃ e. BoundedPowerValuation(x,n,n,e)Definitions: BoundedPowerValuation
  2. L12
    specialize power_valuation_exists (x)
  3. L13
    specialize power_valuation_exists (n)
  4. L14
    apply power_valuation_exists
05Separate the logical casesL15–15

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

  1. L15
    cases he
06Establish henzL16–25

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

  1. L16
    have henz : ~(x1 = 0)
  2. L17
    intro hezero
  3. L18
    specialize prime_divisor_power_valuation_nonzero (x)
  4. L19
    specialize prime_divisor_power_valuation_nonzero (n)
  5. L20
    specialize prime_divisor_power_valuation_nonzero (x1)
  6. L21
    apply prime_divisor_power_valuation_nonzero
  7. L22
    exact hp_witness_left
  8. L23
    exact hn
  9. L24
    exact he_witness
  10. L25
    exact hp_witness_right
07Use earlier factsL26–26

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

  1. L26
    exact hezero
08Establish hcL27–34

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

  1. L27
    have hc : ∃ P. ∃ u. Pow(x,x1,P) ∧ (n = P · u ∧ (¬u = 0 ∧ ¬Dvd(x,u)))Definitions: DvdPow
  2. L28
    specialize power_valuation_exact_cofactor (x)
  3. L29
    specialize power_valuation_exact_cofactor (n)
  4. L30
    specialize power_valuation_exact_cofactor (x1)
  5. L31
    apply power_valuation_exact_cofactor
  6. L32
    exact hp_witness_left
  7. L33
    exact hn
  8. L34
    exact he_witness
09Separate the logical casesL35–39

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

  1. L35
    cases hc
  2. L36
    cases hc_witness
  3. L37
    cases hc_witness_witness
  4. L38
    cases hc_witness_witness_right
  5. L39
    cases hc_witness_witness_right_right
10Establish hpnonunitL40–41

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

  1. L40
    have hpnonunit : ~(x2 = 1)
  2. L41
    intro hPone
11Establish hbaseL42–49

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

  1. L42
    have hbase : exists pvs_factor_strict_base_divisor. (x2) = (x) * pvs_factor_strict_base_divisor
  2. L43
    specialize pow_positive_exponent_base_divides (x)
  3. L44
    specialize pow_positive_exponent_base_divides (x1)
  4. L45
    specialize pow_positive_exponent_base_divides (x2)
  5. L46
    apply pow_positive_exponent_base_divides
  6. L47
    exact henz
  7. L48
    exact hc_witness_witness_left
  8. L49
    rewrite hPone at hbase
12Separate the logical casesL50–50

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

  1. L50
    cases hp_witness_left
13Use earlier factsL51–54

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

  1. L51
    apply hp_witness_left_left
  2. L52
    specialize divisor_one (x)
  3. L53
    apply divisor_one
  4. L54
    exact hbase
14Construct an explicit witnessL55–58

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

  1. L55
    exists x
  2. L56
    exists x1
  3. L57
    exists x2
  4. L58
    exists x3
15Separate the logical casesL59–59

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

  1. L59
    split
16Use earlier factsL60–60

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

  1. L60
    exact hp_witness_left
17Separate the logical casesL61–61

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

  1. L61
    split
18Use earlier factsL62–62

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

  1. L62
    exact henz
19Separate the logical casesL63–63

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

  1. L63
    split
20Use earlier factsL64–64

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

  1. L64
    exact he_witness
21Separate the logical casesL65–65

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

  1. L65
    split
22Use earlier factsL66–66

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

  1. L66
    exact hc_witness_witness_left
23Separate the logical casesL67–67

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

  1. L67
    split
24Use earlier factsL68–68

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

  1. L68
    exact hc_witness_witness_right_left
25Separate the logical casesL69–69

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

  1. L69
    split
26Use earlier factsL70–70

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

  1. L70
    exact hc_witness_witness_right_right_left
27Separate the logical casesL71–71

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

  1. L71
    split
28Use earlier factsL72–77

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

  1. L72
    exact hc_witness_witness_right_right_right
  2. L73
    specialize proper_factor_lt (n)
  3. L74
    specialize proper_factor_lt (x3)
  4. L75
    specialize proper_factor_lt (x2)
  5. L76
    apply proper_factor_lt
  6. L77
    exact hn
29Calculate and transport equalitiesL78–78

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

  1. L78
    trans x2 * x3
30Use earlier factsL79–81

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

  1. L79
    exact hc_witness_witness_right_left
  2. L80
    apply mul_comm
  3. L81
    exact hpnonunit

Library-wide reading audit

Original exact command ledger · 81 lines
  1. 0001intro n
  2. 0002intro hn
  3. 0003intro hunit
  4. 0004have hp : exists p. (~((p) = 1) /\ forall pvs_left_strict_prime pvs_right_strict_prime. (p) = pvs_left_strict_prime * pvs_right_strict_prime -> pvs_left_strict_prime = 1 \/ pvs_right_strict_prime = 1) /\ (exists pvs_factor_strict_divisor. (n) = (p) * pvs_factor_strict_divisor)
  5. 0005specialize prime_divisor_exists (n)
  6. 0006apply prime_divisor_exists
  7. 0007exact hn
  8. 0008exact hunit
  9. 0009cases hp
  10. 0010cases hp_witness
  11. 0011have he : exists e. (((exists bpd_gap_pvs_strict_valuation_selected_bound. bpd_gap_pvs_strict_valuation_selected_bound + (e) = (n)) /\ (exists bpvi_result_pvs_strict_valuation_selected. ((exists bpvi_b_pvs_strict_valuation_selected_power bpvi_c_pvs_strict_valuation_selected_power. ((forall bpvi_i_pvs_strict_valuation_selected_power. (exists bpvi_repeat_gap_pvs_strict_valuation_selected_power. bpvi_repeat_gap_pvs_strict_valuation_selected_power + S bpvi_i_pvs_strict_valuation_selected_power = e) -> (((exists bpvi_h_pvs_strict_valuation_selected_power_repeat. bpvi_h_pvs_strict_valuation_selected_power_repeat + S (x) = S ((S (bpvi_i_pvs_strict_valuation_selected_power)) * bpvi_c_pvs_strict_valuation_selected_power)) /\ exists bpvi_q_pvs_strict_valuation_selected_power_repeat. bpvi_b_pvs_strict_valuation_selected_power = bpvi_q_pvs_strict_valuation_selected_power_repeat * S ((S (bpvi_i_pvs_strict_valuation_selected_power)) * bpvi_c_pvs_strict_valuation_selected_power) + (x)))) /\ (exists bpvi_u_pvs_strict_valuation_selected_power bpvi_v_pvs_strict_valuation_selected_power. ((((exists bpvi_h_pvs_strict_valuation_selected_power_start. bpvi_h_pvs_strict_valuation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_strict_valuation_selected_power)) /\ exists bpvi_q_pvs_strict_valuation_selected_power_start. bpvi_u_pvs_strict_valuation_selected_power = bpvi_q_pvs_strict_valuation_selected_power_start * S ((S (0)) * bpvi_v_pvs_strict_valuation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_strict_valuation_selected_power_terminal. bpvi_h_pvs_strict_valuation_selected_power_terminal + S (bpvi_result_pvs_strict_valuation_selected) = S ((S (e)) * bpvi_v_pvs_strict_valuation_selected_power)) /\ exists bpvi_q_pvs_strict_valuation_selected_power_terminal. bpvi_u_pvs_strict_valuation_selected_power = bpvi_q_pvs_strict_valuation_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_strict_valuation_selected_power) + (bpvi_result_pvs_strict_valuation_selected))) /\ forall bpvi_j_pvs_strict_valuation_selected_power. (exists bpvi_product_gap_pvs_strict_valuation_selected_power. bpvi_product_gap_pvs_strict_valuation_selected_power + S bpvi_j_pvs_strict_valuation_selected_power = e) -> exists bpvi_factor_pvs_strict_valuation_selected_power bpvi_partial_pvs_strict_valuation_selected_power bpvi_successor_pvs_strict_valuation_selected_power. ((((exists bpvi_h_pvs_strict_valuation_selected_power_factor. bpvi_h_pvs_strict_valuation_selected_power_factor + S (bpvi_factor_pvs_strict_valuation_selected_power) = S ((S (bpvi_j_pvs_strict_valuation_selected_power)) * bpvi_c_pvs_strict_valuation_selected_power)) /\ exists bpvi_q_pvs_strict_valuation_selected_power_factor. bpvi_b_pvs_strict_valuation_selected_power = bpvi_q_pvs_strict_valuation_selected_power_factor * S ((S (bpvi_j_pvs_strict_valuation_selected_power)) * bpvi_c_pvs_strict_valuation_selected_power) + (bpvi_factor_pvs_strict_valuation_selected_power))) /\ ((((exists bpvi_h_pvs_strict_valuation_selected_power_partial. bpvi_h_pvs_strict_valuation_selected_power_partial + S (bpvi_partial_pvs_strict_valuation_selected_power) = S ((S (bpvi_j_pvs_strict_valuation_selected_power)) * bpvi_v_pvs_strict_valuation_selected_power)) /\ exists bpvi_q_pvs_strict_valuation_selected_power_partial. bpvi_u_pvs_strict_valuation_selected_power = bpvi_q_pvs_strict_valuation_selected_power_partial * S ((S (bpvi_j_pvs_strict_valuation_selected_power)) * bpvi_v_pvs_strict_valuation_selected_power) + (bpvi_partial_pvs_strict_valuation_selected_power))) /\ ((((exists bpvi_h_pvs_strict_valuation_selected_power_successor. bpvi_h_pvs_strict_valuation_selected_power_successor + S (bpvi_successor_pvs_strict_valuation_selected_power) = S ((S (S bpvi_j_pvs_strict_valuation_selected_power)) * bpvi_v_pvs_strict_valuation_selected_power)) /\ exists bpvi_q_pvs_strict_valuation_selected_power_successor. bpvi_u_pvs_strict_valuation_selected_power = bpvi_q_pvs_strict_valuation_selected_power_successor * S ((S (S bpvi_j_pvs_strict_valuation_selected_power)) * bpvi_v_pvs_strict_valuation_selected_power) + (bpvi_successor_pvs_strict_valuation_selected_power))) /\ bpvi_successor_pvs_strict_valuation_selected_power = bpvi_partial_pvs_strict_valuation_selected_power * bpvi_factor_pvs_strict_valuation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_strict_valuation_selected. n = bpvi_result_pvs_strict_valuation_selected * bpvi_divisor_factor_pvs_strict_valuation_selected))) /\ forall bpd_candidate_pvs_strict_valuation. (exists bpd_gap_pvs_strict_valuation_candidate_bound. bpd_gap_pvs_strict_valuation_candidate_bound + (bpd_candidate_pvs_strict_valuation) = (n)) -> (exists bpvi_result_pvs_strict_valuation_candidate. ((exists bpvi_b_pvs_strict_valuation_candidate_power bpvi_c_pvs_strict_valuation_candidate_power. ((forall bpvi_i_pvs_strict_valuation_candidate_power. (exists bpvi_repeat_gap_pvs_strict_valuation_candidate_power. bpvi_repeat_gap_pvs_strict_valuation_candidate_power + S bpvi_i_pvs_strict_valuation_candidate_power = bpd_candidate_pvs_strict_valuation) -> (((exists bpvi_h_pvs_strict_valuation_candidate_power_repeat. bpvi_h_pvs_strict_valuation_candidate_power_repeat + S (x) = S ((S (bpvi_i_pvs_strict_valuation_candidate_power)) * bpvi_c_pvs_strict_valuation_candidate_power)) /\ exists bpvi_q_pvs_strict_valuation_candidate_power_repeat. bpvi_b_pvs_strict_valuation_candidate_power = bpvi_q_pvs_strict_valuation_candidate_power_repeat * S ((S (bpvi_i_pvs_strict_valuation_candidate_power)) * bpvi_c_pvs_strict_valuation_candidate_power) + (x)))) /\ (exists bpvi_u_pvs_strict_valuation_candidate_power bpvi_v_pvs_strict_valuation_candidate_power. ((((exists bpvi_h_pvs_strict_valuation_candidate_power_start. bpvi_h_pvs_strict_valuation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_strict_valuation_candidate_power)) /\ exists bpvi_q_pvs_strict_valuation_candidate_power_start. bpvi_u_pvs_strict_valuation_candidate_power = bpvi_q_pvs_strict_valuation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_strict_valuation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_strict_valuation_candidate_power_terminal. bpvi_h_pvs_strict_valuation_candidate_power_terminal + S (bpvi_result_pvs_strict_valuation_candidate) = S ((S (bpd_candidate_pvs_strict_valuation)) * bpvi_v_pvs_strict_valuation_candidate_power)) /\ exists bpvi_q_pvs_strict_valuation_candidate_power_terminal. bpvi_u_pvs_strict_valuation_candidate_power = bpvi_q_pvs_strict_valuation_candidate_power_terminal * S ((S (bpd_candidate_pvs_strict_valuation)) * bpvi_v_pvs_strict_valuation_candidate_power) + (bpvi_result_pvs_strict_valuation_candidate))) /\ forall bpvi_j_pvs_strict_valuation_candidate_power. (exists bpvi_product_gap_pvs_strict_valuation_candidate_power. bpvi_product_gap_pvs_strict_valuation_candidate_power + S bpvi_j_pvs_strict_valuation_candidate_power = bpd_candidate_pvs_strict_valuation) -> exists bpvi_factor_pvs_strict_valuation_candidate_power bpvi_partial_pvs_strict_valuation_candidate_power bpvi_successor_pvs_strict_valuation_candidate_power. ((((exists bpvi_h_pvs_strict_valuation_candidate_power_factor. bpvi_h_pvs_strict_valuation_candidate_power_factor + S (bpvi_factor_pvs_strict_valuation_candidate_power) = S ((S (bpvi_j_pvs_strict_valuation_candidate_power)) * bpvi_c_pvs_strict_valuation_candidate_power)) /\ exists bpvi_q_pvs_strict_valuation_candidate_power_factor. bpvi_b_pvs_strict_valuation_candidate_power = bpvi_q_pvs_strict_valuation_candidate_power_factor * S ((S (bpvi_j_pvs_strict_valuation_candidate_power)) * bpvi_c_pvs_strict_valuation_candidate_power) + (bpvi_factor_pvs_strict_valuation_candidate_power))) /\ ((((exists bpvi_h_pvs_strict_valuation_candidate_power_partial. bpvi_h_pvs_strict_valuation_candidate_power_partial + S (bpvi_partial_pvs_strict_valuation_candidate_power) = S ((S (bpvi_j_pvs_strict_valuation_candidate_power)) * bpvi_v_pvs_strict_valuation_candidate_power)) /\ exists bpvi_q_pvs_strict_valuation_candidate_power_partial. bpvi_u_pvs_strict_valuation_candidate_power = bpvi_q_pvs_strict_valuation_candidate_power_partial * S ((S (bpvi_j_pvs_strict_valuation_candidate_power)) * bpvi_v_pvs_strict_valuation_candidate_power) + (bpvi_partial_pvs_strict_valuation_candidate_power))) /\ ((((exists bpvi_h_pvs_strict_valuation_candidate_power_successor. bpvi_h_pvs_strict_valuation_candidate_power_successor + S (bpvi_successor_pvs_strict_valuation_candidate_power) = S ((S (S bpvi_j_pvs_strict_valuation_candidate_power)) * bpvi_v_pvs_strict_valuation_candidate_power)) /\ exists bpvi_q_pvs_strict_valuation_candidate_power_successor. bpvi_u_pvs_strict_valuation_candidate_power = bpvi_q_pvs_strict_valuation_candidate_power_successor * S ((S (S bpvi_j_pvs_strict_valuation_candidate_power)) * bpvi_v_pvs_strict_valuation_candidate_power) + (bpvi_successor_pvs_strict_valuation_candidate_power))) /\ bpvi_successor_pvs_strict_valuation_candidate_power = bpvi_partial_pvs_strict_valuation_candidate_power * bpvi_factor_pvs_strict_valuation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_strict_valuation_candidate. n = bpvi_result_pvs_strict_valuation_candidate * bpvi_divisor_factor_pvs_strict_valuation_candidate)) -> (exists bpd_gap_pvs_strict_valuation_maximal. bpd_gap_pvs_strict_valuation_maximal + (bpd_candidate_pvs_strict_valuation) = (e)))
  12. 0012specialize power_valuation_exists (x)
  13. 0013specialize power_valuation_exists (n)
  14. 0014apply power_valuation_exists
  15. 0015cases he
  16. 0016have henz : ~(x1 = 0)
  17. 0017intro hezero
  18. 0018specialize prime_divisor_power_valuation_nonzero (x)
  19. 0019specialize prime_divisor_power_valuation_nonzero (n)
  20. 0020specialize prime_divisor_power_valuation_nonzero (x1)
  21. 0021apply prime_divisor_power_valuation_nonzero
  22. 0022exact hp_witness_left
  23. 0023exact hn
  24. 0024exact he_witness
  25. 0025exact hp_witness_right
  26. 0026exact hezero
  27. 0027have hc : exists P u. ((exists pa_b_pvs_strict_exact_power pa_c_pvs_strict_exact_power. ((forall pa_i_pvs_strict_exact_power_repeat. (exists pa_lt_pvs_strict_exact_power_repeat_bound. pa_lt_pvs_strict_exact_power_repeat_bound + S pa_i_pvs_strict_exact_power_repeat = x1) -> (((exists pa_h_pvs_strict_exact_power_repeat_decoded. pa_h_pvs_strict_exact_power_repeat_decoded + S (x) = S ((S (pa_i_pvs_strict_exact_power_repeat)) * pa_c_pvs_strict_exact_power)) /\ exists pa_q_pvs_strict_exact_power_repeat_decoded. pa_b_pvs_strict_exact_power = pa_q_pvs_strict_exact_power_repeat_decoded * S ((S (pa_i_pvs_strict_exact_power_repeat)) * pa_c_pvs_strict_exact_power) + (x)))) /\ (exists pa_u_pvs_strict_exact_power_product pa_v_pvs_strict_exact_power_product. ((((exists pa_h_pvs_strict_exact_power_product_start. pa_h_pvs_strict_exact_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_strict_exact_power_product)) /\ exists pa_q_pvs_strict_exact_power_product_start. pa_u_pvs_strict_exact_power_product = pa_q_pvs_strict_exact_power_product_start * S ((S (0)) * pa_v_pvs_strict_exact_power_product) + (1))) /\ ((((exists pa_h_pvs_strict_exact_power_product_terminal. pa_h_pvs_strict_exact_power_product_terminal + S (P) = S ((S (x1)) * pa_v_pvs_strict_exact_power_product)) /\ exists pa_q_pvs_strict_exact_power_product_terminal. pa_u_pvs_strict_exact_power_product = pa_q_pvs_strict_exact_power_product_terminal * S ((S (x1)) * pa_v_pvs_strict_exact_power_product) + (P))) /\ forall pa_i_pvs_strict_exact_power_product. (exists pa_lt_pvs_strict_exact_power_product_bound. pa_lt_pvs_strict_exact_power_product_bound + S pa_i_pvs_strict_exact_power_product = x1) -> exists pa_p_pvs_strict_exact_power_product pa_r_pvs_strict_exact_power_product pa_s_pvs_strict_exact_power_product. ((((exists pa_h_pvs_strict_exact_power_product_factor. pa_h_pvs_strict_exact_power_product_factor + S (pa_p_pvs_strict_exact_power_product) = S ((S (pa_i_pvs_strict_exact_power_product)) * pa_c_pvs_strict_exact_power)) /\ exists pa_q_pvs_strict_exact_power_product_factor. pa_b_pvs_strict_exact_power = pa_q_pvs_strict_exact_power_product_factor * S ((S (pa_i_pvs_strict_exact_power_product)) * pa_c_pvs_strict_exact_power) + (pa_p_pvs_strict_exact_power_product))) /\ ((((exists pa_h_pvs_strict_exact_power_product_partial. pa_h_pvs_strict_exact_power_product_partial + S (pa_r_pvs_strict_exact_power_product) = S ((S (pa_i_pvs_strict_exact_power_product)) * pa_v_pvs_strict_exact_power_product)) /\ exists pa_q_pvs_strict_exact_power_product_partial. pa_u_pvs_strict_exact_power_product = pa_q_pvs_strict_exact_power_product_partial * S ((S (pa_i_pvs_strict_exact_power_product)) * pa_v_pvs_strict_exact_power_product) + (pa_r_pvs_strict_exact_power_product))) /\ ((((exists pa_h_pvs_strict_exact_power_product_successor. pa_h_pvs_strict_exact_power_product_successor + S (pa_s_pvs_strict_exact_power_product) = S ((S (S pa_i_pvs_strict_exact_power_product)) * pa_v_pvs_strict_exact_power_product)) /\ exists pa_q_pvs_strict_exact_power_product_successor. pa_u_pvs_strict_exact_power_product = pa_q_pvs_strict_exact_power_product_successor * S ((S (S pa_i_pvs_strict_exact_power_product)) * pa_v_pvs_strict_exact_power_product) + (pa_s_pvs_strict_exact_power_product))) /\ pa_s_pvs_strict_exact_power_product = pa_r_pvs_strict_exact_power_product * pa_p_pvs_strict_exact_power_product)))))))) /\ (((n = P * u) /\ (((~(u = 0)) /\ (~(exists pvs_factor_strict_exact_fresh. (u) = (x) * pvs_factor_strict_exact_fresh)))))))
  28. 0028specialize power_valuation_exact_cofactor (x)
  29. 0029specialize power_valuation_exact_cofactor (n)
  30. 0030specialize power_valuation_exact_cofactor (x1)
  31. 0031apply power_valuation_exact_cofactor
  32. 0032exact hp_witness_left
  33. 0033exact hn
  34. 0034exact he_witness
  35. 0035cases hc
  36. 0036cases hc_witness
  37. 0037cases hc_witness_witness
  38. 0038cases hc_witness_witness_right
  39. 0039cases hc_witness_witness_right_right
  40. 0040have hpnonunit : ~(x2 = 1)
  41. 0041intro hPone
  42. 0042have hbase : exists pvs_factor_strict_base_divisor. (x2) = (x) * pvs_factor_strict_base_divisor
  43. 0043specialize pow_positive_exponent_base_divides (x)
  44. 0044specialize pow_positive_exponent_base_divides (x1)
  45. 0045specialize pow_positive_exponent_base_divides (x2)
  46. 0046apply pow_positive_exponent_base_divides
  47. 0047exact henz
  48. 0048exact hc_witness_witness_left
  49. 0049rewrite hPone at hbase
  50. 0050cases hp_witness_left
  51. 0051apply hp_witness_left_left
  52. 0052specialize divisor_one (x)
  53. 0053apply divisor_one
  54. 0054exact hbase
  55. 0055exists x
  56. 0056exists x1
  57. 0057exists x2
  58. 0058exists x3
  59. 0059split
  60. 0060exact hp_witness_left
  61. 0061split
  62. 0062exact henz
  63. 0063split
  64. 0064exact he_witness
  65. 0065split
  66. 0066exact hc_witness_witness_left
  67. 0067split
  68. 0068exact hc_witness_witness_right_left
  69. 0069split
  70. 0070exact hc_witness_witness_right_right_left
  71. 0071split
  72. 0072exact hc_witness_witness_right_right_right
  73. 0073specialize proper_factor_lt (n)
  74. 0074specialize proper_factor_lt (x3)
  75. 0075specialize proper_factor_lt (x2)
  76. 0076apply proper_factor_lt
  77. 0077exact hn
  78. 0078trans x2 * x3
  79. 0079exact hc_witness_witness_right_left
  80. 0080apply mul_comm
  81. 0081exact hpnonunit