FP002A

prime_field_arithmetic_laws

Every prime has genuine canonical field arithmetic with distinct zero/one, total unique operations, both distributive laws, additive inverses and precisely nonzero multiplicative inverses.

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.

This checkpoint constructs prime-order fields (k=1), with genuine finite arithmetic tables, cardinality, and characteristic. Inversion is proved only for nonzero elements; the table's zero entry is a zero-to-zero convention. G091 for every prime power p^k, with an irreducible polynomial of degree k, remains open. No extension-field construction or G091 closure is claimed.

Exact theorem in conservative defined notation

∀ p. Prime(p) → FpFieldLaws(p)

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

Definition DAG

FpFieldLaws(p) · 1Prime(p) · 1

Actual proof prerequisites

prime_field_zero_below_primeprime_two_le · checked external prerequisitesucc_ne_zero · checked external prerequisiteprime_field_add_exists_uniqueprime_field_add_commutativeprime_field_add_associativeprime_field_multiply_exists_uniqueprime_field_multiply_commutativeprime_field_multiply_associativeprime_field_left_distributiveprime_field_right_distributiveprime_field_add_zero_rightprime_field_add_zero_leftprime_field_multiply_one_rightprime_field_multiply_one_leftprime_field_multiply_zero_rightprime_field_multiply_zero_leftprime_field_negate_exists_uniqueprime_field_inverse_exists_uniqueprime_field_no_zero_divisors
Original expanded first-order statement 
forall p. (~((p) = 1) /\ forall pfa_factor_left_complete_laws_domain pfa_factor_right_complete_laws_domain. (p) = pfa_factor_left_complete_laws_domain * pfa_factor_right_complete_laws_domain -> pfa_factor_left_complete_laws_domain = 1 \/ pfa_factor_right_complete_laws_domain = 1) -> (((exists pfa_gap_complete_lawszero. pfa_gap_complete_lawszero + S (0) = (p)) /\ (((exists pfa_gap_complete_lawsone. pfa_gap_complete_lawsone + S (1) = (p)) /\ (((~(0 = 1)) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws. (exists pfa_gap_complete_lawsaddleft. pfa_gap_complete_lawsaddleft + S (pfa_law_a_complete_laws) = (p)) -> (exists pfa_gap_complete_lawsaddright. pfa_gap_complete_lawsaddright + S (pfa_law_b_complete_laws) = (p)) -> exists pfa_law_c_complete_laws. (((exists pfa_gap_complete_lawsaddchosenleft. pfa_gap_complete_lawsaddchosenleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddchosenright. pfa_gap_complete_lawsaddchosenright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddchosenresultbound. pfa_gap_complete_lawsaddchosenresultbound + S (pfa_law_c_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddchosenresultcongruence pfa_offset_right_complete_lawsaddchosenresultcongruence. ((pfa_law_a_complete_laws) + (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddchosenresultcongruence = (pfa_law_c_complete_laws) + (p) * pfa_offset_right_complete_lawsaddchosenresultcongruence))))))))) /\ forall pfa_law_d_complete_laws. (((exists pfa_gap_complete_lawsaddotherleft. pfa_gap_complete_lawsaddotherleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddotherright. pfa_gap_complete_lawsaddotherright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddotherresultbound. pfa_gap_complete_lawsaddotherresultbound + S (pfa_law_d_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddotherresultcongruence pfa_offset_right_complete_lawsaddotherresultcongruence. ((pfa_law_a_complete_laws) + (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddotherresultcongruence = (pfa_law_d_complete_laws) + (p) * pfa_offset_right_complete_lawsaddotherresultcongruence))))))))) -> pfa_law_d_complete_laws = pfa_law_c_complete_laws) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws pfa_law_c_complete_laws. (((exists pfa_gap_complete_lawsaddcomm_firstleft. pfa_gap_complete_lawsaddcomm_firstleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddcomm_firstright. pfa_gap_complete_lawsaddcomm_firstright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddcomm_firstresultbound. pfa_gap_complete_lawsaddcomm_firstresultbound + S (pfa_law_c_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddcomm_firstresultcongruence pfa_offset_right_complete_lawsaddcomm_firstresultcongruence. ((pfa_law_a_complete_laws) + (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddcomm_firstresultcongruence = (pfa_law_c_complete_laws) + (p) * pfa_offset_right_complete_lawsaddcomm_firstresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsaddcomm_secondleft. pfa_gap_complete_lawsaddcomm_secondleft + S (pfa_law_b_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddcomm_secondright. pfa_gap_complete_lawsaddcomm_secondright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddcomm_secondresultbound. pfa_gap_complete_lawsaddcomm_secondresultbound + S (pfa_law_c_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddcomm_secondresultcongruence pfa_offset_right_complete_lawsaddcomm_secondresultcongruence. ((pfa_law_b_complete_laws) + (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddcomm_secondresultcongruence = (pfa_law_c_complete_laws) + (p) * pfa_offset_right_complete_lawsaddcomm_secondresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws pfa_law_c_complete_laws pfa_law_x_complete_laws pfa_law_y_complete_laws pfa_law_u_complete_laws pfa_law_v_complete_laws. (((exists pfa_gap_complete_lawsaddassoc_firstleft. pfa_gap_complete_lawsaddassoc_firstleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddassoc_firstright. pfa_gap_complete_lawsaddassoc_firstright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddassoc_firstresultbound. pfa_gap_complete_lawsaddassoc_firstresultbound + S (pfa_law_x_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddassoc_firstresultcongruence pfa_offset_right_complete_lawsaddassoc_firstresultcongruence. ((pfa_law_a_complete_laws) + (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddassoc_firstresultcongruence = (pfa_law_x_complete_laws) + (p) * pfa_offset_right_complete_lawsaddassoc_firstresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsaddassoc_leftleft. pfa_gap_complete_lawsaddassoc_leftleft + S (pfa_law_x_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddassoc_leftright. pfa_gap_complete_lawsaddassoc_leftright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddassoc_leftresultbound. pfa_gap_complete_lawsaddassoc_leftresultbound + S (pfa_law_u_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddassoc_leftresultcongruence pfa_offset_right_complete_lawsaddassoc_leftresultcongruence. ((pfa_law_x_complete_laws) + (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddassoc_leftresultcongruence = (pfa_law_u_complete_laws) + (p) * pfa_offset_right_complete_lawsaddassoc_leftresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsaddassoc_secondleft. pfa_gap_complete_lawsaddassoc_secondleft + S (pfa_law_b_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddassoc_secondright. pfa_gap_complete_lawsaddassoc_secondright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddassoc_secondresultbound. pfa_gap_complete_lawsaddassoc_secondresultbound + S (pfa_law_y_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddassoc_secondresultcongruence pfa_offset_right_complete_lawsaddassoc_secondresultcongruence. ((pfa_law_b_complete_laws) + (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddassoc_secondresultcongruence = (pfa_law_y_complete_laws) + (p) * pfa_offset_right_complete_lawsaddassoc_secondresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsaddassoc_rightleft. pfa_gap_complete_lawsaddassoc_rightleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddassoc_rightright. pfa_gap_complete_lawsaddassoc_rightright + S (pfa_law_y_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddassoc_rightresultbound. pfa_gap_complete_lawsaddassoc_rightresultbound + S (pfa_law_v_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddassoc_rightresultcongruence pfa_offset_right_complete_lawsaddassoc_rightresultcongruence. ((pfa_law_a_complete_laws) + (pfa_law_y_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddassoc_rightresultcongruence = (pfa_law_v_complete_laws) + (p) * pfa_offset_right_complete_lawsaddassoc_rightresultcongruence))))))))) -> pfa_law_u_complete_laws = pfa_law_v_complete_laws) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws. (exists pfa_gap_complete_lawsmultiplyleft. pfa_gap_complete_lawsmultiplyleft + S (pfa_law_a_complete_laws) = (p)) -> (exists pfa_gap_complete_lawsmultiplyright. pfa_gap_complete_lawsmultiplyright + S (pfa_law_b_complete_laws) = (p)) -> exists pfa_law_c_complete_laws. (((exists pfa_gap_complete_lawsmultiplychosenleft. pfa_gap_complete_lawsmultiplychosenleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplychosenright. pfa_gap_complete_lawsmultiplychosenright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplychosenresultbound. pfa_gap_complete_lawsmultiplychosenresultbound + S (pfa_law_c_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplychosenresultcongruence pfa_offset_right_complete_lawsmultiplychosenresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplychosenresultcongruence = (pfa_law_c_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplychosenresultcongruence))))))))) /\ forall pfa_law_d_complete_laws. (((exists pfa_gap_complete_lawsmultiplyotherleft. pfa_gap_complete_lawsmultiplyotherleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplyotherright. pfa_gap_complete_lawsmultiplyotherright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplyotherresultbound. pfa_gap_complete_lawsmultiplyotherresultbound + S (pfa_law_d_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplyotherresultcongruence pfa_offset_right_complete_lawsmultiplyotherresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplyotherresultcongruence = (pfa_law_d_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplyotherresultcongruence))))))))) -> pfa_law_d_complete_laws = pfa_law_c_complete_laws) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws pfa_law_c_complete_laws. (((exists pfa_gap_complete_lawsmultiplycomm_firstleft. pfa_gap_complete_lawsmultiplycomm_firstleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplycomm_firstright. pfa_gap_complete_lawsmultiplycomm_firstright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplycomm_firstresultbound. pfa_gap_complete_lawsmultiplycomm_firstresultbound + S (pfa_law_c_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplycomm_firstresultcongruence pfa_offset_right_complete_lawsmultiplycomm_firstresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplycomm_firstresultcongruence = (pfa_law_c_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplycomm_firstresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsmultiplycomm_secondleft. pfa_gap_complete_lawsmultiplycomm_secondleft + S (pfa_law_b_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplycomm_secondright. pfa_gap_complete_lawsmultiplycomm_secondright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplycomm_secondresultbound. pfa_gap_complete_lawsmultiplycomm_secondresultbound + S (pfa_law_c_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplycomm_secondresultcongruence pfa_offset_right_complete_lawsmultiplycomm_secondresultcongruence. ((pfa_law_b_complete_laws) * (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplycomm_secondresultcongruence = (pfa_law_c_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplycomm_secondresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws pfa_law_c_complete_laws pfa_law_x_complete_laws pfa_law_y_complete_laws pfa_law_u_complete_laws pfa_law_v_complete_laws. (((exists pfa_gap_complete_lawsmultiplyassoc_firstleft. pfa_gap_complete_lawsmultiplyassoc_firstleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplyassoc_firstright. pfa_gap_complete_lawsmultiplyassoc_firstright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplyassoc_firstresultbound. pfa_gap_complete_lawsmultiplyassoc_firstresultbound + S (pfa_law_x_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplyassoc_firstresultcongruence pfa_offset_right_complete_lawsmultiplyassoc_firstresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplyassoc_firstresultcongruence = (pfa_law_x_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplyassoc_firstresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsmultiplyassoc_leftleft. pfa_gap_complete_lawsmultiplyassoc_leftleft + S (pfa_law_x_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplyassoc_leftright. pfa_gap_complete_lawsmultiplyassoc_leftright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplyassoc_leftresultbound. pfa_gap_complete_lawsmultiplyassoc_leftresultbound + S (pfa_law_u_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplyassoc_leftresultcongruence pfa_offset_right_complete_lawsmultiplyassoc_leftresultcongruence. ((pfa_law_x_complete_laws) * (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplyassoc_leftresultcongruence = (pfa_law_u_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplyassoc_leftresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsmultiplyassoc_secondleft. pfa_gap_complete_lawsmultiplyassoc_secondleft + S (pfa_law_b_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplyassoc_secondright. pfa_gap_complete_lawsmultiplyassoc_secondright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplyassoc_secondresultbound. pfa_gap_complete_lawsmultiplyassoc_secondresultbound + S (pfa_law_y_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplyassoc_secondresultcongruence pfa_offset_right_complete_lawsmultiplyassoc_secondresultcongruence. ((pfa_law_b_complete_laws) * (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplyassoc_secondresultcongruence = (pfa_law_y_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplyassoc_secondresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsmultiplyassoc_rightleft. pfa_gap_complete_lawsmultiplyassoc_rightleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplyassoc_rightright. pfa_gap_complete_lawsmultiplyassoc_rightright + S (pfa_law_y_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplyassoc_rightresultbound. pfa_gap_complete_lawsmultiplyassoc_rightresultbound + S (pfa_law_v_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplyassoc_rightresultcongruence pfa_offset_right_complete_lawsmultiplyassoc_rightresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_y_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplyassoc_rightresultcongruence = (pfa_law_v_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplyassoc_rightresultcongruence))))))))) -> pfa_law_u_complete_laws = pfa_law_v_complete_laws) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws pfa_law_c_complete_laws pfa_law_s_complete_laws pfa_law_x_complete_laws pfa_law_y_complete_laws pfa_law_u_complete_laws pfa_law_v_complete_laws. (((exists pfa_gap_complete_lawsleftdistribution_sumleft. pfa_gap_complete_lawsleftdistribution_sumleft + S (pfa_law_b_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsleftdistribution_sumright. pfa_gap_complete_lawsleftdistribution_sumright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsleftdistribution_sumresultbound. pfa_gap_complete_lawsleftdistribution_sumresultbound + S (pfa_law_s_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsleftdistribution_sumresultcongruence pfa_offset_right_complete_lawsleftdistribution_sumresultcongruence. ((pfa_law_b_complete_laws) + (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsleftdistribution_sumresultcongruence = (pfa_law_s_complete_laws) + (p) * pfa_offset_right_complete_lawsleftdistribution_sumresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsleftdistribution_leftleft. pfa_gap_complete_lawsleftdistribution_leftleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsleftdistribution_leftright. pfa_gap_complete_lawsleftdistribution_leftright + S (pfa_law_s_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsleftdistribution_leftresultbound. pfa_gap_complete_lawsleftdistribution_leftresultbound + S (pfa_law_u_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsleftdistribution_leftresultcongruence pfa_offset_right_complete_lawsleftdistribution_leftresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_s_complete_laws)) + (p) * pfa_offset_left_complete_lawsleftdistribution_leftresultcongruence = (pfa_law_u_complete_laws) + (p) * pfa_offset_right_complete_lawsleftdistribution_leftresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsleftdistribution_firstleft. pfa_gap_complete_lawsleftdistribution_firstleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsleftdistribution_firstright. pfa_gap_complete_lawsleftdistribution_firstright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsleftdistribution_firstresultbound. pfa_gap_complete_lawsleftdistribution_firstresultbound + S (pfa_law_x_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsleftdistribution_firstresultcongruence pfa_offset_right_complete_lawsleftdistribution_firstresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsleftdistribution_firstresultcongruence = (pfa_law_x_complete_laws) + (p) * pfa_offset_right_complete_lawsleftdistribution_firstresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsleftdistribution_secondleft. pfa_gap_complete_lawsleftdistribution_secondleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsleftdistribution_secondright. pfa_gap_complete_lawsleftdistribution_secondright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsleftdistribution_secondresultbound. pfa_gap_complete_lawsleftdistribution_secondresultbound + S (pfa_law_y_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsleftdistribution_secondresultcongruence pfa_offset_right_complete_lawsleftdistribution_secondresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsleftdistribution_secondresultcongruence = (pfa_law_y_complete_laws) + (p) * pfa_offset_right_complete_lawsleftdistribution_secondresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsleftdistribution_rightleft. pfa_gap_complete_lawsleftdistribution_rightleft + S (pfa_law_x_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsleftdistribution_rightright. pfa_gap_complete_lawsleftdistribution_rightright + S (pfa_law_y_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsleftdistribution_rightresultbound. pfa_gap_complete_lawsleftdistribution_rightresultbound + S (pfa_law_v_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsleftdistribution_rightresultcongruence pfa_offset_right_complete_lawsleftdistribution_rightresultcongruence. ((pfa_law_x_complete_laws) + (pfa_law_y_complete_laws)) + (p) * pfa_offset_left_complete_lawsleftdistribution_rightresultcongruence = (pfa_law_v_complete_laws) + (p) * pfa_offset_right_complete_lawsleftdistribution_rightresultcongruence))))))))) -> pfa_law_u_complete_laws = pfa_law_v_complete_laws) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws pfa_law_c_complete_laws pfa_law_s_complete_laws pfa_law_x_complete_laws pfa_law_y_complete_laws pfa_law_u_complete_laws pfa_law_v_complete_laws. (((exists pfa_gap_complete_lawsrightdistribution_sumleft. pfa_gap_complete_lawsrightdistribution_sumleft + S (pfa_law_b_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsrightdistribution_sumright. pfa_gap_complete_lawsrightdistribution_sumright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsrightdistribution_sumresultbound. pfa_gap_complete_lawsrightdistribution_sumresultbound + S (pfa_law_s_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsrightdistribution_sumresultcongruence pfa_offset_right_complete_lawsrightdistribution_sumresultcongruence. ((pfa_law_b_complete_laws) + (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsrightdistribution_sumresultcongruence = (pfa_law_s_complete_laws) + (p) * pfa_offset_right_complete_lawsrightdistribution_sumresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsrightdistribution_leftleft. pfa_gap_complete_lawsrightdistribution_leftleft + S (pfa_law_s_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsrightdistribution_leftright. pfa_gap_complete_lawsrightdistribution_leftright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsrightdistribution_leftresultbound. pfa_gap_complete_lawsrightdistribution_leftresultbound + S (pfa_law_u_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsrightdistribution_leftresultcongruence pfa_offset_right_complete_lawsrightdistribution_leftresultcongruence. ((pfa_law_s_complete_laws) * (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsrightdistribution_leftresultcongruence = (pfa_law_u_complete_laws) + (p) * pfa_offset_right_complete_lawsrightdistribution_leftresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsrightdistribution_firstleft. pfa_gap_complete_lawsrightdistribution_firstleft + S (pfa_law_b_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsrightdistribution_firstright. pfa_gap_complete_lawsrightdistribution_firstright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsrightdistribution_firstresultbound. pfa_gap_complete_lawsrightdistribution_firstresultbound + S (pfa_law_x_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsrightdistribution_firstresultcongruence pfa_offset_right_complete_lawsrightdistribution_firstresultcongruence. ((pfa_law_b_complete_laws) * (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsrightdistribution_firstresultcongruence = (pfa_law_x_complete_laws) + (p) * pfa_offset_right_complete_lawsrightdistribution_firstresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsrightdistribution_secondleft. pfa_gap_complete_lawsrightdistribution_secondleft + S (pfa_law_c_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsrightdistribution_secondright. pfa_gap_complete_lawsrightdistribution_secondright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsrightdistribution_secondresultbound. pfa_gap_complete_lawsrightdistribution_secondresultbound + S (pfa_law_y_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsrightdistribution_secondresultcongruence pfa_offset_right_complete_lawsrightdistribution_secondresultcongruence. ((pfa_law_c_complete_laws) * (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsrightdistribution_secondresultcongruence = (pfa_law_y_complete_laws) + (p) * pfa_offset_right_complete_lawsrightdistribution_secondresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsrightdistribution_rightleft. pfa_gap_complete_lawsrightdistribution_rightleft + S (pfa_law_x_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsrightdistribution_rightright. pfa_gap_complete_lawsrightdistribution_rightright + S (pfa_law_y_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsrightdistribution_rightresultbound. pfa_gap_complete_lawsrightdistribution_rightresultbound + S (pfa_law_v_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsrightdistribution_rightresultcongruence pfa_offset_right_complete_lawsrightdistribution_rightresultcongruence. ((pfa_law_x_complete_laws) + (pfa_law_y_complete_laws)) + (p) * pfa_offset_left_complete_lawsrightdistribution_rightresultcongruence = (pfa_law_v_complete_laws) + (p) * pfa_offset_right_complete_lawsrightdistribution_rightresultcongruence))))))))) -> pfa_law_u_complete_laws = pfa_law_v_complete_laws) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsadd_zero_rightinput. pfa_gap_complete_lawsadd_zero_rightinput + S (pfa_law_a_complete_laws) = (p)) -> (((exists pfa_gap_complete_lawsadd_zero_rightleft. pfa_gap_complete_lawsadd_zero_rightleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsadd_zero_rightright. pfa_gap_complete_lawsadd_zero_rightright + S (0) = (p)) /\ ((((exists pfa_gap_complete_lawsadd_zero_rightresultbound. pfa_gap_complete_lawsadd_zero_rightresultbound + S (pfa_law_a_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsadd_zero_rightresultcongruence pfa_offset_right_complete_lawsadd_zero_rightresultcongruence. ((pfa_law_a_complete_laws) + (0)) + (p) * pfa_offset_left_complete_lawsadd_zero_rightresultcongruence = (pfa_law_a_complete_laws) + (p) * pfa_offset_right_complete_lawsadd_zero_rightresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsadd_zero_leftinput. pfa_gap_complete_lawsadd_zero_leftinput + S (pfa_law_a_complete_laws) = (p)) -> (((exists pfa_gap_complete_lawsadd_zero_leftleft. pfa_gap_complete_lawsadd_zero_leftleft + S (0) = (p)) /\ (((exists pfa_gap_complete_lawsadd_zero_leftright. pfa_gap_complete_lawsadd_zero_leftright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsadd_zero_leftresultbound. pfa_gap_complete_lawsadd_zero_leftresultbound + S (pfa_law_a_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsadd_zero_leftresultcongruence pfa_offset_right_complete_lawsadd_zero_leftresultcongruence. ((0) + (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsadd_zero_leftresultcongruence = (pfa_law_a_complete_laws) + (p) * pfa_offset_right_complete_lawsadd_zero_leftresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsmultiply_one_rightinput. pfa_gap_complete_lawsmultiply_one_rightinput + S (pfa_law_a_complete_laws) = (p)) -> (((exists pfa_gap_complete_lawsmultiply_one_rightleft. pfa_gap_complete_lawsmultiply_one_rightleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiply_one_rightright. pfa_gap_complete_lawsmultiply_one_rightright + S (1) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiply_one_rightresultbound. pfa_gap_complete_lawsmultiply_one_rightresultbound + S (pfa_law_a_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiply_one_rightresultcongruence pfa_offset_right_complete_lawsmultiply_one_rightresultcongruence. ((pfa_law_a_complete_laws) * (1)) + (p) * pfa_offset_left_complete_lawsmultiply_one_rightresultcongruence = (pfa_law_a_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiply_one_rightresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsmultiply_one_leftinput. pfa_gap_complete_lawsmultiply_one_leftinput + S (pfa_law_a_complete_laws) = (p)) -> (((exists pfa_gap_complete_lawsmultiply_one_leftleft. pfa_gap_complete_lawsmultiply_one_leftleft + S (1) = (p)) /\ (((exists pfa_gap_complete_lawsmultiply_one_leftright. pfa_gap_complete_lawsmultiply_one_leftright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiply_one_leftresultbound. pfa_gap_complete_lawsmultiply_one_leftresultbound + S (pfa_law_a_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiply_one_leftresultcongruence pfa_offset_right_complete_lawsmultiply_one_leftresultcongruence. ((1) * (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiply_one_leftresultcongruence = (pfa_law_a_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiply_one_leftresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsmultiply_zero_rightinput. pfa_gap_complete_lawsmultiply_zero_rightinput + S (pfa_law_a_complete_laws) = (p)) -> (((exists pfa_gap_complete_lawsmultiply_zero_rightleft. pfa_gap_complete_lawsmultiply_zero_rightleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiply_zero_rightright. pfa_gap_complete_lawsmultiply_zero_rightright + S (0) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiply_zero_rightresultbound. pfa_gap_complete_lawsmultiply_zero_rightresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiply_zero_rightresultcongruence pfa_offset_right_complete_lawsmultiply_zero_rightresultcongruence. ((pfa_law_a_complete_laws) * (0)) + (p) * pfa_offset_left_complete_lawsmultiply_zero_rightresultcongruence = (0) + (p) * pfa_offset_right_complete_lawsmultiply_zero_rightresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsmultiply_zero_leftinput. pfa_gap_complete_lawsmultiply_zero_leftinput + S (pfa_law_a_complete_laws) = (p)) -> (((exists pfa_gap_complete_lawsmultiply_zero_leftleft. pfa_gap_complete_lawsmultiply_zero_leftleft + S (0) = (p)) /\ (((exists pfa_gap_complete_lawsmultiply_zero_leftright. pfa_gap_complete_lawsmultiply_zero_leftright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiply_zero_leftresultbound. pfa_gap_complete_lawsmultiply_zero_leftresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiply_zero_leftresultcongruence pfa_offset_right_complete_lawsmultiply_zero_leftresultcongruence. ((0) * (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiply_zero_leftresultcongruence = (0) + (p) * pfa_offset_right_complete_lawsmultiply_zero_leftresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsnegateinput. pfa_gap_complete_lawsnegateinput + S (pfa_law_a_complete_laws) = (p)) -> exists pfa_law_b_complete_laws. (((exists pfa_gap_complete_lawsnegatechosenadditionleft. pfa_gap_complete_lawsnegatechosenadditionleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsnegatechosenadditionright. pfa_gap_complete_lawsnegatechosenadditionright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsnegatechosenadditionresultbound. pfa_gap_complete_lawsnegatechosenadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_complete_lawsnegatechosenadditionresultcongruence pfa_offset_right_complete_lawsnegatechosenadditionresultcongruence. ((pfa_law_a_complete_laws) + (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsnegatechosenadditionresultcongruence = (0) + (p) * pfa_offset_right_complete_lawsnegatechosenadditionresultcongruence))))))))) /\ forall pfa_law_c_complete_laws. (((exists pfa_gap_complete_lawsnegateotheradditionleft. pfa_gap_complete_lawsnegateotheradditionleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsnegateotheradditionright. pfa_gap_complete_lawsnegateotheradditionright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsnegateotheradditionresultbound. pfa_gap_complete_lawsnegateotheradditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_complete_lawsnegateotheradditionresultcongruence pfa_offset_right_complete_lawsnegateotheradditionresultcongruence. ((pfa_law_a_complete_laws) + (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsnegateotheradditionresultcongruence = (0) + (p) * pfa_offset_right_complete_lawsnegateotheradditionresultcongruence))))))))) -> pfa_law_c_complete_laws = pfa_law_b_complete_laws) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsinverseinput. pfa_gap_complete_lawsinverseinput + S (pfa_law_a_complete_laws) = (p)) -> ~(pfa_law_a_complete_laws = 0) -> exists pfa_law_b_complete_laws. (((~((pfa_law_a_complete_laws) = 0)) /\ ((((exists pfa_gap_complete_lawsinversechosenmultiplicationleft. pfa_gap_complete_lawsinversechosenmultiplicationleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsinversechosenmultiplicationright. pfa_gap_complete_lawsinversechosenmultiplicationright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsinversechosenmultiplicationresultbound. pfa_gap_complete_lawsinversechosenmultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_complete_lawsinversechosenmultiplicationresultcongruence pfa_offset_right_complete_lawsinversechosenmultiplicationresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsinversechosenmultiplicationresultcongruence = (1) + (p) * pfa_offset_right_complete_lawsinversechosenmultiplicationresultcongruence)))))))))))) /\ forall pfa_law_c_complete_laws. (((~((pfa_law_a_complete_laws) = 0)) /\ ((((exists pfa_gap_complete_lawsinverseothermultiplicationleft. pfa_gap_complete_lawsinverseothermultiplicationleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsinverseothermultiplicationright. pfa_gap_complete_lawsinverseothermultiplicationright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsinverseothermultiplicationresultbound. pfa_gap_complete_lawsinverseothermultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_complete_lawsinverseothermultiplicationresultcongruence pfa_offset_right_complete_lawsinverseothermultiplicationresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsinverseothermultiplicationresultcongruence = (1) + (p) * pfa_offset_right_complete_lawsinverseothermultiplicationresultcongruence)))))))))))) -> pfa_law_c_complete_laws = pfa_law_b_complete_laws) /\ ((forall pfa_law_a_complete_laws pfa_law_b_complete_laws. (((exists pfa_gap_complete_lawsnozeroleft. pfa_gap_complete_lawsnozeroleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsnozeroright. pfa_gap_complete_lawsnozeroright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsnozeroresultbound. pfa_gap_complete_lawsnozeroresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_complete_lawsnozeroresultcongruence pfa_offset_right_complete_lawsnozeroresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsnozeroresultcongruence = (0) + (p) * pfa_offset_right_complete_lawsnozeroresultcongruence))))))))) -> pfa_law_a_complete_laws = 0 \/ pfa_law_b_complete_laws = 0))))))))))))))))))))))))))))))))))))))))

Complete tactic proof in conservative notation

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

135 script commands · 52 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 (18)
prime field zero below primeprime field add exists uniqueprime field add commutativeprime field add associativeprime field multiply exists uniqueprime field multiply commutativeprime field multiply associativeprime field left distributiveprime field right distributiveprime field add zero rightprime field add zero leftprime field multiply one rightprime field multiply one leftprime field multiply zero rightprime field multiply zero leftprime field negate exists uniqueprime field inverse exists uniqueprime field no zero divisors
01Fix variables and assumptionsL1–2

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

  1. L1
    intro p
  2. L2
    intro hp
02Separate the logical casesL3–3

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

  1. L3
    split
03Use earlier factsL4–6

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

  1. L4
    specialize prime_field_zero_below_prime (p)
  2. L5
    apply prime_field_zero_below_prime
  3. L6
    exact hp
04Separate the logical casesL7–7

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

  1. L7
    split
05Use earlier factsL8–10

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

  1. L8
    specialize prime_two_le (p)
  2. L9
    apply prime_two_le
  3. L10
    exact hp
06Separate the logical casesL11–11

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

  1. L11
    split
07Fix variables and assumptionsL12–12

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

  1. L12
    intro hzero_one
08Establish hone_zeroL13–18

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

  1. L13
    have hone_zero : 1 = 0
  2. L14
    symm
  3. L15
    exact hzero_one
  4. L16
    specialize succ_ne_zero (0)
  5. L17
    apply succ_ne_zero
  6. L18
    exact hone_zero
09Separate the logical casesL19–19

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

  1. L19
    split
10Fix variables and assumptionsL20–23

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

  1. L20
    intro pfa_law_a_complete_laws
  2. L21
    intro pfa_law_b_complete_laws
  3. L22
    intro ha
  4. L23
    intro hb
11Use earlier factsL24–30

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

  1. L24
    specialize prime_field_add_exists_unique (p)
  2. L25
    specialize prime_field_add_exists_unique (pfa_law_a_complete_laws)
  3. L26
    specialize prime_field_add_exists_unique (pfa_law_b_complete_laws)
  4. L27
    apply prime_field_add_exists_unique
  5. L28
    exact hp
  6. L29
    exact ha
  7. L30
    exact hb
12Separate the logical casesL31–31

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

  1. L31
    split
13Use earlier factsL32–33

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

  1. L32
    specialize prime_field_add_commutative (p)
  2. L33
    apply prime_field_add_commutative
14Separate the logical casesL34–34

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

  1. L34
    split
15Use earlier factsL35–36

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

  1. L35
    specialize prime_field_add_associative (p)
  2. L36
    apply prime_field_add_associative
16Separate the logical casesL37–37

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

  1. L37
    split
17Fix variables and assumptionsL38–41

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

  1. L38
    intro pfa_law_a_complete_laws
  2. L39
    intro pfa_law_b_complete_laws
  3. L40
    intro ha
  4. L41
    intro hb
18Use earlier factsL42–48

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

  1. L42
    specialize prime_field_multiply_exists_unique (p)
  2. L43
    specialize prime_field_multiply_exists_unique (pfa_law_a_complete_laws)
  3. L44
    specialize prime_field_multiply_exists_unique (pfa_law_b_complete_laws)
  4. L45
    apply prime_field_multiply_exists_unique
  5. L46
    exact hp
  6. L47
    exact ha
  7. L48
    exact hb
19Separate the logical casesL49–49

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

  1. L49
    split
20Use earlier factsL50–51

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

  1. L50
    specialize prime_field_multiply_commutative (p)
  2. L51
    apply prime_field_multiply_commutative
21Separate the logical casesL52–52

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

  1. L52
    split
22Use earlier factsL53–54

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

  1. L53
    specialize prime_field_multiply_associative (p)
  2. L54
    apply prime_field_multiply_associative
23Separate the logical casesL55–55

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

  1. L55
    split
24Use earlier factsL56–57

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

  1. L56
    specialize prime_field_left_distributive (p)
  2. L57
    apply prime_field_left_distributive
25Separate the logical casesL58–58

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

  1. L58
    split
26Use earlier factsL59–60

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

  1. L59
    specialize prime_field_right_distributive (p)
  2. L60
    apply prime_field_right_distributive
27Separate the logical casesL61–61

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

  1. L61
    split
28Fix variables and assumptionsL62–63

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

  1. L62
    intro pfa_law_a_complete_laws
  2. L63
    intro ha
29Use earlier factsL64–68

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

  1. L64
    specialize prime_field_add_zero_right (p)
  2. L65
    specialize prime_field_add_zero_right (pfa_law_a_complete_laws)
  3. L66
    apply prime_field_add_zero_right
  4. L67
    exact hp
  5. L68
    exact ha
30Separate the logical casesL69–69

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

  1. L69
    split
31Fix variables and assumptionsL70–71

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

  1. L70
    intro pfa_law_a_complete_laws
  2. L71
    intro ha
32Use earlier factsL72–76

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

  1. L72
    specialize prime_field_add_zero_left (p)
  2. L73
    specialize prime_field_add_zero_left (pfa_law_a_complete_laws)
  3. L74
    apply prime_field_add_zero_left
  4. L75
    exact hp
  5. L76
    exact ha
33Separate the logical casesL77–77

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

  1. L77
    split
34Fix variables and assumptionsL78–79

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

  1. L78
    intro pfa_law_a_complete_laws
  2. L79
    intro ha
35Use earlier factsL80–84

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

  1. L80
    specialize prime_field_multiply_one_right (p)
  2. L81
    specialize prime_field_multiply_one_right (pfa_law_a_complete_laws)
  3. L82
    apply prime_field_multiply_one_right
  4. L83
    exact hp
  5. L84
    exact ha
36Separate the logical casesL85–85

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

  1. L85
    split
37Fix variables and assumptionsL86–87

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

  1. L86
    intro pfa_law_a_complete_laws
  2. L87
    intro ha
38Use earlier factsL88–92

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

  1. L88
    specialize prime_field_multiply_one_left (p)
  2. L89
    specialize prime_field_multiply_one_left (pfa_law_a_complete_laws)
  3. L90
    apply prime_field_multiply_one_left
  4. L91
    exact hp
  5. L92
    exact ha
39Separate the logical casesL93–93

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

  1. L93
    split
40Fix variables and assumptionsL94–95

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

  1. L94
    intro pfa_law_a_complete_laws
  2. L95
    intro ha
41Use earlier factsL96–100

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

  1. L96
    specialize prime_field_multiply_zero_right (p)
  2. L97
    specialize prime_field_multiply_zero_right (pfa_law_a_complete_laws)
  3. L98
    apply prime_field_multiply_zero_right
  4. L99
    exact hp
  5. L100
    exact ha
42Separate the logical casesL101–101

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

  1. L101
    split
43Fix variables and assumptionsL102–103

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

  1. L102
    intro pfa_law_a_complete_laws
  2. L103
    intro ha
44Use earlier factsL104–108

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

  1. L104
    specialize prime_field_multiply_zero_left (p)
  2. L105
    specialize prime_field_multiply_zero_left (pfa_law_a_complete_laws)
  3. L106
    apply prime_field_multiply_zero_left
  4. L107
    exact hp
  5. L108
    exact ha
45Separate the logical casesL109–109

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

  1. L109
    split
46Fix variables and assumptionsL110–111

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

  1. L110
    intro pfa_law_a_complete_laws
  2. L111
    intro ha
47Use earlier factsL112–116

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

  1. L112
    specialize prime_field_negate_exists_unique (p)
  2. L113
    specialize prime_field_negate_exists_unique (pfa_law_a_complete_laws)
  3. L114
    apply prime_field_negate_exists_unique
  4. L115
    exact hp
  5. L116
    exact ha
48Separate the logical casesL117–117

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

  1. L117
    split
49Fix variables and assumptionsL118–120

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

  1. L118
    intro pfa_law_a_complete_laws
  2. L119
    intro ha
  3. L120
    intro hn
50Use earlier factsL121–126

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

  1. L121
    specialize prime_field_inverse_exists_unique (p)
  2. L122
    specialize prime_field_inverse_exists_unique (pfa_law_a_complete_laws)
  3. L123
    apply prime_field_inverse_exists_unique
  4. L124
    exact hp
  5. L125
    exact ha
  6. L126
    exact hn
51Fix variables and assumptionsL127–129

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

  1. L127
    intro pfa_law_a_complete_laws
  2. L128
    intro pfa_law_b_complete_laws
  3. L129
    intro hm
52Use earlier factsL130–135

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

  1. L130
    specialize prime_field_no_zero_divisors (p)
  2. L131
    specialize prime_field_no_zero_divisors (pfa_law_a_complete_laws)
  3. L132
    specialize prime_field_no_zero_divisors (pfa_law_b_complete_laws)
  4. L133
    apply prime_field_no_zero_divisors
  5. L134
    exact hp
  6. L135
    exact hm

Library-wide reading audit

Original defined command ledger · 135 lines
  1. 0001intro p
  2. 0002intro hp
  3. 0003split
  4. 0004specialize prime_field_zero_below_prime (p)
  5. 0005apply prime_field_zero_below_prime
  6. 0006exact hp
  7. 0007split
  8. 0008specialize prime_two_le (p)
  9. 0009apply prime_two_le
  10. 0010exact hp
  11. 0011split
  12. 0012intro hzero_one
  13. 0013have hone_zero : 1 = 0
  14. 0014symm
  15. 0015exact hzero_one
  16. 0016specialize succ_ne_zero (0)
  17. 0017apply succ_ne_zero
  18. 0018exact hone_zero
  19. 0019split
  20. 0020intro pfa_law_a_complete_laws
  21. 0021intro pfa_law_b_complete_laws
  22. 0022intro ha
  23. 0023intro hb
  24. 0024specialize prime_field_add_exists_unique (p)
  25. 0025specialize prime_field_add_exists_unique (pfa_law_a_complete_laws)
  26. 0026specialize prime_field_add_exists_unique (pfa_law_b_complete_laws)
  27. 0027apply prime_field_add_exists_unique
  28. 0028exact hp
  29. 0029exact ha
  30. 0030exact hb
  31. 0031split
  32. 0032specialize prime_field_add_commutative (p)
  33. 0033apply prime_field_add_commutative
  34. 0034split
  35. 0035specialize prime_field_add_associative (p)
  36. 0036apply prime_field_add_associative
  37. 0037split
  38. 0038intro pfa_law_a_complete_laws
  39. 0039intro pfa_law_b_complete_laws
  40. 0040intro ha
  41. 0041intro hb
  42. 0042specialize prime_field_multiply_exists_unique (p)
  43. 0043specialize prime_field_multiply_exists_unique (pfa_law_a_complete_laws)
  44. 0044specialize prime_field_multiply_exists_unique (pfa_law_b_complete_laws)
  45. 0045apply prime_field_multiply_exists_unique
  46. 0046exact hp
  47. 0047exact ha
  48. 0048exact hb
  49. 0049split
  50. 0050specialize prime_field_multiply_commutative (p)
  51. 0051apply prime_field_multiply_commutative
  52. 0052split
  53. 0053specialize prime_field_multiply_associative (p)
  54. 0054apply prime_field_multiply_associative
  55. 0055split
  56. 0056specialize prime_field_left_distributive (p)
  57. 0057apply prime_field_left_distributive
  58. 0058split
  59. 0059specialize prime_field_right_distributive (p)
  60. 0060apply prime_field_right_distributive
  61. 0061split
  62. 0062intro pfa_law_a_complete_laws
  63. 0063intro ha
  64. 0064specialize prime_field_add_zero_right (p)
  65. 0065specialize prime_field_add_zero_right (pfa_law_a_complete_laws)
  66. 0066apply prime_field_add_zero_right
  67. 0067exact hp
  68. 0068exact ha
  69. 0069split
  70. 0070intro pfa_law_a_complete_laws
  71. 0071intro ha
  72. 0072specialize prime_field_add_zero_left (p)
  73. 0073specialize prime_field_add_zero_left (pfa_law_a_complete_laws)
  74. 0074apply prime_field_add_zero_left
  75. 0075exact hp
  76. 0076exact ha
  77. 0077split
  78. 0078intro pfa_law_a_complete_laws
  79. 0079intro ha
  80. 0080specialize prime_field_multiply_one_right (p)
  81. 0081specialize prime_field_multiply_one_right (pfa_law_a_complete_laws)
  82. 0082apply prime_field_multiply_one_right
  83. 0083exact hp
  84. 0084exact ha
  85. 0085split
  86. 0086intro pfa_law_a_complete_laws
  87. 0087intro ha
  88. 0088specialize prime_field_multiply_one_left (p)
  89. 0089specialize prime_field_multiply_one_left (pfa_law_a_complete_laws)
  90. 0090apply prime_field_multiply_one_left
  91. 0091exact hp
  92. 0092exact ha
  93. 0093split
  94. 0094intro pfa_law_a_complete_laws
  95. 0095intro ha
  96. 0096specialize prime_field_multiply_zero_right (p)
  97. 0097specialize prime_field_multiply_zero_right (pfa_law_a_complete_laws)
  98. 0098apply prime_field_multiply_zero_right
  99. 0099exact hp
  100. 0100exact ha
  101. 0101split
  102. 0102intro pfa_law_a_complete_laws
  103. 0103intro ha
  104. 0104specialize prime_field_multiply_zero_left (p)
  105. 0105specialize prime_field_multiply_zero_left (pfa_law_a_complete_laws)
  106. 0106apply prime_field_multiply_zero_left
  107. 0107exact hp
  108. 0108exact ha
  109. 0109split
  110. 0110intro pfa_law_a_complete_laws
  111. 0111intro ha
  112. 0112specialize prime_field_negate_exists_unique (p)
  113. 0113specialize prime_field_negate_exists_unique (pfa_law_a_complete_laws)
  114. 0114apply prime_field_negate_exists_unique
  115. 0115exact hp
  116. 0116exact ha
  117. 0117split
  118. 0118intro pfa_law_a_complete_laws
  119. 0119intro ha
  120. 0120intro hn
  121. 0121specialize prime_field_inverse_exists_unique (p)
  122. 0122specialize prime_field_inverse_exists_unique (pfa_law_a_complete_laws)
  123. 0123apply prime_field_inverse_exists_unique
  124. 0124exact hp
  125. 0125exact ha
  126. 0126exact hn
  127. 0127intro pfa_law_a_complete_laws
  128. 0128intro pfa_law_b_complete_laws
  129. 0129intro hm
  130. 0130specialize prime_field_no_zero_divisors (p)
  131. 0131specialize prime_field_no_zero_divisors (pfa_law_a_complete_laws)
  132. 0132specialize prime_field_no_zero_divisors (pfa_law_b_complete_laws)
  133. 0133apply prime_field_no_zero_divisors
  134. 0134exact hp
  135. 0135exact hm