Conservative definition
Parameters: d, x, tb, tc, N
∀ y. ∀ z. ∀ n. S y ≤ N → S z ≤ S (S y · tc) ∧ (∃ m. tb = m · S (S y · tc) + z) → S n ≤ S (S S y · tc) ∧ (∃ m. tb = m · S (S S y · tc) + n) → S y · d · n = x · zDefinition prerequisites
Theorem uses (notation, not proof premises)
AP002 · AP004 · AP007 · AP008 · AP023 · AP032 · AP034 · AP035 · AP036 · AP038 · AP039 · AP042 · AP043 · AP044 · AP047 · AP050 · AP052 · AP054 · AP055 · AP056 · AP057 · AP058 · AP059 · AP060 · AP061 · AP063 · AP064 · AP065 · AP066 · AP067 · AP068 · AP069 · AP070 · AP071 · AP072 · AP073 · AP074 · AP075 · AP081 · AP082 · AP083 · AP084 · AP085 · AP086 · AP087 · AP088 · AP089 · AP090 · AP091 · AP092 · AP094 · AP095 · CV070 · CV071 · CV073 · CV074 · CV076 · CV077 · CV087 · CV088 · CV094 · CV096 · CV097 · CV098 · CV099 · CV100 · CV101 · CV102