DC001F

dirichlet_convolution_entry_complement

Actual divisor complementation swaps the two signed factors, while fixed zero/nondivisor positions remain genuinely 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.

Each retained summand has a witnessed n=d*q and actual signed multiplication. Zero and nondivisors contribute zero. Input and output values at zero are unrestricted; uniqueness is for positive represented values. The separate inverse family proves the unit-at-one criterion. Full G009 multiplicative-function closure is now admitted in the separate Alpha-v32 multiplicative-convolution family.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ n. ∀ d. ∀ q. ∀ z. ¬n = 0 → DivisorComplement(n,d,q) → DirichletEntry(F,G,n,q,z) → DirichletEntry(G,F,n,d,z)

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

Definition DAG

DivisorComplement(n,d,q) · 1DirichletEntry(F,G,n,d,z) · 2

Actual proof prerequisites

factor_nonzero_right · checked external prerequisitemul_left_cancel_nonzero · checked external prerequisitemul_comm · checked external prerequisitedirichlet_convolution_entry_from_quotientsigned_mul_commutative · checked external prerequisitedirichlet_convolution_entry_omitted_value
Original expanded first-order statement 
forall F G n d q z. ~(n=0) -> ((((~((d)=0)) /\ ((n)=(d)*(q)))) \/ ((((d)=0 \/ ~(exists pvs_factor_swap_complementnondivisor. (n) = (d) * pvs_factor_swap_complementnondivisor)) /\ ((q)=(d))))) -> ((((~((q)=0)) /\ (exists dc_quotient_swap_source dc_left_swap_source dc_right_swap_source. (((n)=(q)*dc_quotient_swap_source) /\ (((exists dst_positive_code_swap_sourceleft dst_positive_scale_swap_sourceleft dst_negative_code_swap_sourceleft dst_negative_scale_swap_sourceleft dst_positive_swap_sourceleft dst_negative_swap_sourceleft. (((F) = (((((dst_positive_code_swap_sourceleft) + (dst_positive_scale_swap_sourceleft)) * S ((dst_positive_code_swap_sourceleft) + (dst_positive_scale_swap_sourceleft)) + ((dst_positive_scale_swap_sourceleft) + (dst_positive_scale_swap_sourceleft))) + (((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) * S ((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) + ((dst_negative_scale_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)))) * S ((((dst_positive_code_swap_sourceleft) + (dst_positive_scale_swap_sourceleft)) * S ((dst_positive_code_swap_sourceleft) + (dst_positive_scale_swap_sourceleft)) + ((dst_positive_scale_swap_sourceleft) + (dst_positive_scale_swap_sourceleft))) + (((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) * S ((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) + ((dst_negative_scale_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)))) + ((((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) * S ((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) + ((dst_negative_scale_swap_sourceleft) + (dst_negative_scale_swap_sourceleft))) + (((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) * S ((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) + ((dst_negative_scale_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)))))) /\ (((((exists ff_h_pvs_swap_sourceleftpositive. ff_h_pvs_swap_sourceleftpositive + S (dst_positive_swap_sourceleft) = S ((S (q)) * dst_positive_scale_swap_sourceleft)) /\ exists ff_q_pvs_swap_sourceleftpositive. dst_positive_code_swap_sourceleft = ff_q_pvs_swap_sourceleftpositive * S ((S (q)) * dst_positive_scale_swap_sourceleft) + (dst_positive_swap_sourceleft))) /\ (((((exists ff_h_pvs_swap_sourceleftnegative. ff_h_pvs_swap_sourceleftnegative + S (dst_negative_swap_sourceleft) = S ((S (q)) * dst_negative_scale_swap_sourceleft)) /\ exists ff_q_pvs_swap_sourceleftnegative. dst_negative_code_swap_sourceleft = ff_q_pvs_swap_sourceleftnegative * S ((S (q)) * dst_negative_scale_swap_sourceleft) + (dst_negative_swap_sourceleft))) /\ (exists ge_balance_positive_swap_sourceleftvalue ge_balance_negative_swap_sourceleftvalue. (((((dc_left_swap_source) = 2 * (ge_balance_positive_swap_sourceleftvalue) /\ (ge_balance_negative_swap_sourceleftvalue) = 0) \/ exists ge_signed_half_swap_sourceleftvaluedecode. (((dc_left_swap_source) = 2 * ge_signed_half_swap_sourceleftvaluedecode + 1 /\ (ge_balance_positive_swap_sourceleftvalue) = 0) /\ (ge_balance_negative_swap_sourceleftvalue) = S ge_signed_half_swap_sourceleftvaluedecode))) /\ ((dst_positive_swap_sourceleft) + ge_balance_negative_swap_sourceleftvalue = (dst_negative_swap_sourceleft) + ge_balance_positive_swap_sourceleftvalue))))))))) /\ (((exists dst_positive_code_swap_sourceright dst_positive_scale_swap_sourceright dst_negative_code_swap_sourceright dst_negative_scale_swap_sourceright dst_positive_swap_sourceright dst_negative_swap_sourceright. (((G) = (((((dst_positive_code_swap_sourceright) + (dst_positive_scale_swap_sourceright)) * S ((dst_positive_code_swap_sourceright) + (dst_positive_scale_swap_sourceright)) + ((dst_positive_scale_swap_sourceright) + (dst_positive_scale_swap_sourceright))) + (((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) * S ((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) + ((dst_negative_scale_swap_sourceright) + (dst_negative_scale_swap_sourceright)))) * S ((((dst_positive_code_swap_sourceright) + (dst_positive_scale_swap_sourceright)) * S ((dst_positive_code_swap_sourceright) + (dst_positive_scale_swap_sourceright)) + ((dst_positive_scale_swap_sourceright) + (dst_positive_scale_swap_sourceright))) + (((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) * S ((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) + ((dst_negative_scale_swap_sourceright) + (dst_negative_scale_swap_sourceright)))) + ((((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) * S ((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) + ((dst_negative_scale_swap_sourceright) + (dst_negative_scale_swap_sourceright))) + (((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) * S ((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) + ((dst_negative_scale_swap_sourceright) + (dst_negative_scale_swap_sourceright)))))) /\ (((((exists ff_h_pvs_swap_sourcerightpositive. ff_h_pvs_swap_sourcerightpositive + S (dst_positive_swap_sourceright) = S ((S (dc_quotient_swap_source)) * dst_positive_scale_swap_sourceright)) /\ exists ff_q_pvs_swap_sourcerightpositive. dst_positive_code_swap_sourceright = ff_q_pvs_swap_sourcerightpositive * S ((S (dc_quotient_swap_source)) * dst_positive_scale_swap_sourceright) + (dst_positive_swap_sourceright))) /\ (((((exists ff_h_pvs_swap_sourcerightnegative. ff_h_pvs_swap_sourcerightnegative + S (dst_negative_swap_sourceright) = S ((S (dc_quotient_swap_source)) * dst_negative_scale_swap_sourceright)) /\ exists ff_q_pvs_swap_sourcerightnegative. dst_negative_code_swap_sourceright = ff_q_pvs_swap_sourcerightnegative * S ((S (dc_quotient_swap_source)) * dst_negative_scale_swap_sourceright) + (dst_negative_swap_sourceright))) /\ (exists ge_balance_positive_swap_sourcerightvalue ge_balance_negative_swap_sourcerightvalue. (((((dc_right_swap_source) = 2 * (ge_balance_positive_swap_sourcerightvalue) /\ (ge_balance_negative_swap_sourcerightvalue) = 0) \/ exists ge_signed_half_swap_sourcerightvaluedecode. (((dc_right_swap_source) = 2 * ge_signed_half_swap_sourcerightvaluedecode + 1 /\ (ge_balance_positive_swap_sourcerightvalue) = 0) /\ (ge_balance_negative_swap_sourcerightvalue) = S ge_signed_half_swap_sourcerightvaluedecode))) /\ ((dst_positive_swap_sourceright) + ge_balance_negative_swap_sourcerightvalue = (dst_negative_swap_sourceright) + ge_balance_positive_swap_sourcerightvalue))))))))) /\ (exists sto_ap_swap_sourceproduct sto_an_swap_sourceproduct sto_bp_swap_sourceproduct sto_bn_swap_sourceproduct sto_cp_swap_sourceproduct sto_cn_swap_sourceproduct. (((((dc_left_swap_source) = 2 * (sto_ap_swap_sourceproduct) /\ (sto_an_swap_sourceproduct) = 0) \/ exists ge_signed_half_swap_sourceproductleft. (((dc_left_swap_source) = 2 * ge_signed_half_swap_sourceproductleft + 1 /\ (sto_ap_swap_sourceproduct) = 0) /\ (sto_an_swap_sourceproduct) = S ge_signed_half_swap_sourceproductleft))) /\ ((((((dc_right_swap_source) = 2 * (sto_bp_swap_sourceproduct) /\ (sto_bn_swap_sourceproduct) = 0) \/ exists ge_signed_half_swap_sourceproductright. (((dc_right_swap_source) = 2 * ge_signed_half_swap_sourceproductright + 1 /\ (sto_bp_swap_sourceproduct) = 0) /\ (sto_bn_swap_sourceproduct) = S ge_signed_half_swap_sourceproductright))) /\ ((((((z) = 2 * (sto_cp_swap_sourceproduct) /\ (sto_cn_swap_sourceproduct) = 0) \/ exists ge_signed_half_swap_sourceproductoutput. (((z) = 2 * ge_signed_half_swap_sourceproductoutput + 1 /\ (sto_cp_swap_sourceproduct) = 0) /\ (sto_cn_swap_sourceproduct) = S ge_signed_half_swap_sourceproductoutput))) /\ ((sto_ap_swap_sourceproduct * sto_bp_swap_sourceproduct + sto_an_swap_sourceproduct * sto_bn_swap_sourceproduct) + sto_cn_swap_sourceproduct = (sto_ap_swap_sourceproduct * sto_bn_swap_sourceproduct + sto_an_swap_sourceproduct * sto_bp_swap_sourceproduct) + sto_cp_swap_sourceproduct))))))))))))))) \/ ((((q)=0 \/ ~(exists pvs_factor_swap_sourcenondivisor. (n) = (q) * pvs_factor_swap_sourcenondivisor)) /\ ((z)=0)))) -> ((((~((d)=0)) /\ (exists dc_quotient_swap_target dc_left_swap_target dc_right_swap_target. (((n)=(d)*dc_quotient_swap_target) /\ (((exists dst_positive_code_swap_targetleft dst_positive_scale_swap_targetleft dst_negative_code_swap_targetleft dst_negative_scale_swap_targetleft dst_positive_swap_targetleft dst_negative_swap_targetleft. (((G) = (((((dst_positive_code_swap_targetleft) + (dst_positive_scale_swap_targetleft)) * S ((dst_positive_code_swap_targetleft) + (dst_positive_scale_swap_targetleft)) + ((dst_positive_scale_swap_targetleft) + (dst_positive_scale_swap_targetleft))) + (((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) * S ((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) + ((dst_negative_scale_swap_targetleft) + (dst_negative_scale_swap_targetleft)))) * S ((((dst_positive_code_swap_targetleft) + (dst_positive_scale_swap_targetleft)) * S ((dst_positive_code_swap_targetleft) + (dst_positive_scale_swap_targetleft)) + ((dst_positive_scale_swap_targetleft) + (dst_positive_scale_swap_targetleft))) + (((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) * S ((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) + ((dst_negative_scale_swap_targetleft) + (dst_negative_scale_swap_targetleft)))) + ((((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) * S ((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) + ((dst_negative_scale_swap_targetleft) + (dst_negative_scale_swap_targetleft))) + (((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) * S ((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) + ((dst_negative_scale_swap_targetleft) + (dst_negative_scale_swap_targetleft)))))) /\ (((((exists ff_h_pvs_swap_targetleftpositive. ff_h_pvs_swap_targetleftpositive + S (dst_positive_swap_targetleft) = S ((S (d)) * dst_positive_scale_swap_targetleft)) /\ exists ff_q_pvs_swap_targetleftpositive. dst_positive_code_swap_targetleft = ff_q_pvs_swap_targetleftpositive * S ((S (d)) * dst_positive_scale_swap_targetleft) + (dst_positive_swap_targetleft))) /\ (((((exists ff_h_pvs_swap_targetleftnegative. ff_h_pvs_swap_targetleftnegative + S (dst_negative_swap_targetleft) = S ((S (d)) * dst_negative_scale_swap_targetleft)) /\ exists ff_q_pvs_swap_targetleftnegative. dst_negative_code_swap_targetleft = ff_q_pvs_swap_targetleftnegative * S ((S (d)) * dst_negative_scale_swap_targetleft) + (dst_negative_swap_targetleft))) /\ (exists ge_balance_positive_swap_targetleftvalue ge_balance_negative_swap_targetleftvalue. (((((dc_left_swap_target) = 2 * (ge_balance_positive_swap_targetleftvalue) /\ (ge_balance_negative_swap_targetleftvalue) = 0) \/ exists ge_signed_half_swap_targetleftvaluedecode. (((dc_left_swap_target) = 2 * ge_signed_half_swap_targetleftvaluedecode + 1 /\ (ge_balance_positive_swap_targetleftvalue) = 0) /\ (ge_balance_negative_swap_targetleftvalue) = S ge_signed_half_swap_targetleftvaluedecode))) /\ ((dst_positive_swap_targetleft) + ge_balance_negative_swap_targetleftvalue = (dst_negative_swap_targetleft) + ge_balance_positive_swap_targetleftvalue))))))))) /\ (((exists dst_positive_code_swap_targetright dst_positive_scale_swap_targetright dst_negative_code_swap_targetright dst_negative_scale_swap_targetright dst_positive_swap_targetright dst_negative_swap_targetright. (((F) = (((((dst_positive_code_swap_targetright) + (dst_positive_scale_swap_targetright)) * S ((dst_positive_code_swap_targetright) + (dst_positive_scale_swap_targetright)) + ((dst_positive_scale_swap_targetright) + (dst_positive_scale_swap_targetright))) + (((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) * S ((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) + ((dst_negative_scale_swap_targetright) + (dst_negative_scale_swap_targetright)))) * S ((((dst_positive_code_swap_targetright) + (dst_positive_scale_swap_targetright)) * S ((dst_positive_code_swap_targetright) + (dst_positive_scale_swap_targetright)) + ((dst_positive_scale_swap_targetright) + (dst_positive_scale_swap_targetright))) + (((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) * S ((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) + ((dst_negative_scale_swap_targetright) + (dst_negative_scale_swap_targetright)))) + ((((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) * S ((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) + ((dst_negative_scale_swap_targetright) + (dst_negative_scale_swap_targetright))) + (((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) * S ((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) + ((dst_negative_scale_swap_targetright) + (dst_negative_scale_swap_targetright)))))) /\ (((((exists ff_h_pvs_swap_targetrightpositive. ff_h_pvs_swap_targetrightpositive + S (dst_positive_swap_targetright) = S ((S (dc_quotient_swap_target)) * dst_positive_scale_swap_targetright)) /\ exists ff_q_pvs_swap_targetrightpositive. dst_positive_code_swap_targetright = ff_q_pvs_swap_targetrightpositive * S ((S (dc_quotient_swap_target)) * dst_positive_scale_swap_targetright) + (dst_positive_swap_targetright))) /\ (((((exists ff_h_pvs_swap_targetrightnegative. ff_h_pvs_swap_targetrightnegative + S (dst_negative_swap_targetright) = S ((S (dc_quotient_swap_target)) * dst_negative_scale_swap_targetright)) /\ exists ff_q_pvs_swap_targetrightnegative. dst_negative_code_swap_targetright = ff_q_pvs_swap_targetrightnegative * S ((S (dc_quotient_swap_target)) * dst_negative_scale_swap_targetright) + (dst_negative_swap_targetright))) /\ (exists ge_balance_positive_swap_targetrightvalue ge_balance_negative_swap_targetrightvalue. (((((dc_right_swap_target) = 2 * (ge_balance_positive_swap_targetrightvalue) /\ (ge_balance_negative_swap_targetrightvalue) = 0) \/ exists ge_signed_half_swap_targetrightvaluedecode. (((dc_right_swap_target) = 2 * ge_signed_half_swap_targetrightvaluedecode + 1 /\ (ge_balance_positive_swap_targetrightvalue) = 0) /\ (ge_balance_negative_swap_targetrightvalue) = S ge_signed_half_swap_targetrightvaluedecode))) /\ ((dst_positive_swap_targetright) + ge_balance_negative_swap_targetrightvalue = (dst_negative_swap_targetright) + ge_balance_positive_swap_targetrightvalue))))))))) /\ (exists sto_ap_swap_targetproduct sto_an_swap_targetproduct sto_bp_swap_targetproduct sto_bn_swap_targetproduct sto_cp_swap_targetproduct sto_cn_swap_targetproduct. (((((dc_left_swap_target) = 2 * (sto_ap_swap_targetproduct) /\ (sto_an_swap_targetproduct) = 0) \/ exists ge_signed_half_swap_targetproductleft. (((dc_left_swap_target) = 2 * ge_signed_half_swap_targetproductleft + 1 /\ (sto_ap_swap_targetproduct) = 0) /\ (sto_an_swap_targetproduct) = S ge_signed_half_swap_targetproductleft))) /\ ((((((dc_right_swap_target) = 2 * (sto_bp_swap_targetproduct) /\ (sto_bn_swap_targetproduct) = 0) \/ exists ge_signed_half_swap_targetproductright. (((dc_right_swap_target) = 2 * ge_signed_half_swap_targetproductright + 1 /\ (sto_bp_swap_targetproduct) = 0) /\ (sto_bn_swap_targetproduct) = S ge_signed_half_swap_targetproductright))) /\ ((((((z) = 2 * (sto_cp_swap_targetproduct) /\ (sto_cn_swap_targetproduct) = 0) \/ exists ge_signed_half_swap_targetproductoutput. (((z) = 2 * ge_signed_half_swap_targetproductoutput + 1 /\ (sto_cp_swap_targetproduct) = 0) /\ (sto_cn_swap_targetproduct) = S ge_signed_half_swap_targetproductoutput))) /\ ((sto_ap_swap_targetproduct * sto_bp_swap_targetproduct + sto_an_swap_targetproduct * sto_bn_swap_targetproduct) + sto_cn_swap_targetproduct = (sto_ap_swap_targetproduct * sto_bn_swap_targetproduct + sto_an_swap_targetproduct * sto_bp_swap_targetproduct) + sto_cp_swap_targetproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_swap_targetnondivisor. (n) = (d) * pvs_factor_swap_targetnondivisor)) /\ ((z)=0))))

Complete tactic proof in conservative notation

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

92 script commands · 18 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.

Named ingredients (2)
dirichlet convolution entry from quotientdirichlet convolution entry omitted value
01Fix variables and assumptionsL1–9

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro n
  4. L4
    intro d
  5. L5
    intro q
  6. L6
    intro z
  7. L7
    intro hn
  8. L8
    intro hc
  9. L9
    intro he
02Separate the logical casesL10–11

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

  1. L10
    cases hc
  2. L11
    cases hc_left
03Establish hqL12–20

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

  1. L12
    have hq : ~(q=0)
  2. L13
    intro hqzero
  3. L14
    specialize factor_nonzero_right (n)
  4. L15
    specialize factor_nonzero_right (d)
  5. L16
    specialize factor_nonzero_right (q)
  6. L17
    apply factor_nonzero_right
  7. L18
    exact hn
  8. L19
    exact hc_left_right
  9. L20
    exact hqzero
04Separate the logical casesL21–28

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

  1. L21
    cases he
  2. L22
    cases he_left
  3. L23
    cases he_left_right
  4. L24
    cases he_left_right_witness
  5. L25
    cases he_left_right_witness_witness
  6. L26
    cases he_left_right_witness_witness_witness
  7. L27
    cases he_left_right_witness_witness_witness_right
  8. L28
    cases he_left_right_witness_witness_witness_right_right
05Establish hrL29–38

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

  1. L29
    have hr : x=d
  2. L30
    specialize mul_left_cancel_nonzero (q)
  3. L31
    specialize mul_left_cancel_nonzero (x)
  4. L32
    specialize mul_left_cancel_nonzero (d)
  5. L33
    apply mul_left_cancel_nonzero
  6. L34
    exact hq
  7. L35
    trans n
  8. L36
    symm
  9. L37
    exact he_left_right_witness_witness_witness_left
  10. L38
    trans d*q
06Use earlier factsL39–40

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

  1. L39
    exact hc_left_right
  2. L40
    apply mul_comm
07Calculate and transport equalitiesL41–44

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

  1. L41
    rewrite hr at he_left_right_witness_witness_witness_right_right_left
  2. L42
    rewrite hr at he_left_right_witness_witness_witness_right_right_left
  3. L43
    rewrite hr at he_left_right_witness_witness_witness_right_right_left
  4. L44
    rewrite hr at he_left_right_witness_witness_witness_right_right_left
08Use earlier factsL45–54

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

  1. L45
    specialize dirichlet_convolution_entry_from_quotient (G)
  2. L46
    specialize dirichlet_convolution_entry_from_quotient (F)
  3. L47
    specialize dirichlet_convolution_entry_from_quotient (n)
  4. L48
    specialize dirichlet_convolution_entry_from_quotient (d)
  5. L49
    specialize dirichlet_convolution_entry_from_quotient (q)
  6. L50
    specialize dirichlet_convolution_entry_from_quotient (x2)
  7. L51
    specialize dirichlet_convolution_entry_from_quotient (x1)
  8. L52
    specialize dirichlet_convolution_entry_from_quotient (z)
  9. L53
    apply dirichlet_convolution_entry_from_quotient
  10. L54
    exact hc_left_left
09Use earlier factsL55–62

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

  1. L55
    exact hc_left_right
  2. L56
    exact he_left_right_witness_witness_witness_right_right_left
  3. L57
    exact he_left_right_witness_witness_witness_right_left
  4. L58
    specialize signed_mul_commutative (x1)
  5. L59
    specialize signed_mul_commutative (x2)
  6. L60
    specialize signed_mul_commutative (z)
  7. L61
    apply signed_mul_commutative
  8. L62
    exact he_left_right_witness_witness_witness_right_right_right
10Separate the logical casesL63–65

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

  1. L63
    cases he_right
  2. L64
    exfalso
  3. L65
    cases he_right_left
11Use earlier factsL66–68

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

  1. L66
    apply hq
  2. L67
    exact he_right_left_left
  3. L68
    apply he_right_left_right
12Construct an explicit witnessL69–69

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

  1. L69
    exists d
13Calculate and transport equalitiesL70–70

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

  1. L70
    trans d*q
14Use earlier factsL71–72

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

  1. L71
    exact hc_left_right
  2. L72
    apply mul_comm
15Separate the logical casesL73–73

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

  1. L73
    cases hc_right
16Calculate and transport equalitiesL74–81

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

  1. L74
    rewrite hc_right_right at he
  2. L75
    rewrite hc_right_right at he
  3. L76
    rewrite hc_right_right at he
  4. L77
    rewrite hc_right_right at he
  5. L78
    rewrite hc_right_right at he
  6. L79
    rewrite hc_right_right at he
  7. L80
    rewrite hc_right_right at he
  8. L81
    rewrite hc_right_right at he
17Separate the logical casesL82–83

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

  1. L82
    right
  2. L83
    split
18Use earlier factsL84–92

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

  1. L84
    exact hc_right_left
  2. L85
    specialize dirichlet_convolution_entry_omitted_value (F)
  3. L86
    specialize dirichlet_convolution_entry_omitted_value (G)
  4. L87
    specialize dirichlet_convolution_entry_omitted_value (n)
  5. L88
    specialize dirichlet_convolution_entry_omitted_value (d)
  6. L89
    specialize dirichlet_convolution_entry_omitted_value (z)
  7. L90
    apply dirichlet_convolution_entry_omitted_value
  8. L91
    exact hc_right_left
  9. L92
    exact he

Library-wide reading audit

Original defined command ledger · 92 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro n
  4. 0004intro d
  5. 0005intro q
  6. 0006intro z
  7. 0007intro hn
  8. 0008intro hc
  9. 0009intro he
  10. 0010cases hc
  11. 0011cases hc_left
  12. 0012have hq : ~(q=0)
  13. 0013intro hqzero
  14. 0014specialize factor_nonzero_right (n)
  15. 0015specialize factor_nonzero_right (d)
  16. 0016specialize factor_nonzero_right (q)
  17. 0017apply factor_nonzero_right
  18. 0018exact hn
  19. 0019exact hc_left_right
  20. 0020exact hqzero
  21. 0021cases he
  22. 0022cases he_left
  23. 0023cases he_left_right
  24. 0024cases he_left_right_witness
  25. 0025cases he_left_right_witness_witness
  26. 0026cases he_left_right_witness_witness_witness
  27. 0027cases he_left_right_witness_witness_witness_right
  28. 0028cases he_left_right_witness_witness_witness_right_right
  29. 0029have hr : x=d
  30. 0030specialize mul_left_cancel_nonzero (q)
  31. 0031specialize mul_left_cancel_nonzero (x)
  32. 0032specialize mul_left_cancel_nonzero (d)
  33. 0033apply mul_left_cancel_nonzero
  34. 0034exact hq
  35. 0035trans n
  36. 0036symm
  37. 0037exact he_left_right_witness_witness_witness_left
  38. 0038trans d*q
  39. 0039exact hc_left_right
  40. 0040apply mul_comm
  41. 0041rewrite hr at he_left_right_witness_witness_witness_right_right_left
  42. 0042rewrite hr at he_left_right_witness_witness_witness_right_right_left
  43. 0043rewrite hr at he_left_right_witness_witness_witness_right_right_left
  44. 0044rewrite hr at he_left_right_witness_witness_witness_right_right_left
  45. 0045specialize dirichlet_convolution_entry_from_quotient (G)
  46. 0046specialize dirichlet_convolution_entry_from_quotient (F)
  47. 0047specialize dirichlet_convolution_entry_from_quotient (n)
  48. 0048specialize dirichlet_convolution_entry_from_quotient (d)
  49. 0049specialize dirichlet_convolution_entry_from_quotient (q)
  50. 0050specialize dirichlet_convolution_entry_from_quotient (x2)
  51. 0051specialize dirichlet_convolution_entry_from_quotient (x1)
  52. 0052specialize dirichlet_convolution_entry_from_quotient (z)
  53. 0053apply dirichlet_convolution_entry_from_quotient
  54. 0054exact hc_left_left
  55. 0055exact hc_left_right
  56. 0056exact he_left_right_witness_witness_witness_right_right_left
  57. 0057exact he_left_right_witness_witness_witness_right_left
  58. 0058specialize signed_mul_commutative (x1)
  59. 0059specialize signed_mul_commutative (x2)
  60. 0060specialize signed_mul_commutative (z)
  61. 0061apply signed_mul_commutative
  62. 0062exact he_left_right_witness_witness_witness_right_right_right
  63. 0063cases he_right
  64. 0064exfalso
  65. 0065cases he_right_left
  66. 0066apply hq
  67. 0067exact he_right_left_left
  68. 0068apply he_right_left_right
  69. 0069exists d
  70. 0070trans d*q
  71. 0071exact hc_left_right
  72. 0072apply mul_comm
  73. 0073cases hc_right
  74. 0074rewrite hc_right_right at he
  75. 0075rewrite hc_right_right at he
  76. 0076rewrite hc_right_right at he
  77. 0077rewrite hc_right_right at he
  78. 0078rewrite hc_right_right at he
  79. 0079rewrite hc_right_right at he
  80. 0080rewrite hc_right_right at he
  81. 0081rewrite hc_right_right at he
  82. 0082right
  83. 0083split
  84. 0084exact hc_right_left
  85. 0085specialize dirichlet_convolution_entry_omitted_value (F)
  86. 0086specialize dirichlet_convolution_entry_omitted_value (G)
  87. 0087specialize dirichlet_convolution_entry_omitted_value (n)
  88. 0088specialize dirichlet_convolution_entry_omitted_value (d)
  89. 0089specialize dirichlet_convolution_entry_omitted_value (z)
  90. 0090apply dirichlet_convolution_entry_omitted_value
  91. 0091exact hc_right_left
  92. 0092exact he