ND0240

UnitProductPrefix(m,b,c,l)

Every actual beta entry in 0<=i<l satisfies UnitProductFactor at the same index. Product values are computed by the existing finite-product graph.

Conservative notation; not a theorem, primitive, or axiom.

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

∀ eu_factor_index_bottomlayer. Lt(eu_factor_index_bottomlayer,l) → ∃ x. BetaAt(b,c,eu_factor_index_bottomlayer,x) ∧ UnitProductFactor(m,eu_factor_index_bottomlayer,x)

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

Hygienic expanded first-order definition 
forall eu_factor_index_bottomlayer. (exists eut_gap_eu_bottomlayer_index. eut_gap_eu_bottomlayer_index + S (eu_factor_index_bottomlayer) = ((l))) -> exists eu_factor_value_bottomlayer. (((exists fs_h_eu_bottomlayer_at. fs_h_eu_bottomlayer_at + S (eu_factor_value_bottomlayer) = S ((S (eu_factor_index_bottomlayer)) * (c))) /\ exists fs_q_eu_bottomlayer_at. (b) = fs_q_eu_bottomlayer_at * S ((S (eu_factor_index_bottomlayer)) * (c)) + (eu_factor_value_bottomlayer))) /\ ((((forall eut_divisor_eu_bottomlayer_choice_coprime. (exists eut_left_eu_bottomlayer_choice_coprime. (eu_factor_index_bottomlayer) = eut_divisor_eu_bottomlayer_choice_coprime * eut_left_eu_bottomlayer_choice_coprime) -> (exists eut_right_eu_bottomlayer_choice_coprime. ((m)) = eut_divisor_eu_bottomlayer_choice_coprime * eut_right_eu_bottomlayer_choice_coprime) -> eut_divisor_eu_bottomlayer_choice_coprime = 1) /\ (eu_factor_value_bottomlayer)=(eu_factor_index_bottomlayer)) \/ (~(forall eut_divisor_eu_bottomlayer_choice_coprime. (exists eut_left_eu_bottomlayer_choice_coprime. (eu_factor_index_bottomlayer) = eut_divisor_eu_bottomlayer_choice_coprime * eut_left_eu_bottomlayer_choice_coprime) -> (exists eut_right_eu_bottomlayer_choice_coprime. ((m)) = eut_divisor_eu_bottomlayer_choice_coprime * eut_right_eu_bottomlayer_choice_coprime) -> eut_divisor_eu_bottomlayer_choice_coprime = 1) /\ (eu_factor_value_bottomlayer)=1)))

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)UnitProductFactor(m,i,v)

Definitions depending on this notation

none

Checked theorems using this definition

EU0012 · euler_unit_product_prefix_emptyEU0013 · euler_unit_product_prefix_extendEU0014 · euler_unit_product_prefix_existsEU0015 · euler_unit_product_prefix_drop_lastEU0016 · euler_unit_product_prefix_entryEU0017 · euler_unit_product_coprimeEU001B · euler_unit_product_reindex_scaleEU001F · euler_coprime_totient_power_value