ND0269 — FpCoefficientReduction(p,b,c,d,e,l)

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

Definition in prerequisite notation

∀ pfp_index_lowertier. Lt(pfp_index_lowertier,l) → ∃ x. ∃ y. BetaAt(b,c,pfp_index_lowertier,x) ∧ (BetaAt(d,e,pfp_index_lowertier,y) ∧ CanonicalModularResidue(p,x,y))

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition

forall pfp_index_lowertier. (exists pfa_gap_lowertierindex. pfa_gap_lowertierindex + S (pfp_index_lowertier) = ((l))) -> exists pfp_source_lowertier pfp_residue_lowertier. ((((exists ff_h_pfp_lowertiersource. ff_h_pfp_lowertiersource + S (pfp_source_lowertier) = S ((S (pfp_index_lowertier)) * (c))) /\ exists ff_q_pfp_lowertiersource. (b) = ff_q_pfp_lowertiersource * S ((S (pfp_index_lowertier)) * (c)) + (pfp_source_lowertier))) /\ (((((exists ff_h_pfp_lowertiertarget. ff_h_pfp_lowertiertarget + S (pfp_residue_lowertier) = S ((S (pfp_index_lowertier)) * (e))) /\ exists ff_q_pfp_lowertiertarget. (d) = ff_q_pfp_lowertiertarget * S ((S (pfp_index_lowertier)) * (e)) + (pfp_residue_lowertier))) /\ ((((exists pfa_gap_lowertierresiduebound. pfa_gap_lowertierresiduebound + S (pfp_residue_lowertier) = ((p))) /\ ((exists pfa_offset_left_lowertierresiduecongruence pfa_offset_right_lowertierresiduecongruence. (pfp_source_lowertier) + ((p)) * pfa_offset_left_lowertierresiduecongruence = (pfp_residue_lowertier) + ((p)) * pfa_offset_right_lowertierresiduecongruence))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Lt(a,b)BetaAt(b,c,i,x)CanonicalModularResidue(m,a,r)

Definitions depending on this notation

none

Checked theorems using this definition