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. 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
2 occurrences
In local proof propositions
1 occurrences
Exact expanded native-PA statement
forall a e r n. (exists ff_b_bpb_predecessor ff_c_bpb_predecessor. ((forall ff_i_bpb_predecessor_repeat. (exists ff_lt_bpb_predecessor_repeat_bound. ff_lt_bpb_predecessor_repeat_bound + S ff_i_bpb_predecessor_repeat = e) -> (((exists ff_h_bpb_predecessor_repeat_decoded. ff_h_bpb_predecessor_repeat_decoded + S (a) = S ((S (ff_i_bpb_predecessor_repeat)) * ff_c_bpb_predecessor)) /\ exists ff_q_bpb_predecessor_repeat_decoded. ff_b_bpb_predecessor = ff_q_bpb_predecessor_repeat_decoded * S ((S (ff_i_bpb_predecessor_repeat)) * ff_c_bpb_predecessor) + (a)))) /\ (exists ff_u_bpb_predecessor_product ff_v_bpb_predecessor_product. ((((exists ff_h_bpb_predecessor_product_start. ff_h_bpb_predecessor_product_start + S (1) = S ((S (0)) * ff_v_bpb_predecessor_product)) /\ exists ff_q_bpb_predecessor_product_start. ff_u_bpb_predecessor_product = ff_q_bpb_predecessor_product_start * S ((S (0)) * ff_v_bpb_predecessor_product) + (1))) /\ ((((exists ff_h_bpb_predecessor_product_terminal. ff_h_bpb_predecessor_product_terminal + S (r) = S ((S (e)) * ff_v_bpb_predecessor_product)) /\ exists ff_q_bpb_predecessor_product_terminal. ff_u_bpb_predecessor_product = ff_q_bpb_predecessor_product_terminal * S ((S (e)) * ff_v_bpb_predecessor_product) + (r))) /\ forall ff_i_bpb_predecessor_product. (exists ff_lt_bpb_predecessor_product_bound. ff_lt_bpb_predecessor_product_bound + S ff_i_bpb_predecessor_product = e) -> exists ff_p_bpb_predecessor_product ff_r_bpb_predecessor_product ff_s_bpb_predecessor_product. ((((exists ff_h_bpb_predecessor_product_factor. ff_h_bpb_predecessor_product_factor + S (ff_p_bpb_predecessor_product) = S ((S (ff_i_bpb_predecessor_product)) * ff_c_bpb_predecessor)) /\ exists ff_q_bpb_predecessor_product_factor. ff_b_bpb_predecessor = ff_q_bpb_predecessor_product_factor * S ((S (ff_i_bpb_predecessor_product)) * ff_c_bpb_predecessor) + (ff_p_bpb_predecessor_product))) /\ ((((exists ff_h_bpb_predecessor_product_partial. ff_h_bpb_predecessor_product_partial + S (ff_r_bpb_predecessor_product) = S ((S (ff_i_bpb_predecessor_product)) * ff_v_bpb_predecessor_product)) /\ exists ff_q_bpb_predecessor_product_partial. ff_u_bpb_predecessor_product = ff_q_bpb_predecessor_product_partial * S ((S (ff_i_bpb_predecessor_product)) * ff_v_bpb_predecessor_product) + (ff_r_bpb_predecessor_product))) /\ ((((exists ff_h_bpb_predecessor_product_successor. ff_h_bpb_predecessor_product_successor + S (ff_s_bpb_predecessor_product) = S ((S (S ff_i_bpb_predecessor_product)) * ff_v_bpb_predecessor_product)) /\ exists ff_q_bpb_predecessor_product_successor. ff_u_bpb_predecessor_product = ff_q_bpb_predecessor_product_successor * S ((S (S ff_i_bpb_predecessor_product)) * ff_v_bpb_predecessor_product) + (ff_s_bpb_predecessor_product))) /\ ff_s_bpb_predecessor_product = ff_r_bpb_predecessor_product * ff_p_bpb_predecessor_product)))))))) -> n = r * a -> (exists pa_b_bpb_successor pa_c_bpb_successor. ((forall pa_i_bpb_successor_repeat. (exists pa_lt_bpb_successor_repeat_bound. pa_lt_bpb_successor_repeat_bound + S pa_i_bpb_successor_repeat = S e) -> (((exists pa_h_bpb_successor_repeat_decoded. pa_h_bpb_successor_repeat_decoded + S (a) = S ((S (pa_i_bpb_successor_repeat)) * pa_c_bpb_successor)) /\ exists pa_q_bpb_successor_repeat_decoded. pa_b_bpb_successor = pa_q_bpb_successor_repeat_decoded * S ((S (pa_i_bpb_successor_repeat)) * pa_c_bpb_successor) + (a)))) /\ (exists pa_u_bpb_successor_product pa_v_bpb_successor_product. ((((exists pa_h_bpb_successor_product_start. pa_h_bpb_successor_product_start + S (1) = S ((S (0)) * pa_v_bpb_successor_product)) /\ exists pa_q_bpb_successor_product_start. pa_u_bpb_successor_product = pa_q_bpb_successor_product_start * S ((S (0)) * pa_v_bpb_successor_product) + (1))) /\ ((((exists pa_h_bpb_successor_product_terminal. pa_h_bpb_successor_product_terminal + S (n) = S ((S (S e)) * pa_v_bpb_successor_product)) /\ exists pa_q_bpb_successor_product_terminal. pa_u_bpb_successor_product = pa_q_bpb_successor_product_terminal * S ((S (S e)) * pa_v_bpb_successor_product) + (n))) /\ forall pa_i_bpb_successor_product. (exists pa_lt_bpb_successor_product_bound. pa_lt_bpb_successor_product_bound + S pa_i_bpb_successor_product = S e) -> exists pa_p_bpb_successor_product pa_r_bpb_successor_product pa_s_bpb_successor_product. ((((exists pa_h_bpb_successor_product_factor. pa_h_bpb_successor_product_factor + S (pa_p_bpb_successor_product) = S ((S (pa_i_bpb_successor_product)) * pa_c_bpb_successor)) /\ exists pa_q_bpb_successor_product_factor. pa_b_bpb_successor = pa_q_bpb_successor_product_factor * S ((S (pa_i_bpb_successor_product)) * pa_c_bpb_successor) + (pa_p_bpb_successor_product))) /\ ((((exists pa_h_bpb_successor_product_partial. pa_h_bpb_successor_product_partial + S (pa_r_bpb_successor_product) = S ((S (pa_i_bpb_successor_product)) * pa_v_bpb_successor_product)) /\ exists pa_q_bpb_successor_product_partial. pa_u_bpb_successor_product = pa_q_bpb_successor_product_partial * S ((S (pa_i_bpb_successor_product)) * pa_v_bpb_successor_product) + (pa_r_bpb_successor_product))) /\ ((((exists pa_h_bpb_successor_product_successor. pa_h_bpb_successor_product_successor + S (pa_s_bpb_successor_product) = S ((S (S pa_i_bpb_successor_product)) * pa_v_bpb_successor_product)) /\ exists pa_q_bpb_successor_product_successor. pa_u_bpb_successor_product = pa_q_bpb_successor_product_successor * S ((S (S pa_i_bpb_successor_product)) * pa_v_bpb_successor_product) + (pa_s_bpb_successor_product))) /\ pa_s_bpb_successor_product = pa_r_bpb_successor_product * pa_p_bpb_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 (2)
01Fix variables and assumptionsL1–6
02Establish hsuccessorL7–10
Establish this local claim before using it. It is not an additional assumption.
- L7
have hsuccessor : ∃ x. Pow(a,S e,x)Definitions: Pow(a,S e,x)Original native command in the exact edition - L8
specialize pow_exists a - L9
specialize pow_exists (S e) - L10
exact pow_exists
03Separate the logical casesL11–11
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L11
cases hsuccessor
04Establish hxL12–21
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 · 29 lines
- 0001
intro a - 0002
intro e - 0003
intro r - 0004
intro n - 0005
intro hprevious - 0006
intro hn - 0007
have hsuccessor : ∃ x. Pow(a,S e,x)Exact native replay line
have hsuccessor : exists x. (exists pa_b_bpb_successor_witness pa_c_bpb_successor_witness. ((forall pa_i_bpb_successor_witness_repeat. (exists pa_lt_bpb_successor_witness_repeat_bound. pa_lt_bpb_successor_witness_repeat_bound + S pa_i_bpb_successor_witness_repeat = S e) -> (((exists pa_h_bpb_successor_witness_repeat_decoded. pa_h_bpb_successor_witness_repeat_decoded + S (a) = S ((S (pa_i_bpb_successor_witness_repeat)) * pa_c_bpb_successor_witness)) /\ exists pa_q_bpb_successor_witness_repeat_decoded. pa_b_bpb_successor_witness = pa_q_bpb_successor_witness_repeat_decoded * S ((S (pa_i_bpb_successor_witness_repeat)) * pa_c_bpb_successor_witness) + (a)))) /\ (exists pa_u_bpb_successor_witness_product pa_v_bpb_successor_witness_product. ((((exists pa_h_bpb_successor_witness_product_start. pa_h_bpb_successor_witness_product_start + S (1) = S ((S (0)) * pa_v_bpb_successor_witness_product)) /\ exists pa_q_bpb_successor_witness_product_start. pa_u_bpb_successor_witness_product = pa_q_bpb_successor_witness_product_start * S ((S (0)) * pa_v_bpb_successor_witness_product) + (1))) /\ ((((exists pa_h_bpb_successor_witness_product_terminal. pa_h_bpb_successor_witness_product_terminal + S (x) = S ((S (S e)) * pa_v_bpb_successor_witness_product)) /\ exists pa_q_bpb_successor_witness_product_terminal. pa_u_bpb_successor_witness_product = pa_q_bpb_successor_witness_product_terminal * S ((S (S e)) * pa_v_bpb_successor_witness_product) + (x))) /\ forall pa_i_bpb_successor_witness_product. (exists pa_lt_bpb_successor_witness_product_bound. pa_lt_bpb_successor_witness_product_bound + S pa_i_bpb_successor_witness_product = S e) -> exists pa_p_bpb_successor_witness_product pa_r_bpb_successor_witness_product pa_s_bpb_successor_witness_product. ((((exists pa_h_bpb_successor_witness_product_factor. pa_h_bpb_successor_witness_product_factor + S (pa_p_bpb_successor_witness_product) = S ((S (pa_i_bpb_successor_witness_product)) * pa_c_bpb_successor_witness)) /\ exists pa_q_bpb_successor_witness_product_factor. pa_b_bpb_successor_witness = pa_q_bpb_successor_witness_product_factor * S ((S (pa_i_bpb_successor_witness_product)) * pa_c_bpb_successor_witness) + (pa_p_bpb_successor_witness_product))) /\ ((((exists pa_h_bpb_successor_witness_product_partial. pa_h_bpb_successor_witness_product_partial + S (pa_r_bpb_successor_witness_product) = S ((S (pa_i_bpb_successor_witness_product)) * pa_v_bpb_successor_witness_product)) /\ exists pa_q_bpb_successor_witness_product_partial. pa_u_bpb_successor_witness_product = pa_q_bpb_successor_witness_product_partial * S ((S (pa_i_bpb_successor_witness_product)) * pa_v_bpb_successor_witness_product) + (pa_r_bpb_successor_witness_product))) /\ ((((exists pa_h_bpb_successor_witness_product_successor. pa_h_bpb_successor_witness_product_successor + S (pa_s_bpb_successor_witness_product) = S ((S (S pa_i_bpb_successor_witness_product)) * pa_v_bpb_successor_witness_product)) /\ exists pa_q_bpb_successor_witness_product_successor. pa_u_bpb_successor_witness_product = pa_q_bpb_successor_witness_product_successor * S ((S (S pa_i_bpb_successor_witness_product)) * pa_v_bpb_successor_witness_product) + (pa_s_bpb_successor_witness_product))) /\ pa_s_bpb_successor_witness_product = pa_r_bpb_successor_witness_product * pa_p_bpb_successor_witness_product)))))))) - 0008
specialize pow_exists a - 0009
specialize pow_exists (S e) - 0010
exact pow_exists - 0011
cases hsuccessor - 0012
have hx : x = r * a - 0013
specialize pow_successor_pair_mul a - 0014
specialize pow_successor_pair_mul e - 0015
specialize pow_successor_pair_mul (S e) - 0016
specialize pow_successor_pair_mul r - 0017
specialize pow_successor_pair_mul x - 0018
apply pow_successor_pair_mul - 0019
refl - 0020
exact hprevious - 0021
exact hsuccessor_witness - 0022
have hxn : x = n - 0023
trans r * a - 0024
exact hx - 0025
symm - 0026
exact hn - 0027
rewrite <- hxn - 0028
rewrite <- hxn - 0029
exact hsuccessor_witness