DC0006

dirichlet_convolution_entry_functional

Actual quotient, lookup and signed-product functionality determine one canonical summand, without identifying table codes.

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. ∀ u. ∀ v. DirichletEntry(F,G,n,d,u) → DirichletEntry(F,G,n,d,v) → u = v

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

Definition DAG

DirichletEntry(F,G,n,d,z) · 2

Actual proof prerequisites

signed_mul_functional · checked external prerequisitedirichlet_convolution_entry_quotient_productdirichlet_convolution_entry_omitted_value
Original expanded first-order statement 
forall F G n d u v. ((((~((d)=0)) /\ (exists dc_quotient_unique_first dc_left_unique_first dc_right_unique_first. (((n)=(d)*dc_quotient_unique_first) /\ (((exists dst_positive_code_unique_firstleft dst_positive_scale_unique_firstleft dst_negative_code_unique_firstleft dst_negative_scale_unique_firstleft dst_positive_unique_firstleft dst_negative_unique_firstleft. (((F) = (((((dst_positive_code_unique_firstleft) + (dst_positive_scale_unique_firstleft)) * S ((dst_positive_code_unique_firstleft) + (dst_positive_scale_unique_firstleft)) + ((dst_positive_scale_unique_firstleft) + (dst_positive_scale_unique_firstleft))) + (((dst_negative_code_unique_firstleft) + (dst_negative_scale_unique_firstleft)) * S ((dst_negative_code_unique_firstleft) + (dst_negative_scale_unique_firstleft)) + ((dst_negative_scale_unique_firstleft) + (dst_negative_scale_unique_firstleft)))) * S ((((dst_positive_code_unique_firstleft) + (dst_positive_scale_unique_firstleft)) * S ((dst_positive_code_unique_firstleft) + (dst_positive_scale_unique_firstleft)) + ((dst_positive_scale_unique_firstleft) + (dst_positive_scale_unique_firstleft))) + (((dst_negative_code_unique_firstleft) + (dst_negative_scale_unique_firstleft)) * S ((dst_negative_code_unique_firstleft) + (dst_negative_scale_unique_firstleft)) + ((dst_negative_scale_unique_firstleft) + (dst_negative_scale_unique_firstleft)))) + ((((dst_negative_code_unique_firstleft) + (dst_negative_scale_unique_firstleft)) * S ((dst_negative_code_unique_firstleft) + (dst_negative_scale_unique_firstleft)) + ((dst_negative_scale_unique_firstleft) + (dst_negative_scale_unique_firstleft))) + (((dst_negative_code_unique_firstleft) + (dst_negative_scale_unique_firstleft)) * S ((dst_negative_code_unique_firstleft) + (dst_negative_scale_unique_firstleft)) + ((dst_negative_scale_unique_firstleft) + (dst_negative_scale_unique_firstleft)))))) /\ (((((exists ff_h_pvs_unique_firstleftpositive. ff_h_pvs_unique_firstleftpositive + S (dst_positive_unique_firstleft) = S ((S (d)) * dst_positive_scale_unique_firstleft)) /\ exists ff_q_pvs_unique_firstleftpositive. dst_positive_code_unique_firstleft = ff_q_pvs_unique_firstleftpositive * S ((S (d)) * dst_positive_scale_unique_firstleft) + (dst_positive_unique_firstleft))) /\ (((((exists ff_h_pvs_unique_firstleftnegative. ff_h_pvs_unique_firstleftnegative + S (dst_negative_unique_firstleft) = S ((S (d)) * dst_negative_scale_unique_firstleft)) /\ exists ff_q_pvs_unique_firstleftnegative. dst_negative_code_unique_firstleft = ff_q_pvs_unique_firstleftnegative * S ((S (d)) * dst_negative_scale_unique_firstleft) + (dst_negative_unique_firstleft))) /\ (exists ge_balance_positive_unique_firstleftvalue ge_balance_negative_unique_firstleftvalue. (((((dc_left_unique_first) = 2 * (ge_balance_positive_unique_firstleftvalue) /\ (ge_balance_negative_unique_firstleftvalue) = 0) \/ exists ge_signed_half_unique_firstleftvaluedecode. (((dc_left_unique_first) = 2 * ge_signed_half_unique_firstleftvaluedecode + 1 /\ (ge_balance_positive_unique_firstleftvalue) = 0) /\ (ge_balance_negative_unique_firstleftvalue) = S ge_signed_half_unique_firstleftvaluedecode))) /\ ((dst_positive_unique_firstleft) + ge_balance_negative_unique_firstleftvalue = (dst_negative_unique_firstleft) + ge_balance_positive_unique_firstleftvalue))))))))) /\ (((exists dst_positive_code_unique_firstright dst_positive_scale_unique_firstright dst_negative_code_unique_firstright dst_negative_scale_unique_firstright dst_positive_unique_firstright dst_negative_unique_firstright. (((G) = (((((dst_positive_code_unique_firstright) + (dst_positive_scale_unique_firstright)) * S ((dst_positive_code_unique_firstright) + (dst_positive_scale_unique_firstright)) + ((dst_positive_scale_unique_firstright) + (dst_positive_scale_unique_firstright))) + (((dst_negative_code_unique_firstright) + (dst_negative_scale_unique_firstright)) * S ((dst_negative_code_unique_firstright) + (dst_negative_scale_unique_firstright)) + ((dst_negative_scale_unique_firstright) + (dst_negative_scale_unique_firstright)))) * S ((((dst_positive_code_unique_firstright) + (dst_positive_scale_unique_firstright)) * S ((dst_positive_code_unique_firstright) + (dst_positive_scale_unique_firstright)) + ((dst_positive_scale_unique_firstright) + (dst_positive_scale_unique_firstright))) + (((dst_negative_code_unique_firstright) + (dst_negative_scale_unique_firstright)) * S ((dst_negative_code_unique_firstright) + (dst_negative_scale_unique_firstright)) + ((dst_negative_scale_unique_firstright) + (dst_negative_scale_unique_firstright)))) + ((((dst_negative_code_unique_firstright) + (dst_negative_scale_unique_firstright)) * S ((dst_negative_code_unique_firstright) + (dst_negative_scale_unique_firstright)) + ((dst_negative_scale_unique_firstright) + (dst_negative_scale_unique_firstright))) + (((dst_negative_code_unique_firstright) + (dst_negative_scale_unique_firstright)) * S ((dst_negative_code_unique_firstright) + (dst_negative_scale_unique_firstright)) + ((dst_negative_scale_unique_firstright) + (dst_negative_scale_unique_firstright)))))) /\ (((((exists ff_h_pvs_unique_firstrightpositive. ff_h_pvs_unique_firstrightpositive + S (dst_positive_unique_firstright) = S ((S (dc_quotient_unique_first)) * dst_positive_scale_unique_firstright)) /\ exists ff_q_pvs_unique_firstrightpositive. dst_positive_code_unique_firstright = ff_q_pvs_unique_firstrightpositive * S ((S (dc_quotient_unique_first)) * dst_positive_scale_unique_firstright) + (dst_positive_unique_firstright))) /\ (((((exists ff_h_pvs_unique_firstrightnegative. ff_h_pvs_unique_firstrightnegative + S (dst_negative_unique_firstright) = S ((S (dc_quotient_unique_first)) * dst_negative_scale_unique_firstright)) /\ exists ff_q_pvs_unique_firstrightnegative. dst_negative_code_unique_firstright = ff_q_pvs_unique_firstrightnegative * S ((S (dc_quotient_unique_first)) * dst_negative_scale_unique_firstright) + (dst_negative_unique_firstright))) /\ (exists ge_balance_positive_unique_firstrightvalue ge_balance_negative_unique_firstrightvalue. (((((dc_right_unique_first) = 2 * (ge_balance_positive_unique_firstrightvalue) /\ (ge_balance_negative_unique_firstrightvalue) = 0) \/ exists ge_signed_half_unique_firstrightvaluedecode. (((dc_right_unique_first) = 2 * ge_signed_half_unique_firstrightvaluedecode + 1 /\ (ge_balance_positive_unique_firstrightvalue) = 0) /\ (ge_balance_negative_unique_firstrightvalue) = S ge_signed_half_unique_firstrightvaluedecode))) /\ ((dst_positive_unique_firstright) + ge_balance_negative_unique_firstrightvalue = (dst_negative_unique_firstright) + ge_balance_positive_unique_firstrightvalue))))))))) /\ (exists sto_ap_unique_firstproduct sto_an_unique_firstproduct sto_bp_unique_firstproduct sto_bn_unique_firstproduct sto_cp_unique_firstproduct sto_cn_unique_firstproduct. (((((dc_left_unique_first) = 2 * (sto_ap_unique_firstproduct) /\ (sto_an_unique_firstproduct) = 0) \/ exists ge_signed_half_unique_firstproductleft. (((dc_left_unique_first) = 2 * ge_signed_half_unique_firstproductleft + 1 /\ (sto_ap_unique_firstproduct) = 0) /\ (sto_an_unique_firstproduct) = S ge_signed_half_unique_firstproductleft))) /\ ((((((dc_right_unique_first) = 2 * (sto_bp_unique_firstproduct) /\ (sto_bn_unique_firstproduct) = 0) \/ exists ge_signed_half_unique_firstproductright. (((dc_right_unique_first) = 2 * ge_signed_half_unique_firstproductright + 1 /\ (sto_bp_unique_firstproduct) = 0) /\ (sto_bn_unique_firstproduct) = S ge_signed_half_unique_firstproductright))) /\ ((((((u) = 2 * (sto_cp_unique_firstproduct) /\ (sto_cn_unique_firstproduct) = 0) \/ exists ge_signed_half_unique_firstproductoutput. (((u) = 2 * ge_signed_half_unique_firstproductoutput + 1 /\ (sto_cp_unique_firstproduct) = 0) /\ (sto_cn_unique_firstproduct) = S ge_signed_half_unique_firstproductoutput))) /\ ((sto_ap_unique_firstproduct * sto_bp_unique_firstproduct + sto_an_unique_firstproduct * sto_bn_unique_firstproduct) + sto_cn_unique_firstproduct = (sto_ap_unique_firstproduct * sto_bn_unique_firstproduct + sto_an_unique_firstproduct * sto_bp_unique_firstproduct) + sto_cp_unique_firstproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_unique_firstnondivisor. (n) = (d) * pvs_factor_unique_firstnondivisor)) /\ ((u)=0)))) -> ((((~((d)=0)) /\ (exists dc_quotient_unique_second dc_left_unique_second dc_right_unique_second. (((n)=(d)*dc_quotient_unique_second) /\ (((exists dst_positive_code_unique_secondleft dst_positive_scale_unique_secondleft dst_negative_code_unique_secondleft dst_negative_scale_unique_secondleft dst_positive_unique_secondleft dst_negative_unique_secondleft. (((F) = (((((dst_positive_code_unique_secondleft) + (dst_positive_scale_unique_secondleft)) * S ((dst_positive_code_unique_secondleft) + (dst_positive_scale_unique_secondleft)) + ((dst_positive_scale_unique_secondleft) + (dst_positive_scale_unique_secondleft))) + (((dst_negative_code_unique_secondleft) + (dst_negative_scale_unique_secondleft)) * S ((dst_negative_code_unique_secondleft) + (dst_negative_scale_unique_secondleft)) + ((dst_negative_scale_unique_secondleft) + (dst_negative_scale_unique_secondleft)))) * S ((((dst_positive_code_unique_secondleft) + (dst_positive_scale_unique_secondleft)) * S ((dst_positive_code_unique_secondleft) + (dst_positive_scale_unique_secondleft)) + ((dst_positive_scale_unique_secondleft) + (dst_positive_scale_unique_secondleft))) + (((dst_negative_code_unique_secondleft) + (dst_negative_scale_unique_secondleft)) * S ((dst_negative_code_unique_secondleft) + (dst_negative_scale_unique_secondleft)) + ((dst_negative_scale_unique_secondleft) + (dst_negative_scale_unique_secondleft)))) + ((((dst_negative_code_unique_secondleft) + (dst_negative_scale_unique_secondleft)) * S ((dst_negative_code_unique_secondleft) + (dst_negative_scale_unique_secondleft)) + ((dst_negative_scale_unique_secondleft) + (dst_negative_scale_unique_secondleft))) + (((dst_negative_code_unique_secondleft) + (dst_negative_scale_unique_secondleft)) * S ((dst_negative_code_unique_secondleft) + (dst_negative_scale_unique_secondleft)) + ((dst_negative_scale_unique_secondleft) + (dst_negative_scale_unique_secondleft)))))) /\ (((((exists ff_h_pvs_unique_secondleftpositive. ff_h_pvs_unique_secondleftpositive + S (dst_positive_unique_secondleft) = S ((S (d)) * dst_positive_scale_unique_secondleft)) /\ exists ff_q_pvs_unique_secondleftpositive. dst_positive_code_unique_secondleft = ff_q_pvs_unique_secondleftpositive * S ((S (d)) * dst_positive_scale_unique_secondleft) + (dst_positive_unique_secondleft))) /\ (((((exists ff_h_pvs_unique_secondleftnegative. ff_h_pvs_unique_secondleftnegative + S (dst_negative_unique_secondleft) = S ((S (d)) * dst_negative_scale_unique_secondleft)) /\ exists ff_q_pvs_unique_secondleftnegative. dst_negative_code_unique_secondleft = ff_q_pvs_unique_secondleftnegative * S ((S (d)) * dst_negative_scale_unique_secondleft) + (dst_negative_unique_secondleft))) /\ (exists ge_balance_positive_unique_secondleftvalue ge_balance_negative_unique_secondleftvalue. (((((dc_left_unique_second) = 2 * (ge_balance_positive_unique_secondleftvalue) /\ (ge_balance_negative_unique_secondleftvalue) = 0) \/ exists ge_signed_half_unique_secondleftvaluedecode. (((dc_left_unique_second) = 2 * ge_signed_half_unique_secondleftvaluedecode + 1 /\ (ge_balance_positive_unique_secondleftvalue) = 0) /\ (ge_balance_negative_unique_secondleftvalue) = S ge_signed_half_unique_secondleftvaluedecode))) /\ ((dst_positive_unique_secondleft) + ge_balance_negative_unique_secondleftvalue = (dst_negative_unique_secondleft) + ge_balance_positive_unique_secondleftvalue))))))))) /\ (((exists dst_positive_code_unique_secondright dst_positive_scale_unique_secondright dst_negative_code_unique_secondright dst_negative_scale_unique_secondright dst_positive_unique_secondright dst_negative_unique_secondright. (((G) = (((((dst_positive_code_unique_secondright) + (dst_positive_scale_unique_secondright)) * S ((dst_positive_code_unique_secondright) + (dst_positive_scale_unique_secondright)) + ((dst_positive_scale_unique_secondright) + (dst_positive_scale_unique_secondright))) + (((dst_negative_code_unique_secondright) + (dst_negative_scale_unique_secondright)) * S ((dst_negative_code_unique_secondright) + (dst_negative_scale_unique_secondright)) + ((dst_negative_scale_unique_secondright) + (dst_negative_scale_unique_secondright)))) * S ((((dst_positive_code_unique_secondright) + (dst_positive_scale_unique_secondright)) * S ((dst_positive_code_unique_secondright) + (dst_positive_scale_unique_secondright)) + ((dst_positive_scale_unique_secondright) + (dst_positive_scale_unique_secondright))) + (((dst_negative_code_unique_secondright) + (dst_negative_scale_unique_secondright)) * S ((dst_negative_code_unique_secondright) + (dst_negative_scale_unique_secondright)) + ((dst_negative_scale_unique_secondright) + (dst_negative_scale_unique_secondright)))) + ((((dst_negative_code_unique_secondright) + (dst_negative_scale_unique_secondright)) * S ((dst_negative_code_unique_secondright) + (dst_negative_scale_unique_secondright)) + ((dst_negative_scale_unique_secondright) + (dst_negative_scale_unique_secondright))) + (((dst_negative_code_unique_secondright) + (dst_negative_scale_unique_secondright)) * S ((dst_negative_code_unique_secondright) + (dst_negative_scale_unique_secondright)) + ((dst_negative_scale_unique_secondright) + (dst_negative_scale_unique_secondright)))))) /\ (((((exists ff_h_pvs_unique_secondrightpositive. ff_h_pvs_unique_secondrightpositive + S (dst_positive_unique_secondright) = S ((S (dc_quotient_unique_second)) * dst_positive_scale_unique_secondright)) /\ exists ff_q_pvs_unique_secondrightpositive. dst_positive_code_unique_secondright = ff_q_pvs_unique_secondrightpositive * S ((S (dc_quotient_unique_second)) * dst_positive_scale_unique_secondright) + (dst_positive_unique_secondright))) /\ (((((exists ff_h_pvs_unique_secondrightnegative. ff_h_pvs_unique_secondrightnegative + S (dst_negative_unique_secondright) = S ((S (dc_quotient_unique_second)) * dst_negative_scale_unique_secondright)) /\ exists ff_q_pvs_unique_secondrightnegative. dst_negative_code_unique_secondright = ff_q_pvs_unique_secondrightnegative * S ((S (dc_quotient_unique_second)) * dst_negative_scale_unique_secondright) + (dst_negative_unique_secondright))) /\ (exists ge_balance_positive_unique_secondrightvalue ge_balance_negative_unique_secondrightvalue. (((((dc_right_unique_second) = 2 * (ge_balance_positive_unique_secondrightvalue) /\ (ge_balance_negative_unique_secondrightvalue) = 0) \/ exists ge_signed_half_unique_secondrightvaluedecode. (((dc_right_unique_second) = 2 * ge_signed_half_unique_secondrightvaluedecode + 1 /\ (ge_balance_positive_unique_secondrightvalue) = 0) /\ (ge_balance_negative_unique_secondrightvalue) = S ge_signed_half_unique_secondrightvaluedecode))) /\ ((dst_positive_unique_secondright) + ge_balance_negative_unique_secondrightvalue = (dst_negative_unique_secondright) + ge_balance_positive_unique_secondrightvalue))))))))) /\ (exists sto_ap_unique_secondproduct sto_an_unique_secondproduct sto_bp_unique_secondproduct sto_bn_unique_secondproduct sto_cp_unique_secondproduct sto_cn_unique_secondproduct. (((((dc_left_unique_second) = 2 * (sto_ap_unique_secondproduct) /\ (sto_an_unique_secondproduct) = 0) \/ exists ge_signed_half_unique_secondproductleft. (((dc_left_unique_second) = 2 * ge_signed_half_unique_secondproductleft + 1 /\ (sto_ap_unique_secondproduct) = 0) /\ (sto_an_unique_secondproduct) = S ge_signed_half_unique_secondproductleft))) /\ ((((((dc_right_unique_second) = 2 * (sto_bp_unique_secondproduct) /\ (sto_bn_unique_secondproduct) = 0) \/ exists ge_signed_half_unique_secondproductright. (((dc_right_unique_second) = 2 * ge_signed_half_unique_secondproductright + 1 /\ (sto_bp_unique_secondproduct) = 0) /\ (sto_bn_unique_secondproduct) = S ge_signed_half_unique_secondproductright))) /\ ((((((v) = 2 * (sto_cp_unique_secondproduct) /\ (sto_cn_unique_secondproduct) = 0) \/ exists ge_signed_half_unique_secondproductoutput. (((v) = 2 * ge_signed_half_unique_secondproductoutput + 1 /\ (sto_cp_unique_secondproduct) = 0) /\ (sto_cn_unique_secondproduct) = S ge_signed_half_unique_secondproductoutput))) /\ ((sto_ap_unique_secondproduct * sto_bp_unique_secondproduct + sto_an_unique_secondproduct * sto_bn_unique_secondproduct) + sto_cn_unique_secondproduct = (sto_ap_unique_secondproduct * sto_bn_unique_secondproduct + sto_an_unique_secondproduct * sto_bp_unique_secondproduct) + sto_cp_unique_secondproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_unique_secondnondivisor. (n) = (d) * pvs_factor_unique_secondnondivisor)) /\ ((v)=0)))) -> u=v

Complete tactic proof in conservative notation

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

50 script commands · 9 reading checkpoints · 1 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 quotient productdirichlet convolution entry omitted value
01Fix variables and assumptionsL1–8

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 u
  6. L6
    intro v
  7. L7
    intro hu
  8. L8
    intro hv
02Separate the logical casesL9–16

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

  1. L9
    cases hu
  2. L10
    cases hu_left
  3. L11
    cases hu_left_right
  4. L12
    cases hu_left_right_witness
  5. L13
    cases hu_left_right_witness_witness
  6. L14
    cases hu_left_right_witness_witness_witness
  7. L15
    cases hu_left_right_witness_witness_witness_right
  8. L16
    cases hu_left_right_witness_witness_witness_right_right
03Use earlier factsL17–26

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

  1. L17
    specialize signed_mul_functional (x1)
  2. L18
    specialize signed_mul_functional (x2)
  3. L19
    specialize signed_mul_functional (u)
  4. L20
    specialize signed_mul_functional (v)
  5. L21
    apply signed_mul_functional
  6. L22
    exact hu_left_right_witness_witness_witness_right_right_right
  7. L23
    specialize dirichlet_convolution_entry_quotient_product (F)
  8. L24
    specialize dirichlet_convolution_entry_quotient_product (G)
  9. L25
    specialize dirichlet_convolution_entry_quotient_product (n)
  10. L26
    specialize dirichlet_convolution_entry_quotient_product (d)
04Use earlier factsL27–36

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

  1. L27
    specialize dirichlet_convolution_entry_quotient_product (x)
  2. L28
    specialize dirichlet_convolution_entry_quotient_product (x1)
  3. L29
    specialize dirichlet_convolution_entry_quotient_product (x2)
  4. L30
    specialize dirichlet_convolution_entry_quotient_product (v)
  5. L31
    apply dirichlet_convolution_entry_quotient_product
  6. L32
    exact hu_left_left
  7. L33
    exact hu_left_right_witness_witness_witness_left
  8. L34
    exact hu_left_right_witness_witness_witness_right_left
  9. L35
    exact hu_left_right_witness_witness_witness_right_right_left
  10. L36
    exact hv
05Separate the logical casesL37–37

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

  1. L37
    cases hu_right
06Establish hvzeroL38–47

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution entry omitted value.

  1. L38
    have hvzero : v=0
  2. L39
    specialize dirichlet_convolution_entry_omitted_value (F)
  3. L40
    specialize dirichlet_convolution_entry_omitted_value (G)
  4. L41
    specialize dirichlet_convolution_entry_omitted_value (n)
  5. L42
    specialize dirichlet_convolution_entry_omitted_value (d)
  6. L43
    specialize dirichlet_convolution_entry_omitted_value (v)
  7. L44
    apply dirichlet_convolution_entry_omitted_value
  8. L45
    exact hu_right_left
  9. L46
    exact hv
  10. L47
    trans 0
07Use earlier factsL48–48

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

  1. L48
    exact hu_right_right
08Calculate and transport equalitiesL49–49

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

  1. L49
    symm
09Use earlier factsL50–50

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

  1. L50
    exact hvzero

Library-wide reading audit

Original defined command ledger · 50 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro n
  4. 0004intro d
  5. 0005intro u
  6. 0006intro v
  7. 0007intro hu
  8. 0008intro hv
  9. 0009cases hu
  10. 0010cases hu_left
  11. 0011cases hu_left_right
  12. 0012cases hu_left_right_witness
  13. 0013cases hu_left_right_witness_witness
  14. 0014cases hu_left_right_witness_witness_witness
  15. 0015cases hu_left_right_witness_witness_witness_right
  16. 0016cases hu_left_right_witness_witness_witness_right_right
  17. 0017specialize signed_mul_functional (x1)
  18. 0018specialize signed_mul_functional (x2)
  19. 0019specialize signed_mul_functional (u)
  20. 0020specialize signed_mul_functional (v)
  21. 0021apply signed_mul_functional
  22. 0022exact hu_left_right_witness_witness_witness_right_right_right
  23. 0023specialize dirichlet_convolution_entry_quotient_product (F)
  24. 0024specialize dirichlet_convolution_entry_quotient_product (G)
  25. 0025specialize dirichlet_convolution_entry_quotient_product (n)
  26. 0026specialize dirichlet_convolution_entry_quotient_product (d)
  27. 0027specialize dirichlet_convolution_entry_quotient_product (x)
  28. 0028specialize dirichlet_convolution_entry_quotient_product (x1)
  29. 0029specialize dirichlet_convolution_entry_quotient_product (x2)
  30. 0030specialize dirichlet_convolution_entry_quotient_product (v)
  31. 0031apply dirichlet_convolution_entry_quotient_product
  32. 0032exact hu_left_left
  33. 0033exact hu_left_right_witness_witness_witness_left
  34. 0034exact hu_left_right_witness_witness_witness_right_left
  35. 0035exact hu_left_right_witness_witness_witness_right_right_left
  36. 0036exact hv
  37. 0037cases hu_right
  38. 0038have hvzero : v=0
  39. 0039specialize dirichlet_convolution_entry_omitted_value (F)
  40. 0040specialize dirichlet_convolution_entry_omitted_value (G)
  41. 0041specialize dirichlet_convolution_entry_omitted_value (n)
  42. 0042specialize dirichlet_convolution_entry_omitted_value (d)
  43. 0043specialize dirichlet_convolution_entry_omitted_value (v)
  44. 0044apply dirichlet_convolution_entry_omitted_value
  45. 0045exact hu_right_left
  46. 0046exact hv
  47. 0047trans 0
  48. 0048exact hu_right_right
  49. 0049symm
  50. 0050exact hvzero