Conservative definition
Parameters: d, ab, ac, N
∀ x. ∀ y. S x ≤ N → S y ≤ S (S x · ac) ∧ (∃ z. ab = z · S (S x · ac) + y) → (∃ z. x = 2 · z ∧ y = 0) ∨ (∃ z. x = S (2 · z) ∧ x · y = 2 · d)Definition prerequisites
Theorem uses (notation, not proof premises)
AP016 · AP019 · AP020 · AP022 · AP026 · AP032 · AP034 · AP047 · AP050 · AP082 · AP083 · AP084 · AP085 · AP086 · AP087 · AP088 · AP089 · AP090 · AP091 · AP092 · CV025 · CV026 · CV028 · CV029 · CV031 · CV034 · CV066 · CV074 · CV076 · CV077 · CV080 · CV085 · CV086 · CV090 · CV091 · CV092 · CV093