MV0015

mobius_fresh_prime_negates

For an actual prime not dividing n, adjoining that prime negates the genuine Möbius value, including all nonsquarefree zero cases.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Mobius(n,z) is positive-domain only, independently defined from squarefreeness and actual prime-factor parity. Signed codes 0, 2 and 1 represent zero, +1 and -1. This family proves values and prime-adjunction laws; the separate Möbius-inversion family supplies the complete G007 endpoint.

Exact theorem in conservative defined notation

∀ p. ∀ n. ∀ a. ∀ b. Prime(p) → ¬Dvd(p,n) → Mobius(n,a) → Mobius(p · n,b) → SignedNegate(a,b)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

SignedNegate(a,b) · 1PrimeFactorList(n,b,c,l) · 1Squarefree(n) · 1AlternatingSignedUnit(n,z) · 1Mobius(n,z) · 2Dvd(d,n) · 1Prime(p) · 1

Actual proof prerequisites

mobius_prime_square_value_zeromultiple_mul_left · checked external prerequisitesigned_negate_zero · checked external prerequisitemobius_prime_factor_list_appendmobius_squarefree_fresh_prime_productmobius_squarefree_evaluationalternating_signed_unit_successor_negatesmul_comm · checked external prerequisite
Original expanded first-order statement 
forall p n a b. (~((p) = 1) /\ forall pvs_left_step_prime pvs_right_step_prime. (p) = pvs_left_step_prime * pvs_right_step_prime -> pvs_left_step_prime = 1 \/ pvs_right_step_prime = 1) -> ~(exists pvs_factor_step_fresh. (n) = (p) * pvs_factor_step_fresh) -> (((~((n) = 0)) /\ ((((exists mv_square_prime_step_sourcesquare. ((~((mv_square_prime_step_sourcesquare) = 1) /\ forall pvs_left_step_sourcesquareprime pvs_right_step_sourcesquareprime. (mv_square_prime_step_sourcesquare) = pvs_left_step_sourcesquareprime * pvs_right_step_sourcesquareprime -> pvs_left_step_sourcesquareprime = 1 \/ pvs_right_step_sourcesquareprime = 1) /\ (exists pvs_factor_step_sourcesquaredivisor. (n) = (mv_square_prime_step_sourcesquare * mv_square_prime_step_sourcesquare) * pvs_factor_step_sourcesquaredivisor))) /\ ((a) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_step_sourcesquarefree. (~((sfd_prime_step_sourcesquarefree) = 1) /\ forall pvs_left_step_sourcesquarefreedomain pvs_right_step_sourcesquarefreedomain. (sfd_prime_step_sourcesquarefree) = pvs_left_step_sourcesquarefreedomain * pvs_right_step_sourcesquarefreedomain -> pvs_left_step_sourcesquarefreedomain = 1 \/ pvs_right_step_sourcesquarefreedomain = 1) -> (exists pvs_le_gap_step_sourcesquarefreebound. pvs_le_gap_step_sourcesquarefreebound + (sfd_prime_step_sourcesquarefree) = (n)) -> ~(exists pvs_factor_step_sourcesquarefreesquare. (n) = (sfd_prime_step_sourcesquarefree * sfd_prime_step_sourcesquarefree) * pvs_factor_step_sourcesquarefreesquare)))) /\ (exists mv_factor_code_step_sourcefactors mv_factor_scale_step_sourcefactors mv_factor_count_step_sourcefactors. (((~(n = 0) /\ ((exists ff_u_fsat_step_sourcefactorsfactorization_product ff_v_fsat_step_sourcefactorsfactorization_product. ((((exists ff_h_fsat_step_sourcefactorsfactorization_product_start. ff_h_fsat_step_sourcefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_step_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_step_sourcefactorsfactorization_product_start. ff_u_fsat_step_sourcefactorsfactorization_product = ff_q_fsat_step_sourcefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_step_sourcefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_step_sourcefactorsfactorization_product_terminal. ff_h_fsat_step_sourcefactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_step_sourcefactors)) * ff_v_fsat_step_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_step_sourcefactorsfactorization_product_terminal. ff_u_fsat_step_sourcefactorsfactorization_product = ff_q_fsat_step_sourcefactorsfactorization_product_terminal * S ((S (mv_factor_count_step_sourcefactors)) * ff_v_fsat_step_sourcefactorsfactorization_product) + (n))) /\ forall ff_i_fsat_step_sourcefactorsfactorization_product. (exists ff_lt_fsat_step_sourcefactorsfactorization_product_bound. ff_lt_fsat_step_sourcefactorsfactorization_product_bound + S ff_i_fsat_step_sourcefactorsfactorization_product = mv_factor_count_step_sourcefactors) -> exists ff_p_fsat_step_sourcefactorsfactorization_product ff_r_fsat_step_sourcefactorsfactorization_product ff_s_fsat_step_sourcefactorsfactorization_product. ((((exists ff_h_fsat_step_sourcefactorsfactorization_product_factor. ff_h_fsat_step_sourcefactorsfactorization_product_factor + S (ff_p_fsat_step_sourcefactorsfactorization_product) = S ((S (ff_i_fsat_step_sourcefactorsfactorization_product)) * mv_factor_scale_step_sourcefactors)) /\ exists ff_q_fsat_step_sourcefactorsfactorization_product_factor. mv_factor_code_step_sourcefactors = ff_q_fsat_step_sourcefactorsfactorization_product_factor * S ((S (ff_i_fsat_step_sourcefactorsfactorization_product)) * mv_factor_scale_step_sourcefactors) + (ff_p_fsat_step_sourcefactorsfactorization_product))) /\ ((((exists ff_h_fsat_step_sourcefactorsfactorization_product_partial. ff_h_fsat_step_sourcefactorsfactorization_product_partial + S (ff_r_fsat_step_sourcefactorsfactorization_product) = S ((S (ff_i_fsat_step_sourcefactorsfactorization_product)) * ff_v_fsat_step_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_step_sourcefactorsfactorization_product_partial. ff_u_fsat_step_sourcefactorsfactorization_product = ff_q_fsat_step_sourcefactorsfactorization_product_partial * S ((S (ff_i_fsat_step_sourcefactorsfactorization_product)) * ff_v_fsat_step_sourcefactorsfactorization_product) + (ff_r_fsat_step_sourcefactorsfactorization_product))) /\ ((((exists ff_h_fsat_step_sourcefactorsfactorization_product_successor. ff_h_fsat_step_sourcefactorsfactorization_product_successor + S (ff_s_fsat_step_sourcefactorsfactorization_product) = S ((S (S ff_i_fsat_step_sourcefactorsfactorization_product)) * ff_v_fsat_step_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_step_sourcefactorsfactorization_product_successor. ff_u_fsat_step_sourcefactorsfactorization_product = ff_q_fsat_step_sourcefactorsfactorization_product_successor * S ((S (S ff_i_fsat_step_sourcefactorsfactorization_product)) * ff_v_fsat_step_sourcefactorsfactorization_product) + (ff_s_fsat_step_sourcefactorsfactorization_product))) /\ ff_s_fsat_step_sourcefactorsfactorization_product = ff_r_fsat_step_sourcefactorsfactorization_product * ff_p_fsat_step_sourcefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_step_sourcefactorsfactorization_primes. (exists ftsf_gap_fsat_step_sourcefactorsfactorization_primes_bound. ftsf_gap_fsat_step_sourcefactorsfactorization_primes_bound + S ftsf_index_fsat_step_sourcefactorsfactorization_primes = (mv_factor_count_step_sourcefactors)) -> exists ftsf_factor_fsat_step_sourcefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_step_sourcefactorsfactorization_primes_entry. ff_h_ftsf_fsat_step_sourcefactorsfactorization_primes_entry + S (ftsf_factor_fsat_step_sourcefactorsfactorization_primes) = S ((S (ftsf_index_fsat_step_sourcefactorsfactorization_primes)) * mv_factor_scale_step_sourcefactors)) /\ exists ff_q_ftsf_fsat_step_sourcefactorsfactorization_primes_entry. mv_factor_code_step_sourcefactors = ff_q_ftsf_fsat_step_sourcefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_step_sourcefactorsfactorization_primes)) * mv_factor_scale_step_sourcefactors) + (ftsf_factor_fsat_step_sourcefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_step_sourcefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_step_sourcefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_step_sourcefactorsfactorization_primes_prime. ftsf_factor_fsat_step_sourcefactorsfactorization_primes = frm_prime_left_ftsf_fsat_step_sourcefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_step_sourcefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_step_sourcefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_step_sourcefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_step_sourcefactorsparityeven. (mv_factor_count_step_sourcefactors) = 2 * mv_even_half_step_sourcefactorsparityeven) /\ ((a) = 2))) \/ (((exists mv_odd_half_step_sourcefactorsparityodd. (mv_factor_count_step_sourcefactors) = 2 * mv_odd_half_step_sourcefactorsparityodd + 1) /\ ((a) = 1))))))))))) -> (((~((p * n) = 0)) /\ ((((exists mv_square_prime_step_targetsquare. ((~((mv_square_prime_step_targetsquare) = 1) /\ forall pvs_left_step_targetsquareprime pvs_right_step_targetsquareprime. (mv_square_prime_step_targetsquare) = pvs_left_step_targetsquareprime * pvs_right_step_targetsquareprime -> pvs_left_step_targetsquareprime = 1 \/ pvs_right_step_targetsquareprime = 1) /\ (exists pvs_factor_step_targetsquaredivisor. (p * n) = (mv_square_prime_step_targetsquare * mv_square_prime_step_targetsquare) * pvs_factor_step_targetsquaredivisor))) /\ ((b) = 0))) \/ (((((~((p * n) = 0)) /\ (forall sfd_prime_step_targetsquarefree. (~((sfd_prime_step_targetsquarefree) = 1) /\ forall pvs_left_step_targetsquarefreedomain pvs_right_step_targetsquarefreedomain. (sfd_prime_step_targetsquarefree) = pvs_left_step_targetsquarefreedomain * pvs_right_step_targetsquarefreedomain -> pvs_left_step_targetsquarefreedomain = 1 \/ pvs_right_step_targetsquarefreedomain = 1) -> (exists pvs_le_gap_step_targetsquarefreebound. pvs_le_gap_step_targetsquarefreebound + (sfd_prime_step_targetsquarefree) = (p * n)) -> ~(exists pvs_factor_step_targetsquarefreesquare. (p * n) = (sfd_prime_step_targetsquarefree * sfd_prime_step_targetsquarefree) * pvs_factor_step_targetsquarefreesquare)))) /\ (exists mv_factor_code_step_targetfactors mv_factor_scale_step_targetfactors mv_factor_count_step_targetfactors. (((~(p * n = 0) /\ ((exists ff_u_fsat_step_targetfactorsfactorization_product ff_v_fsat_step_targetfactorsfactorization_product. ((((exists ff_h_fsat_step_targetfactorsfactorization_product_start. ff_h_fsat_step_targetfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_step_targetfactorsfactorization_product)) /\ exists ff_q_fsat_step_targetfactorsfactorization_product_start. ff_u_fsat_step_targetfactorsfactorization_product = ff_q_fsat_step_targetfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_step_targetfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_step_targetfactorsfactorization_product_terminal. ff_h_fsat_step_targetfactorsfactorization_product_terminal + S (p * n) = S ((S (mv_factor_count_step_targetfactors)) * ff_v_fsat_step_targetfactorsfactorization_product)) /\ exists ff_q_fsat_step_targetfactorsfactorization_product_terminal. ff_u_fsat_step_targetfactorsfactorization_product = ff_q_fsat_step_targetfactorsfactorization_product_terminal * S ((S (mv_factor_count_step_targetfactors)) * ff_v_fsat_step_targetfactorsfactorization_product) + (p * n))) /\ forall ff_i_fsat_step_targetfactorsfactorization_product. (exists ff_lt_fsat_step_targetfactorsfactorization_product_bound. ff_lt_fsat_step_targetfactorsfactorization_product_bound + S ff_i_fsat_step_targetfactorsfactorization_product = mv_factor_count_step_targetfactors) -> exists ff_p_fsat_step_targetfactorsfactorization_product ff_r_fsat_step_targetfactorsfactorization_product ff_s_fsat_step_targetfactorsfactorization_product. ((((exists ff_h_fsat_step_targetfactorsfactorization_product_factor. ff_h_fsat_step_targetfactorsfactorization_product_factor + S (ff_p_fsat_step_targetfactorsfactorization_product) = S ((S (ff_i_fsat_step_targetfactorsfactorization_product)) * mv_factor_scale_step_targetfactors)) /\ exists ff_q_fsat_step_targetfactorsfactorization_product_factor. mv_factor_code_step_targetfactors = ff_q_fsat_step_targetfactorsfactorization_product_factor * S ((S (ff_i_fsat_step_targetfactorsfactorization_product)) * mv_factor_scale_step_targetfactors) + (ff_p_fsat_step_targetfactorsfactorization_product))) /\ ((((exists ff_h_fsat_step_targetfactorsfactorization_product_partial. ff_h_fsat_step_targetfactorsfactorization_product_partial + S (ff_r_fsat_step_targetfactorsfactorization_product) = S ((S (ff_i_fsat_step_targetfactorsfactorization_product)) * ff_v_fsat_step_targetfactorsfactorization_product)) /\ exists ff_q_fsat_step_targetfactorsfactorization_product_partial. ff_u_fsat_step_targetfactorsfactorization_product = ff_q_fsat_step_targetfactorsfactorization_product_partial * S ((S (ff_i_fsat_step_targetfactorsfactorization_product)) * ff_v_fsat_step_targetfactorsfactorization_product) + (ff_r_fsat_step_targetfactorsfactorization_product))) /\ ((((exists ff_h_fsat_step_targetfactorsfactorization_product_successor. ff_h_fsat_step_targetfactorsfactorization_product_successor + S (ff_s_fsat_step_targetfactorsfactorization_product) = S ((S (S ff_i_fsat_step_targetfactorsfactorization_product)) * ff_v_fsat_step_targetfactorsfactorization_product)) /\ exists ff_q_fsat_step_targetfactorsfactorization_product_successor. ff_u_fsat_step_targetfactorsfactorization_product = ff_q_fsat_step_targetfactorsfactorization_product_successor * S ((S (S ff_i_fsat_step_targetfactorsfactorization_product)) * ff_v_fsat_step_targetfactorsfactorization_product) + (ff_s_fsat_step_targetfactorsfactorization_product))) /\ ff_s_fsat_step_targetfactorsfactorization_product = ff_r_fsat_step_targetfactorsfactorization_product * ff_p_fsat_step_targetfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_step_targetfactorsfactorization_primes. (exists ftsf_gap_fsat_step_targetfactorsfactorization_primes_bound. ftsf_gap_fsat_step_targetfactorsfactorization_primes_bound + S ftsf_index_fsat_step_targetfactorsfactorization_primes = (mv_factor_count_step_targetfactors)) -> exists ftsf_factor_fsat_step_targetfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_step_targetfactorsfactorization_primes_entry. ff_h_ftsf_fsat_step_targetfactorsfactorization_primes_entry + S (ftsf_factor_fsat_step_targetfactorsfactorization_primes) = S ((S (ftsf_index_fsat_step_targetfactorsfactorization_primes)) * mv_factor_scale_step_targetfactors)) /\ exists ff_q_ftsf_fsat_step_targetfactorsfactorization_primes_entry. mv_factor_code_step_targetfactors = ff_q_ftsf_fsat_step_targetfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_step_targetfactorsfactorization_primes)) * mv_factor_scale_step_targetfactors) + (ftsf_factor_fsat_step_targetfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_step_targetfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_step_targetfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_step_targetfactorsfactorization_primes_prime. ftsf_factor_fsat_step_targetfactorsfactorization_primes = frm_prime_left_ftsf_fsat_step_targetfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_step_targetfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_step_targetfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_step_targetfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_step_targetfactorsparityeven. (mv_factor_count_step_targetfactors) = 2 * mv_even_half_step_targetfactorsparityeven) /\ ((b) = 2))) \/ (((exists mv_odd_half_step_targetfactorsparityodd. (mv_factor_count_step_targetfactors) = 2 * mv_odd_half_step_targetfactorsparityodd + 1) /\ ((b) = 1))))))))))) -> (exists mps_positive_step_result mps_negative_step_result. (((((a) = 2 * (mps_positive_step_result) /\ (mps_negative_step_result) = 0) \/ exists ge_signed_half_step_resultsource. (((a) = 2 * ge_signed_half_step_resultsource + 1 /\ (mps_positive_step_result) = 0) /\ (mps_negative_step_result) = S ge_signed_half_step_resultsource))) /\ ((((b) = 2 * (mps_negative_step_result) /\ (mps_positive_step_result) = 0) \/ exists ge_signed_half_step_resulttarget. (((b) = 2 * ge_signed_half_step_resulttarget + 1 /\ (mps_negative_step_result) = 0) /\ (mps_positive_step_result) = S ge_signed_half_step_resulttarget)))))

Complete tactic proof in conservative notation

All 74 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

74 script commands · 13 reading checkpoints · 5 local claims

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

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (5)
mobius prime square value zeromobius prime factor list appendmobius squarefree fresh prime productmobius squarefree evaluationalternating signed unit successor negates
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro hp
  6. L6
    intro hfresh
  7. L7
    intro ha
  8. L8
    intro hb
02Separate the logical casesL9–13

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

  1. L9
    cases ha
  2. L10
    cases ha_right
  3. L11
    cases ha_right_left
  4. L12
    cases ha_right_left_left
  5. L13
    cases ha_right_left_left_witness
03Establish heqL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mobius prime square value zero.

  1. L14
    have heq : b = 0
  2. L15
    specialize mobius_prime_square_value_zero (p * n)
  3. L16
    specialize mobius_prime_square_value_zero (x)
  4. L17
    specialize mobius_prime_square_value_zero (b)
  5. L18
    apply mobius_prime_square_value_zero
  6. L19
    exact ha_right_left_left_witness_left
  7. L20
    specialize multiple_mul_left (x * x)
  8. L21
    specialize multiple_mul_left (n)
  9. L22
    specialize multiple_mul_left (p)
  10. L23
    apply multiple_mul_left
04Use earlier factsL24–25

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

  1. L24
    exact ha_right_left_left_witness_right
  2. L25
    exact hb
05Calculate and transport equalitiesL26–29

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

  1. L26
    rewrite ha_right_left_right
  2. L27
    rewrite ha_right_left_right
  3. L28
    rewrite heq
  4. L29
    rewrite heq
06Use earlier factsL30–30

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

  1. L30
    apply signed_negate_zero
07Separate the logical casesL31–35

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

  1. L31
    cases ha_right_right
  2. L32
    cases ha_right_right_right
  3. L33
    cases ha_right_right_right_witness
  4. L34
    cases ha_right_right_right_witness_witness
  5. L35
    cases ha_right_right_right_witness_witness_witness
08Establish hlistL36–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mobius prime factor list append.

  1. L36
    have hlist : ∃ d. ∃ e. PrimeFactorList(n · p,d,e,S x2)Definitions: PrimeFactorList(n · p,d,e,S x2)Original native command in the exact edition
  2. L37
    specialize mobius_prime_factor_list_append (n)
  3. L38
    specialize mobius_prime_factor_list_append (x)
  4. L39
    specialize mobius_prime_factor_list_append (x1)
  5. L40
    specialize mobius_prime_factor_list_append (x2)
  6. L41
    specialize mobius_prime_factor_list_append (p)
  7. L42
    apply mobius_prime_factor_list_append
  8. L43
    exact ha_right_right_right_witness_witness_witness_left
  9. L44
    exact hp
09Separate the logical casesL45–46

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

  1. L45
    cases hlist
  2. L46
    cases hlist_witness
10Establish hsfL47–53

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

  1. L47
    have hsf : Squarefree(p · n)Definitions: Squarefree(p · n)Original native command in the exact edition
  2. L48
    specialize mobius_squarefree_fresh_prime_product (p)
  3. L49
    specialize mobius_squarefree_fresh_prime_product (n)
  4. L50
    apply mobius_squarefree_fresh_prime_product
  5. L51
    exact hp
  6. L52
    exact ha_right_right_left
  7. L53
    exact hfresh
11Establish hsignL54–61

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

  1. L54
    have hsign : AlternatingSignedUnit(S x2,b)Definitions: AlternatingSignedUnit(S x2,b)Original native command in the exact edition
  2. L55
    specialize mobius_squarefree_evaluation (p * n)
  3. L56
    specialize mobius_squarefree_evaluation (x3)
  4. L57
    specialize mobius_squarefree_evaluation (x4)
  5. L58
    specialize mobius_squarefree_evaluation (S x2)
  6. L59
    specialize mobius_squarefree_evaluation (b)
  7. L60
    apply mobius_squarefree_evaluation
  8. L61
    exact hsf
12Establish heqL62–71

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

  1. L62
    have heq : n * p = p * n
  2. L63
    apply mul_comm
  3. L64
    rewrite heq at hlist_witness_witness
  4. L65
    rewrite heq at hlist_witness_witness
  5. L66
    rewrite heq at hlist_witness_witness
  6. L67
    exact hlist_witness_witness
  7. L68
    exact hb
  8. L69
    specialize alternating_signed_unit_successor_negates (x2)
  9. L70
    specialize alternating_signed_unit_successor_negates (a)
  10. L71
    specialize alternating_signed_unit_successor_negates (b)
13Use earlier factsL72–74

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

  1. L72
    apply alternating_signed_unit_successor_negates
  2. L73
    exact ha_right_right_right_witness_witness_witness_right
  3. L74
    exact hsign

Library-wide reading audit

Original defined command ledger · 74 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro a
  4. 0004intro b
  5. 0005intro hp
  6. 0006intro hfresh
  7. 0007intro ha
  8. 0008intro hb
  9. 0009cases ha
  10. 0010cases ha_right
  11. 0011cases ha_right_left
  12. 0012cases ha_right_left_left
  13. 0013cases ha_right_left_left_witness
  14. 0014have heq : b = 0
  15. 0015specialize mobius_prime_square_value_zero (p * n)
  16. 0016specialize mobius_prime_square_value_zero (x)
  17. 0017specialize mobius_prime_square_value_zero (b)
  18. 0018apply mobius_prime_square_value_zero
  19. 0019exact ha_right_left_left_witness_left
  20. 0020specialize multiple_mul_left (x * x)
  21. 0021specialize multiple_mul_left (n)
  22. 0022specialize multiple_mul_left (p)
  23. 0023apply multiple_mul_left
  24. 0024exact ha_right_left_left_witness_right
  25. 0025exact hb
  26. 0026rewrite ha_right_left_right
  27. 0027rewrite ha_right_left_right
  28. 0028rewrite heq
  29. 0029rewrite heq
  30. 0030apply signed_negate_zero
  31. 0031cases ha_right_right
  32. 0032cases ha_right_right_right
  33. 0033cases ha_right_right_right_witness
  34. 0034cases ha_right_right_right_witness_witness
  35. 0035cases ha_right_right_right_witness_witness_witness
  36. 0036have hlist : ∃ d. ∃ e. PrimeFactorList(n · p,d,e,S x2)
  37. 0037specialize mobius_prime_factor_list_append (n)
  38. 0038specialize mobius_prime_factor_list_append (x)
  39. 0039specialize mobius_prime_factor_list_append (x1)
  40. 0040specialize mobius_prime_factor_list_append (x2)
  41. 0041specialize mobius_prime_factor_list_append (p)
  42. 0042apply mobius_prime_factor_list_append
  43. 0043exact ha_right_right_right_witness_witness_witness_left
  44. 0044exact hp
  45. 0045cases hlist
  46. 0046cases hlist_witness
  47. 0047have hsf : Squarefree(p · n)
  48. 0048specialize mobius_squarefree_fresh_prime_product (p)
  49. 0049specialize mobius_squarefree_fresh_prime_product (n)
  50. 0050apply mobius_squarefree_fresh_prime_product
  51. 0051exact hp
  52. 0052exact ha_right_right_left
  53. 0053exact hfresh
  54. 0054have hsign : AlternatingSignedUnit(S x2,b)
  55. 0055specialize mobius_squarefree_evaluation (p * n)
  56. 0056specialize mobius_squarefree_evaluation (x3)
  57. 0057specialize mobius_squarefree_evaluation (x4)
  58. 0058specialize mobius_squarefree_evaluation (S x2)
  59. 0059specialize mobius_squarefree_evaluation (b)
  60. 0060apply mobius_squarefree_evaluation
  61. 0061exact hsf
  62. 0062have heq : n * p = p * n
  63. 0063apply mul_comm
  64. 0064rewrite heq at hlist_witness_witness
  65. 0065rewrite heq at hlist_witness_witness
  66. 0066rewrite heq at hlist_witness_witness
  67. 0067exact hlist_witness_witness
  68. 0068exact hb
  69. 0069specialize alternating_signed_unit_successor_negates (x2)
  70. 0070specialize alternating_signed_unit_successor_negates (a)
  71. 0071specialize alternating_signed_unit_successor_negates (b)
  72. 0072apply alternating_signed_unit_successor_negates
  73. 0073exact ha_right_right_right_witness_witness_witness_right
  74. 0074exact hsign