DC0014

dirichlet_convolution_entry_positive_source_extensional

Only positive in-domain source values matter: a genuine quotient is proved positive and bounded before either source equality is applied.

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. ∀ H. ∀ K. ∀ n. ∀ d. ∀ a. ∀ b. ¬n = 0 → ArithPositiveEqual(F,H,n) → ArithPositiveEqual(G,K,n) → Le(d,n) → DirichletEntry(F,G,n,d,a) → DirichletEntry(H,K,n,d,b) → a = b

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

Definition DAG

ArithPositiveEqual(F,G,N) · 2DirichletEntry(F,G,n,d,z) · 2Le(a,b) · 2

Actual proof prerequisites

mul_left_cancel_nonzero · checked external prerequisitefactor_nonzero_right · checked external prerequisitedivisor_le_nonzero · checked external prerequisitemul_comm · checked external prerequisitesigned_mul_functional · checked external prerequisite
Original expanded first-order statement 
forall F G H K n d a b. ~(n=0) -> (forall dm_index_source_equal_left dm_first_value_source_equal_left dm_second_value_source_equal_left. ~(dm_index_source_equal_left=0) -> (exists pvs_le_gap_source_equal_leftdomain. pvs_le_gap_source_equal_leftdomain + (dm_index_source_equal_left) = (n)) -> (exists dst_positive_code_source_equal_leftfirst dst_positive_scale_source_equal_leftfirst dst_negative_code_source_equal_leftfirst dst_negative_scale_source_equal_leftfirst dst_positive_source_equal_leftfirst dst_negative_source_equal_leftfirst. (((F) = (((((dst_positive_code_source_equal_leftfirst) + (dst_positive_scale_source_equal_leftfirst)) * S ((dst_positive_code_source_equal_leftfirst) + (dst_positive_scale_source_equal_leftfirst)) + ((dst_positive_scale_source_equal_leftfirst) + (dst_positive_scale_source_equal_leftfirst))) + (((dst_negative_code_source_equal_leftfirst) + (dst_negative_scale_source_equal_leftfirst)) * S ((dst_negative_code_source_equal_leftfirst) + (dst_negative_scale_source_equal_leftfirst)) + ((dst_negative_scale_source_equal_leftfirst) + (dst_negative_scale_source_equal_leftfirst)))) * S ((((dst_positive_code_source_equal_leftfirst) + (dst_positive_scale_source_equal_leftfirst)) * S ((dst_positive_code_source_equal_leftfirst) + (dst_positive_scale_source_equal_leftfirst)) + ((dst_positive_scale_source_equal_leftfirst) + (dst_positive_scale_source_equal_leftfirst))) + (((dst_negative_code_source_equal_leftfirst) + (dst_negative_scale_source_equal_leftfirst)) * S ((dst_negative_code_source_equal_leftfirst) + (dst_negative_scale_source_equal_leftfirst)) + ((dst_negative_scale_source_equal_leftfirst) + (dst_negative_scale_source_equal_leftfirst)))) + ((((dst_negative_code_source_equal_leftfirst) + (dst_negative_scale_source_equal_leftfirst)) * S ((dst_negative_code_source_equal_leftfirst) + (dst_negative_scale_source_equal_leftfirst)) + ((dst_negative_scale_source_equal_leftfirst) + (dst_negative_scale_source_equal_leftfirst))) + (((dst_negative_code_source_equal_leftfirst) + (dst_negative_scale_source_equal_leftfirst)) * S ((dst_negative_code_source_equal_leftfirst) + (dst_negative_scale_source_equal_leftfirst)) + ((dst_negative_scale_source_equal_leftfirst) + (dst_negative_scale_source_equal_leftfirst)))))) /\ (((((exists ff_h_pvs_source_equal_leftfirstpositive. ff_h_pvs_source_equal_leftfirstpositive + S (dst_positive_source_equal_leftfirst) = S ((S (dm_index_source_equal_left)) * dst_positive_scale_source_equal_leftfirst)) /\ exists ff_q_pvs_source_equal_leftfirstpositive. dst_positive_code_source_equal_leftfirst = ff_q_pvs_source_equal_leftfirstpositive * S ((S (dm_index_source_equal_left)) * dst_positive_scale_source_equal_leftfirst) + (dst_positive_source_equal_leftfirst))) /\ (((((exists ff_h_pvs_source_equal_leftfirstnegative. ff_h_pvs_source_equal_leftfirstnegative + S (dst_negative_source_equal_leftfirst) = S ((S (dm_index_source_equal_left)) * dst_negative_scale_source_equal_leftfirst)) /\ exists ff_q_pvs_source_equal_leftfirstnegative. dst_negative_code_source_equal_leftfirst = ff_q_pvs_source_equal_leftfirstnegative * S ((S (dm_index_source_equal_left)) * dst_negative_scale_source_equal_leftfirst) + (dst_negative_source_equal_leftfirst))) /\ (exists ge_balance_positive_source_equal_leftfirstvalue ge_balance_negative_source_equal_leftfirstvalue. (((((dm_first_value_source_equal_left) = 2 * (ge_balance_positive_source_equal_leftfirstvalue) /\ (ge_balance_negative_source_equal_leftfirstvalue) = 0) \/ exists ge_signed_half_source_equal_leftfirstvaluedecode. (((dm_first_value_source_equal_left) = 2 * ge_signed_half_source_equal_leftfirstvaluedecode + 1 /\ (ge_balance_positive_source_equal_leftfirstvalue) = 0) /\ (ge_balance_negative_source_equal_leftfirstvalue) = S ge_signed_half_source_equal_leftfirstvaluedecode))) /\ ((dst_positive_source_equal_leftfirst) + ge_balance_negative_source_equal_leftfirstvalue = (dst_negative_source_equal_leftfirst) + ge_balance_positive_source_equal_leftfirstvalue))))))))) -> (exists dst_positive_code_source_equal_leftsecond dst_positive_scale_source_equal_leftsecond dst_negative_code_source_equal_leftsecond dst_negative_scale_source_equal_leftsecond dst_positive_source_equal_leftsecond dst_negative_source_equal_leftsecond. (((H) = (((((dst_positive_code_source_equal_leftsecond) + (dst_positive_scale_source_equal_leftsecond)) * S ((dst_positive_code_source_equal_leftsecond) + (dst_positive_scale_source_equal_leftsecond)) + ((dst_positive_scale_source_equal_leftsecond) + (dst_positive_scale_source_equal_leftsecond))) + (((dst_negative_code_source_equal_leftsecond) + (dst_negative_scale_source_equal_leftsecond)) * S ((dst_negative_code_source_equal_leftsecond) + (dst_negative_scale_source_equal_leftsecond)) + ((dst_negative_scale_source_equal_leftsecond) + (dst_negative_scale_source_equal_leftsecond)))) * S ((((dst_positive_code_source_equal_leftsecond) + (dst_positive_scale_source_equal_leftsecond)) * S ((dst_positive_code_source_equal_leftsecond) + (dst_positive_scale_source_equal_leftsecond)) + ((dst_positive_scale_source_equal_leftsecond) + (dst_positive_scale_source_equal_leftsecond))) + (((dst_negative_code_source_equal_leftsecond) + (dst_negative_scale_source_equal_leftsecond)) * S ((dst_negative_code_source_equal_leftsecond) + (dst_negative_scale_source_equal_leftsecond)) + ((dst_negative_scale_source_equal_leftsecond) + (dst_negative_scale_source_equal_leftsecond)))) + ((((dst_negative_code_source_equal_leftsecond) + (dst_negative_scale_source_equal_leftsecond)) * S ((dst_negative_code_source_equal_leftsecond) + (dst_negative_scale_source_equal_leftsecond)) + ((dst_negative_scale_source_equal_leftsecond) + (dst_negative_scale_source_equal_leftsecond))) + (((dst_negative_code_source_equal_leftsecond) + (dst_negative_scale_source_equal_leftsecond)) * S ((dst_negative_code_source_equal_leftsecond) + (dst_negative_scale_source_equal_leftsecond)) + ((dst_negative_scale_source_equal_leftsecond) + (dst_negative_scale_source_equal_leftsecond)))))) /\ (((((exists ff_h_pvs_source_equal_leftsecondpositive. ff_h_pvs_source_equal_leftsecondpositive + S (dst_positive_source_equal_leftsecond) = S ((S (dm_index_source_equal_left)) * dst_positive_scale_source_equal_leftsecond)) /\ exists ff_q_pvs_source_equal_leftsecondpositive. dst_positive_code_source_equal_leftsecond = ff_q_pvs_source_equal_leftsecondpositive * S ((S (dm_index_source_equal_left)) * dst_positive_scale_source_equal_leftsecond) + (dst_positive_source_equal_leftsecond))) /\ (((((exists ff_h_pvs_source_equal_leftsecondnegative. ff_h_pvs_source_equal_leftsecondnegative + S (dst_negative_source_equal_leftsecond) = S ((S (dm_index_source_equal_left)) * dst_negative_scale_source_equal_leftsecond)) /\ exists ff_q_pvs_source_equal_leftsecondnegative. dst_negative_code_source_equal_leftsecond = ff_q_pvs_source_equal_leftsecondnegative * S ((S (dm_index_source_equal_left)) * dst_negative_scale_source_equal_leftsecond) + (dst_negative_source_equal_leftsecond))) /\ (exists ge_balance_positive_source_equal_leftsecondvalue ge_balance_negative_source_equal_leftsecondvalue. (((((dm_second_value_source_equal_left) = 2 * (ge_balance_positive_source_equal_leftsecondvalue) /\ (ge_balance_negative_source_equal_leftsecondvalue) = 0) \/ exists ge_signed_half_source_equal_leftsecondvaluedecode. (((dm_second_value_source_equal_left) = 2 * ge_signed_half_source_equal_leftsecondvaluedecode + 1 /\ (ge_balance_positive_source_equal_leftsecondvalue) = 0) /\ (ge_balance_negative_source_equal_leftsecondvalue) = S ge_signed_half_source_equal_leftsecondvaluedecode))) /\ ((dst_positive_source_equal_leftsecond) + ge_balance_negative_source_equal_leftsecondvalue = (dst_negative_source_equal_leftsecond) + ge_balance_positive_source_equal_leftsecondvalue))))))))) -> dm_first_value_source_equal_left=dm_second_value_source_equal_left) -> (forall dm_index_source_equal_right dm_first_value_source_equal_right dm_second_value_source_equal_right. ~(dm_index_source_equal_right=0) -> (exists pvs_le_gap_source_equal_rightdomain. pvs_le_gap_source_equal_rightdomain + (dm_index_source_equal_right) = (n)) -> (exists dst_positive_code_source_equal_rightfirst dst_positive_scale_source_equal_rightfirst dst_negative_code_source_equal_rightfirst dst_negative_scale_source_equal_rightfirst dst_positive_source_equal_rightfirst dst_negative_source_equal_rightfirst. (((G) = (((((dst_positive_code_source_equal_rightfirst) + (dst_positive_scale_source_equal_rightfirst)) * S ((dst_positive_code_source_equal_rightfirst) + (dst_positive_scale_source_equal_rightfirst)) + ((dst_positive_scale_source_equal_rightfirst) + (dst_positive_scale_source_equal_rightfirst))) + (((dst_negative_code_source_equal_rightfirst) + (dst_negative_scale_source_equal_rightfirst)) * S ((dst_negative_code_source_equal_rightfirst) + (dst_negative_scale_source_equal_rightfirst)) + ((dst_negative_scale_source_equal_rightfirst) + (dst_negative_scale_source_equal_rightfirst)))) * S ((((dst_positive_code_source_equal_rightfirst) + (dst_positive_scale_source_equal_rightfirst)) * S ((dst_positive_code_source_equal_rightfirst) + (dst_positive_scale_source_equal_rightfirst)) + ((dst_positive_scale_source_equal_rightfirst) + (dst_positive_scale_source_equal_rightfirst))) + (((dst_negative_code_source_equal_rightfirst) + (dst_negative_scale_source_equal_rightfirst)) * S ((dst_negative_code_source_equal_rightfirst) + (dst_negative_scale_source_equal_rightfirst)) + ((dst_negative_scale_source_equal_rightfirst) + (dst_negative_scale_source_equal_rightfirst)))) + ((((dst_negative_code_source_equal_rightfirst) + (dst_negative_scale_source_equal_rightfirst)) * S ((dst_negative_code_source_equal_rightfirst) + (dst_negative_scale_source_equal_rightfirst)) + ((dst_negative_scale_source_equal_rightfirst) + (dst_negative_scale_source_equal_rightfirst))) + (((dst_negative_code_source_equal_rightfirst) + (dst_negative_scale_source_equal_rightfirst)) * S ((dst_negative_code_source_equal_rightfirst) + (dst_negative_scale_source_equal_rightfirst)) + ((dst_negative_scale_source_equal_rightfirst) + (dst_negative_scale_source_equal_rightfirst)))))) /\ (((((exists ff_h_pvs_source_equal_rightfirstpositive. ff_h_pvs_source_equal_rightfirstpositive + S (dst_positive_source_equal_rightfirst) = S ((S (dm_index_source_equal_right)) * dst_positive_scale_source_equal_rightfirst)) /\ exists ff_q_pvs_source_equal_rightfirstpositive. dst_positive_code_source_equal_rightfirst = ff_q_pvs_source_equal_rightfirstpositive * S ((S (dm_index_source_equal_right)) * dst_positive_scale_source_equal_rightfirst) + (dst_positive_source_equal_rightfirst))) /\ (((((exists ff_h_pvs_source_equal_rightfirstnegative. ff_h_pvs_source_equal_rightfirstnegative + S (dst_negative_source_equal_rightfirst) = S ((S (dm_index_source_equal_right)) * dst_negative_scale_source_equal_rightfirst)) /\ exists ff_q_pvs_source_equal_rightfirstnegative. dst_negative_code_source_equal_rightfirst = ff_q_pvs_source_equal_rightfirstnegative * S ((S (dm_index_source_equal_right)) * dst_negative_scale_source_equal_rightfirst) + (dst_negative_source_equal_rightfirst))) /\ (exists ge_balance_positive_source_equal_rightfirstvalue ge_balance_negative_source_equal_rightfirstvalue. (((((dm_first_value_source_equal_right) = 2 * (ge_balance_positive_source_equal_rightfirstvalue) /\ (ge_balance_negative_source_equal_rightfirstvalue) = 0) \/ exists ge_signed_half_source_equal_rightfirstvaluedecode. (((dm_first_value_source_equal_right) = 2 * ge_signed_half_source_equal_rightfirstvaluedecode + 1 /\ (ge_balance_positive_source_equal_rightfirstvalue) = 0) /\ (ge_balance_negative_source_equal_rightfirstvalue) = S ge_signed_half_source_equal_rightfirstvaluedecode))) /\ ((dst_positive_source_equal_rightfirst) + ge_balance_negative_source_equal_rightfirstvalue = (dst_negative_source_equal_rightfirst) + ge_balance_positive_source_equal_rightfirstvalue))))))))) -> (exists dst_positive_code_source_equal_rightsecond dst_positive_scale_source_equal_rightsecond dst_negative_code_source_equal_rightsecond dst_negative_scale_source_equal_rightsecond dst_positive_source_equal_rightsecond dst_negative_source_equal_rightsecond. (((K) = (((((dst_positive_code_source_equal_rightsecond) + (dst_positive_scale_source_equal_rightsecond)) * S ((dst_positive_code_source_equal_rightsecond) + (dst_positive_scale_source_equal_rightsecond)) + ((dst_positive_scale_source_equal_rightsecond) + (dst_positive_scale_source_equal_rightsecond))) + (((dst_negative_code_source_equal_rightsecond) + (dst_negative_scale_source_equal_rightsecond)) * S ((dst_negative_code_source_equal_rightsecond) + (dst_negative_scale_source_equal_rightsecond)) + ((dst_negative_scale_source_equal_rightsecond) + (dst_negative_scale_source_equal_rightsecond)))) * S ((((dst_positive_code_source_equal_rightsecond) + (dst_positive_scale_source_equal_rightsecond)) * S ((dst_positive_code_source_equal_rightsecond) + (dst_positive_scale_source_equal_rightsecond)) + ((dst_positive_scale_source_equal_rightsecond) + (dst_positive_scale_source_equal_rightsecond))) + (((dst_negative_code_source_equal_rightsecond) + (dst_negative_scale_source_equal_rightsecond)) * S ((dst_negative_code_source_equal_rightsecond) + (dst_negative_scale_source_equal_rightsecond)) + ((dst_negative_scale_source_equal_rightsecond) + (dst_negative_scale_source_equal_rightsecond)))) + ((((dst_negative_code_source_equal_rightsecond) + (dst_negative_scale_source_equal_rightsecond)) * S ((dst_negative_code_source_equal_rightsecond) + (dst_negative_scale_source_equal_rightsecond)) + ((dst_negative_scale_source_equal_rightsecond) + (dst_negative_scale_source_equal_rightsecond))) + (((dst_negative_code_source_equal_rightsecond) + (dst_negative_scale_source_equal_rightsecond)) * S ((dst_negative_code_source_equal_rightsecond) + (dst_negative_scale_source_equal_rightsecond)) + ((dst_negative_scale_source_equal_rightsecond) + (dst_negative_scale_source_equal_rightsecond)))))) /\ (((((exists ff_h_pvs_source_equal_rightsecondpositive. ff_h_pvs_source_equal_rightsecondpositive + S (dst_positive_source_equal_rightsecond) = S ((S (dm_index_source_equal_right)) * dst_positive_scale_source_equal_rightsecond)) /\ exists ff_q_pvs_source_equal_rightsecondpositive. dst_positive_code_source_equal_rightsecond = ff_q_pvs_source_equal_rightsecondpositive * S ((S (dm_index_source_equal_right)) * dst_positive_scale_source_equal_rightsecond) + (dst_positive_source_equal_rightsecond))) /\ (((((exists ff_h_pvs_source_equal_rightsecondnegative. ff_h_pvs_source_equal_rightsecondnegative + S (dst_negative_source_equal_rightsecond) = S ((S (dm_index_source_equal_right)) * dst_negative_scale_source_equal_rightsecond)) /\ exists ff_q_pvs_source_equal_rightsecondnegative. dst_negative_code_source_equal_rightsecond = ff_q_pvs_source_equal_rightsecondnegative * S ((S (dm_index_source_equal_right)) * dst_negative_scale_source_equal_rightsecond) + (dst_negative_source_equal_rightsecond))) /\ (exists ge_balance_positive_source_equal_rightsecondvalue ge_balance_negative_source_equal_rightsecondvalue. (((((dm_second_value_source_equal_right) = 2 * (ge_balance_positive_source_equal_rightsecondvalue) /\ (ge_balance_negative_source_equal_rightsecondvalue) = 0) \/ exists ge_signed_half_source_equal_rightsecondvaluedecode. (((dm_second_value_source_equal_right) = 2 * ge_signed_half_source_equal_rightsecondvaluedecode + 1 /\ (ge_balance_positive_source_equal_rightsecondvalue) = 0) /\ (ge_balance_negative_source_equal_rightsecondvalue) = S ge_signed_half_source_equal_rightsecondvaluedecode))) /\ ((dst_positive_source_equal_rightsecond) + ge_balance_negative_source_equal_rightsecondvalue = (dst_negative_source_equal_rightsecond) + ge_balance_positive_source_equal_rightsecondvalue))))))))) -> dm_first_value_source_equal_right=dm_second_value_source_equal_right) -> (exists pvs_le_gap_source_index_bound. pvs_le_gap_source_index_bound + (d) = (n)) -> ((((~((d)=0)) /\ (exists dc_quotient_source_entry_first dc_left_source_entry_first dc_right_source_entry_first. (((n)=(d)*dc_quotient_source_entry_first) /\ (((exists dst_positive_code_source_entry_firstleft dst_positive_scale_source_entry_firstleft dst_negative_code_source_entry_firstleft dst_negative_scale_source_entry_firstleft dst_positive_source_entry_firstleft dst_negative_source_entry_firstleft. (((F) = (((((dst_positive_code_source_entry_firstleft) + (dst_positive_scale_source_entry_firstleft)) * S ((dst_positive_code_source_entry_firstleft) + (dst_positive_scale_source_entry_firstleft)) + ((dst_positive_scale_source_entry_firstleft) + (dst_positive_scale_source_entry_firstleft))) + (((dst_negative_code_source_entry_firstleft) + (dst_negative_scale_source_entry_firstleft)) * S ((dst_negative_code_source_entry_firstleft) + (dst_negative_scale_source_entry_firstleft)) + ((dst_negative_scale_source_entry_firstleft) + (dst_negative_scale_source_entry_firstleft)))) * S ((((dst_positive_code_source_entry_firstleft) + (dst_positive_scale_source_entry_firstleft)) * S ((dst_positive_code_source_entry_firstleft) + (dst_positive_scale_source_entry_firstleft)) + ((dst_positive_scale_source_entry_firstleft) + (dst_positive_scale_source_entry_firstleft))) + (((dst_negative_code_source_entry_firstleft) + (dst_negative_scale_source_entry_firstleft)) * S ((dst_negative_code_source_entry_firstleft) + (dst_negative_scale_source_entry_firstleft)) + ((dst_negative_scale_source_entry_firstleft) + (dst_negative_scale_source_entry_firstleft)))) + ((((dst_negative_code_source_entry_firstleft) + (dst_negative_scale_source_entry_firstleft)) * S ((dst_negative_code_source_entry_firstleft) + (dst_negative_scale_source_entry_firstleft)) + ((dst_negative_scale_source_entry_firstleft) + (dst_negative_scale_source_entry_firstleft))) + (((dst_negative_code_source_entry_firstleft) + (dst_negative_scale_source_entry_firstleft)) * S ((dst_negative_code_source_entry_firstleft) + (dst_negative_scale_source_entry_firstleft)) + ((dst_negative_scale_source_entry_firstleft) + (dst_negative_scale_source_entry_firstleft)))))) /\ (((((exists ff_h_pvs_source_entry_firstleftpositive. ff_h_pvs_source_entry_firstleftpositive + S (dst_positive_source_entry_firstleft) = S ((S (d)) * dst_positive_scale_source_entry_firstleft)) /\ exists ff_q_pvs_source_entry_firstleftpositive. dst_positive_code_source_entry_firstleft = ff_q_pvs_source_entry_firstleftpositive * S ((S (d)) * dst_positive_scale_source_entry_firstleft) + (dst_positive_source_entry_firstleft))) /\ (((((exists ff_h_pvs_source_entry_firstleftnegative. ff_h_pvs_source_entry_firstleftnegative + S (dst_negative_source_entry_firstleft) = S ((S (d)) * dst_negative_scale_source_entry_firstleft)) /\ exists ff_q_pvs_source_entry_firstleftnegative. dst_negative_code_source_entry_firstleft = ff_q_pvs_source_entry_firstleftnegative * S ((S (d)) * dst_negative_scale_source_entry_firstleft) + (dst_negative_source_entry_firstleft))) /\ (exists ge_balance_positive_source_entry_firstleftvalue ge_balance_negative_source_entry_firstleftvalue. (((((dc_left_source_entry_first) = 2 * (ge_balance_positive_source_entry_firstleftvalue) /\ (ge_balance_negative_source_entry_firstleftvalue) = 0) \/ exists ge_signed_half_source_entry_firstleftvaluedecode. (((dc_left_source_entry_first) = 2 * ge_signed_half_source_entry_firstleftvaluedecode + 1 /\ (ge_balance_positive_source_entry_firstleftvalue) = 0) /\ (ge_balance_negative_source_entry_firstleftvalue) = S ge_signed_half_source_entry_firstleftvaluedecode))) /\ ((dst_positive_source_entry_firstleft) + ge_balance_negative_source_entry_firstleftvalue = (dst_negative_source_entry_firstleft) + ge_balance_positive_source_entry_firstleftvalue))))))))) /\ (((exists dst_positive_code_source_entry_firstright dst_positive_scale_source_entry_firstright dst_negative_code_source_entry_firstright dst_negative_scale_source_entry_firstright dst_positive_source_entry_firstright dst_negative_source_entry_firstright. (((G) = (((((dst_positive_code_source_entry_firstright) + (dst_positive_scale_source_entry_firstright)) * S ((dst_positive_code_source_entry_firstright) + (dst_positive_scale_source_entry_firstright)) + ((dst_positive_scale_source_entry_firstright) + (dst_positive_scale_source_entry_firstright))) + (((dst_negative_code_source_entry_firstright) + (dst_negative_scale_source_entry_firstright)) * S ((dst_negative_code_source_entry_firstright) + (dst_negative_scale_source_entry_firstright)) + ((dst_negative_scale_source_entry_firstright) + (dst_negative_scale_source_entry_firstright)))) * S ((((dst_positive_code_source_entry_firstright) + (dst_positive_scale_source_entry_firstright)) * S ((dst_positive_code_source_entry_firstright) + (dst_positive_scale_source_entry_firstright)) + ((dst_positive_scale_source_entry_firstright) + (dst_positive_scale_source_entry_firstright))) + (((dst_negative_code_source_entry_firstright) + (dst_negative_scale_source_entry_firstright)) * S ((dst_negative_code_source_entry_firstright) + (dst_negative_scale_source_entry_firstright)) + ((dst_negative_scale_source_entry_firstright) + (dst_negative_scale_source_entry_firstright)))) + ((((dst_negative_code_source_entry_firstright) + (dst_negative_scale_source_entry_firstright)) * S ((dst_negative_code_source_entry_firstright) + (dst_negative_scale_source_entry_firstright)) + ((dst_negative_scale_source_entry_firstright) + (dst_negative_scale_source_entry_firstright))) + (((dst_negative_code_source_entry_firstright) + (dst_negative_scale_source_entry_firstright)) * S ((dst_negative_code_source_entry_firstright) + (dst_negative_scale_source_entry_firstright)) + ((dst_negative_scale_source_entry_firstright) + (dst_negative_scale_source_entry_firstright)))))) /\ (((((exists ff_h_pvs_source_entry_firstrightpositive. ff_h_pvs_source_entry_firstrightpositive + S (dst_positive_source_entry_firstright) = S ((S (dc_quotient_source_entry_first)) * dst_positive_scale_source_entry_firstright)) /\ exists ff_q_pvs_source_entry_firstrightpositive. dst_positive_code_source_entry_firstright = ff_q_pvs_source_entry_firstrightpositive * S ((S (dc_quotient_source_entry_first)) * dst_positive_scale_source_entry_firstright) + (dst_positive_source_entry_firstright))) /\ (((((exists ff_h_pvs_source_entry_firstrightnegative. ff_h_pvs_source_entry_firstrightnegative + S (dst_negative_source_entry_firstright) = S ((S (dc_quotient_source_entry_first)) * dst_negative_scale_source_entry_firstright)) /\ exists ff_q_pvs_source_entry_firstrightnegative. dst_negative_code_source_entry_firstright = ff_q_pvs_source_entry_firstrightnegative * S ((S (dc_quotient_source_entry_first)) * dst_negative_scale_source_entry_firstright) + (dst_negative_source_entry_firstright))) /\ (exists ge_balance_positive_source_entry_firstrightvalue ge_balance_negative_source_entry_firstrightvalue. (((((dc_right_source_entry_first) = 2 * (ge_balance_positive_source_entry_firstrightvalue) /\ (ge_balance_negative_source_entry_firstrightvalue) = 0) \/ exists ge_signed_half_source_entry_firstrightvaluedecode. (((dc_right_source_entry_first) = 2 * ge_signed_half_source_entry_firstrightvaluedecode + 1 /\ (ge_balance_positive_source_entry_firstrightvalue) = 0) /\ (ge_balance_negative_source_entry_firstrightvalue) = S ge_signed_half_source_entry_firstrightvaluedecode))) /\ ((dst_positive_source_entry_firstright) + ge_balance_negative_source_entry_firstrightvalue = (dst_negative_source_entry_firstright) + ge_balance_positive_source_entry_firstrightvalue))))))))) /\ (exists sto_ap_source_entry_firstproduct sto_an_source_entry_firstproduct sto_bp_source_entry_firstproduct sto_bn_source_entry_firstproduct sto_cp_source_entry_firstproduct sto_cn_source_entry_firstproduct. (((((dc_left_source_entry_first) = 2 * (sto_ap_source_entry_firstproduct) /\ (sto_an_source_entry_firstproduct) = 0) \/ exists ge_signed_half_source_entry_firstproductleft. (((dc_left_source_entry_first) = 2 * ge_signed_half_source_entry_firstproductleft + 1 /\ (sto_ap_source_entry_firstproduct) = 0) /\ (sto_an_source_entry_firstproduct) = S ge_signed_half_source_entry_firstproductleft))) /\ ((((((dc_right_source_entry_first) = 2 * (sto_bp_source_entry_firstproduct) /\ (sto_bn_source_entry_firstproduct) = 0) \/ exists ge_signed_half_source_entry_firstproductright. (((dc_right_source_entry_first) = 2 * ge_signed_half_source_entry_firstproductright + 1 /\ (sto_bp_source_entry_firstproduct) = 0) /\ (sto_bn_source_entry_firstproduct) = S ge_signed_half_source_entry_firstproductright))) /\ ((((((a) = 2 * (sto_cp_source_entry_firstproduct) /\ (sto_cn_source_entry_firstproduct) = 0) \/ exists ge_signed_half_source_entry_firstproductoutput. (((a) = 2 * ge_signed_half_source_entry_firstproductoutput + 1 /\ (sto_cp_source_entry_firstproduct) = 0) /\ (sto_cn_source_entry_firstproduct) = S ge_signed_half_source_entry_firstproductoutput))) /\ ((sto_ap_source_entry_firstproduct * sto_bp_source_entry_firstproduct + sto_an_source_entry_firstproduct * sto_bn_source_entry_firstproduct) + sto_cn_source_entry_firstproduct = (sto_ap_source_entry_firstproduct * sto_bn_source_entry_firstproduct + sto_an_source_entry_firstproduct * sto_bp_source_entry_firstproduct) + sto_cp_source_entry_firstproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_source_entry_firstnondivisor. (n) = (d) * pvs_factor_source_entry_firstnondivisor)) /\ ((a)=0)))) -> ((((~((d)=0)) /\ (exists dc_quotient_source_entry_second dc_left_source_entry_second dc_right_source_entry_second. (((n)=(d)*dc_quotient_source_entry_second) /\ (((exists dst_positive_code_source_entry_secondleft dst_positive_scale_source_entry_secondleft dst_negative_code_source_entry_secondleft dst_negative_scale_source_entry_secondleft dst_positive_source_entry_secondleft dst_negative_source_entry_secondleft. (((H) = (((((dst_positive_code_source_entry_secondleft) + (dst_positive_scale_source_entry_secondleft)) * S ((dst_positive_code_source_entry_secondleft) + (dst_positive_scale_source_entry_secondleft)) + ((dst_positive_scale_source_entry_secondleft) + (dst_positive_scale_source_entry_secondleft))) + (((dst_negative_code_source_entry_secondleft) + (dst_negative_scale_source_entry_secondleft)) * S ((dst_negative_code_source_entry_secondleft) + (dst_negative_scale_source_entry_secondleft)) + ((dst_negative_scale_source_entry_secondleft) + (dst_negative_scale_source_entry_secondleft)))) * S ((((dst_positive_code_source_entry_secondleft) + (dst_positive_scale_source_entry_secondleft)) * S ((dst_positive_code_source_entry_secondleft) + (dst_positive_scale_source_entry_secondleft)) + ((dst_positive_scale_source_entry_secondleft) + (dst_positive_scale_source_entry_secondleft))) + (((dst_negative_code_source_entry_secondleft) + (dst_negative_scale_source_entry_secondleft)) * S ((dst_negative_code_source_entry_secondleft) + (dst_negative_scale_source_entry_secondleft)) + ((dst_negative_scale_source_entry_secondleft) + (dst_negative_scale_source_entry_secondleft)))) + ((((dst_negative_code_source_entry_secondleft) + (dst_negative_scale_source_entry_secondleft)) * S ((dst_negative_code_source_entry_secondleft) + (dst_negative_scale_source_entry_secondleft)) + ((dst_negative_scale_source_entry_secondleft) + (dst_negative_scale_source_entry_secondleft))) + (((dst_negative_code_source_entry_secondleft) + (dst_negative_scale_source_entry_secondleft)) * S ((dst_negative_code_source_entry_secondleft) + (dst_negative_scale_source_entry_secondleft)) + ((dst_negative_scale_source_entry_secondleft) + (dst_negative_scale_source_entry_secondleft)))))) /\ (((((exists ff_h_pvs_source_entry_secondleftpositive. ff_h_pvs_source_entry_secondleftpositive + S (dst_positive_source_entry_secondleft) = S ((S (d)) * dst_positive_scale_source_entry_secondleft)) /\ exists ff_q_pvs_source_entry_secondleftpositive. dst_positive_code_source_entry_secondleft = ff_q_pvs_source_entry_secondleftpositive * S ((S (d)) * dst_positive_scale_source_entry_secondleft) + (dst_positive_source_entry_secondleft))) /\ (((((exists ff_h_pvs_source_entry_secondleftnegative. ff_h_pvs_source_entry_secondleftnegative + S (dst_negative_source_entry_secondleft) = S ((S (d)) * dst_negative_scale_source_entry_secondleft)) /\ exists ff_q_pvs_source_entry_secondleftnegative. dst_negative_code_source_entry_secondleft = ff_q_pvs_source_entry_secondleftnegative * S ((S (d)) * dst_negative_scale_source_entry_secondleft) + (dst_negative_source_entry_secondleft))) /\ (exists ge_balance_positive_source_entry_secondleftvalue ge_balance_negative_source_entry_secondleftvalue. (((((dc_left_source_entry_second) = 2 * (ge_balance_positive_source_entry_secondleftvalue) /\ (ge_balance_negative_source_entry_secondleftvalue) = 0) \/ exists ge_signed_half_source_entry_secondleftvaluedecode. (((dc_left_source_entry_second) = 2 * ge_signed_half_source_entry_secondleftvaluedecode + 1 /\ (ge_balance_positive_source_entry_secondleftvalue) = 0) /\ (ge_balance_negative_source_entry_secondleftvalue) = S ge_signed_half_source_entry_secondleftvaluedecode))) /\ ((dst_positive_source_entry_secondleft) + ge_balance_negative_source_entry_secondleftvalue = (dst_negative_source_entry_secondleft) + ge_balance_positive_source_entry_secondleftvalue))))))))) /\ (((exists dst_positive_code_source_entry_secondright dst_positive_scale_source_entry_secondright dst_negative_code_source_entry_secondright dst_negative_scale_source_entry_secondright dst_positive_source_entry_secondright dst_negative_source_entry_secondright. (((K) = (((((dst_positive_code_source_entry_secondright) + (dst_positive_scale_source_entry_secondright)) * S ((dst_positive_code_source_entry_secondright) + (dst_positive_scale_source_entry_secondright)) + ((dst_positive_scale_source_entry_secondright) + (dst_positive_scale_source_entry_secondright))) + (((dst_negative_code_source_entry_secondright) + (dst_negative_scale_source_entry_secondright)) * S ((dst_negative_code_source_entry_secondright) + (dst_negative_scale_source_entry_secondright)) + ((dst_negative_scale_source_entry_secondright) + (dst_negative_scale_source_entry_secondright)))) * S ((((dst_positive_code_source_entry_secondright) + (dst_positive_scale_source_entry_secondright)) * S ((dst_positive_code_source_entry_secondright) + (dst_positive_scale_source_entry_secondright)) + ((dst_positive_scale_source_entry_secondright) + (dst_positive_scale_source_entry_secondright))) + (((dst_negative_code_source_entry_secondright) + (dst_negative_scale_source_entry_secondright)) * S ((dst_negative_code_source_entry_secondright) + (dst_negative_scale_source_entry_secondright)) + ((dst_negative_scale_source_entry_secondright) + (dst_negative_scale_source_entry_secondright)))) + ((((dst_negative_code_source_entry_secondright) + (dst_negative_scale_source_entry_secondright)) * S ((dst_negative_code_source_entry_secondright) + (dst_negative_scale_source_entry_secondright)) + ((dst_negative_scale_source_entry_secondright) + (dst_negative_scale_source_entry_secondright))) + (((dst_negative_code_source_entry_secondright) + (dst_negative_scale_source_entry_secondright)) * S ((dst_negative_code_source_entry_secondright) + (dst_negative_scale_source_entry_secondright)) + ((dst_negative_scale_source_entry_secondright) + (dst_negative_scale_source_entry_secondright)))))) /\ (((((exists ff_h_pvs_source_entry_secondrightpositive. ff_h_pvs_source_entry_secondrightpositive + S (dst_positive_source_entry_secondright) = S ((S (dc_quotient_source_entry_second)) * dst_positive_scale_source_entry_secondright)) /\ exists ff_q_pvs_source_entry_secondrightpositive. dst_positive_code_source_entry_secondright = ff_q_pvs_source_entry_secondrightpositive * S ((S (dc_quotient_source_entry_second)) * dst_positive_scale_source_entry_secondright) + (dst_positive_source_entry_secondright))) /\ (((((exists ff_h_pvs_source_entry_secondrightnegative. ff_h_pvs_source_entry_secondrightnegative + S (dst_negative_source_entry_secondright) = S ((S (dc_quotient_source_entry_second)) * dst_negative_scale_source_entry_secondright)) /\ exists ff_q_pvs_source_entry_secondrightnegative. dst_negative_code_source_entry_secondright = ff_q_pvs_source_entry_secondrightnegative * S ((S (dc_quotient_source_entry_second)) * dst_negative_scale_source_entry_secondright) + (dst_negative_source_entry_secondright))) /\ (exists ge_balance_positive_source_entry_secondrightvalue ge_balance_negative_source_entry_secondrightvalue. (((((dc_right_source_entry_second) = 2 * (ge_balance_positive_source_entry_secondrightvalue) /\ (ge_balance_negative_source_entry_secondrightvalue) = 0) \/ exists ge_signed_half_source_entry_secondrightvaluedecode. (((dc_right_source_entry_second) = 2 * ge_signed_half_source_entry_secondrightvaluedecode + 1 /\ (ge_balance_positive_source_entry_secondrightvalue) = 0) /\ (ge_balance_negative_source_entry_secondrightvalue) = S ge_signed_half_source_entry_secondrightvaluedecode))) /\ ((dst_positive_source_entry_secondright) + ge_balance_negative_source_entry_secondrightvalue = (dst_negative_source_entry_secondright) + ge_balance_positive_source_entry_secondrightvalue))))))))) /\ (exists sto_ap_source_entry_secondproduct sto_an_source_entry_secondproduct sto_bp_source_entry_secondproduct sto_bn_source_entry_secondproduct sto_cp_source_entry_secondproduct sto_cn_source_entry_secondproduct. (((((dc_left_source_entry_second) = 2 * (sto_ap_source_entry_secondproduct) /\ (sto_an_source_entry_secondproduct) = 0) \/ exists ge_signed_half_source_entry_secondproductleft. (((dc_left_source_entry_second) = 2 * ge_signed_half_source_entry_secondproductleft + 1 /\ (sto_ap_source_entry_secondproduct) = 0) /\ (sto_an_source_entry_secondproduct) = S ge_signed_half_source_entry_secondproductleft))) /\ ((((((dc_right_source_entry_second) = 2 * (sto_bp_source_entry_secondproduct) /\ (sto_bn_source_entry_secondproduct) = 0) \/ exists ge_signed_half_source_entry_secondproductright. (((dc_right_source_entry_second) = 2 * ge_signed_half_source_entry_secondproductright + 1 /\ (sto_bp_source_entry_secondproduct) = 0) /\ (sto_bn_source_entry_secondproduct) = S ge_signed_half_source_entry_secondproductright))) /\ ((((((b) = 2 * (sto_cp_source_entry_secondproduct) /\ (sto_cn_source_entry_secondproduct) = 0) \/ exists ge_signed_half_source_entry_secondproductoutput. (((b) = 2 * ge_signed_half_source_entry_secondproductoutput + 1 /\ (sto_cp_source_entry_secondproduct) = 0) /\ (sto_cn_source_entry_secondproduct) = S ge_signed_half_source_entry_secondproductoutput))) /\ ((sto_ap_source_entry_secondproduct * sto_bp_source_entry_secondproduct + sto_an_source_entry_secondproduct * sto_bn_source_entry_secondproduct) + sto_cn_source_entry_secondproduct = (sto_ap_source_entry_secondproduct * sto_bn_source_entry_secondproduct + sto_an_source_entry_secondproduct * sto_bp_source_entry_secondproduct) + sto_cp_source_entry_secondproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_source_entry_secondnondivisor. (n) = (d) * pvs_factor_source_entry_secondnondivisor)) /\ ((b)=0)))) -> a=b

Complete tactic proof in conservative notation

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

120 script commands · 29 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro H
  4. L4
    intro K
  5. L5
    intro n
  6. L6
    intro d
  7. L7
    intro a
  8. L8
    intro b
  9. L9
    intro hn
  10. L10
    intro hF
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hG
  2. L12
    intro hd
  3. L13
    intro ha
  4. L14
    intro hb
03Separate the logical casesL15–24

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

  1. L15
    cases ha
  2. L16
    cases ha_left
  3. L17
    cases ha_left_right
  4. L18
    cases ha_left_right_witness
  5. L19
    cases ha_left_right_witness_witness
  6. L20
    cases ha_left_right_witness_witness_witness
  7. L21
    cases ha_left_right_witness_witness_witness_right
  8. L22
    cases ha_left_right_witness_witness_witness_right_right
  9. L23
    cases hb
  10. L24
    cases hb_left
04Separate the logical casesL25–30

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

  1. L25
    cases hb_left_right
  2. L26
    cases hb_left_right_witness
  3. L27
    cases hb_left_right_witness_witness
  4. L28
    cases hb_left_right_witness_witness_witness
  5. L29
    cases hb_left_right_witness_witness_witness_right
  6. L30
    cases hb_left_right_witness_witness_witness_right_right
05Establish heqqL31–40

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

  1. L31
    have heqq : x3=x
  2. L32
    specialize mul_left_cancel_nonzero (d)
  3. L33
    specialize mul_left_cancel_nonzero (x3)
  4. L34
    specialize mul_left_cancel_nonzero (x)
  5. L35
    apply mul_left_cancel_nonzero
  6. L36
    exact ha_left_left
  7. L37
    trans n
  8. L38
    symm
  9. L39
    exact hb_left_right_witness_witness_witness_left
  10. L40
    exact ha_left_right_witness_witness_witness_left
06Calculate and transport equalitiesL41–44

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

  1. L41
    rewrite heqq at hb_left_right_witness_witness_witness_right_right_left
  2. L42
    rewrite heqq at hb_left_right_witness_witness_witness_right_right_left
  3. L43
    rewrite heqq at hb_left_right_witness_witness_witness_right_right_left
  4. L44
    rewrite heqq at hb_left_right_witness_witness_witness_right_right_left
07Establish hqpositiveL45–53

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

  1. L45
    have hqpositive : ~(x=0)
  2. L46
    intro hxzero
  3. L47
    specialize factor_nonzero_right (n)
  4. L48
    specialize factor_nonzero_right (d)
  5. L49
    specialize factor_nonzero_right (x)
  6. L50
    apply factor_nonzero_right
  7. L51
    exact hn
  8. L52
    exact ha_left_right_witness_witness_witness_left
  9. L53
    exact hxzero
08Establish hqboundL54–58

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

  1. L54
    have hqbound : Le(x,n)Definitions: Le(x,n)Original native command in the exact edition
  2. L55
    specialize divisor_le_nonzero (x)
  3. L56
    specialize divisor_le_nonzero (n)
  4. L57
    apply divisor_le_nonzero
  5. L58
    exact hn
09Construct an explicit witnessL59–59

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

  1. L59
    exists d
10Calculate and transport equalitiesL60–60

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

  1. L60
    trans d*x
11Use earlier factsL61–62

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

  1. L61
    exact ha_left_right_witness_witness_witness_left
  2. L62
    apply mul_comm
12Establish heqaL63–71

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

  1. L63
    have heqa : x1=x4
  2. L64
    specialize hF (d)
  3. L65
    specialize hF (x1)
  4. L66
    specialize hF (x4)
  5. L67
    apply hF
  6. L68
    exact ha_left_left
  7. L69
    exact hd
  8. L70
    exact ha_left_right_witness_witness_witness_right_left
  9. L71
    exact hb_left_right_witness_witness_witness_right_left
13Establish heqbL72–81

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

  1. L72
    have heqb : x2=x5
  2. L73
    specialize hG (x)
  3. L74
    specialize hG (x2)
  4. L75
    specialize hG (x5)
  5. L76
    apply hG
  6. L77
    exact hqpositive
  7. L78
    exact hqbound
  8. L79
    exact ha_left_right_witness_witness_witness_right_right_left
  9. L80
    exact hb_left_right_witness_witness_witness_right_right_left
  10. L81
    rewrite heqa at ha_left_right_witness_witness_witness_right_right_right
14Calculate and transport equalitiesL82–84

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

  1. L82
    rewrite heqa at ha_left_right_witness_witness_witness_right_right_right
  2. L83
    rewrite heqb at ha_left_right_witness_witness_witness_right_right_right
  3. L84
    rewrite heqb at ha_left_right_witness_witness_witness_right_right_right
15Use earlier factsL85–91

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

  1. L85
    specialize signed_mul_functional (x4)
  2. L86
    specialize signed_mul_functional (x5)
  3. L87
    specialize signed_mul_functional (a)
  4. L88
    specialize signed_mul_functional (b)
  5. L89
    apply signed_mul_functional
  6. L90
    exact ha_left_right_witness_witness_witness_right_right_right
  7. L91
    exact hb_left_right_witness_witness_witness_right_right_right
16Separate the logical casesL92–94

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

  1. L92
    cases hb_right
  2. L93
    exfalso
  3. L94
    cases hb_right_left
17Use earlier factsL95–97

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

  1. L95
    apply ha_left_left
  2. L96
    exact hb_right_left_left
  3. L97
    apply hb_right_left_right
18Construct an explicit witnessL98–98

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

  1. L98
    exists x
19Use earlier factsL99–99

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

  1. L99
    exact ha_left_right_witness_witness_witness_left
20Separate the logical casesL100–109

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

  1. L100
    cases ha_right
  2. L101
    cases hb
  3. L102
    cases hb_left
  4. L103
    cases hb_left_right
  5. L104
    cases hb_left_right_witness
  6. L105
    cases hb_left_right_witness_witness
  7. L106
    cases hb_left_right_witness_witness_witness
  8. L107
    cases hb_left_right_witness_witness_witness_right
  9. L108
    cases hb_left_right_witness_witness_witness_right_right
  10. L109
    exfalso
21Separate the logical casesL110–110

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

  1. L110
    cases ha_right_left
22Use earlier factsL111–113

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

  1. L111
    apply hb_left_left
  2. L112
    exact ha_right_left_left
  3. L113
    apply ha_right_left_right
23Construct an explicit witnessL114–114

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

  1. L114
    exists x
24Use earlier factsL115–115

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

  1. L115
    exact hb_left_right_witness_witness_witness_left
25Separate the logical casesL116–116

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

  1. L116
    cases hb_right
26Calculate and transport equalitiesL117–117

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

  1. L117
    trans 0
27Use earlier factsL118–118

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

  1. L118
    exact ha_right_right
28Calculate and transport equalitiesL119–119

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

  1. L119
    symm
29Use earlier factsL120–120

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

  1. L120
    exact hb_right_right

Library-wide reading audit

Original defined command ledger · 120 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro H
  4. 0004intro K
  5. 0005intro n
  6. 0006intro d
  7. 0007intro a
  8. 0008intro b
  9. 0009intro hn
  10. 0010intro hF
  11. 0011intro hG
  12. 0012intro hd
  13. 0013intro ha
  14. 0014intro hb
  15. 0015cases ha
  16. 0016cases ha_left
  17. 0017cases ha_left_right
  18. 0018cases ha_left_right_witness
  19. 0019cases ha_left_right_witness_witness
  20. 0020cases ha_left_right_witness_witness_witness
  21. 0021cases ha_left_right_witness_witness_witness_right
  22. 0022cases ha_left_right_witness_witness_witness_right_right
  23. 0023cases hb
  24. 0024cases hb_left
  25. 0025cases hb_left_right
  26. 0026cases hb_left_right_witness
  27. 0027cases hb_left_right_witness_witness
  28. 0028cases hb_left_right_witness_witness_witness
  29. 0029cases hb_left_right_witness_witness_witness_right
  30. 0030cases hb_left_right_witness_witness_witness_right_right
  31. 0031have heqq : x3=x
  32. 0032specialize mul_left_cancel_nonzero (d)
  33. 0033specialize mul_left_cancel_nonzero (x3)
  34. 0034specialize mul_left_cancel_nonzero (x)
  35. 0035apply mul_left_cancel_nonzero
  36. 0036exact ha_left_left
  37. 0037trans n
  38. 0038symm
  39. 0039exact hb_left_right_witness_witness_witness_left
  40. 0040exact ha_left_right_witness_witness_witness_left
  41. 0041rewrite heqq at hb_left_right_witness_witness_witness_right_right_left
  42. 0042rewrite heqq at hb_left_right_witness_witness_witness_right_right_left
  43. 0043rewrite heqq at hb_left_right_witness_witness_witness_right_right_left
  44. 0044rewrite heqq at hb_left_right_witness_witness_witness_right_right_left
  45. 0045have hqpositive : ~(x=0)
  46. 0046intro hxzero
  47. 0047specialize factor_nonzero_right (n)
  48. 0048specialize factor_nonzero_right (d)
  49. 0049specialize factor_nonzero_right (x)
  50. 0050apply factor_nonzero_right
  51. 0051exact hn
  52. 0052exact ha_left_right_witness_witness_witness_left
  53. 0053exact hxzero
  54. 0054have hqbound : Le(x,n)
  55. 0055specialize divisor_le_nonzero (x)
  56. 0056specialize divisor_le_nonzero (n)
  57. 0057apply divisor_le_nonzero
  58. 0058exact hn
  59. 0059exists d
  60. 0060trans d*x
  61. 0061exact ha_left_right_witness_witness_witness_left
  62. 0062apply mul_comm
  63. 0063have heqa : x1=x4
  64. 0064specialize hF (d)
  65. 0065specialize hF (x1)
  66. 0066specialize hF (x4)
  67. 0067apply hF
  68. 0068exact ha_left_left
  69. 0069exact hd
  70. 0070exact ha_left_right_witness_witness_witness_right_left
  71. 0071exact hb_left_right_witness_witness_witness_right_left
  72. 0072have heqb : x2=x5
  73. 0073specialize hG (x)
  74. 0074specialize hG (x2)
  75. 0075specialize hG (x5)
  76. 0076apply hG
  77. 0077exact hqpositive
  78. 0078exact hqbound
  79. 0079exact ha_left_right_witness_witness_witness_right_right_left
  80. 0080exact hb_left_right_witness_witness_witness_right_right_left
  81. 0081rewrite heqa at ha_left_right_witness_witness_witness_right_right_right
  82. 0082rewrite heqa at ha_left_right_witness_witness_witness_right_right_right
  83. 0083rewrite heqb at ha_left_right_witness_witness_witness_right_right_right
  84. 0084rewrite heqb at ha_left_right_witness_witness_witness_right_right_right
  85. 0085specialize signed_mul_functional (x4)
  86. 0086specialize signed_mul_functional (x5)
  87. 0087specialize signed_mul_functional (a)
  88. 0088specialize signed_mul_functional (b)
  89. 0089apply signed_mul_functional
  90. 0090exact ha_left_right_witness_witness_witness_right_right_right
  91. 0091exact hb_left_right_witness_witness_witness_right_right_right
  92. 0092cases hb_right
  93. 0093exfalso
  94. 0094cases hb_right_left
  95. 0095apply ha_left_left
  96. 0096exact hb_right_left_left
  97. 0097apply hb_right_left_right
  98. 0098exists x
  99. 0099exact ha_left_right_witness_witness_witness_left
  100. 0100cases ha_right
  101. 0101cases hb
  102. 0102cases hb_left
  103. 0103cases hb_left_right
  104. 0104cases hb_left_right_witness
  105. 0105cases hb_left_right_witness_witness
  106. 0106cases hb_left_right_witness_witness_witness
  107. 0107cases hb_left_right_witness_witness_witness_right
  108. 0108cases hb_left_right_witness_witness_witness_right_right
  109. 0109exfalso
  110. 0110cases ha_right_left
  111. 0111apply hb_left_left
  112. 0112exact ha_right_left_left
  113. 0113apply ha_right_left_right
  114. 0114exists x
  115. 0115exact hb_left_right_witness_witness_witness_left
  116. 0116cases hb_right
  117. 0117trans 0
  118. 0118exact ha_right_right
  119. 0119symm
  120. 0120exact hb_right_right