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.
Statement with defined notation
∀ a. ∀ e. ∀ r. ∀ n. (∀ x. ∀ y. ∃ z. Pow(x,y,z)) → Pow(a,e,r) → n = r · a → Pow(a,S e,n)Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
3 occurrences
In local proof propositions
1 occurrences
Exact expanded native-PA statement
forall a e r n. (forall bpt_a_successor bpt_e_successor. exists bpt_x_successor. (exists ff_b_bpt_value_successor ff_c_bpt_value_successor. ((forall ff_i_bpt_value_successor_repeat. (exists ff_lt_bpt_value_successor_repeat_bound. ff_lt_bpt_value_successor_repeat_bound + S ff_i_bpt_value_successor_repeat = bpt_e_successor) -> (((exists ff_h_bpt_value_successor_repeat_decoded. ff_h_bpt_value_successor_repeat_decoded + S (bpt_a_successor) = S ((S (ff_i_bpt_value_successor_repeat)) * ff_c_bpt_value_successor)) /\ exists ff_q_bpt_value_successor_repeat_decoded. ff_b_bpt_value_successor = ff_q_bpt_value_successor_repeat_decoded * S ((S (ff_i_bpt_value_successor_repeat)) * ff_c_bpt_value_successor) + (bpt_a_successor)))) /\ (exists ff_u_bpt_value_successor_product ff_v_bpt_value_successor_product. ((((exists ff_h_bpt_value_successor_product_start. ff_h_bpt_value_successor_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_successor_product)) /\ exists ff_q_bpt_value_successor_product_start. ff_u_bpt_value_successor_product = ff_q_bpt_value_successor_product_start * S ((S (0)) * ff_v_bpt_value_successor_product) + (1))) /\ ((((exists ff_h_bpt_value_successor_product_terminal. ff_h_bpt_value_successor_product_terminal + S (bpt_x_successor) = S ((S (bpt_e_successor)) * ff_v_bpt_value_successor_product)) /\ exists ff_q_bpt_value_successor_product_terminal. ff_u_bpt_value_successor_product = ff_q_bpt_value_successor_product_terminal * S ((S (bpt_e_successor)) * ff_v_bpt_value_successor_product) + (bpt_x_successor))) /\ forall ff_i_bpt_value_successor_product. (exists ff_lt_bpt_value_successor_product_bound. ff_lt_bpt_value_successor_product_bound + S ff_i_bpt_value_successor_product = bpt_e_successor) -> exists ff_p_bpt_value_successor_product ff_r_bpt_value_successor_product ff_s_bpt_value_successor_product. ((((exists ff_h_bpt_value_successor_product_factor. ff_h_bpt_value_successor_product_factor + S (ff_p_bpt_value_successor_product) = S ((S (ff_i_bpt_value_successor_product)) * ff_c_bpt_value_successor)) /\ exists ff_q_bpt_value_successor_product_factor. ff_b_bpt_value_successor = ff_q_bpt_value_successor_product_factor * S ((S (ff_i_bpt_value_successor_product)) * ff_c_bpt_value_successor) + (ff_p_bpt_value_successor_product))) /\ ((((exists ff_h_bpt_value_successor_product_partial. ff_h_bpt_value_successor_product_partial + S (ff_r_bpt_value_successor_product) = S ((S (ff_i_bpt_value_successor_product)) * ff_v_bpt_value_successor_product)) /\ exists ff_q_bpt_value_successor_product_partial. ff_u_bpt_value_successor_product = ff_q_bpt_value_successor_product_partial * S ((S (ff_i_bpt_value_successor_product)) * ff_v_bpt_value_successor_product) + (ff_r_bpt_value_successor_product))) /\ ((((exists ff_h_bpt_value_successor_product_successor. ff_h_bpt_value_successor_product_successor + S (ff_s_bpt_value_successor_product) = S ((S (S ff_i_bpt_value_successor_product)) * ff_v_bpt_value_successor_product)) /\ exists ff_q_bpt_value_successor_product_successor. ff_u_bpt_value_successor_product = ff_q_bpt_value_successor_product_successor * S ((S (S ff_i_bpt_value_successor_product)) * ff_v_bpt_value_successor_product) + (ff_s_bpt_value_successor_product))) /\ ff_s_bpt_value_successor_product = ff_r_bpt_value_successor_product * ff_p_bpt_value_successor_product))))))))) -> (exists ff_b_bpt_predecessor ff_c_bpt_predecessor. ((forall ff_i_bpt_predecessor_repeat. (exists ff_lt_bpt_predecessor_repeat_bound. ff_lt_bpt_predecessor_repeat_bound + S ff_i_bpt_predecessor_repeat = e) -> (((exists ff_h_bpt_predecessor_repeat_decoded. ff_h_bpt_predecessor_repeat_decoded + S (a) = S ((S (ff_i_bpt_predecessor_repeat)) * ff_c_bpt_predecessor)) /\ exists ff_q_bpt_predecessor_repeat_decoded. ff_b_bpt_predecessor = ff_q_bpt_predecessor_repeat_decoded * S ((S (ff_i_bpt_predecessor_repeat)) * ff_c_bpt_predecessor) + (a)))) /\ (exists ff_u_bpt_predecessor_product ff_v_bpt_predecessor_product. ((((exists ff_h_bpt_predecessor_product_start. ff_h_bpt_predecessor_product_start + S (1) = S ((S (0)) * ff_v_bpt_predecessor_product)) /\ exists ff_q_bpt_predecessor_product_start. ff_u_bpt_predecessor_product = ff_q_bpt_predecessor_product_start * S ((S (0)) * ff_v_bpt_predecessor_product) + (1))) /\ ((((exists ff_h_bpt_predecessor_product_terminal. ff_h_bpt_predecessor_product_terminal + S (r) = S ((S (e)) * ff_v_bpt_predecessor_product)) /\ exists ff_q_bpt_predecessor_product_terminal. ff_u_bpt_predecessor_product = ff_q_bpt_predecessor_product_terminal * S ((S (e)) * ff_v_bpt_predecessor_product) + (r))) /\ forall ff_i_bpt_predecessor_product. (exists ff_lt_bpt_predecessor_product_bound. ff_lt_bpt_predecessor_product_bound + S ff_i_bpt_predecessor_product = e) -> exists ff_p_bpt_predecessor_product ff_r_bpt_predecessor_product ff_s_bpt_predecessor_product. ((((exists ff_h_bpt_predecessor_product_factor. ff_h_bpt_predecessor_product_factor + S (ff_p_bpt_predecessor_product) = S ((S (ff_i_bpt_predecessor_product)) * ff_c_bpt_predecessor)) /\ exists ff_q_bpt_predecessor_product_factor. ff_b_bpt_predecessor = ff_q_bpt_predecessor_product_factor * S ((S (ff_i_bpt_predecessor_product)) * ff_c_bpt_predecessor) + (ff_p_bpt_predecessor_product))) /\ ((((exists ff_h_bpt_predecessor_product_partial. ff_h_bpt_predecessor_product_partial + S (ff_r_bpt_predecessor_product) = S ((S (ff_i_bpt_predecessor_product)) * ff_v_bpt_predecessor_product)) /\ exists ff_q_bpt_predecessor_product_partial. ff_u_bpt_predecessor_product = ff_q_bpt_predecessor_product_partial * S ((S (ff_i_bpt_predecessor_product)) * ff_v_bpt_predecessor_product) + (ff_r_bpt_predecessor_product))) /\ ((((exists ff_h_bpt_predecessor_product_successor. ff_h_bpt_predecessor_product_successor + S (ff_s_bpt_predecessor_product) = S ((S (S ff_i_bpt_predecessor_product)) * ff_v_bpt_predecessor_product)) /\ exists ff_q_bpt_predecessor_product_successor. ff_u_bpt_predecessor_product = ff_q_bpt_predecessor_product_successor * S ((S (S ff_i_bpt_predecessor_product)) * ff_v_bpt_predecessor_product) + (ff_s_bpt_predecessor_product))) /\ ff_s_bpt_predecessor_product = ff_r_bpt_predecessor_product * ff_p_bpt_predecessor_product)))))))) -> n = r * a -> (exists pa_b_bpt_successor pa_c_bpt_successor. ((forall pa_i_bpt_successor_repeat. (exists pa_lt_bpt_successor_repeat_bound. pa_lt_bpt_successor_repeat_bound + S pa_i_bpt_successor_repeat = S e) -> (((exists pa_h_bpt_successor_repeat_decoded. pa_h_bpt_successor_repeat_decoded + S (a) = S ((S (pa_i_bpt_successor_repeat)) * pa_c_bpt_successor)) /\ exists pa_q_bpt_successor_repeat_decoded. pa_b_bpt_successor = pa_q_bpt_successor_repeat_decoded * S ((S (pa_i_bpt_successor_repeat)) * pa_c_bpt_successor) + (a)))) /\ (exists pa_u_bpt_successor_product pa_v_bpt_successor_product. ((((exists pa_h_bpt_successor_product_start. pa_h_bpt_successor_product_start + S (1) = S ((S (0)) * pa_v_bpt_successor_product)) /\ exists pa_q_bpt_successor_product_start. pa_u_bpt_successor_product = pa_q_bpt_successor_product_start * S ((S (0)) * pa_v_bpt_successor_product) + (1))) /\ ((((exists pa_h_bpt_successor_product_terminal. pa_h_bpt_successor_product_terminal + S (n) = S ((S (S e)) * pa_v_bpt_successor_product)) /\ exists pa_q_bpt_successor_product_terminal. pa_u_bpt_successor_product = pa_q_bpt_successor_product_terminal * S ((S (S e)) * pa_v_bpt_successor_product) + (n))) /\ forall pa_i_bpt_successor_product. (exists pa_lt_bpt_successor_product_bound. pa_lt_bpt_successor_product_bound + S pa_i_bpt_successor_product = S e) -> exists pa_p_bpt_successor_product pa_r_bpt_successor_product pa_s_bpt_successor_product. ((((exists pa_h_bpt_successor_product_factor. pa_h_bpt_successor_product_factor + S (pa_p_bpt_successor_product) = S ((S (pa_i_bpt_successor_product)) * pa_c_bpt_successor)) /\ exists pa_q_bpt_successor_product_factor. pa_b_bpt_successor = pa_q_bpt_successor_product_factor * S ((S (pa_i_bpt_successor_product)) * pa_c_bpt_successor) + (pa_p_bpt_successor_product))) /\ ((((exists pa_h_bpt_successor_product_partial. pa_h_bpt_successor_product_partial + S (pa_r_bpt_successor_product) = S ((S (pa_i_bpt_successor_product)) * pa_v_bpt_successor_product)) /\ exists pa_q_bpt_successor_product_partial. pa_u_bpt_successor_product = pa_q_bpt_successor_product_partial * S ((S (pa_i_bpt_successor_product)) * pa_v_bpt_successor_product) + (pa_r_bpt_successor_product))) /\ ((((exists pa_h_bpt_successor_product_successor. pa_h_bpt_successor_product_successor + S (pa_s_bpt_successor_product) = S ((S (S pa_i_bpt_successor_product)) * pa_v_bpt_successor_product)) /\ exists pa_q_bpt_successor_product_successor. pa_u_bpt_successor_product = pa_q_bpt_successor_product_successor * S ((S (S pa_i_bpt_successor_product)) * pa_v_bpt_successor_product) + (pa_s_bpt_successor_product))) /\ pa_s_bpt_successor_product = pa_r_bpt_successor_product * pa_p_bpt_successor_product))))))))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (1)
01Fix variables and assumptionsL1–7
02Establish hsuccessorL8–11
Establish this local claim before using it. It is not an additional assumption.
- L8
have hsuccessor : ∃ x. Pow(a,S e,x)Definitions: Pow(a,S e,x)Original native command in the exact edition - L9
specialize htotal a - L10
specialize htotal (S e) - L11
exact htotal
03Separate the logical casesL12–12
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L12
cases hsuccessor
04Establish hxL13–22
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor pair mul.
Original defined command ledger · 30 lines
- 0001
intro a - 0002
intro e - 0003
intro r - 0004
intro n - 0005
intro htotal - 0006
intro hprevious - 0007
intro hn - 0008
have hsuccessor : ∃ x. Pow(a,S e,x)Exact native replay line
have hsuccessor : exists x. (exists pa_b_bpt_successor_witness pa_c_bpt_successor_witness. ((forall pa_i_bpt_successor_witness_repeat. (exists pa_lt_bpt_successor_witness_repeat_bound. pa_lt_bpt_successor_witness_repeat_bound + S pa_i_bpt_successor_witness_repeat = S e) -> (((exists pa_h_bpt_successor_witness_repeat_decoded. pa_h_bpt_successor_witness_repeat_decoded + S (a) = S ((S (pa_i_bpt_successor_witness_repeat)) * pa_c_bpt_successor_witness)) /\ exists pa_q_bpt_successor_witness_repeat_decoded. pa_b_bpt_successor_witness = pa_q_bpt_successor_witness_repeat_decoded * S ((S (pa_i_bpt_successor_witness_repeat)) * pa_c_bpt_successor_witness) + (a)))) /\ (exists pa_u_bpt_successor_witness_product pa_v_bpt_successor_witness_product. ((((exists pa_h_bpt_successor_witness_product_start. pa_h_bpt_successor_witness_product_start + S (1) = S ((S (0)) * pa_v_bpt_successor_witness_product)) /\ exists pa_q_bpt_successor_witness_product_start. pa_u_bpt_successor_witness_product = pa_q_bpt_successor_witness_product_start * S ((S (0)) * pa_v_bpt_successor_witness_product) + (1))) /\ ((((exists pa_h_bpt_successor_witness_product_terminal. pa_h_bpt_successor_witness_product_terminal + S (x) = S ((S (S e)) * pa_v_bpt_successor_witness_product)) /\ exists pa_q_bpt_successor_witness_product_terminal. pa_u_bpt_successor_witness_product = pa_q_bpt_successor_witness_product_terminal * S ((S (S e)) * pa_v_bpt_successor_witness_product) + (x))) /\ forall pa_i_bpt_successor_witness_product. (exists pa_lt_bpt_successor_witness_product_bound. pa_lt_bpt_successor_witness_product_bound + S pa_i_bpt_successor_witness_product = S e) -> exists pa_p_bpt_successor_witness_product pa_r_bpt_successor_witness_product pa_s_bpt_successor_witness_product. ((((exists pa_h_bpt_successor_witness_product_factor. pa_h_bpt_successor_witness_product_factor + S (pa_p_bpt_successor_witness_product) = S ((S (pa_i_bpt_successor_witness_product)) * pa_c_bpt_successor_witness)) /\ exists pa_q_bpt_successor_witness_product_factor. pa_b_bpt_successor_witness = pa_q_bpt_successor_witness_product_factor * S ((S (pa_i_bpt_successor_witness_product)) * pa_c_bpt_successor_witness) + (pa_p_bpt_successor_witness_product))) /\ ((((exists pa_h_bpt_successor_witness_product_partial. pa_h_bpt_successor_witness_product_partial + S (pa_r_bpt_successor_witness_product) = S ((S (pa_i_bpt_successor_witness_product)) * pa_v_bpt_successor_witness_product)) /\ exists pa_q_bpt_successor_witness_product_partial. pa_u_bpt_successor_witness_product = pa_q_bpt_successor_witness_product_partial * S ((S (pa_i_bpt_successor_witness_product)) * pa_v_bpt_successor_witness_product) + (pa_r_bpt_successor_witness_product))) /\ ((((exists pa_h_bpt_successor_witness_product_successor. pa_h_bpt_successor_witness_product_successor + S (pa_s_bpt_successor_witness_product) = S ((S (S pa_i_bpt_successor_witness_product)) * pa_v_bpt_successor_witness_product)) /\ exists pa_q_bpt_successor_witness_product_successor. pa_u_bpt_successor_witness_product = pa_q_bpt_successor_witness_product_successor * S ((S (S pa_i_bpt_successor_witness_product)) * pa_v_bpt_successor_witness_product) + (pa_s_bpt_successor_witness_product))) /\ pa_s_bpt_successor_witness_product = pa_r_bpt_successor_witness_product * pa_p_bpt_successor_witness_product)))))))) - 0009
specialize htotal a - 0010
specialize htotal (S e) - 0011
exact htotal - 0012
cases hsuccessor - 0013
have hx : x = r * a - 0014
specialize pow_successor_pair_mul a - 0015
specialize pow_successor_pair_mul e - 0016
specialize pow_successor_pair_mul (S e) - 0017
specialize pow_successor_pair_mul r - 0018
specialize pow_successor_pair_mul x - 0019
apply pow_successor_pair_mul - 0020
refl - 0021
exact hprevious - 0022
exact hsuccessor_witness - 0023
have hxn : x = n - 0024
trans r * a - 0025
exact hx - 0026
symm - 0027
exact hn - 0028
rewrite <- hxn - 0029
rewrite <- hxn - 0030
exact hsuccessor_witness