DU000D

dirichlet_delta_right_entry_before_input

Every actual summand before n vanishes: a real complementary quotient is positive and cannot be one, while omitted indices are already 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.

Signed one is code 2. Positive-only table graphs preserve arbitrary zeroth values, including N=0. The unit and divisor-sum identities are proved, never embedded in definitions. The separate inverse family proves the general unit-at-one criterion; multiplicative-function closure remains open.

Exact theorem in conservative defined notation

∀ N. ∀ F. ∀ E. ∀ n. ∀ d. ∀ z. KroneckerDeltaTable(N,E) → ¬n = 0 → Le(n,N) → Lt(d,n) → DirichletEntry(F,E,n,d,z) → z = 0

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

Definition DAG

DirichletEntry(F,G,n,d,z) · 1KroneckerDeltaTable(N,E) · 1Le(a,b) · 2Lt(a,b) · 1

Actual proof prerequisites

factor_nonzero_right · checked external prerequisitele_trans · checked external prerequisitedivisor_le_nonzero · checked external prerequisitemul_comm · checked external prerequisitemul_one · checked external prerequisitelt_not_le · checked external prerequisitele_refl · checked external prerequisitedirichlet_kronecker_delta_table_other_valuesigned_mul_functional · checked external prerequisitesigned_mul_zero_right · checked external prerequisite
Original expanded first-order statement 
forall N F E n d z. (((exists dst_positive_code_before_deltatable dst_positive_scale_before_deltatable dst_negative_code_before_deltatable dst_negative_scale_before_deltatable. (((E) = (((((dst_positive_code_before_deltatable) + (dst_positive_scale_before_deltatable)) * S ((dst_positive_code_before_deltatable) + (dst_positive_scale_before_deltatable)) + ((dst_positive_scale_before_deltatable) + (dst_positive_scale_before_deltatable))) + (((dst_negative_code_before_deltatable) + (dst_negative_scale_before_deltatable)) * S ((dst_negative_code_before_deltatable) + (dst_negative_scale_before_deltatable)) + ((dst_negative_scale_before_deltatable) + (dst_negative_scale_before_deltatable)))) * S ((((dst_positive_code_before_deltatable) + (dst_positive_scale_before_deltatable)) * S ((dst_positive_code_before_deltatable) + (dst_positive_scale_before_deltatable)) + ((dst_positive_scale_before_deltatable) + (dst_positive_scale_before_deltatable))) + (((dst_negative_code_before_deltatable) + (dst_negative_scale_before_deltatable)) * S ((dst_negative_code_before_deltatable) + (dst_negative_scale_before_deltatable)) + ((dst_negative_scale_before_deltatable) + (dst_negative_scale_before_deltatable)))) + ((((dst_negative_code_before_deltatable) + (dst_negative_scale_before_deltatable)) * S ((dst_negative_code_before_deltatable) + (dst_negative_scale_before_deltatable)) + ((dst_negative_scale_before_deltatable) + (dst_negative_scale_before_deltatable))) + (((dst_negative_code_before_deltatable) + (dst_negative_scale_before_deltatable)) * S ((dst_negative_code_before_deltatable) + (dst_negative_scale_before_deltatable)) + ((dst_negative_scale_before_deltatable) + (dst_negative_scale_before_deltatable)))))) /\ (forall dst_index_before_deltatable. (exists pvs_le_gap_before_deltatabledomain. pvs_le_gap_before_deltatabledomain + (dst_index_before_deltatable) = (N)) -> exists dst_positive_before_deltatable dst_negative_before_deltatable dst_value_before_deltatable. ((((exists ff_h_pvs_before_deltatableentrypositive. ff_h_pvs_before_deltatableentrypositive + S (dst_positive_before_deltatable) = S ((S (dst_index_before_deltatable)) * dst_positive_scale_before_deltatable)) /\ exists ff_q_pvs_before_deltatableentrypositive. dst_positive_code_before_deltatable = ff_q_pvs_before_deltatableentrypositive * S ((S (dst_index_before_deltatable)) * dst_positive_scale_before_deltatable) + (dst_positive_before_deltatable))) /\ (((((exists ff_h_pvs_before_deltatableentrynegative. ff_h_pvs_before_deltatableentrynegative + S (dst_negative_before_deltatable) = S ((S (dst_index_before_deltatable)) * dst_negative_scale_before_deltatable)) /\ exists ff_q_pvs_before_deltatableentrynegative. dst_negative_code_before_deltatable = ff_q_pvs_before_deltatableentrynegative * S ((S (dst_index_before_deltatable)) * dst_negative_scale_before_deltatable) + (dst_negative_before_deltatable))) /\ (exists ge_balance_positive_before_deltatableentryvalue ge_balance_negative_before_deltatableentryvalue. (((((dst_value_before_deltatable) = 2 * (ge_balance_positive_before_deltatableentryvalue) /\ (ge_balance_negative_before_deltatableentryvalue) = 0) \/ exists ge_signed_half_before_deltatableentryvaluedecode. (((dst_value_before_deltatable) = 2 * ge_signed_half_before_deltatableentryvaluedecode + 1 /\ (ge_balance_positive_before_deltatableentryvalue) = 0) /\ (ge_balance_negative_before_deltatableentryvalue) = S ge_signed_half_before_deltatableentryvaluedecode))) /\ ((dst_positive_before_deltatable) + ge_balance_negative_before_deltatableentryvalue = (dst_negative_before_deltatable) + ge_balance_positive_before_deltatableentryvalue))))))))) /\ (forall du_index_before_delta du_value_before_delta. ~(du_index_before_delta=0) -> (exists pvs_le_gap_before_deltabound. pvs_le_gap_before_deltabound + (du_index_before_delta) = (N)) -> (exists dst_positive_code_before_deltaentry dst_positive_scale_before_deltaentry dst_negative_code_before_deltaentry dst_negative_scale_before_deltaentry dst_positive_before_deltaentry dst_negative_before_deltaentry. (((E) = (((((dst_positive_code_before_deltaentry) + (dst_positive_scale_before_deltaentry)) * S ((dst_positive_code_before_deltaentry) + (dst_positive_scale_before_deltaentry)) + ((dst_positive_scale_before_deltaentry) + (dst_positive_scale_before_deltaentry))) + (((dst_negative_code_before_deltaentry) + (dst_negative_scale_before_deltaentry)) * S ((dst_negative_code_before_deltaentry) + (dst_negative_scale_before_deltaentry)) + ((dst_negative_scale_before_deltaentry) + (dst_negative_scale_before_deltaentry)))) * S ((((dst_positive_code_before_deltaentry) + (dst_positive_scale_before_deltaentry)) * S ((dst_positive_code_before_deltaentry) + (dst_positive_scale_before_deltaentry)) + ((dst_positive_scale_before_deltaentry) + (dst_positive_scale_before_deltaentry))) + (((dst_negative_code_before_deltaentry) + (dst_negative_scale_before_deltaentry)) * S ((dst_negative_code_before_deltaentry) + (dst_negative_scale_before_deltaentry)) + ((dst_negative_scale_before_deltaentry) + (dst_negative_scale_before_deltaentry)))) + ((((dst_negative_code_before_deltaentry) + (dst_negative_scale_before_deltaentry)) * S ((dst_negative_code_before_deltaentry) + (dst_negative_scale_before_deltaentry)) + ((dst_negative_scale_before_deltaentry) + (dst_negative_scale_before_deltaentry))) + (((dst_negative_code_before_deltaentry) + (dst_negative_scale_before_deltaentry)) * S ((dst_negative_code_before_deltaentry) + (dst_negative_scale_before_deltaentry)) + ((dst_negative_scale_before_deltaentry) + (dst_negative_scale_before_deltaentry)))))) /\ (((((exists ff_h_pvs_before_deltaentrypositive. ff_h_pvs_before_deltaentrypositive + S (dst_positive_before_deltaentry) = S ((S (du_index_before_delta)) * dst_positive_scale_before_deltaentry)) /\ exists ff_q_pvs_before_deltaentrypositive. dst_positive_code_before_deltaentry = ff_q_pvs_before_deltaentrypositive * S ((S (du_index_before_delta)) * dst_positive_scale_before_deltaentry) + (dst_positive_before_deltaentry))) /\ (((((exists ff_h_pvs_before_deltaentrynegative. ff_h_pvs_before_deltaentrynegative + S (dst_negative_before_deltaentry) = S ((S (du_index_before_delta)) * dst_negative_scale_before_deltaentry)) /\ exists ff_q_pvs_before_deltaentrynegative. dst_negative_code_before_deltaentry = ff_q_pvs_before_deltaentrynegative * S ((S (du_index_before_delta)) * dst_negative_scale_before_deltaentry) + (dst_negative_before_deltaentry))) /\ (exists ge_balance_positive_before_deltaentryvalue ge_balance_negative_before_deltaentryvalue. (((((du_value_before_delta) = 2 * (ge_balance_positive_before_deltaentryvalue) /\ (ge_balance_negative_before_deltaentryvalue) = 0) \/ exists ge_signed_half_before_deltaentryvaluedecode. (((du_value_before_delta) = 2 * ge_signed_half_before_deltaentryvaluedecode + 1 /\ (ge_balance_positive_before_deltaentryvalue) = 0) /\ (ge_balance_negative_before_deltaentryvalue) = S ge_signed_half_before_deltaentryvaluedecode))) /\ ((dst_positive_before_deltaentry) + ge_balance_negative_before_deltaentryvalue = (dst_negative_before_deltaentry) + ge_balance_positive_before_deltaentryvalue))))))))) -> ((((du_index_before_delta)=1 -> (du_value_before_delta)=2) /\ (~((du_index_before_delta)=1) -> (du_value_before_delta)=0)))))) -> ~(n=0) -> (exists pvs_le_gap_before_domain. pvs_le_gap_before_domain + (n) = (N)) -> (exists pvs_gap_before_index. pvs_gap_before_index + S (d) = (n)) -> ((((~((d)=0)) /\ (exists dc_quotient_before_entry dc_left_before_entry dc_right_before_entry. (((n)=(d)*dc_quotient_before_entry) /\ (((exists dst_positive_code_before_entryleft dst_positive_scale_before_entryleft dst_negative_code_before_entryleft dst_negative_scale_before_entryleft dst_positive_before_entryleft dst_negative_before_entryleft. (((F) = (((((dst_positive_code_before_entryleft) + (dst_positive_scale_before_entryleft)) * S ((dst_positive_code_before_entryleft) + (dst_positive_scale_before_entryleft)) + ((dst_positive_scale_before_entryleft) + (dst_positive_scale_before_entryleft))) + (((dst_negative_code_before_entryleft) + (dst_negative_scale_before_entryleft)) * S ((dst_negative_code_before_entryleft) + (dst_negative_scale_before_entryleft)) + ((dst_negative_scale_before_entryleft) + (dst_negative_scale_before_entryleft)))) * S ((((dst_positive_code_before_entryleft) + (dst_positive_scale_before_entryleft)) * S ((dst_positive_code_before_entryleft) + (dst_positive_scale_before_entryleft)) + ((dst_positive_scale_before_entryleft) + (dst_positive_scale_before_entryleft))) + (((dst_negative_code_before_entryleft) + (dst_negative_scale_before_entryleft)) * S ((dst_negative_code_before_entryleft) + (dst_negative_scale_before_entryleft)) + ((dst_negative_scale_before_entryleft) + (dst_negative_scale_before_entryleft)))) + ((((dst_negative_code_before_entryleft) + (dst_negative_scale_before_entryleft)) * S ((dst_negative_code_before_entryleft) + (dst_negative_scale_before_entryleft)) + ((dst_negative_scale_before_entryleft) + (dst_negative_scale_before_entryleft))) + (((dst_negative_code_before_entryleft) + (dst_negative_scale_before_entryleft)) * S ((dst_negative_code_before_entryleft) + (dst_negative_scale_before_entryleft)) + ((dst_negative_scale_before_entryleft) + (dst_negative_scale_before_entryleft)))))) /\ (((((exists ff_h_pvs_before_entryleftpositive. ff_h_pvs_before_entryleftpositive + S (dst_positive_before_entryleft) = S ((S (d)) * dst_positive_scale_before_entryleft)) /\ exists ff_q_pvs_before_entryleftpositive. dst_positive_code_before_entryleft = ff_q_pvs_before_entryleftpositive * S ((S (d)) * dst_positive_scale_before_entryleft) + (dst_positive_before_entryleft))) /\ (((((exists ff_h_pvs_before_entryleftnegative. ff_h_pvs_before_entryleftnegative + S (dst_negative_before_entryleft) = S ((S (d)) * dst_negative_scale_before_entryleft)) /\ exists ff_q_pvs_before_entryleftnegative. dst_negative_code_before_entryleft = ff_q_pvs_before_entryleftnegative * S ((S (d)) * dst_negative_scale_before_entryleft) + (dst_negative_before_entryleft))) /\ (exists ge_balance_positive_before_entryleftvalue ge_balance_negative_before_entryleftvalue. (((((dc_left_before_entry) = 2 * (ge_balance_positive_before_entryleftvalue) /\ (ge_balance_negative_before_entryleftvalue) = 0) \/ exists ge_signed_half_before_entryleftvaluedecode. (((dc_left_before_entry) = 2 * ge_signed_half_before_entryleftvaluedecode + 1 /\ (ge_balance_positive_before_entryleftvalue) = 0) /\ (ge_balance_negative_before_entryleftvalue) = S ge_signed_half_before_entryleftvaluedecode))) /\ ((dst_positive_before_entryleft) + ge_balance_negative_before_entryleftvalue = (dst_negative_before_entryleft) + ge_balance_positive_before_entryleftvalue))))))))) /\ (((exists dst_positive_code_before_entryright dst_positive_scale_before_entryright dst_negative_code_before_entryright dst_negative_scale_before_entryright dst_positive_before_entryright dst_negative_before_entryright. (((E) = (((((dst_positive_code_before_entryright) + (dst_positive_scale_before_entryright)) * S ((dst_positive_code_before_entryright) + (dst_positive_scale_before_entryright)) + ((dst_positive_scale_before_entryright) + (dst_positive_scale_before_entryright))) + (((dst_negative_code_before_entryright) + (dst_negative_scale_before_entryright)) * S ((dst_negative_code_before_entryright) + (dst_negative_scale_before_entryright)) + ((dst_negative_scale_before_entryright) + (dst_negative_scale_before_entryright)))) * S ((((dst_positive_code_before_entryright) + (dst_positive_scale_before_entryright)) * S ((dst_positive_code_before_entryright) + (dst_positive_scale_before_entryright)) + ((dst_positive_scale_before_entryright) + (dst_positive_scale_before_entryright))) + (((dst_negative_code_before_entryright) + (dst_negative_scale_before_entryright)) * S ((dst_negative_code_before_entryright) + (dst_negative_scale_before_entryright)) + ((dst_negative_scale_before_entryright) + (dst_negative_scale_before_entryright)))) + ((((dst_negative_code_before_entryright) + (dst_negative_scale_before_entryright)) * S ((dst_negative_code_before_entryright) + (dst_negative_scale_before_entryright)) + ((dst_negative_scale_before_entryright) + (dst_negative_scale_before_entryright))) + (((dst_negative_code_before_entryright) + (dst_negative_scale_before_entryright)) * S ((dst_negative_code_before_entryright) + (dst_negative_scale_before_entryright)) + ((dst_negative_scale_before_entryright) + (dst_negative_scale_before_entryright)))))) /\ (((((exists ff_h_pvs_before_entryrightpositive. ff_h_pvs_before_entryrightpositive + S (dst_positive_before_entryright) = S ((S (dc_quotient_before_entry)) * dst_positive_scale_before_entryright)) /\ exists ff_q_pvs_before_entryrightpositive. dst_positive_code_before_entryright = ff_q_pvs_before_entryrightpositive * S ((S (dc_quotient_before_entry)) * dst_positive_scale_before_entryright) + (dst_positive_before_entryright))) /\ (((((exists ff_h_pvs_before_entryrightnegative. ff_h_pvs_before_entryrightnegative + S (dst_negative_before_entryright) = S ((S (dc_quotient_before_entry)) * dst_negative_scale_before_entryright)) /\ exists ff_q_pvs_before_entryrightnegative. dst_negative_code_before_entryright = ff_q_pvs_before_entryrightnegative * S ((S (dc_quotient_before_entry)) * dst_negative_scale_before_entryright) + (dst_negative_before_entryright))) /\ (exists ge_balance_positive_before_entryrightvalue ge_balance_negative_before_entryrightvalue. (((((dc_right_before_entry) = 2 * (ge_balance_positive_before_entryrightvalue) /\ (ge_balance_negative_before_entryrightvalue) = 0) \/ exists ge_signed_half_before_entryrightvaluedecode. (((dc_right_before_entry) = 2 * ge_signed_half_before_entryrightvaluedecode + 1 /\ (ge_balance_positive_before_entryrightvalue) = 0) /\ (ge_balance_negative_before_entryrightvalue) = S ge_signed_half_before_entryrightvaluedecode))) /\ ((dst_positive_before_entryright) + ge_balance_negative_before_entryrightvalue = (dst_negative_before_entryright) + ge_balance_positive_before_entryrightvalue))))))))) /\ (exists sto_ap_before_entryproduct sto_an_before_entryproduct sto_bp_before_entryproduct sto_bn_before_entryproduct sto_cp_before_entryproduct sto_cn_before_entryproduct. (((((dc_left_before_entry) = 2 * (sto_ap_before_entryproduct) /\ (sto_an_before_entryproduct) = 0) \/ exists ge_signed_half_before_entryproductleft. (((dc_left_before_entry) = 2 * ge_signed_half_before_entryproductleft + 1 /\ (sto_ap_before_entryproduct) = 0) /\ (sto_an_before_entryproduct) = S ge_signed_half_before_entryproductleft))) /\ ((((((dc_right_before_entry) = 2 * (sto_bp_before_entryproduct) /\ (sto_bn_before_entryproduct) = 0) \/ exists ge_signed_half_before_entryproductright. (((dc_right_before_entry) = 2 * ge_signed_half_before_entryproductright + 1 /\ (sto_bp_before_entryproduct) = 0) /\ (sto_bn_before_entryproduct) = S ge_signed_half_before_entryproductright))) /\ ((((((z) = 2 * (sto_cp_before_entryproduct) /\ (sto_cn_before_entryproduct) = 0) \/ exists ge_signed_half_before_entryproductoutput. (((z) = 2 * ge_signed_half_before_entryproductoutput + 1 /\ (sto_cp_before_entryproduct) = 0) /\ (sto_cn_before_entryproduct) = S ge_signed_half_before_entryproductoutput))) /\ ((sto_ap_before_entryproduct * sto_bp_before_entryproduct + sto_an_before_entryproduct * sto_bn_before_entryproduct) + sto_cn_before_entryproduct = (sto_ap_before_entryproduct * sto_bn_before_entryproduct + sto_an_before_entryproduct * sto_bp_before_entryproduct) + sto_cp_before_entryproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_before_entrynondivisor. (n) = (d) * pvs_factor_before_entrynondivisor)) /\ ((z)=0)))) -> z=0

Complete tactic proof in conservative notation

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

81 script commands · 19 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 (1)
dirichlet kronecker delta table other value
01Fix variables and assumptionsL1–10

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro E
  4. L4
    intro n
  5. L5
    intro d
  6. L6
    intro z
  7. L7
    intro hd
  8. L8
    intro hn
  9. L9
    intro hb
  10. L10
    intro hbefore
02Fix variables and assumptionsL11–11

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

  1. L11
    intro he
03Separate the logical casesL12–19

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

  1. L12
    cases he
  2. L13
    cases he_left
  3. L14
    cases he_left_right
  4. L15
    cases he_left_right_witness
  5. L16
    cases he_left_right_witness_witness
  6. L17
    cases he_left_right_witness_witness_witness
  7. L18
    cases he_left_right_witness_witness_witness_right
  8. L19
    cases he_left_right_witness_witness_witness_right_right
04Establish hqpositiveL20–28

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

  1. L20
    have hqpositive : ~(x=0)
  2. L21
    intro hqzero
  3. L22
    specialize factor_nonzero_right (n)
  4. L23
    specialize factor_nonzero_right (d)
  5. L24
    specialize factor_nonzero_right (x)
  6. L25
    apply factor_nonzero_right
  7. L26
    exact hn
  8. L27
    exact he_left_right_witness_witness_witness_left
  9. L28
    exact hqzero
05Establish hqboundL29–37

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

  1. L29
    have hqbound : Le(x,N)Definitions: Le(x,N)Original native command in the exact edition
  2. L30
    specialize le_trans (x)
  3. L31
    specialize le_trans (n)
  4. L32
    specialize le_trans (N)
  5. L33
    apply le_trans
  6. L34
    specialize divisor_le_nonzero (x)
  7. L35
    specialize divisor_le_nonzero (n)
  8. L36
    apply divisor_le_nonzero
  9. L37
    exact hn
06Construct an explicit witnessL38–38

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

  1. L38
    exists d
07Calculate and transport equalitiesL39–39

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

  1. L39
    trans (d)*(x)
08Use earlier factsL40–42

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

  1. L40
    exact he_left_right_witness_witness_witness_left
  2. L41
    apply mul_comm
  3. L42
    exact hb
09Establish hqnotoneL43–44

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

  1. L43
    have hqnotone : ~(x=1)
  2. L44
    intro hqone
10Establish heqL45–54

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

  1. L45
    have heq : n=d
  2. L46
    trans d*x
  3. L47
    exact he_left_right_witness_witness_witness_left
  4. L48
    trans d*1
  5. L49
    rewrite hqone
  6. L50
    refl
  7. L51
    apply mul_one
  8. L52
    specialize lt_not_le (d)
  9. L53
    specialize lt_not_le (n)
  10. L54
    apply lt_not_le
11Use earlier factsL55–55

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

  1. L55
    exact hbefore
12Calculate and transport equalitiesL56–56

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

  1. L56
    rewrite heq
13Use earlier factsL57–58

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

  1. L57
    specialize le_refl (d)
  2. L58
    apply le_refl
14Establish hzeroL59–68

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet kronecker delta table other value.

  1. L59
    have hzero : x2=0
  2. L60
    specialize dirichlet_kronecker_delta_table_other_value (N)
  3. L61
    specialize dirichlet_kronecker_delta_table_other_value (E)
  4. L62
    specialize dirichlet_kronecker_delta_table_other_value (x)
  5. L63
    specialize dirichlet_kronecker_delta_table_other_value (x2)
  6. L64
    apply dirichlet_kronecker_delta_table_other_value
  7. L65
    exact hd
  8. L66
    exact hqpositive
  9. L67
    exact hqnotone
  10. L68
    exact hqbound
15Use earlier factsL69–69

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

  1. L69
    exact he_left_right_witness_witness_witness_right_right_left
16Calculate and transport equalitiesL70–71

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

  1. L70
    rewrite hzero at he_left_right_witness_witness_witness_right_right_right
  2. L71
    rewrite hzero at he_left_right_witness_witness_witness_right_right_right
17Use earlier factsL72–79

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

  1. L72
    specialize signed_mul_functional (x1)
  2. L73
    specialize signed_mul_functional (0)
  3. L74
    specialize signed_mul_functional (z)
  4. L75
    specialize signed_mul_functional (0)
  5. L76
    apply signed_mul_functional
  6. L77
    exact he_left_right_witness_witness_witness_right_right_right
  7. L78
    specialize signed_mul_zero_right (x1)
  8. L79
    apply signed_mul_zero_right
18Separate the logical casesL80–80

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

  1. L80
    cases he_right
19Use earlier factsL81–81

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

  1. L81
    exact he_right_right

Library-wide reading audit

Original defined command ledger · 81 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro E
  4. 0004intro n
  5. 0005intro d
  6. 0006intro z
  7. 0007intro hd
  8. 0008intro hn
  9. 0009intro hb
  10. 0010intro hbefore
  11. 0011intro he
  12. 0012cases he
  13. 0013cases he_left
  14. 0014cases he_left_right
  15. 0015cases he_left_right_witness
  16. 0016cases he_left_right_witness_witness
  17. 0017cases he_left_right_witness_witness_witness
  18. 0018cases he_left_right_witness_witness_witness_right
  19. 0019cases he_left_right_witness_witness_witness_right_right
  20. 0020have hqpositive : ~(x=0)
  21. 0021intro hqzero
  22. 0022specialize factor_nonzero_right (n)
  23. 0023specialize factor_nonzero_right (d)
  24. 0024specialize factor_nonzero_right (x)
  25. 0025apply factor_nonzero_right
  26. 0026exact hn
  27. 0027exact he_left_right_witness_witness_witness_left
  28. 0028exact hqzero
  29. 0029have hqbound : Le(x,N)
  30. 0030specialize le_trans (x)
  31. 0031specialize le_trans (n)
  32. 0032specialize le_trans (N)
  33. 0033apply le_trans
  34. 0034specialize divisor_le_nonzero (x)
  35. 0035specialize divisor_le_nonzero (n)
  36. 0036apply divisor_le_nonzero
  37. 0037exact hn
  38. 0038exists d
  39. 0039trans (d)*(x)
  40. 0040exact he_left_right_witness_witness_witness_left
  41. 0041apply mul_comm
  42. 0042exact hb
  43. 0043have hqnotone : ~(x=1)
  44. 0044intro hqone
  45. 0045have heq : n=d
  46. 0046trans d*x
  47. 0047exact he_left_right_witness_witness_witness_left
  48. 0048trans d*1
  49. 0049rewrite hqone
  50. 0050refl
  51. 0051apply mul_one
  52. 0052specialize lt_not_le (d)
  53. 0053specialize lt_not_le (n)
  54. 0054apply lt_not_le
  55. 0055exact hbefore
  56. 0056rewrite heq
  57. 0057specialize le_refl (d)
  58. 0058apply le_refl
  59. 0059have hzero : x2=0
  60. 0060specialize dirichlet_kronecker_delta_table_other_value (N)
  61. 0061specialize dirichlet_kronecker_delta_table_other_value (E)
  62. 0062specialize dirichlet_kronecker_delta_table_other_value (x)
  63. 0063specialize dirichlet_kronecker_delta_table_other_value (x2)
  64. 0064apply dirichlet_kronecker_delta_table_other_value
  65. 0065exact hd
  66. 0066exact hqpositive
  67. 0067exact hqnotone
  68. 0068exact hqbound
  69. 0069exact he_left_right_witness_witness_witness_right_right_left
  70. 0070rewrite hzero at he_left_right_witness_witness_witness_right_right_right
  71. 0071rewrite hzero at he_left_right_witness_witness_witness_right_right_right
  72. 0072specialize signed_mul_functional (x1)
  73. 0073specialize signed_mul_functional (0)
  74. 0074specialize signed_mul_functional (z)
  75. 0075specialize signed_mul_functional (0)
  76. 0076apply signed_mul_functional
  77. 0077exact he_left_right_witness_witness_witness_right_right_right
  78. 0078specialize signed_mul_zero_right (x1)
  79. 0079apply signed_mul_zero_right
  80. 0080cases he_right
  81. 0081exact he_right_right