MC0010

mobius_prime_factor_toggle_negates

Actual prime toggling negates independently defined Möbius values, including fixed nonsquarefree values, which are proved to be zero.

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.

The input n is positive. Signed code 2 denotes +1, so the actual sum is +1 at n=1 and zero for n>1. The positive-values result permits arbitrary F(0), which the divisor mask excludes. Prime-square multiples contribute zero. Full G007 inversion is established in its separate family.

Exact theorem in conservative defined notation

∀ p. ∀ d. ∀ e. ∀ a. ∀ b. Prime(p) → PrimeFactorToggle(p,d,e) → Mobius(d,a) → Mobius(e,b) → SignedNegate(a,b)

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

Definition DAG

SignedNegate(a,b) · 1Mobius(n,z) · 2PrimeFactorToggle(p,d,e) · 1Prime(p) · 1

Actual proof prerequisites

mobius_fresh_prime_negates · checked external prerequisitesigned_negate_symmetric · checked external prerequisitemobius_prime_square_value_zero · checked external prerequisitesigned_negate_zero · checked external prerequisite
Original expanded first-order statement 
forall p d e a b. (~((p) = 1) /\ forall pvs_left_value_prime pvs_right_value_prime. (p) = pvs_left_value_prime * pvs_right_value_prime -> pvs_left_value_prime = 1 \/ pvs_right_value_prime = 1) -> ((((~(exists pvs_factor_value_togglefresh_input. (d) = (p) * pvs_factor_value_togglefresh_input)) /\ ((e)=(p)*(d)))) \/ (((((d)=(p)*(e)) /\ (~(exists pvs_factor_value_togglefresh_output. (e) = (p) * pvs_factor_value_togglefresh_output)))) \/ (((exists pvs_factor_value_togglesquare. (d) = ((p)*(p)) * pvs_factor_value_togglesquare) /\ ((e)=(d)))))) -> (((~((d) = 0)) /\ ((((exists mv_square_prime_value_sourcesquare. ((~((mv_square_prime_value_sourcesquare) = 1) /\ forall pvs_left_value_sourcesquareprime pvs_right_value_sourcesquareprime. (mv_square_prime_value_sourcesquare) = pvs_left_value_sourcesquareprime * pvs_right_value_sourcesquareprime -> pvs_left_value_sourcesquareprime = 1 \/ pvs_right_value_sourcesquareprime = 1) /\ (exists pvs_factor_value_sourcesquaredivisor. (d) = (mv_square_prime_value_sourcesquare * mv_square_prime_value_sourcesquare) * pvs_factor_value_sourcesquaredivisor))) /\ ((a) = 0))) \/ (((((~((d) = 0)) /\ (forall sfd_prime_value_sourcesquarefree. (~((sfd_prime_value_sourcesquarefree) = 1) /\ forall pvs_left_value_sourcesquarefreedomain pvs_right_value_sourcesquarefreedomain. (sfd_prime_value_sourcesquarefree) = pvs_left_value_sourcesquarefreedomain * pvs_right_value_sourcesquarefreedomain -> pvs_left_value_sourcesquarefreedomain = 1 \/ pvs_right_value_sourcesquarefreedomain = 1) -> (exists pvs_le_gap_value_sourcesquarefreebound. pvs_le_gap_value_sourcesquarefreebound + (sfd_prime_value_sourcesquarefree) = (d)) -> ~(exists pvs_factor_value_sourcesquarefreesquare. (d) = (sfd_prime_value_sourcesquarefree * sfd_prime_value_sourcesquarefree) * pvs_factor_value_sourcesquarefreesquare)))) /\ (exists mv_factor_code_value_sourcefactors mv_factor_scale_value_sourcefactors mv_factor_count_value_sourcefactors. (((~(d = 0) /\ ((exists ff_u_fsat_value_sourcefactorsfactorization_product ff_v_fsat_value_sourcefactorsfactorization_product. ((((exists ff_h_fsat_value_sourcefactorsfactorization_product_start. ff_h_fsat_value_sourcefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_value_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_value_sourcefactorsfactorization_product_start. ff_u_fsat_value_sourcefactorsfactorization_product = ff_q_fsat_value_sourcefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_value_sourcefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_value_sourcefactorsfactorization_product_terminal. ff_h_fsat_value_sourcefactorsfactorization_product_terminal + S (d) = S ((S (mv_factor_count_value_sourcefactors)) * ff_v_fsat_value_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_value_sourcefactorsfactorization_product_terminal. ff_u_fsat_value_sourcefactorsfactorization_product = ff_q_fsat_value_sourcefactorsfactorization_product_terminal * S ((S (mv_factor_count_value_sourcefactors)) * ff_v_fsat_value_sourcefactorsfactorization_product) + (d))) /\ forall ff_i_fsat_value_sourcefactorsfactorization_product. (exists ff_lt_fsat_value_sourcefactorsfactorization_product_bound. ff_lt_fsat_value_sourcefactorsfactorization_product_bound + S ff_i_fsat_value_sourcefactorsfactorization_product = mv_factor_count_value_sourcefactors) -> exists ff_p_fsat_value_sourcefactorsfactorization_product ff_r_fsat_value_sourcefactorsfactorization_product ff_s_fsat_value_sourcefactorsfactorization_product. ((((exists ff_h_fsat_value_sourcefactorsfactorization_product_factor. ff_h_fsat_value_sourcefactorsfactorization_product_factor + S (ff_p_fsat_value_sourcefactorsfactorization_product) = S ((S (ff_i_fsat_value_sourcefactorsfactorization_product)) * mv_factor_scale_value_sourcefactors)) /\ exists ff_q_fsat_value_sourcefactorsfactorization_product_factor. mv_factor_code_value_sourcefactors = ff_q_fsat_value_sourcefactorsfactorization_product_factor * S ((S (ff_i_fsat_value_sourcefactorsfactorization_product)) * mv_factor_scale_value_sourcefactors) + (ff_p_fsat_value_sourcefactorsfactorization_product))) /\ ((((exists ff_h_fsat_value_sourcefactorsfactorization_product_partial. ff_h_fsat_value_sourcefactorsfactorization_product_partial + S (ff_r_fsat_value_sourcefactorsfactorization_product) = S ((S (ff_i_fsat_value_sourcefactorsfactorization_product)) * ff_v_fsat_value_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_value_sourcefactorsfactorization_product_partial. ff_u_fsat_value_sourcefactorsfactorization_product = ff_q_fsat_value_sourcefactorsfactorization_product_partial * S ((S (ff_i_fsat_value_sourcefactorsfactorization_product)) * ff_v_fsat_value_sourcefactorsfactorization_product) + (ff_r_fsat_value_sourcefactorsfactorization_product))) /\ ((((exists ff_h_fsat_value_sourcefactorsfactorization_product_successor. ff_h_fsat_value_sourcefactorsfactorization_product_successor + S (ff_s_fsat_value_sourcefactorsfactorization_product) = S ((S (S ff_i_fsat_value_sourcefactorsfactorization_product)) * ff_v_fsat_value_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_value_sourcefactorsfactorization_product_successor. ff_u_fsat_value_sourcefactorsfactorization_product = ff_q_fsat_value_sourcefactorsfactorization_product_successor * S ((S (S ff_i_fsat_value_sourcefactorsfactorization_product)) * ff_v_fsat_value_sourcefactorsfactorization_product) + (ff_s_fsat_value_sourcefactorsfactorization_product))) /\ ff_s_fsat_value_sourcefactorsfactorization_product = ff_r_fsat_value_sourcefactorsfactorization_product * ff_p_fsat_value_sourcefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_value_sourcefactorsfactorization_primes. (exists ftsf_gap_fsat_value_sourcefactorsfactorization_primes_bound. ftsf_gap_fsat_value_sourcefactorsfactorization_primes_bound + S ftsf_index_fsat_value_sourcefactorsfactorization_primes = (mv_factor_count_value_sourcefactors)) -> exists ftsf_factor_fsat_value_sourcefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_value_sourcefactorsfactorization_primes_entry. ff_h_ftsf_fsat_value_sourcefactorsfactorization_primes_entry + S (ftsf_factor_fsat_value_sourcefactorsfactorization_primes) = S ((S (ftsf_index_fsat_value_sourcefactorsfactorization_primes)) * mv_factor_scale_value_sourcefactors)) /\ exists ff_q_ftsf_fsat_value_sourcefactorsfactorization_primes_entry. mv_factor_code_value_sourcefactors = ff_q_ftsf_fsat_value_sourcefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_value_sourcefactorsfactorization_primes)) * mv_factor_scale_value_sourcefactors) + (ftsf_factor_fsat_value_sourcefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_value_sourcefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_value_sourcefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_value_sourcefactorsfactorization_primes_prime. ftsf_factor_fsat_value_sourcefactorsfactorization_primes = frm_prime_left_ftsf_fsat_value_sourcefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_value_sourcefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_value_sourcefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_value_sourcefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_value_sourcefactorsparityeven. (mv_factor_count_value_sourcefactors) = 2 * mv_even_half_value_sourcefactorsparityeven) /\ ((a) = 2))) \/ (((exists mv_odd_half_value_sourcefactorsparityodd. (mv_factor_count_value_sourcefactors) = 2 * mv_odd_half_value_sourcefactorsparityodd + 1) /\ ((a) = 1))))))))))) -> (((~((e) = 0)) /\ ((((exists mv_square_prime_value_targetsquare. ((~((mv_square_prime_value_targetsquare) = 1) /\ forall pvs_left_value_targetsquareprime pvs_right_value_targetsquareprime. (mv_square_prime_value_targetsquare) = pvs_left_value_targetsquareprime * pvs_right_value_targetsquareprime -> pvs_left_value_targetsquareprime = 1 \/ pvs_right_value_targetsquareprime = 1) /\ (exists pvs_factor_value_targetsquaredivisor. (e) = (mv_square_prime_value_targetsquare * mv_square_prime_value_targetsquare) * pvs_factor_value_targetsquaredivisor))) /\ ((b) = 0))) \/ (((((~((e) = 0)) /\ (forall sfd_prime_value_targetsquarefree. (~((sfd_prime_value_targetsquarefree) = 1) /\ forall pvs_left_value_targetsquarefreedomain pvs_right_value_targetsquarefreedomain. (sfd_prime_value_targetsquarefree) = pvs_left_value_targetsquarefreedomain * pvs_right_value_targetsquarefreedomain -> pvs_left_value_targetsquarefreedomain = 1 \/ pvs_right_value_targetsquarefreedomain = 1) -> (exists pvs_le_gap_value_targetsquarefreebound. pvs_le_gap_value_targetsquarefreebound + (sfd_prime_value_targetsquarefree) = (e)) -> ~(exists pvs_factor_value_targetsquarefreesquare. (e) = (sfd_prime_value_targetsquarefree * sfd_prime_value_targetsquarefree) * pvs_factor_value_targetsquarefreesquare)))) /\ (exists mv_factor_code_value_targetfactors mv_factor_scale_value_targetfactors mv_factor_count_value_targetfactors. (((~(e = 0) /\ ((exists ff_u_fsat_value_targetfactorsfactorization_product ff_v_fsat_value_targetfactorsfactorization_product. ((((exists ff_h_fsat_value_targetfactorsfactorization_product_start. ff_h_fsat_value_targetfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_value_targetfactorsfactorization_product)) /\ exists ff_q_fsat_value_targetfactorsfactorization_product_start. ff_u_fsat_value_targetfactorsfactorization_product = ff_q_fsat_value_targetfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_value_targetfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_value_targetfactorsfactorization_product_terminal. ff_h_fsat_value_targetfactorsfactorization_product_terminal + S (e) = S ((S (mv_factor_count_value_targetfactors)) * ff_v_fsat_value_targetfactorsfactorization_product)) /\ exists ff_q_fsat_value_targetfactorsfactorization_product_terminal. ff_u_fsat_value_targetfactorsfactorization_product = ff_q_fsat_value_targetfactorsfactorization_product_terminal * S ((S (mv_factor_count_value_targetfactors)) * ff_v_fsat_value_targetfactorsfactorization_product) + (e))) /\ forall ff_i_fsat_value_targetfactorsfactorization_product. (exists ff_lt_fsat_value_targetfactorsfactorization_product_bound. ff_lt_fsat_value_targetfactorsfactorization_product_bound + S ff_i_fsat_value_targetfactorsfactorization_product = mv_factor_count_value_targetfactors) -> exists ff_p_fsat_value_targetfactorsfactorization_product ff_r_fsat_value_targetfactorsfactorization_product ff_s_fsat_value_targetfactorsfactorization_product. ((((exists ff_h_fsat_value_targetfactorsfactorization_product_factor. ff_h_fsat_value_targetfactorsfactorization_product_factor + S (ff_p_fsat_value_targetfactorsfactorization_product) = S ((S (ff_i_fsat_value_targetfactorsfactorization_product)) * mv_factor_scale_value_targetfactors)) /\ exists ff_q_fsat_value_targetfactorsfactorization_product_factor. mv_factor_code_value_targetfactors = ff_q_fsat_value_targetfactorsfactorization_product_factor * S ((S (ff_i_fsat_value_targetfactorsfactorization_product)) * mv_factor_scale_value_targetfactors) + (ff_p_fsat_value_targetfactorsfactorization_product))) /\ ((((exists ff_h_fsat_value_targetfactorsfactorization_product_partial. ff_h_fsat_value_targetfactorsfactorization_product_partial + S (ff_r_fsat_value_targetfactorsfactorization_product) = S ((S (ff_i_fsat_value_targetfactorsfactorization_product)) * ff_v_fsat_value_targetfactorsfactorization_product)) /\ exists ff_q_fsat_value_targetfactorsfactorization_product_partial. ff_u_fsat_value_targetfactorsfactorization_product = ff_q_fsat_value_targetfactorsfactorization_product_partial * S ((S (ff_i_fsat_value_targetfactorsfactorization_product)) * ff_v_fsat_value_targetfactorsfactorization_product) + (ff_r_fsat_value_targetfactorsfactorization_product))) /\ ((((exists ff_h_fsat_value_targetfactorsfactorization_product_successor. ff_h_fsat_value_targetfactorsfactorization_product_successor + S (ff_s_fsat_value_targetfactorsfactorization_product) = S ((S (S ff_i_fsat_value_targetfactorsfactorization_product)) * ff_v_fsat_value_targetfactorsfactorization_product)) /\ exists ff_q_fsat_value_targetfactorsfactorization_product_successor. ff_u_fsat_value_targetfactorsfactorization_product = ff_q_fsat_value_targetfactorsfactorization_product_successor * S ((S (S ff_i_fsat_value_targetfactorsfactorization_product)) * ff_v_fsat_value_targetfactorsfactorization_product) + (ff_s_fsat_value_targetfactorsfactorization_product))) /\ ff_s_fsat_value_targetfactorsfactorization_product = ff_r_fsat_value_targetfactorsfactorization_product * ff_p_fsat_value_targetfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_value_targetfactorsfactorization_primes. (exists ftsf_gap_fsat_value_targetfactorsfactorization_primes_bound. ftsf_gap_fsat_value_targetfactorsfactorization_primes_bound + S ftsf_index_fsat_value_targetfactorsfactorization_primes = (mv_factor_count_value_targetfactors)) -> exists ftsf_factor_fsat_value_targetfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_value_targetfactorsfactorization_primes_entry. ff_h_ftsf_fsat_value_targetfactorsfactorization_primes_entry + S (ftsf_factor_fsat_value_targetfactorsfactorization_primes) = S ((S (ftsf_index_fsat_value_targetfactorsfactorization_primes)) * mv_factor_scale_value_targetfactors)) /\ exists ff_q_ftsf_fsat_value_targetfactorsfactorization_primes_entry. mv_factor_code_value_targetfactors = ff_q_ftsf_fsat_value_targetfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_value_targetfactorsfactorization_primes)) * mv_factor_scale_value_targetfactors) + (ftsf_factor_fsat_value_targetfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_value_targetfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_value_targetfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_value_targetfactorsfactorization_primes_prime. ftsf_factor_fsat_value_targetfactorsfactorization_primes = frm_prime_left_ftsf_fsat_value_targetfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_value_targetfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_value_targetfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_value_targetfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_value_targetfactorsparityeven. (mv_factor_count_value_targetfactors) = 2 * mv_even_half_value_targetfactorsparityeven) /\ ((b) = 2))) \/ (((exists mv_odd_half_value_targetfactorsparityodd. (mv_factor_count_value_targetfactors) = 2 * mv_odd_half_value_targetfactorsparityodd + 1) /\ ((b) = 1))))))))))) -> (exists mps_positive_value_negation mps_negative_value_negation. (((((a) = 2 * (mps_positive_value_negation) /\ (mps_negative_value_negation) = 0) \/ exists ge_signed_half_value_negationsource. (((a) = 2 * ge_signed_half_value_negationsource + 1 /\ (mps_positive_value_negation) = 0) /\ (mps_negative_value_negation) = S ge_signed_half_value_negationsource))) /\ ((((b) = 2 * (mps_negative_value_negation) /\ (mps_positive_value_negation) = 0) \/ exists ge_signed_half_value_negationtarget. (((b) = 2 * ge_signed_half_value_negationtarget + 1 /\ (mps_negative_value_negation) = 0) /\ (mps_positive_value_negation) = S ge_signed_half_value_negationtarget)))))

Complete tactic proof in conservative notation

All 80 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

80 script commands · 15 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.

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

01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro d
  3. L3
    intro e
  4. L4
    intro a
  5. L5
    intro b
  6. L6
    intro hp
  7. L7
    intro ht
  8. L8
    intro ha
  9. L9
    intro hb
02Separate the logical casesL10–11

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

  1. L10
    cases ht
  2. L11
    cases ht_left
03Calculate and transport equalitiesL12–19

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

  1. L12
    rewrite ht_left_right at hb
  2. L13
    rewrite ht_left_right at hb
  3. L14
    rewrite ht_left_right at hb
  4. L15
    rewrite ht_left_right at hb
  5. L16
    rewrite ht_left_right at hb
  6. L17
    rewrite ht_left_right at hb
  7. L18
    rewrite ht_left_right at hb
  8. L19
    rewrite ht_left_right at hb
04Use earlier factsL20–28

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

  1. L20
    specialize mobius_fresh_prime_negates (p)
  2. L21
    specialize mobius_fresh_prime_negates (d)
  3. L22
    specialize mobius_fresh_prime_negates (a)
  4. L23
    specialize mobius_fresh_prime_negates (b)
  5. L24
    apply mobius_fresh_prime_negates
  6. L25
    exact hp
  7. L26
    exact ht_left_left
  8. L27
    exact ha
  9. L28
    exact hb
05Separate the logical casesL29–30

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

  1. L29
    cases ht_right
  2. L30
    cases ht_right_left
06Calculate and transport equalitiesL31–38

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

  1. L31
    rewrite ht_right_left_left at ha
  2. L32
    rewrite ht_right_left_left at ha
  3. L33
    rewrite ht_right_left_left at ha
  4. L34
    rewrite ht_right_left_left at ha
  5. L35
    rewrite ht_right_left_left at ha
  6. L36
    rewrite ht_right_left_left at ha
  7. L37
    rewrite ht_right_left_left at ha
  8. L38
    rewrite ht_right_left_left at ha
07Use earlier factsL39–48

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

  1. L39
    specialize signed_negate_symmetric (b)
  2. L40
    specialize signed_negate_symmetric (a)
  3. L41
    apply signed_negate_symmetric
  4. L42
    specialize mobius_fresh_prime_negates (p)
  5. L43
    specialize mobius_fresh_prime_negates (e)
  6. L44
    specialize mobius_fresh_prime_negates (b)
  7. L45
    specialize mobius_fresh_prime_negates (a)
  8. L46
    apply mobius_fresh_prime_negates
  9. L47
    exact hp
  10. L48
    exact ht_right_left_right
08Use earlier factsL49–50

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

  1. L49
    exact hb
  2. L50
    exact ha
09Separate the logical casesL51–51

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

  1. L51
    cases ht_right_right
10Establish hzeroaL52–59

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

  1. L52
    have hzeroa : a=0
  2. L53
    specialize mobius_prime_square_value_zero (d)
  3. L54
    specialize mobius_prime_square_value_zero (p)
  4. L55
    specialize mobius_prime_square_value_zero (a)
  5. L56
    apply mobius_prime_square_value_zero
  6. L57
    exact hp
  7. L58
    exact ht_right_right_left
  8. L59
    exact ha
11Establish hzerobL60–69

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

  1. L60
    have hzerob : b=0
  2. L61
    specialize mobius_prime_square_value_zero (d)
  3. L62
    specialize mobius_prime_square_value_zero (p)
  4. L63
    specialize mobius_prime_square_value_zero (b)
  5. L64
    apply mobius_prime_square_value_zero
  6. L65
    exact hp
  7. L66
    exact ht_right_right_left
  8. L67
    rewrite ht_right_right_right at hb
  9. L68
    rewrite ht_right_right_right at hb
  10. L69
    rewrite ht_right_right_right at hb
12Calculate and transport equalitiesL70–74

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

  1. L70
    rewrite ht_right_right_right at hb
  2. L71
    rewrite ht_right_right_right at hb
  3. L72
    rewrite ht_right_right_right at hb
  4. L73
    rewrite ht_right_right_right at hb
  5. L74
    rewrite ht_right_right_right at hb
13Use earlier factsL75–75

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

  1. L75
    exact hb
14Calculate and transport equalitiesL76–79

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

  1. L76
    rewrite hzeroa
  2. L77
    rewrite hzeroa
  3. L78
    rewrite hzerob
  4. L79
    rewrite hzerob
15Use earlier factsL80–80

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

  1. L80
    apply signed_negate_zero

Library-wide reading audit

Original defined command ledger · 80 lines
  1. 0001intro p
  2. 0002intro d
  3. 0003intro e
  4. 0004intro a
  5. 0005intro b
  6. 0006intro hp
  7. 0007intro ht
  8. 0008intro ha
  9. 0009intro hb
  10. 0010cases ht
  11. 0011cases ht_left
  12. 0012rewrite ht_left_right at hb
  13. 0013rewrite ht_left_right at hb
  14. 0014rewrite ht_left_right at hb
  15. 0015rewrite ht_left_right at hb
  16. 0016rewrite ht_left_right at hb
  17. 0017rewrite ht_left_right at hb
  18. 0018rewrite ht_left_right at hb
  19. 0019rewrite ht_left_right at hb
  20. 0020specialize mobius_fresh_prime_negates (p)
  21. 0021specialize mobius_fresh_prime_negates (d)
  22. 0022specialize mobius_fresh_prime_negates (a)
  23. 0023specialize mobius_fresh_prime_negates (b)
  24. 0024apply mobius_fresh_prime_negates
  25. 0025exact hp
  26. 0026exact ht_left_left
  27. 0027exact ha
  28. 0028exact hb
  29. 0029cases ht_right
  30. 0030cases ht_right_left
  31. 0031rewrite ht_right_left_left at ha
  32. 0032rewrite ht_right_left_left at ha
  33. 0033rewrite ht_right_left_left at ha
  34. 0034rewrite ht_right_left_left at ha
  35. 0035rewrite ht_right_left_left at ha
  36. 0036rewrite ht_right_left_left at ha
  37. 0037rewrite ht_right_left_left at ha
  38. 0038rewrite ht_right_left_left at ha
  39. 0039specialize signed_negate_symmetric (b)
  40. 0040specialize signed_negate_symmetric (a)
  41. 0041apply signed_negate_symmetric
  42. 0042specialize mobius_fresh_prime_negates (p)
  43. 0043specialize mobius_fresh_prime_negates (e)
  44. 0044specialize mobius_fresh_prime_negates (b)
  45. 0045specialize mobius_fresh_prime_negates (a)
  46. 0046apply mobius_fresh_prime_negates
  47. 0047exact hp
  48. 0048exact ht_right_left_right
  49. 0049exact hb
  50. 0050exact ha
  51. 0051cases ht_right_right
  52. 0052have hzeroa : a=0
  53. 0053specialize mobius_prime_square_value_zero (d)
  54. 0054specialize mobius_prime_square_value_zero (p)
  55. 0055specialize mobius_prime_square_value_zero (a)
  56. 0056apply mobius_prime_square_value_zero
  57. 0057exact hp
  58. 0058exact ht_right_right_left
  59. 0059exact ha
  60. 0060have hzerob : b=0
  61. 0061specialize mobius_prime_square_value_zero (d)
  62. 0062specialize mobius_prime_square_value_zero (p)
  63. 0063specialize mobius_prime_square_value_zero (b)
  64. 0064apply mobius_prime_square_value_zero
  65. 0065exact hp
  66. 0066exact ht_right_right_left
  67. 0067rewrite ht_right_right_right at hb
  68. 0068rewrite ht_right_right_right at hb
  69. 0069rewrite ht_right_right_right at hb
  70. 0070rewrite ht_right_right_right at hb
  71. 0071rewrite ht_right_right_right at hb
  72. 0072rewrite ht_right_right_right at hb
  73. 0073rewrite ht_right_right_right at hb
  74. 0074rewrite ht_right_right_right at hb
  75. 0075exact hb
  76. 0076rewrite hzeroa
  77. 0077rewrite hzeroa
  78. 0078rewrite hzerob
  79. 0079rewrite hzerob
  80. 0080apply signed_negate_zero