BT00RL

prime_power_valuation_one_zero

Alpha body-checked · checked-use disabled

At a prime base, the bounded valuation of one has exponent zero.

Exact expanded PA statement

forall p one e. one = 1 -> ((~(p = 1) /\ forall frm_prime_left_bfv_prime frm_prime_right_bfv_prime. p = frm_prime_left_bfv_prime * frm_prime_right_bfv_prime -> frm_prime_left_bfv_prime = 1 \/ frm_prime_right_bfv_prime = 1)) -> (((exists bpv_gap_bfv_one_exponent_bound. bpv_gap_bfv_one_exponent_bound + e = one) /\ (exists bpv_result_bfv_one_selected. ((exists ff_b_bfv_one_selected_power ff_c_bfv_one_selected_power. ((forall ff_i_bfv_one_selected_power_repeat. (exists ff_lt_bfv_one_selected_power_repeat_bound. ff_lt_bfv_one_selected_power_repeat_bound + S ff_i_bfv_one_selected_power_repeat = e) -> (((exists ff_h_bfv_one_selected_power_repeat_decoded. ff_h_bfv_one_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_one_selected_power_repeat)) * ff_c_bfv_one_selected_power)) /\ exists ff_q_bfv_one_selected_power_repeat_decoded. ff_b_bfv_one_selected_power = ff_q_bfv_one_selected_power_repeat_decoded * S ((S (ff_i_bfv_one_selected_power_repeat)) * ff_c_bfv_one_selected_power) + (p)))) /\ (exists ff_u_bfv_one_selected_power_product ff_v_bfv_one_selected_power_product. ((((exists ff_h_bfv_one_selected_power_product_start. ff_h_bfv_one_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_start. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_start * S ((S (0)) * ff_v_bfv_one_selected_power_product) + (1))) /\ ((((exists ff_h_bfv_one_selected_power_product_terminal. ff_h_bfv_one_selected_power_product_terminal + S (bpv_result_bfv_one_selected) = S ((S (e)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_terminal. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_terminal * S ((S (e)) * ff_v_bfv_one_selected_power_product) + (bpv_result_bfv_one_selected))) /\ forall ff_i_bfv_one_selected_power_product. (exists ff_lt_bfv_one_selected_power_product_bound. ff_lt_bfv_one_selected_power_product_bound + S ff_i_bfv_one_selected_power_product = e) -> exists ff_p_bfv_one_selected_power_product ff_r_bfv_one_selected_power_product ff_s_bfv_one_selected_power_product. ((((exists ff_h_bfv_one_selected_power_product_factor. ff_h_bfv_one_selected_power_product_factor + S (ff_p_bfv_one_selected_power_product) = S ((S (ff_i_bfv_one_selected_power_product)) * ff_c_bfv_one_selected_power)) /\ exists ff_q_bfv_one_selected_power_product_factor. ff_b_bfv_one_selected_power = ff_q_bfv_one_selected_power_product_factor * S ((S (ff_i_bfv_one_selected_power_product)) * ff_c_bfv_one_selected_power) + (ff_p_bfv_one_selected_power_product))) /\ ((((exists ff_h_bfv_one_selected_power_product_partial. ff_h_bfv_one_selected_power_product_partial + S (ff_r_bfv_one_selected_power_product) = S ((S (ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_partial. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_partial * S ((S (ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product) + (ff_r_bfv_one_selected_power_product))) /\ ((((exists ff_h_bfv_one_selected_power_product_successor. ff_h_bfv_one_selected_power_product_successor + S (ff_s_bfv_one_selected_power_product) = S ((S (S ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_successor. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_successor * S ((S (S ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product) + (ff_s_bfv_one_selected_power_product))) /\ ff_s_bfv_one_selected_power_product = ff_r_bfv_one_selected_power_product * ff_p_bfv_one_selected_power_product)))))))) /\ (exists bpv_factor_bfv_one_selected_divides. one = bpv_result_bfv_one_selected * bpv_factor_bfv_one_selected_divides)))) /\ forall bpv_candidate_bfv_one. (exists bpv_gap_bfv_one_candidate_bound. bpv_gap_bfv_one_candidate_bound + bpv_candidate_bfv_one = one) -> (exists bpv_result_bfv_one_candidate. ((exists ff_b_bfv_one_candidate_power ff_c_bfv_one_candidate_power. ((forall ff_i_bfv_one_candidate_power_repeat. (exists ff_lt_bfv_one_candidate_power_repeat_bound. ff_lt_bfv_one_candidate_power_repeat_bound + S ff_i_bfv_one_candidate_power_repeat = bpv_candidate_bfv_one) -> (((exists ff_h_bfv_one_candidate_power_repeat_decoded. ff_h_bfv_one_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_one_candidate_power_repeat)) * ff_c_bfv_one_candidate_power)) /\ exists ff_q_bfv_one_candidate_power_repeat_decoded. ff_b_bfv_one_candidate_power = ff_q_bfv_one_candidate_power_repeat_decoded * S ((S (ff_i_bfv_one_candidate_power_repeat)) * ff_c_bfv_one_candidate_power) + (p)))) /\ (exists ff_u_bfv_one_candidate_power_product ff_v_bfv_one_candidate_power_product. ((((exists ff_h_bfv_one_candidate_power_product_start. ff_h_bfv_one_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_one_candidate_power_product)) /\ exists ff_q_bfv_one_candidate_power_product_start. ff_u_bfv_one_candidate_power_product = ff_q_bfv_one_candidate_power_product_start * S ((S (0)) * ff_v_bfv_one_candidate_power_product) + (1))) /\ ((((exists ff_h_bfv_one_candidate_power_product_terminal. ff_h_bfv_one_candidate_power_product_terminal + S (bpv_result_bfv_one_candidate) = S ((S (bpv_candidate_bfv_one)) * ff_v_bfv_one_candidate_power_product)) /\ exists ff_q_bfv_one_candidate_power_product_terminal. ff_u_bfv_one_candidate_power_product = ff_q_bfv_one_candidate_power_product_terminal * S ((S (bpv_candidate_bfv_one)) * ff_v_bfv_one_candidate_power_product) + (bpv_result_bfv_one_candidate))) /\ forall ff_i_bfv_one_candidate_power_product. (exists ff_lt_bfv_one_candidate_power_product_bound. ff_lt_bfv_one_candidate_power_product_bound + S ff_i_bfv_one_candidate_power_product = bpv_candidate_bfv_one) -> exists ff_p_bfv_one_candidate_power_product ff_r_bfv_one_candidate_power_product ff_s_bfv_one_candidate_power_product. ((((exists ff_h_bfv_one_candidate_power_product_factor. ff_h_bfv_one_candidate_power_product_factor + S (ff_p_bfv_one_candidate_power_product) = S ((S (ff_i_bfv_one_candidate_power_product)) * ff_c_bfv_one_candidate_power)) /\ exists ff_q_bfv_one_candidate_power_product_factor. ff_b_bfv_one_candidate_power = ff_q_bfv_one_candidate_power_product_factor * S ((S (ff_i_bfv_one_candidate_power_product)) * ff_c_bfv_one_candidate_power) + (ff_p_bfv_one_candidate_power_product))) /\ ((((exists ff_h_bfv_one_candidate_power_product_partial. ff_h_bfv_one_candidate_power_product_partial + S (ff_r_bfv_one_candidate_power_product) = S ((S (ff_i_bfv_one_candidate_power_product)) * ff_v_bfv_one_candidate_power_product)) /\ exists ff_q_bfv_one_candidate_power_product_partial. ff_u_bfv_one_candidate_power_product = ff_q_bfv_one_candidate_power_product_partial * S ((S (ff_i_bfv_one_candidate_power_product)) * ff_v_bfv_one_candidate_power_product) + (ff_r_bfv_one_candidate_power_product))) /\ ((((exists ff_h_bfv_one_candidate_power_product_successor. ff_h_bfv_one_candidate_power_product_successor + S (ff_s_bfv_one_candidate_power_product) = S ((S (S ff_i_bfv_one_candidate_power_product)) * ff_v_bfv_one_candidate_power_product)) /\ exists ff_q_bfv_one_candidate_power_product_successor. ff_u_bfv_one_candidate_power_product = ff_q_bfv_one_candidate_power_product_successor * S ((S (S ff_i_bfv_one_candidate_power_product)) * ff_v_bfv_one_candidate_power_product) + (ff_s_bfv_one_candidate_power_product))) /\ ff_s_bfv_one_candidate_power_product = ff_r_bfv_one_candidate_power_product * ff_p_bfv_one_candidate_power_product)))))))) /\ (exists bpv_factor_bfv_one_candidate_divides. one = bpv_result_bfv_one_candidate * bpv_factor_bfv_one_candidate_divides))) -> (exists bpv_gap_bfv_one_maximal. bpv_gap_bfv_one_maximal + bpv_candidate_bfv_one = e)) -> e = 0

Structural proof guide

At a prime base, the bounded valuation of one has exponent zero.

Direct prerequisites: power_valuation_power_divides, zero_or_succ, pow_successor_decompose, mul_eq_one_components. The authored body proceeds by case analysis (10), intermediate claims (6).

Proof neighborhood

Direct dependencies

BT00Q9 power_valuation_power_divides BT000Q zero_or_succ BT0083 pow_successor_decompose BT0020 mul_eq_one_components

Direct dependents

BT00RO prime_factorial_valuation_zero

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro p
  2. 0002intro one
  3. 0003intro e
  4. 0004intro hone
  5. 0005intro hp
  6. 0006intro hvaluation
  7. 0007cases hp
  8. 0008have hselected : exists bpv_result_bfv_one_selected. ((exists ff_b_bfv_one_selected_power ff_c_bfv_one_selected_power. ((forall ff_i_bfv_one_selected_power_repeat. (exists ff_lt_bfv_one_selected_power_repeat_bound. ff_lt_bfv_one_selected_power_repeat_bound + S ff_i_bfv_one_selected_power_repeat = e) -> (((exists ff_h_bfv_one_selected_power_repeat_decoded. ff_h_bfv_one_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_one_selected_power_repeat)) * ff_c_bfv_one_selected_power)) /\ exists ff_q_bfv_one_selected_power_repeat_decoded. ff_b_bfv_one_selected_power = ff_q_bfv_one_selected_power_repeat_decoded * S ((S (ff_i_bfv_one_selected_power_repeat)) * ff_c_bfv_one_selected_power) + (p)))) /\ (exists ff_u_bfv_one_selected_power_product ff_v_bfv_one_selected_power_product. ((((exists ff_h_bfv_one_selected_power_product_start. ff_h_bfv_one_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_start. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_start * S ((S (0)) * ff_v_bfv_one_selected_power_product) + (1))) /\ ((((exists ff_h_bfv_one_selected_power_product_terminal. ff_h_bfv_one_selected_power_product_terminal + S (bpv_result_bfv_one_selected) = S ((S (e)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_terminal. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_terminal * S ((S (e)) * ff_v_bfv_one_selected_power_product) + (bpv_result_bfv_one_selected))) /\ forall ff_i_bfv_one_selected_power_product. (exists ff_lt_bfv_one_selected_power_product_bound. ff_lt_bfv_one_selected_power_product_bound + S ff_i_bfv_one_selected_power_product = e) -> exists ff_p_bfv_one_selected_power_product ff_r_bfv_one_selected_power_product ff_s_bfv_one_selected_power_product. ((((exists ff_h_bfv_one_selected_power_product_factor. ff_h_bfv_one_selected_power_product_factor + S (ff_p_bfv_one_selected_power_product) = S ((S (ff_i_bfv_one_selected_power_product)) * ff_c_bfv_one_selected_power)) /\ exists ff_q_bfv_one_selected_power_product_factor. ff_b_bfv_one_selected_power = ff_q_bfv_one_selected_power_product_factor * S ((S (ff_i_bfv_one_selected_power_product)) * ff_c_bfv_one_selected_power) + (ff_p_bfv_one_selected_power_product))) /\ ((((exists ff_h_bfv_one_selected_power_product_partial. ff_h_bfv_one_selected_power_product_partial + S (ff_r_bfv_one_selected_power_product) = S ((S (ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_partial. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_partial * S ((S (ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product) + (ff_r_bfv_one_selected_power_product))) /\ ((((exists ff_h_bfv_one_selected_power_product_successor. ff_h_bfv_one_selected_power_product_successor + S (ff_s_bfv_one_selected_power_product) = S ((S (S ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product)) /\ exists ff_q_bfv_one_selected_power_product_successor. ff_u_bfv_one_selected_power_product = ff_q_bfv_one_selected_power_product_successor * S ((S (S ff_i_bfv_one_selected_power_product)) * ff_v_bfv_one_selected_power_product) + (ff_s_bfv_one_selected_power_product))) /\ ff_s_bfv_one_selected_power_product = ff_r_bfv_one_selected_power_product * ff_p_bfv_one_selected_power_product)))))))) /\ (exists bpv_factor_bfv_one_selected_divides. one = bpv_result_bfv_one_selected * bpv_factor_bfv_one_selected_divides))
  9. 0009specialize power_valuation_power_divides p
  10. 0010specialize power_valuation_power_divides one
  11. 0011specialize power_valuation_power_divides e
  12. 0012apply power_valuation_power_divides
  13. 0013exact hvaluation
  14. 0014cases hselected
  15. 0015cases hselected_witness
  16. 0016cases hselected_witness_right
  17. 0017specialize zero_or_succ e
  18. 0018cases zero_or_succ
  19. 0019exact zero_or_succ_left
  20. 0020cases zero_or_succ_right
  21. 0021have hstep : exists R. (exists ff_b_bfv_one_prefix ff_c_bfv_one_prefix. ((forall ff_i_bfv_one_prefix_repeat. (exists ff_lt_bfv_one_prefix_repeat_bound. ff_lt_bfv_one_prefix_repeat_bound + S ff_i_bfv_one_prefix_repeat = x2) -> (((exists ff_h_bfv_one_prefix_repeat_decoded. ff_h_bfv_one_prefix_repeat_decoded + S (p) = S ((S (ff_i_bfv_one_prefix_repeat)) * ff_c_bfv_one_prefix)) /\ exists ff_q_bfv_one_prefix_repeat_decoded. ff_b_bfv_one_prefix = ff_q_bfv_one_prefix_repeat_decoded * S ((S (ff_i_bfv_one_prefix_repeat)) * ff_c_bfv_one_prefix) + (p)))) /\ (exists ff_u_bfv_one_prefix_product ff_v_bfv_one_prefix_product. ((((exists ff_h_bfv_one_prefix_product_start. ff_h_bfv_one_prefix_product_start + S (1) = S ((S (0)) * ff_v_bfv_one_prefix_product)) /\ exists ff_q_bfv_one_prefix_product_start. ff_u_bfv_one_prefix_product = ff_q_bfv_one_prefix_product_start * S ((S (0)) * ff_v_bfv_one_prefix_product) + (1))) /\ ((((exists ff_h_bfv_one_prefix_product_terminal. ff_h_bfv_one_prefix_product_terminal + S (R) = S ((S (x2)) * ff_v_bfv_one_prefix_product)) /\ exists ff_q_bfv_one_prefix_product_terminal. ff_u_bfv_one_prefix_product = ff_q_bfv_one_prefix_product_terminal * S ((S (x2)) * ff_v_bfv_one_prefix_product) + (R))) /\ forall ff_i_bfv_one_prefix_product. (exists ff_lt_bfv_one_prefix_product_bound. ff_lt_bfv_one_prefix_product_bound + S ff_i_bfv_one_prefix_product = x2) -> exists ff_p_bfv_one_prefix_product ff_r_bfv_one_prefix_product ff_s_bfv_one_prefix_product. ((((exists ff_h_bfv_one_prefix_product_factor. ff_h_bfv_one_prefix_product_factor + S (ff_p_bfv_one_prefix_product) = S ((S (ff_i_bfv_one_prefix_product)) * ff_c_bfv_one_prefix)) /\ exists ff_q_bfv_one_prefix_product_factor. ff_b_bfv_one_prefix = ff_q_bfv_one_prefix_product_factor * S ((S (ff_i_bfv_one_prefix_product)) * ff_c_bfv_one_prefix) + (ff_p_bfv_one_prefix_product))) /\ ((((exists ff_h_bfv_one_prefix_product_partial. ff_h_bfv_one_prefix_product_partial + S (ff_r_bfv_one_prefix_product) = S ((S (ff_i_bfv_one_prefix_product)) * ff_v_bfv_one_prefix_product)) /\ exists ff_q_bfv_one_prefix_product_partial. ff_u_bfv_one_prefix_product = ff_q_bfv_one_prefix_product_partial * S ((S (ff_i_bfv_one_prefix_product)) * ff_v_bfv_one_prefix_product) + (ff_r_bfv_one_prefix_product))) /\ ((((exists ff_h_bfv_one_prefix_product_successor. ff_h_bfv_one_prefix_product_successor + S (ff_s_bfv_one_prefix_product) = S ((S (S ff_i_bfv_one_prefix_product)) * ff_v_bfv_one_prefix_product)) /\ exists ff_q_bfv_one_prefix_product_successor. ff_u_bfv_one_prefix_product = ff_q_bfv_one_prefix_product_successor * S ((S (S ff_i_bfv_one_prefix_product)) * ff_v_bfv_one_prefix_product) + (ff_s_bfv_one_prefix_product))) /\ ff_s_bfv_one_prefix_product = ff_r_bfv_one_prefix_product * ff_p_bfv_one_prefix_product)))))))) /\ x = R * p
  22. 0022specialize pow_successor_decompose p
  23. 0023specialize pow_successor_decompose x2
  24. 0024specialize pow_successor_decompose e
  25. 0025specialize pow_successor_decompose x
  26. 0026apply pow_successor_decompose
  27. 0027exact zero_or_succ_right_witness
  28. 0028exact hselected_witness_left
  29. 0029cases hstep
  30. 0030cases hstep_witness
  31. 0031have hresult_one : x = 1
  32. 0032specialize mul_eq_one_components x
  33. 0033specialize mul_eq_one_components x1
  34. 0034have hresult_parts : x = 1 /\ x1 = 1
  35. 0035apply mul_eq_one_components
  36. 0036symm
  37. 0037trans one
  38. 0038symm
  39. 0039exact hone
  40. 0040exact hselected_witness_right_witness
  41. 0041cases hresult_parts
  42. 0042exact hresult_parts_left
  43. 0043have hprime_one : p = 1
  44. 0044specialize mul_eq_one_components x3
  45. 0045specialize mul_eq_one_components p
  46. 0046have hstep_parts : x3 = 1 /\ p = 1
  47. 0047apply mul_eq_one_components
  48. 0048trans x
  49. 0049symm
  50. 0050exact hstep_witness_right
  51. 0051exact hresult_one
  52. 0052cases hstep_parts
  53. 0053exact hstep_parts_right
  54. 0054exfalso
  55. 0055apply hp_left
  56. 0056exact hprime_one