Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Definition in prerequisite notation
CornacchiaRoot(p,z) ∧ (¬r = 0 ∧ (Lt(r,a) ∧ (¬t = 0 ∧ (Lt(p,a · a) ∧ (p = a · t + r · u ∧ (Coprime(a,r) ∧ CornacchiaAlternatingCongruences(p,z,a,r,u,t)))))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
(((((~(p = 1) /\ forall frm_prime_left_cor_secondwave_root_prime frm_prime_right_cor_secondwave_root_prime. p = frm_prime_left_cor_secondwave_root_prime * frm_prime_right_cor_secondwave_root_prime -> frm_prime_left_cor_secondwave_root_prime = 1 \/ frm_prime_right_cor_secondwave_root_prime = 1)) /\ (((~(z = 0)) /\ (((exists cor_gap_secondwave_root_bound. cor_gap_secondwave_root_bound + S (z) = (p)) /\ (exists cor_factor_secondwave_root. z * z + 1 = p * cor_factor_secondwave_root))))))) /\ (((~(r = 0)) /\ (((exists cor_gap_secondwave_order. cor_gap_secondwave_order + S (r) = (a)) /\ (((~(t = 0)) /\ (((exists cor_gap_secondwave_previous. cor_gap_secondwave_previous + S (p) = (a * a)) /\ (((p = a * t + r * u) /\ (((forall frp_divisor_cor_secondwave_coprime. (exists frp_left_factor_cor_secondwave_coprime. a = frp_divisor_cor_secondwave_coprime * frp_left_factor_cor_secondwave_coprime) -> (exists frp_right_factor_cor_secondwave_coprime. r = frp_divisor_cor_secondwave_coprime * frp_right_factor_cor_secondwave_coprime) -> frp_divisor_cor_secondwave_coprime = 1) /\ ((((exists hgcrt_mod_left_cor_secondwave_alternating_ap hgcrt_mod_right_cor_secondwave_alternating_ap. a + p * hgcrt_mod_left_cor_secondwave_alternating_ap = (z * u) + p * hgcrt_mod_right_cor_secondwave_alternating_ap) /\ (exists hgcrt_mod_left_cor_secondwave_alternating_rn hgcrt_mod_right_cor_secondwave_alternating_rn. (r + z * t) + p * hgcrt_mod_left_cor_secondwave_alternating_rn = 0 + p * hgcrt_mod_right_cor_secondwave_alternating_rn)) \/ ((exists hgcrt_mod_left_cor_secondwave_alternating_an hgcrt_mod_right_cor_secondwave_alternating_an. (a + z * u) + p * hgcrt_mod_left_cor_secondwave_alternating_an = 0 + p * hgcrt_mod_right_cor_secondwave_alternating_an) /\ (exists hgcrt_mod_left_cor_secondwave_alternating_rp hgcrt_mod_right_cor_secondwave_alternating_rp. r + p * hgcrt_mod_left_cor_secondwave_alternating_rp = (z * t) + p * hgcrt_mod_right_cor_secondwave_alternating_rp)))))))))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
none