MX004D

signed_mul_nonzero_factors

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

A nonzero actual signed product has two nonzero factors, by the signed zero laws and functionality.

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

Exact expanded first-order arithmetic statement

forall a b z. (exists sto_ap_nonzero_product sto_an_nonzero_product sto_bp_nonzero_product sto_bn_nonzero_product sto_cp_nonzero_product sto_cn_nonzero_product. (((((a) = 2 * (sto_ap_nonzero_product) /\ (sto_an_nonzero_product) = 0) \/ exists ge_signed_half_nonzero_productleft. (((a) = 2 * ge_signed_half_nonzero_productleft + 1 /\ (sto_ap_nonzero_product) = 0) /\ (sto_an_nonzero_product) = S ge_signed_half_nonzero_productleft))) /\ ((((((b) = 2 * (sto_bp_nonzero_product) /\ (sto_bn_nonzero_product) = 0) \/ exists ge_signed_half_nonzero_productright. (((b) = 2 * ge_signed_half_nonzero_productright + 1 /\ (sto_bp_nonzero_product) = 0) /\ (sto_bn_nonzero_product) = S ge_signed_half_nonzero_productright))) /\ ((((((z) = 2 * (sto_cp_nonzero_product) /\ (sto_cn_nonzero_product) = 0) \/ exists ge_signed_half_nonzero_productoutput. (((z) = 2 * ge_signed_half_nonzero_productoutput + 1 /\ (sto_cp_nonzero_product) = 0) /\ (sto_cn_nonzero_product) = S ge_signed_half_nonzero_productoutput))) /\ ((sto_ap_nonzero_product * sto_bp_nonzero_product + sto_an_nonzero_product * sto_bn_nonzero_product) + sto_cn_nonzero_product = (sto_ap_nonzero_product * sto_bn_nonzero_product + sto_an_nonzero_product * sto_bp_nonzero_product) + sto_cp_nonzero_product))))))) -> ~(z=0) -> (~(a=0) /\ ~(b=0))

Constructive proof overview

Generated structural guide

A nonzero actual signed product has two nonzero factors, by the signed zero laws and functionality.

The unchanged tactic script uses 3 declared prerequisites and contains 30 exact native proof lines.

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

Proof neighborhood

Direct dependencies

signed_mul_functional Alpha theorem; checked-use authorized signed_mul_zero_left Alpha theorem; checked-use authorized signed_mul_zero_right Alpha theorem; checked-use authorized

Direct dependents

MX0051 dirichlet_coprime_grid_nonzero_coordinates

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

30 script commands · 10 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–5

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro z
  4. L4
    intro hp
  5. L5
    intro hz
02Separate the logical casesL6–6

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

  1. L6
    split
03Fix variables and assumptionsL7–7

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

  1. L7
    intro ha
04Use earlier factsL8–8

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

  1. L8
    apply hz
05Calculate and transport equalitiesL9–10

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

  1. L9
    rewrite ha at hp
  2. L10
    rewrite ha at hp
06Use earlier factsL11–18

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

  1. L11
    specialize signed_mul_functional (0)
  2. L12
    specialize signed_mul_functional (b)
  3. L13
    specialize signed_mul_functional (z)
  4. L14
    specialize signed_mul_functional (0)
  5. L15
    apply signed_mul_functional
  6. L16
    exact hp
  7. L17
    specialize signed_mul_zero_left (b)
  8. L18
    apply signed_mul_zero_left
07Fix variables and assumptionsL19–19

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

  1. L19
    intro hb
08Use earlier factsL20–20

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

  1. L20
    apply hz
09Calculate and transport equalitiesL21–22

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

  1. L21
    rewrite hb at hp
  2. L22
    rewrite hb at hp
10Use earlier factsL23–30

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

  1. L23
    specialize signed_mul_functional (a)
  2. L24
    specialize signed_mul_functional (0)
  3. L25
    specialize signed_mul_functional (z)
  4. L26
    specialize signed_mul_functional (0)
  5. L27
    apply signed_mul_functional
  6. L28
    exact hp
  7. L29
    specialize signed_mul_zero_right (a)
  8. L30
    apply signed_mul_zero_right

Library-wide reading audit

Original exact command ledger · 30 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro z
  4. 0004intro hp
  5. 0005intro hz
  6. 0006split
  7. 0007intro ha
  8. 0008apply hz
  9. 0009rewrite ha at hp
  10. 0010rewrite ha at hp
  11. 0011specialize signed_mul_functional (0)
  12. 0012specialize signed_mul_functional (b)
  13. 0013specialize signed_mul_functional (z)
  14. 0014specialize signed_mul_functional (0)
  15. 0015apply signed_mul_functional
  16. 0016exact hp
  17. 0017specialize signed_mul_zero_left (b)
  18. 0018apply signed_mul_zero_left
  19. 0019intro hb
  20. 0020apply hz
  21. 0021rewrite hb at hp
  22. 0022rewrite hb at hp
  23. 0023specialize signed_mul_functional (a)
  24. 0024specialize signed_mul_functional (0)
  25. 0025specialize signed_mul_functional (z)
  26. 0026specialize signed_mul_functional (0)
  27. 0027apply signed_mul_functional
  28. 0028exact hp
  29. 0029specialize signed_mul_zero_right (a)
  30. 0030apply signed_mul_zero_right