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
∀ n. ∀ b. ∀ c. ∀ m. (∀ x. Lt(x,m) → ∃ y. BetaAt(b,c,x,y) ∧ (Prime(S x) ∧ (∃ z. PowerValuation(S x,n,z) ∧ Pow(S x,z,y)) ∨ ¬Prime(S x) ∧ y = 1)) → ∀ x. ∀ y. ∀ z. ∀ k. Lt(x,m) → Lt(y,m) → BetaAt(b,c,x,z) → BetaAt(b,c,y,k) → ¬x = y → Coprime(z,k)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
11 occurrences
In local proof propositions
12 occurrences
Exact expanded native-PA statement
forall n b c m. (forall bpr_prefix_index_bpcppc_source. (exists bpr_gap_bpcppc_source_bound. bpr_gap_bpcppc_source_bound + S (bpr_prefix_index_bpcppc_source) = m) -> exists bpr_prefix_value_bpcppc_source. ((((exists bpr_height_bpcppc_source_decoded. bpr_height_bpcppc_source_decoded + S (bpr_prefix_value_bpcppc_source) = S ((S (bpr_prefix_index_bpcppc_source)) * c)) /\ exists bpr_quotient_bpcppc_source_decoded. b = bpr_quotient_bpcppc_source_decoded * S ((S (bpr_prefix_index_bpcppc_source)) * c) + (bpr_prefix_value_bpcppc_source))) /\ (((((~(S (bpr_prefix_index_bpcppc_source) = 1) /\ forall bpr_left_bpcppc_source_choice_prime bpr_right_bpcppc_source_choice_prime. S (bpr_prefix_index_bpcppc_source) = bpr_left_bpcppc_source_choice_prime * bpr_right_bpcppc_source_choice_prime -> bpr_left_bpcppc_source_choice_prime = 1 \/ bpr_right_bpcppc_source_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcppc_source_choice. ((((exists bpr_le_gap_bpcppc_source_choice_valuation_selected_bound. bpr_le_gap_bpcppc_source_choice_valuation_selected_bound + (bpr_choice_exponent_bpcppc_source_choice) = (n)) /\ (exists bpr_power_value_bpcppc_source_choice_valuation_selected. ((exists bpr_power_code_bpcppc_source_choice_valuation_selected_power bpr_power_scale_bpcppc_source_choice_valuation_selected_power. ((forall bpr_power_index_bpcppc_source_choice_valuation_selected_power. (exists bpr_gap_bpcppc_source_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcppc_source_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcppc_source_choice_valuation_selected_power) = bpr_choice_exponent_bpcppc_source_choice) -> (((exists bpr_height_bpcppc_source_choice_valuation_selected_power_repeat_entry. bpr_height_bpcppc_source_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcppc_source)) = S ((S (bpr_power_index_bpcppc_source_choice_valuation_selected_power)) * bpr_power_scale_bpcppc_source_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcppc_source_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcppc_source_choice_valuation_selected_power = bpr_quotient_bpcppc_source_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcppc_source_choice_valuation_selected_power)) * bpr_power_scale_bpcppc_source_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcppc_source))))) /\ (exists ff_u_bpcppc_source_choice_valuation_selected_power_product ff_v_bpcppc_source_choice_valuation_selected_power_product. ((((exists ff_h_bpcppc_source_choice_valuation_selected_power_product_start. ff_h_bpcppc_source_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcppc_source_choice_valuation_selected_power_product)) /\ exists ff_q_bpcppc_source_choice_valuation_selected_power_product_start. ff_u_bpcppc_source_choice_valuation_selected_power_product = ff_q_bpcppc_source_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcppc_source_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcppc_source_choice_valuation_selected_power_product_terminal. ff_h_bpcppc_source_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcppc_source_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcppc_source_choice)) * ff_v_bpcppc_source_choice_valuation_selected_power_product)) /\ exists ff_q_bpcppc_source_choice_valuation_selected_power_product_terminal. ff_u_bpcppc_source_choice_valuation_selected_power_product = ff_q_bpcppc_source_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcppc_source_choice)) * ff_v_bpcppc_source_choice_valuation_selected_power_product) + (bpr_power_value_bpcppc_source_choice_valuation_selected))) /\ forall ff_i_bpcppc_source_choice_valuation_selected_power_product. (exists ff_lt_bpcppc_source_choice_valuation_selected_power_product_bound. ff_lt_bpcppc_source_choice_valuation_selected_power_product_bound + S ff_i_bpcppc_source_choice_valuation_selected_power_product = bpr_choice_exponent_bpcppc_source_choice) -> exists ff_p_bpcppc_source_choice_valuation_selected_power_product ff_r_bpcppc_source_choice_valuation_selected_power_product ff_s_bpcppc_source_choice_valuation_selected_power_product. ((((exists ff_h_bpcppc_source_choice_valuation_selected_power_product_factor. ff_h_bpcppc_source_choice_valuation_selected_power_product_factor + S (ff_p_bpcppc_source_choice_valuation_selected_power_product) = S ((S (ff_i_bpcppc_source_choice_valuation_selected_power_product)) * bpr_power_scale_bpcppc_source_choice_valuation_selected_power)) /\ exists ff_q_bpcppc_source_choice_valuation_selected_power_product_factor. bpr_power_code_bpcppc_source_choice_valuation_selected_power = ff_q_bpcppc_source_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcppc_source_choice_valuation_selected_power_product)) * bpr_power_scale_bpcppc_source_choice_valuation_selected_power) + (ff_p_bpcppc_source_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcppc_source_choice_valuation_selected_power_product_partial. ff_h_bpcppc_source_choice_valuation_selected_power_product_partial + S (ff_r_bpcppc_source_choice_valuation_selected_power_product) = S ((S (ff_i_bpcppc_source_choice_valuation_selected_power_product)) * ff_v_bpcppc_source_choice_valuation_selected_power_product)) /\ exists ff_q_bpcppc_source_choice_valuation_selected_power_product_partial. ff_u_bpcppc_source_choice_valuation_selected_power_product = ff_q_bpcppc_source_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcppc_source_choice_valuation_selected_power_product)) * ff_v_bpcppc_source_choice_valuation_selected_power_product) + (ff_r_bpcppc_source_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcppc_source_choice_valuation_selected_power_product_successor. ff_h_bpcppc_source_choice_valuation_selected_power_product_successor + S (ff_s_bpcppc_source_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcppc_source_choice_valuation_selected_power_product)) * ff_v_bpcppc_source_choice_valuation_selected_power_product)) /\ exists ff_q_bpcppc_source_choice_valuation_selected_power_product_successor. ff_u_bpcppc_source_choice_valuation_selected_power_product = ff_q_bpcppc_source_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcppc_source_choice_valuation_selected_power_product)) * ff_v_bpcppc_source_choice_valuation_selected_power_product) + (ff_s_bpcppc_source_choice_valuation_selected_power_product))) /\ ff_s_bpcppc_source_choice_valuation_selected_power_product = ff_r_bpcppc_source_choice_valuation_selected_power_product * ff_p_bpcppc_source_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcppc_source_choice_valuation_selected_divides. n = (bpr_power_value_bpcppc_source_choice_valuation_selected) * bpr_divides_quotient_bpcppc_source_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcppc_source_choice_valuation. (exists bpr_le_gap_bpcppc_source_choice_valuation_candidate_bound. bpr_le_gap_bpcppc_source_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcppc_source_choice_valuation) = (n)) -> (exists bpr_power_value_bpcppc_source_choice_valuation_candidate. ((exists bpr_power_code_bpcppc_source_choice_valuation_candidate_power bpr_power_scale_bpcppc_source_choice_valuation_candidate_power. ((forall bpr_power_index_bpcppc_source_choice_valuation_candidate_power. (exists bpr_gap_bpcppc_source_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcppc_source_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcppc_source_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcppc_source_choice_valuation) -> (((exists bpr_height_bpcppc_source_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcppc_source_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcppc_source)) = S ((S (bpr_power_index_bpcppc_source_choice_valuation_candidate_power)) * bpr_power_scale_bpcppc_source_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcppc_source_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcppc_source_choice_valuation_candidate_power = bpr_quotient_bpcppc_source_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcppc_source_choice_valuation_candidate_power)) * bpr_power_scale_bpcppc_source_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcppc_source))))) /\ (exists ff_u_bpcppc_source_choice_valuation_candidate_power_product ff_v_bpcppc_source_choice_valuation_candidate_power_product. ((((exists ff_h_bpcppc_source_choice_valuation_candidate_power_product_start. ff_h_bpcppc_source_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcppc_source_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcppc_source_choice_valuation_candidate_power_product_start. ff_u_bpcppc_source_choice_valuation_candidate_power_product = ff_q_bpcppc_source_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcppc_source_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcppc_source_choice_valuation_candidate_power_product_terminal. ff_h_bpcppc_source_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcppc_source_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcppc_source_choice_valuation)) * ff_v_bpcppc_source_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcppc_source_choice_valuation_candidate_power_product_terminal. ff_u_bpcppc_source_choice_valuation_candidate_power_product = ff_q_bpcppc_source_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcppc_source_choice_valuation)) * ff_v_bpcppc_source_choice_valuation_candidate_power_product) + (bpr_power_value_bpcppc_source_choice_valuation_candidate))) /\ forall ff_i_bpcppc_source_choice_valuation_candidate_power_product. (exists ff_lt_bpcppc_source_choice_valuation_candidate_power_product_bound. ff_lt_bpcppc_source_choice_valuation_candidate_power_product_bound + S ff_i_bpcppc_source_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcppc_source_choice_valuation) -> exists ff_p_bpcppc_source_choice_valuation_candidate_power_product ff_r_bpcppc_source_choice_valuation_candidate_power_product ff_s_bpcppc_source_choice_valuation_candidate_power_product. ((((exists ff_h_bpcppc_source_choice_valuation_candidate_power_product_factor. ff_h_bpcppc_source_choice_valuation_candidate_power_product_factor + S (ff_p_bpcppc_source_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcppc_source_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcppc_source_choice_valuation_candidate_power)) /\ exists ff_q_bpcppc_source_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcppc_source_choice_valuation_candidate_power = ff_q_bpcppc_source_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcppc_source_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcppc_source_choice_valuation_candidate_power) + (ff_p_bpcppc_source_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcppc_source_choice_valuation_candidate_power_product_partial. ff_h_bpcppc_source_choice_valuation_candidate_power_product_partial + S (ff_r_bpcppc_source_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcppc_source_choice_valuation_candidate_power_product)) * ff_v_bpcppc_source_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcppc_source_choice_valuation_candidate_power_product_partial. ff_u_bpcppc_source_choice_valuation_candidate_power_product = ff_q_bpcppc_source_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcppc_source_choice_valuation_candidate_power_product)) * ff_v_bpcppc_source_choice_valuation_candidate_power_product) + (ff_r_bpcppc_source_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcppc_source_choice_valuation_candidate_power_product_successor. ff_h_bpcppc_source_choice_valuation_candidate_power_product_successor + S (ff_s_bpcppc_source_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcppc_source_choice_valuation_candidate_power_product)) * ff_v_bpcppc_source_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcppc_source_choice_valuation_candidate_power_product_successor. ff_u_bpcppc_source_choice_valuation_candidate_power_product = ff_q_bpcppc_source_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcppc_source_choice_valuation_candidate_power_product)) * ff_v_bpcppc_source_choice_valuation_candidate_power_product) + (ff_s_bpcppc_source_choice_valuation_candidate_power_product))) /\ ff_s_bpcppc_source_choice_valuation_candidate_power_product = ff_r_bpcppc_source_choice_valuation_candidate_power_product * ff_p_bpcppc_source_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcppc_source_choice_valuation_candidate_divides. n = (bpr_power_value_bpcppc_source_choice_valuation_candidate) * bpr_divides_quotient_bpcppc_source_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcppc_source_choice_valuation_candidate_below. bpr_le_gap_bpcppc_source_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcppc_source_choice_valuation) = (bpr_choice_exponent_bpcppc_source_choice))) /\ (exists bpr_power_code_bpcppc_source_choice_power bpr_power_scale_bpcppc_source_choice_power. ((forall bpr_power_index_bpcppc_source_choice_power. (exists bpr_gap_bpcppc_source_choice_power_repeat_bound. bpr_gap_bpcppc_source_choice_power_repeat_bound + S (bpr_power_index_bpcppc_source_choice_power) = bpr_choice_exponent_bpcppc_source_choice) -> (((exists bpr_height_bpcppc_source_choice_power_repeat_entry. bpr_height_bpcppc_source_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcppc_source)) = S ((S (bpr_power_index_bpcppc_source_choice_power)) * bpr_power_scale_bpcppc_source_choice_power)) /\ exists bpr_quotient_bpcppc_source_choice_power_repeat_entry. bpr_power_code_bpcppc_source_choice_power = bpr_quotient_bpcppc_source_choice_power_repeat_entry * S ((S (bpr_power_index_bpcppc_source_choice_power)) * bpr_power_scale_bpcppc_source_choice_power) + (S (bpr_prefix_index_bpcppc_source))))) /\ (exists ff_u_bpcppc_source_choice_power_product ff_v_bpcppc_source_choice_power_product. ((((exists ff_h_bpcppc_source_choice_power_product_start. ff_h_bpcppc_source_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcppc_source_choice_power_product)) /\ exists ff_q_bpcppc_source_choice_power_product_start. ff_u_bpcppc_source_choice_power_product = ff_q_bpcppc_source_choice_power_product_start * S ((S (0)) * ff_v_bpcppc_source_choice_power_product) + (1))) /\ ((((exists ff_h_bpcppc_source_choice_power_product_terminal. ff_h_bpcppc_source_choice_power_product_terminal + S (bpr_prefix_value_bpcppc_source) = S ((S (bpr_choice_exponent_bpcppc_source_choice)) * ff_v_bpcppc_source_choice_power_product)) /\ exists ff_q_bpcppc_source_choice_power_product_terminal. ff_u_bpcppc_source_choice_power_product = ff_q_bpcppc_source_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcppc_source_choice)) * ff_v_bpcppc_source_choice_power_product) + (bpr_prefix_value_bpcppc_source))) /\ forall ff_i_bpcppc_source_choice_power_product. (exists ff_lt_bpcppc_source_choice_power_product_bound. ff_lt_bpcppc_source_choice_power_product_bound + S ff_i_bpcppc_source_choice_power_product = bpr_choice_exponent_bpcppc_source_choice) -> exists ff_p_bpcppc_source_choice_power_product ff_r_bpcppc_source_choice_power_product ff_s_bpcppc_source_choice_power_product. ((((exists ff_h_bpcppc_source_choice_power_product_factor. ff_h_bpcppc_source_choice_power_product_factor + S (ff_p_bpcppc_source_choice_power_product) = S ((S (ff_i_bpcppc_source_choice_power_product)) * bpr_power_scale_bpcppc_source_choice_power)) /\ exists ff_q_bpcppc_source_choice_power_product_factor. bpr_power_code_bpcppc_source_choice_power = ff_q_bpcppc_source_choice_power_product_factor * S ((S (ff_i_bpcppc_source_choice_power_product)) * bpr_power_scale_bpcppc_source_choice_power) + (ff_p_bpcppc_source_choice_power_product))) /\ ((((exists ff_h_bpcppc_source_choice_power_product_partial. ff_h_bpcppc_source_choice_power_product_partial + S (ff_r_bpcppc_source_choice_power_product) = S ((S (ff_i_bpcppc_source_choice_power_product)) * ff_v_bpcppc_source_choice_power_product)) /\ exists ff_q_bpcppc_source_choice_power_product_partial. ff_u_bpcppc_source_choice_power_product = ff_q_bpcppc_source_choice_power_product_partial * S ((S (ff_i_bpcppc_source_choice_power_product)) * ff_v_bpcppc_source_choice_power_product) + (ff_r_bpcppc_source_choice_power_product))) /\ ((((exists ff_h_bpcppc_source_choice_power_product_successor. ff_h_bpcppc_source_choice_power_product_successor + S (ff_s_bpcppc_source_choice_power_product) = S ((S (S ff_i_bpcppc_source_choice_power_product)) * ff_v_bpcppc_source_choice_power_product)) /\ exists ff_q_bpcppc_source_choice_power_product_successor. ff_u_bpcppc_source_choice_power_product = ff_q_bpcppc_source_choice_power_product_successor * S ((S (S ff_i_bpcppc_source_choice_power_product)) * ff_v_bpcppc_source_choice_power_product) + (ff_s_bpcppc_source_choice_power_product))) /\ ff_s_bpcppc_source_choice_power_product = ff_r_bpcppc_source_choice_power_product * ff_p_bpcppc_source_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcppc_source) = 1) /\ forall bpr_left_bpcppc_source_choice_prime bpr_right_bpcppc_source_choice_prime. S (bpr_prefix_index_bpcppc_source) = bpr_left_bpcppc_source_choice_prime * bpr_right_bpcppc_source_choice_prime -> bpr_left_bpcppc_source_choice_prime = 1 \/ bpr_right_bpcppc_source_choice_prime = 1)) /\ bpr_prefix_value_bpcppc_source = 1))))) -> (forall bpr_pair_left_index_bpcppc_result bpr_pair_right_index_bpcppc_result bpr_pair_left_bpcppc_result bpr_pair_right_bpcppc_result. (exists bpr_gap_bpcppc_result_left_bound. bpr_gap_bpcppc_result_left_bound + S (bpr_pair_left_index_bpcppc_result) = m) -> (exists bpr_gap_bpcppc_result_right_bound. bpr_gap_bpcppc_result_right_bound + S (bpr_pair_right_index_bpcppc_result) = m) -> (((exists bpr_height_bpcppc_result_left_entry. bpr_height_bpcppc_result_left_entry + S (bpr_pair_left_bpcppc_result) = S ((S (bpr_pair_left_index_bpcppc_result)) * c)) /\ exists bpr_quotient_bpcppc_result_left_entry. b = bpr_quotient_bpcppc_result_left_entry * S ((S (bpr_pair_left_index_bpcppc_result)) * c) + (bpr_pair_left_bpcppc_result))) -> (((exists bpr_height_bpcppc_result_right_entry. bpr_height_bpcppc_result_right_entry + S (bpr_pair_right_bpcppc_result) = S ((S (bpr_pair_right_index_bpcppc_result)) * c)) /\ exists bpr_quotient_bpcppc_result_right_entry. b = bpr_quotient_bpcppc_result_right_entry * S ((S (bpr_pair_right_index_bpcppc_result)) * c) + (bpr_pair_right_bpcppc_result))) -> ~(bpr_pair_left_index_bpcppc_result = bpr_pair_right_index_bpcppc_result) -> (forall bpr_coprime_divisor_bpcppc_result_coprime. (exists bpr_coprime_left_bpcppc_result_coprime. bpr_pair_left_bpcppc_result = bpr_coprime_divisor_bpcppc_result_coprime * bpr_coprime_left_bpcppc_result_coprime) -> (exists bpr_coprime_right_bpcppc_result_coprime. bpr_pair_right_bpcppc_result = bpr_coprime_divisor_bpcppc_result_coprime * bpr_coprime_right_bpcppc_result_coprime) -> bpr_coprime_divisor_bpcppc_result_coprime = 1))Proof neighborhood
Direct theorem prerequisites
BT0042 beta_at_unique BT008S distinct_primes_coprime BT002Y coprime_one_left BT002X coprime_one_right BT00YV coprime_powersDirect 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 (5)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–14
03Establish hleftL15–17
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.
- L15
have hleft : ∃ x. BetaAt(b,c,i,x) ∧ (Prime(S i) ∧ (∃ y. PowerValuation(S i,n,y) ∧ Pow(S i,y,x)) ∨ ¬Prime(S i) ∧ x = 1)Definitions: BetaAt(b,c,i,x)Prime(S i)PowerValuation(S i,n,y)Pow(S i,y,x)Original native command in the exact edition - L16
apply hprefix - L17
exact hi
04Separate the logical casesL18–19
05Establish hrightL20–22
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.
- L20
have hright : ∃ x1. BetaAt(b,c,j,x1) ∧ (Prime(S j) ∧ (∃ x. PowerValuation(S j,n,x) ∧ Pow(S j,x,x1)) ∨ ¬Prime(S j) ∧ x1 = 1)Definitions: BetaAt(b,c,j,x1)Prime(S j)PowerValuation(S j,n,x)Pow(S j,x,x1)Original native command in the exact edition - L21
apply hprefix - L22
exact hj
06Separate the logical casesL23–24
07Establish haxL25–28
08Establish hxzL29–32
09Establish hcoprimeL33–33
Establish this local claim before using it. It is not an additional assumption.
10Separate the logical casesL34–41
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
11Establish hbase_neL42–46
12Establish hbase_coprimeL47–56
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply distinct primes coprime.
- L47
have hbase_coprime : Coprime(S i,S j)Definitions: Coprime(S i,S j)Original native command in the exact edition - L48
specialize distinct_primes_coprime (S i) - L49
specialize distinct_primes_coprime (S j) - L50
apply distinct_primes_coprime - L51
exact hleft_witness_right_left_left - L52
exact hright_witness_right_left_left - L53
exact hbase_ne - L54
specialize coprime_powers (S i) - L55
specialize coprime_powers (S j) - L56
specialize coprime_powers x2
13Use earlier factsL57–63
Instantiate or apply named facts and discharge the corresponding proof obligations.
14Separate the logical casesL64–64
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L64
cases hright_witness_right_right
15Calculate and transport equalitiesL65–65
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L65
rewrite hright_witness_right_right_right
16Use earlier factsL66–67
17Separate the logical casesL68–69
18Calculate and transport equalitiesL70–70
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L70
rewrite hleft_witness_right_right_right
19Use earlier factsL71–72
20Separate the logical casesL73–73
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L73
cases hright_witness_right_right
21Calculate and transport equalitiesL74–74
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L74
rewrite hleft_witness_right_right_right
22Use earlier factsL75–76
23Calculate and transport equalitiesL77–78
24Use earlier factsL79–79
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L79
exact hcoprime
Original defined command ledger · 79 lines
- 0001
intro n - 0002
intro b - 0003
intro c - 0004
intro m - 0005
intro hprefix - 0006
intro i - 0007
intro j - 0008
intro a - 0009
intro z - 0010
intro hi - 0011
intro hj - 0012
intro ha - 0013
intro hz - 0014
intro hij - 0015
have hleft : ∃ x. BetaAt(b,c,i,x) ∧ (Prime(S i) ∧ (∃ y. PowerValuation(S i,n,y) ∧ Pow(S i,y,x)) ∨ ¬Prime(S i) ∧ x = 1)Exact native replay line
have hleft : exists x. (((exists bpr_height_bpcppc_left_entry. bpr_height_bpcppc_left_entry + S (x) = S ((S (i)) * c)) /\ exists bpr_quotient_bpcppc_left_entry. b = bpr_quotient_bpcppc_left_entry * S ((S (i)) * c) + (x))) /\ (((((~(S (i) = 1) /\ forall bpr_left_bpcppc_left_choice_prime bpr_right_bpcppc_left_choice_prime. S (i) = bpr_left_bpcppc_left_choice_prime * bpr_right_bpcppc_left_choice_prime -> bpr_left_bpcppc_left_choice_prime = 1 \/ bpr_right_bpcppc_left_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcppc_left_choice. ((((exists bpr_le_gap_bpcppc_left_choice_valuation_selected_bound. bpr_le_gap_bpcppc_left_choice_valuation_selected_bound + (bpr_choice_exponent_bpcppc_left_choice) = (n)) /\ (exists bpr_power_value_bpcppc_left_choice_valuation_selected. ((exists bpr_power_code_bpcppc_left_choice_valuation_selected_power bpr_power_scale_bpcppc_left_choice_valuation_selected_power. ((forall bpr_power_index_bpcppc_left_choice_valuation_selected_power. (exists bpr_gap_bpcppc_left_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcppc_left_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcppc_left_choice_valuation_selected_power) = bpr_choice_exponent_bpcppc_left_choice) -> (((exists bpr_height_bpcppc_left_choice_valuation_selected_power_repeat_entry. bpr_height_bpcppc_left_choice_valuation_selected_power_repeat_entry + S (S (i)) = S ((S (bpr_power_index_bpcppc_left_choice_valuation_selected_power)) * bpr_power_scale_bpcppc_left_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcppc_left_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcppc_left_choice_valuation_selected_power = bpr_quotient_bpcppc_left_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcppc_left_choice_valuation_selected_power)) * bpr_power_scale_bpcppc_left_choice_valuation_selected_power) + (S (i))))) /\ (exists ff_u_bpcppc_left_choice_valuation_selected_power_product ff_v_bpcppc_left_choice_valuation_selected_power_product. ((((exists ff_h_bpcppc_left_choice_valuation_selected_power_product_start. ff_h_bpcppc_left_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcppc_left_choice_valuation_selected_power_product)) /\ exists ff_q_bpcppc_left_choice_valuation_selected_power_product_start. ff_u_bpcppc_left_choice_valuation_selected_power_product = ff_q_bpcppc_left_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcppc_left_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcppc_left_choice_valuation_selected_power_product_terminal. ff_h_bpcppc_left_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcppc_left_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcppc_left_choice)) * ff_v_bpcppc_left_choice_valuation_selected_power_product)) /\ exists ff_q_bpcppc_left_choice_valuation_selected_power_product_terminal. ff_u_bpcppc_left_choice_valuation_selected_power_product = ff_q_bpcppc_left_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcppc_left_choice)) * ff_v_bpcppc_left_choice_valuation_selected_power_product) + (bpr_power_value_bpcppc_left_choice_valuation_selected))) /\ forall ff_i_bpcppc_left_choice_valuation_selected_power_product. (exists ff_lt_bpcppc_left_choice_valuation_selected_power_product_bound. ff_lt_bpcppc_left_choice_valuation_selected_power_product_bound + S ff_i_bpcppc_left_choice_valuation_selected_power_product = bpr_choice_exponent_bpcppc_left_choice) -> exists ff_p_bpcppc_left_choice_valuation_selected_power_product ff_r_bpcppc_left_choice_valuation_selected_power_product ff_s_bpcppc_left_choice_valuation_selected_power_product. ((((exists ff_h_bpcppc_left_choice_valuation_selected_power_product_factor. ff_h_bpcppc_left_choice_valuation_selected_power_product_factor + S (ff_p_bpcppc_left_choice_valuation_selected_power_product) = S ((S (ff_i_bpcppc_left_choice_valuation_selected_power_product)) * bpr_power_scale_bpcppc_left_choice_valuation_selected_power)) /\ exists ff_q_bpcppc_left_choice_valuation_selected_power_product_factor. bpr_power_code_bpcppc_left_choice_valuation_selected_power = ff_q_bpcppc_left_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcppc_left_choice_valuation_selected_power_product)) * bpr_power_scale_bpcppc_left_choice_valuation_selected_power) + (ff_p_bpcppc_left_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcppc_left_choice_valuation_selected_power_product_partial. ff_h_bpcppc_left_choice_valuation_selected_power_product_partial + S (ff_r_bpcppc_left_choice_valuation_selected_power_product) = S ((S (ff_i_bpcppc_left_choice_valuation_selected_power_product)) * ff_v_bpcppc_left_choice_valuation_selected_power_product)) /\ exists ff_q_bpcppc_left_choice_valuation_selected_power_product_partial. ff_u_bpcppc_left_choice_valuation_selected_power_product = ff_q_bpcppc_left_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcppc_left_choice_valuation_selected_power_product)) * ff_v_bpcppc_left_choice_valuation_selected_power_product) + (ff_r_bpcppc_left_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcppc_left_choice_valuation_selected_power_product_successor. ff_h_bpcppc_left_choice_valuation_selected_power_product_successor + S (ff_s_bpcppc_left_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcppc_left_choice_valuation_selected_power_product)) * ff_v_bpcppc_left_choice_valuation_selected_power_product)) /\ exists ff_q_bpcppc_left_choice_valuation_selected_power_product_successor. ff_u_bpcppc_left_choice_valuation_selected_power_product = ff_q_bpcppc_left_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcppc_left_choice_valuation_selected_power_product)) * ff_v_bpcppc_left_choice_valuation_selected_power_product) + (ff_s_bpcppc_left_choice_valuation_selected_power_product))) /\ ff_s_bpcppc_left_choice_valuation_selected_power_product = ff_r_bpcppc_left_choice_valuation_selected_power_product * ff_p_bpcppc_left_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcppc_left_choice_valuation_selected_divides. n = (bpr_power_value_bpcppc_left_choice_valuation_selected) * bpr_divides_quotient_bpcppc_left_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcppc_left_choice_valuation. (exists bpr_le_gap_bpcppc_left_choice_valuation_candidate_bound. bpr_le_gap_bpcppc_left_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcppc_left_choice_valuation) = (n)) -> (exists bpr_power_value_bpcppc_left_choice_valuation_candidate. ((exists bpr_power_code_bpcppc_left_choice_valuation_candidate_power bpr_power_scale_bpcppc_left_choice_valuation_candidate_power. ((forall bpr_power_index_bpcppc_left_choice_valuation_candidate_power. (exists bpr_gap_bpcppc_left_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcppc_left_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcppc_left_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcppc_left_choice_valuation) -> (((exists bpr_height_bpcppc_left_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcppc_left_choice_valuation_candidate_power_repeat_entry + S (S (i)) = S ((S (bpr_power_index_bpcppc_left_choice_valuation_candidate_power)) * bpr_power_scale_bpcppc_left_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcppc_left_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcppc_left_choice_valuation_candidate_power = bpr_quotient_bpcppc_left_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcppc_left_choice_valuation_candidate_power)) * bpr_power_scale_bpcppc_left_choice_valuation_candidate_power) + (S (i))))) /\ (exists ff_u_bpcppc_left_choice_valuation_candidate_power_product ff_v_bpcppc_left_choice_valuation_candidate_power_product. ((((exists ff_h_bpcppc_left_choice_valuation_candidate_power_product_start. ff_h_bpcppc_left_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcppc_left_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcppc_left_choice_valuation_candidate_power_product_start. ff_u_bpcppc_left_choice_valuation_candidate_power_product = ff_q_bpcppc_left_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcppc_left_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcppc_left_choice_valuation_candidate_power_product_terminal. ff_h_bpcppc_left_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcppc_left_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcppc_left_choice_valuation)) * ff_v_bpcppc_left_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcppc_left_choice_valuation_candidate_power_product_terminal. ff_u_bpcppc_left_choice_valuation_candidate_power_product = ff_q_bpcppc_left_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcppc_left_choice_valuation)) * ff_v_bpcppc_left_choice_valuation_candidate_power_product) + (bpr_power_value_bpcppc_left_choice_valuation_candidate))) /\ forall ff_i_bpcppc_left_choice_valuation_candidate_power_product. (exists ff_lt_bpcppc_left_choice_valuation_candidate_power_product_bound. ff_lt_bpcppc_left_choice_valuation_candidate_power_product_bound + S ff_i_bpcppc_left_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcppc_left_choice_valuation) -> exists ff_p_bpcppc_left_choice_valuation_candidate_power_product ff_r_bpcppc_left_choice_valuation_candidate_power_product ff_s_bpcppc_left_choice_valuation_candidate_power_product. ((((exists ff_h_bpcppc_left_choice_valuation_candidate_power_product_factor. ff_h_bpcppc_left_choice_valuation_candidate_power_product_factor + S (ff_p_bpcppc_left_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcppc_left_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcppc_left_choice_valuation_candidate_power)) /\ exists ff_q_bpcppc_left_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcppc_left_choice_valuation_candidate_power = ff_q_bpcppc_left_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcppc_left_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcppc_left_choice_valuation_candidate_power) + (ff_p_bpcppc_left_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcppc_left_choice_valuation_candidate_power_product_partial. ff_h_bpcppc_left_choice_valuation_candidate_power_product_partial + S (ff_r_bpcppc_left_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcppc_left_choice_valuation_candidate_power_product)) * ff_v_bpcppc_left_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcppc_left_choice_valuation_candidate_power_product_partial. ff_u_bpcppc_left_choice_valuation_candidate_power_product = ff_q_bpcppc_left_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcppc_left_choice_valuation_candidate_power_product)) * ff_v_bpcppc_left_choice_valuation_candidate_power_product) + (ff_r_bpcppc_left_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcppc_left_choice_valuation_candidate_power_product_successor. ff_h_bpcppc_left_choice_valuation_candidate_power_product_successor + S (ff_s_bpcppc_left_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcppc_left_choice_valuation_candidate_power_product)) * ff_v_bpcppc_left_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcppc_left_choice_valuation_candidate_power_product_successor. ff_u_bpcppc_left_choice_valuation_candidate_power_product = ff_q_bpcppc_left_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcppc_left_choice_valuation_candidate_power_product)) * ff_v_bpcppc_left_choice_valuation_candidate_power_product) + (ff_s_bpcppc_left_choice_valuation_candidate_power_product))) /\ ff_s_bpcppc_left_choice_valuation_candidate_power_product = ff_r_bpcppc_left_choice_valuation_candidate_power_product * ff_p_bpcppc_left_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcppc_left_choice_valuation_candidate_divides. n = (bpr_power_value_bpcppc_left_choice_valuation_candidate) * bpr_divides_quotient_bpcppc_left_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcppc_left_choice_valuation_candidate_below. bpr_le_gap_bpcppc_left_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcppc_left_choice_valuation) = (bpr_choice_exponent_bpcppc_left_choice))) /\ (exists bpr_power_code_bpcppc_left_choice_power bpr_power_scale_bpcppc_left_choice_power. ((forall bpr_power_index_bpcppc_left_choice_power. (exists bpr_gap_bpcppc_left_choice_power_repeat_bound. bpr_gap_bpcppc_left_choice_power_repeat_bound + S (bpr_power_index_bpcppc_left_choice_power) = bpr_choice_exponent_bpcppc_left_choice) -> (((exists bpr_height_bpcppc_left_choice_power_repeat_entry. bpr_height_bpcppc_left_choice_power_repeat_entry + S (S (i)) = S ((S (bpr_power_index_bpcppc_left_choice_power)) * bpr_power_scale_bpcppc_left_choice_power)) /\ exists bpr_quotient_bpcppc_left_choice_power_repeat_entry. bpr_power_code_bpcppc_left_choice_power = bpr_quotient_bpcppc_left_choice_power_repeat_entry * S ((S (bpr_power_index_bpcppc_left_choice_power)) * bpr_power_scale_bpcppc_left_choice_power) + (S (i))))) /\ (exists ff_u_bpcppc_left_choice_power_product ff_v_bpcppc_left_choice_power_product. ((((exists ff_h_bpcppc_left_choice_power_product_start. ff_h_bpcppc_left_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcppc_left_choice_power_product)) /\ exists ff_q_bpcppc_left_choice_power_product_start. ff_u_bpcppc_left_choice_power_product = ff_q_bpcppc_left_choice_power_product_start * S ((S (0)) * ff_v_bpcppc_left_choice_power_product) + (1))) /\ ((((exists ff_h_bpcppc_left_choice_power_product_terminal. ff_h_bpcppc_left_choice_power_product_terminal + S (x) = S ((S (bpr_choice_exponent_bpcppc_left_choice)) * ff_v_bpcppc_left_choice_power_product)) /\ exists ff_q_bpcppc_left_choice_power_product_terminal. ff_u_bpcppc_left_choice_power_product = ff_q_bpcppc_left_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcppc_left_choice)) * ff_v_bpcppc_left_choice_power_product) + (x))) /\ forall ff_i_bpcppc_left_choice_power_product. (exists ff_lt_bpcppc_left_choice_power_product_bound. ff_lt_bpcppc_left_choice_power_product_bound + S ff_i_bpcppc_left_choice_power_product = bpr_choice_exponent_bpcppc_left_choice) -> exists ff_p_bpcppc_left_choice_power_product ff_r_bpcppc_left_choice_power_product ff_s_bpcppc_left_choice_power_product. ((((exists ff_h_bpcppc_left_choice_power_product_factor. ff_h_bpcppc_left_choice_power_product_factor + S (ff_p_bpcppc_left_choice_power_product) = S ((S (ff_i_bpcppc_left_choice_power_product)) * bpr_power_scale_bpcppc_left_choice_power)) /\ exists ff_q_bpcppc_left_choice_power_product_factor. bpr_power_code_bpcppc_left_choice_power = ff_q_bpcppc_left_choice_power_product_factor * S ((S (ff_i_bpcppc_left_choice_power_product)) * bpr_power_scale_bpcppc_left_choice_power) + (ff_p_bpcppc_left_choice_power_product))) /\ ((((exists ff_h_bpcppc_left_choice_power_product_partial. ff_h_bpcppc_left_choice_power_product_partial + S (ff_r_bpcppc_left_choice_power_product) = S ((S (ff_i_bpcppc_left_choice_power_product)) * ff_v_bpcppc_left_choice_power_product)) /\ exists ff_q_bpcppc_left_choice_power_product_partial. ff_u_bpcppc_left_choice_power_product = ff_q_bpcppc_left_choice_power_product_partial * S ((S (ff_i_bpcppc_left_choice_power_product)) * ff_v_bpcppc_left_choice_power_product) + (ff_r_bpcppc_left_choice_power_product))) /\ ((((exists ff_h_bpcppc_left_choice_power_product_successor. ff_h_bpcppc_left_choice_power_product_successor + S (ff_s_bpcppc_left_choice_power_product) = S ((S (S ff_i_bpcppc_left_choice_power_product)) * ff_v_bpcppc_left_choice_power_product)) /\ exists ff_q_bpcppc_left_choice_power_product_successor. ff_u_bpcppc_left_choice_power_product = ff_q_bpcppc_left_choice_power_product_successor * S ((S (S ff_i_bpcppc_left_choice_power_product)) * ff_v_bpcppc_left_choice_power_product) + (ff_s_bpcppc_left_choice_power_product))) /\ ff_s_bpcppc_left_choice_power_product = ff_r_bpcppc_left_choice_power_product * ff_p_bpcppc_left_choice_power_product)))))))))) \/ (~((~(S (i) = 1) /\ forall bpr_left_bpcppc_left_choice_prime bpr_right_bpcppc_left_choice_prime. S (i) = bpr_left_bpcppc_left_choice_prime * bpr_right_bpcppc_left_choice_prime -> bpr_left_bpcppc_left_choice_prime = 1 \/ bpr_right_bpcppc_left_choice_prime = 1)) /\ x = 1))) - 0016
apply hprefix - 0017
exact hi - 0018
cases hleft - 0019
cases hleft_witness - 0020
have hright : ∃ x1. BetaAt(b,c,j,x1) ∧ (Prime(S j) ∧ (∃ x. PowerValuation(S j,n,x) ∧ Pow(S j,x,x1)) ∨ ¬Prime(S j) ∧ x1 = 1)Exact native replay line
have hright : exists x1. (((exists bpr_height_bpcppc_right_entry. bpr_height_bpcppc_right_entry + S (x1) = S ((S (j)) * c)) /\ exists bpr_quotient_bpcppc_right_entry. b = bpr_quotient_bpcppc_right_entry * S ((S (j)) * c) + (x1))) /\ (((((~(S (j) = 1) /\ forall bpr_left_bpcppc_right_choice_prime bpr_right_bpcppc_right_choice_prime. S (j) = bpr_left_bpcppc_right_choice_prime * bpr_right_bpcppc_right_choice_prime -> bpr_left_bpcppc_right_choice_prime = 1 \/ bpr_right_bpcppc_right_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcppc_right_choice. ((((exists bpr_le_gap_bpcppc_right_choice_valuation_selected_bound. bpr_le_gap_bpcppc_right_choice_valuation_selected_bound + (bpr_choice_exponent_bpcppc_right_choice) = (n)) /\ (exists bpr_power_value_bpcppc_right_choice_valuation_selected. ((exists bpr_power_code_bpcppc_right_choice_valuation_selected_power bpr_power_scale_bpcppc_right_choice_valuation_selected_power. ((forall bpr_power_index_bpcppc_right_choice_valuation_selected_power. (exists bpr_gap_bpcppc_right_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcppc_right_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcppc_right_choice_valuation_selected_power) = bpr_choice_exponent_bpcppc_right_choice) -> (((exists bpr_height_bpcppc_right_choice_valuation_selected_power_repeat_entry. bpr_height_bpcppc_right_choice_valuation_selected_power_repeat_entry + S (S (j)) = S ((S (bpr_power_index_bpcppc_right_choice_valuation_selected_power)) * bpr_power_scale_bpcppc_right_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcppc_right_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcppc_right_choice_valuation_selected_power = bpr_quotient_bpcppc_right_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcppc_right_choice_valuation_selected_power)) * bpr_power_scale_bpcppc_right_choice_valuation_selected_power) + (S (j))))) /\ (exists ff_u_bpcppc_right_choice_valuation_selected_power_product ff_v_bpcppc_right_choice_valuation_selected_power_product. ((((exists ff_h_bpcppc_right_choice_valuation_selected_power_product_start. ff_h_bpcppc_right_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcppc_right_choice_valuation_selected_power_product)) /\ exists ff_q_bpcppc_right_choice_valuation_selected_power_product_start. ff_u_bpcppc_right_choice_valuation_selected_power_product = ff_q_bpcppc_right_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcppc_right_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcppc_right_choice_valuation_selected_power_product_terminal. ff_h_bpcppc_right_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcppc_right_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcppc_right_choice)) * ff_v_bpcppc_right_choice_valuation_selected_power_product)) /\ exists ff_q_bpcppc_right_choice_valuation_selected_power_product_terminal. ff_u_bpcppc_right_choice_valuation_selected_power_product = ff_q_bpcppc_right_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcppc_right_choice)) * ff_v_bpcppc_right_choice_valuation_selected_power_product) + (bpr_power_value_bpcppc_right_choice_valuation_selected))) /\ forall ff_i_bpcppc_right_choice_valuation_selected_power_product. (exists ff_lt_bpcppc_right_choice_valuation_selected_power_product_bound. ff_lt_bpcppc_right_choice_valuation_selected_power_product_bound + S ff_i_bpcppc_right_choice_valuation_selected_power_product = bpr_choice_exponent_bpcppc_right_choice) -> exists ff_p_bpcppc_right_choice_valuation_selected_power_product ff_r_bpcppc_right_choice_valuation_selected_power_product ff_s_bpcppc_right_choice_valuation_selected_power_product. ((((exists ff_h_bpcppc_right_choice_valuation_selected_power_product_factor. ff_h_bpcppc_right_choice_valuation_selected_power_product_factor + S (ff_p_bpcppc_right_choice_valuation_selected_power_product) = S ((S (ff_i_bpcppc_right_choice_valuation_selected_power_product)) * bpr_power_scale_bpcppc_right_choice_valuation_selected_power)) /\ exists ff_q_bpcppc_right_choice_valuation_selected_power_product_factor. bpr_power_code_bpcppc_right_choice_valuation_selected_power = ff_q_bpcppc_right_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcppc_right_choice_valuation_selected_power_product)) * bpr_power_scale_bpcppc_right_choice_valuation_selected_power) + (ff_p_bpcppc_right_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcppc_right_choice_valuation_selected_power_product_partial. ff_h_bpcppc_right_choice_valuation_selected_power_product_partial + S (ff_r_bpcppc_right_choice_valuation_selected_power_product) = S ((S (ff_i_bpcppc_right_choice_valuation_selected_power_product)) * ff_v_bpcppc_right_choice_valuation_selected_power_product)) /\ exists ff_q_bpcppc_right_choice_valuation_selected_power_product_partial. ff_u_bpcppc_right_choice_valuation_selected_power_product = ff_q_bpcppc_right_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcppc_right_choice_valuation_selected_power_product)) * ff_v_bpcppc_right_choice_valuation_selected_power_product) + (ff_r_bpcppc_right_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcppc_right_choice_valuation_selected_power_product_successor. ff_h_bpcppc_right_choice_valuation_selected_power_product_successor + S (ff_s_bpcppc_right_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcppc_right_choice_valuation_selected_power_product)) * ff_v_bpcppc_right_choice_valuation_selected_power_product)) /\ exists ff_q_bpcppc_right_choice_valuation_selected_power_product_successor. ff_u_bpcppc_right_choice_valuation_selected_power_product = ff_q_bpcppc_right_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcppc_right_choice_valuation_selected_power_product)) * ff_v_bpcppc_right_choice_valuation_selected_power_product) + (ff_s_bpcppc_right_choice_valuation_selected_power_product))) /\ ff_s_bpcppc_right_choice_valuation_selected_power_product = ff_r_bpcppc_right_choice_valuation_selected_power_product * ff_p_bpcppc_right_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcppc_right_choice_valuation_selected_divides. n = (bpr_power_value_bpcppc_right_choice_valuation_selected) * bpr_divides_quotient_bpcppc_right_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcppc_right_choice_valuation. (exists bpr_le_gap_bpcppc_right_choice_valuation_candidate_bound. bpr_le_gap_bpcppc_right_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcppc_right_choice_valuation) = (n)) -> (exists bpr_power_value_bpcppc_right_choice_valuation_candidate. ((exists bpr_power_code_bpcppc_right_choice_valuation_candidate_power bpr_power_scale_bpcppc_right_choice_valuation_candidate_power. ((forall bpr_power_index_bpcppc_right_choice_valuation_candidate_power. (exists bpr_gap_bpcppc_right_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcppc_right_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcppc_right_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcppc_right_choice_valuation) -> (((exists bpr_height_bpcppc_right_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcppc_right_choice_valuation_candidate_power_repeat_entry + S (S (j)) = S ((S (bpr_power_index_bpcppc_right_choice_valuation_candidate_power)) * bpr_power_scale_bpcppc_right_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcppc_right_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcppc_right_choice_valuation_candidate_power = bpr_quotient_bpcppc_right_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcppc_right_choice_valuation_candidate_power)) * bpr_power_scale_bpcppc_right_choice_valuation_candidate_power) + (S (j))))) /\ (exists ff_u_bpcppc_right_choice_valuation_candidate_power_product ff_v_bpcppc_right_choice_valuation_candidate_power_product. ((((exists ff_h_bpcppc_right_choice_valuation_candidate_power_product_start. ff_h_bpcppc_right_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcppc_right_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcppc_right_choice_valuation_candidate_power_product_start. ff_u_bpcppc_right_choice_valuation_candidate_power_product = ff_q_bpcppc_right_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcppc_right_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcppc_right_choice_valuation_candidate_power_product_terminal. ff_h_bpcppc_right_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcppc_right_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcppc_right_choice_valuation)) * ff_v_bpcppc_right_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcppc_right_choice_valuation_candidate_power_product_terminal. ff_u_bpcppc_right_choice_valuation_candidate_power_product = ff_q_bpcppc_right_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcppc_right_choice_valuation)) * ff_v_bpcppc_right_choice_valuation_candidate_power_product) + (bpr_power_value_bpcppc_right_choice_valuation_candidate))) /\ forall ff_i_bpcppc_right_choice_valuation_candidate_power_product. (exists ff_lt_bpcppc_right_choice_valuation_candidate_power_product_bound. ff_lt_bpcppc_right_choice_valuation_candidate_power_product_bound + S ff_i_bpcppc_right_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcppc_right_choice_valuation) -> exists ff_p_bpcppc_right_choice_valuation_candidate_power_product ff_r_bpcppc_right_choice_valuation_candidate_power_product ff_s_bpcppc_right_choice_valuation_candidate_power_product. ((((exists ff_h_bpcppc_right_choice_valuation_candidate_power_product_factor. ff_h_bpcppc_right_choice_valuation_candidate_power_product_factor + S (ff_p_bpcppc_right_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcppc_right_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcppc_right_choice_valuation_candidate_power)) /\ exists ff_q_bpcppc_right_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcppc_right_choice_valuation_candidate_power = ff_q_bpcppc_right_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcppc_right_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcppc_right_choice_valuation_candidate_power) + (ff_p_bpcppc_right_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcppc_right_choice_valuation_candidate_power_product_partial. ff_h_bpcppc_right_choice_valuation_candidate_power_product_partial + S (ff_r_bpcppc_right_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcppc_right_choice_valuation_candidate_power_product)) * ff_v_bpcppc_right_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcppc_right_choice_valuation_candidate_power_product_partial. ff_u_bpcppc_right_choice_valuation_candidate_power_product = ff_q_bpcppc_right_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcppc_right_choice_valuation_candidate_power_product)) * ff_v_bpcppc_right_choice_valuation_candidate_power_product) + (ff_r_bpcppc_right_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcppc_right_choice_valuation_candidate_power_product_successor. ff_h_bpcppc_right_choice_valuation_candidate_power_product_successor + S (ff_s_bpcppc_right_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcppc_right_choice_valuation_candidate_power_product)) * ff_v_bpcppc_right_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcppc_right_choice_valuation_candidate_power_product_successor. ff_u_bpcppc_right_choice_valuation_candidate_power_product = ff_q_bpcppc_right_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcppc_right_choice_valuation_candidate_power_product)) * ff_v_bpcppc_right_choice_valuation_candidate_power_product) + (ff_s_bpcppc_right_choice_valuation_candidate_power_product))) /\ ff_s_bpcppc_right_choice_valuation_candidate_power_product = ff_r_bpcppc_right_choice_valuation_candidate_power_product * ff_p_bpcppc_right_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcppc_right_choice_valuation_candidate_divides. n = (bpr_power_value_bpcppc_right_choice_valuation_candidate) * bpr_divides_quotient_bpcppc_right_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcppc_right_choice_valuation_candidate_below. bpr_le_gap_bpcppc_right_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcppc_right_choice_valuation) = (bpr_choice_exponent_bpcppc_right_choice))) /\ (exists bpr_power_code_bpcppc_right_choice_power bpr_power_scale_bpcppc_right_choice_power. ((forall bpr_power_index_bpcppc_right_choice_power. (exists bpr_gap_bpcppc_right_choice_power_repeat_bound. bpr_gap_bpcppc_right_choice_power_repeat_bound + S (bpr_power_index_bpcppc_right_choice_power) = bpr_choice_exponent_bpcppc_right_choice) -> (((exists bpr_height_bpcppc_right_choice_power_repeat_entry. bpr_height_bpcppc_right_choice_power_repeat_entry + S (S (j)) = S ((S (bpr_power_index_bpcppc_right_choice_power)) * bpr_power_scale_bpcppc_right_choice_power)) /\ exists bpr_quotient_bpcppc_right_choice_power_repeat_entry. bpr_power_code_bpcppc_right_choice_power = bpr_quotient_bpcppc_right_choice_power_repeat_entry * S ((S (bpr_power_index_bpcppc_right_choice_power)) * bpr_power_scale_bpcppc_right_choice_power) + (S (j))))) /\ (exists ff_u_bpcppc_right_choice_power_product ff_v_bpcppc_right_choice_power_product. ((((exists ff_h_bpcppc_right_choice_power_product_start. ff_h_bpcppc_right_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcppc_right_choice_power_product)) /\ exists ff_q_bpcppc_right_choice_power_product_start. ff_u_bpcppc_right_choice_power_product = ff_q_bpcppc_right_choice_power_product_start * S ((S (0)) * ff_v_bpcppc_right_choice_power_product) + (1))) /\ ((((exists ff_h_bpcppc_right_choice_power_product_terminal. ff_h_bpcppc_right_choice_power_product_terminal + S (x1) = S ((S (bpr_choice_exponent_bpcppc_right_choice)) * ff_v_bpcppc_right_choice_power_product)) /\ exists ff_q_bpcppc_right_choice_power_product_terminal. ff_u_bpcppc_right_choice_power_product = ff_q_bpcppc_right_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcppc_right_choice)) * ff_v_bpcppc_right_choice_power_product) + (x1))) /\ forall ff_i_bpcppc_right_choice_power_product. (exists ff_lt_bpcppc_right_choice_power_product_bound. ff_lt_bpcppc_right_choice_power_product_bound + S ff_i_bpcppc_right_choice_power_product = bpr_choice_exponent_bpcppc_right_choice) -> exists ff_p_bpcppc_right_choice_power_product ff_r_bpcppc_right_choice_power_product ff_s_bpcppc_right_choice_power_product. ((((exists ff_h_bpcppc_right_choice_power_product_factor. ff_h_bpcppc_right_choice_power_product_factor + S (ff_p_bpcppc_right_choice_power_product) = S ((S (ff_i_bpcppc_right_choice_power_product)) * bpr_power_scale_bpcppc_right_choice_power)) /\ exists ff_q_bpcppc_right_choice_power_product_factor. bpr_power_code_bpcppc_right_choice_power = ff_q_bpcppc_right_choice_power_product_factor * S ((S (ff_i_bpcppc_right_choice_power_product)) * bpr_power_scale_bpcppc_right_choice_power) + (ff_p_bpcppc_right_choice_power_product))) /\ ((((exists ff_h_bpcppc_right_choice_power_product_partial. ff_h_bpcppc_right_choice_power_product_partial + S (ff_r_bpcppc_right_choice_power_product) = S ((S (ff_i_bpcppc_right_choice_power_product)) * ff_v_bpcppc_right_choice_power_product)) /\ exists ff_q_bpcppc_right_choice_power_product_partial. ff_u_bpcppc_right_choice_power_product = ff_q_bpcppc_right_choice_power_product_partial * S ((S (ff_i_bpcppc_right_choice_power_product)) * ff_v_bpcppc_right_choice_power_product) + (ff_r_bpcppc_right_choice_power_product))) /\ ((((exists ff_h_bpcppc_right_choice_power_product_successor. ff_h_bpcppc_right_choice_power_product_successor + S (ff_s_bpcppc_right_choice_power_product) = S ((S (S ff_i_bpcppc_right_choice_power_product)) * ff_v_bpcppc_right_choice_power_product)) /\ exists ff_q_bpcppc_right_choice_power_product_successor. ff_u_bpcppc_right_choice_power_product = ff_q_bpcppc_right_choice_power_product_successor * S ((S (S ff_i_bpcppc_right_choice_power_product)) * ff_v_bpcppc_right_choice_power_product) + (ff_s_bpcppc_right_choice_power_product))) /\ ff_s_bpcppc_right_choice_power_product = ff_r_bpcppc_right_choice_power_product * ff_p_bpcppc_right_choice_power_product)))))))))) \/ (~((~(S (j) = 1) /\ forall bpr_left_bpcppc_right_choice_prime bpr_right_bpcppc_right_choice_prime. S (j) = bpr_left_bpcppc_right_choice_prime * bpr_right_bpcppc_right_choice_prime -> bpr_left_bpcppc_right_choice_prime = 1 \/ bpr_right_bpcppc_right_choice_prime = 1)) /\ x1 = 1))) - 0021
apply hprefix - 0022
exact hj - 0023
cases hright - 0024
cases hright_witness - 0025
have hax : x = a - 0026
apply beta_at_unique - 0027
exact hleft_witness_left - 0028
exact ha - 0029
have hxz : x1 = z - 0030
apply beta_at_unique - 0031
exact hright_witness_left - 0032
exact hz - 0033
have hcoprime : Coprime(x,x1)Exact native replay line
have hcoprime : forall d. (exists u. x = d * u) -> (exists v. x1 = d * v) -> d = 1 - 0034
cases hleft_witness_right - 0035
cases hleft_witness_right_left - 0036
cases hleft_witness_right_left_right - 0037
cases hleft_witness_right_left_right_witness - 0038
cases hright_witness_right - 0039
cases hright_witness_right_left - 0040
cases hright_witness_right_left_right - 0041
cases hright_witness_right_left_right_witness - 0042
have hbase_ne : ~(S i = S j) - 0043
intro hbase - 0044
apply hij - 0045
apply PA2 - 0046
exact hbase - 0047
have hbase_coprime : Coprime(S i,S j)Exact native replay line
have hbase_coprime : forall d. (exists u. S i = d * u) -> (exists v. S j = d * v) -> d = 1 - 0048
specialize distinct_primes_coprime (S i) - 0049
specialize distinct_primes_coprime (S j) - 0050
apply distinct_primes_coprime - 0051
exact hleft_witness_right_left_left - 0052
exact hright_witness_right_left_left - 0053
exact hbase_ne - 0054
specialize coprime_powers (S i) - 0055
specialize coprime_powers (S j) - 0056
specialize coprime_powers x2 - 0057
specialize coprime_powers x3 - 0058
specialize coprime_powers x - 0059
specialize coprime_powers x1 - 0060
apply coprime_powers - 0061
exact hbase_coprime - 0062
exact hleft_witness_right_left_right_witness_right - 0063
exact hright_witness_right_left_right_witness_right - 0064
cases hright_witness_right_right - 0065
rewrite hright_witness_right_right_right - 0066
specialize coprime_one_right x - 0067
apply coprime_one_right - 0068
cases hleft_witness_right_right - 0069
cases hright_witness_right - 0070
rewrite hleft_witness_right_right_right - 0071
specialize coprime_one_left x1 - 0072
apply coprime_one_left - 0073
cases hright_witness_right_right - 0074
rewrite hleft_witness_right_right_right - 0075
specialize coprime_one_left x1 - 0076
apply coprime_one_left - 0077
rewrite <- hax - 0078
rewrite <- hxz - 0079
exact hcoprime