BT00QF

prime_power_exponent_le

Alpha body-checked · checked-use disabled

The exponent of a relational power at a prime base is bounded by its value.

Exact expanded PA statement

forall p e x. ((~(p = 1) /\ forall frm_prime_left_bpvl_prime frm_prime_right_bpvl_prime. p = frm_prime_left_bpvl_prime * frm_prime_right_bpvl_prime -> frm_prime_left_bpvl_prime = 1 \/ frm_prime_right_bpvl_prime = 1)) -> (exists ff_b_bpvl_exponent_bound ff_c_bpvl_exponent_bound. ((forall ff_i_bpvl_exponent_bound_repeat. (exists ff_lt_bpvl_exponent_bound_repeat_bound. ff_lt_bpvl_exponent_bound_repeat_bound + S ff_i_bpvl_exponent_bound_repeat = e) -> (((exists ff_h_bpvl_exponent_bound_repeat_decoded. ff_h_bpvl_exponent_bound_repeat_decoded + S (p) = S ((S (ff_i_bpvl_exponent_bound_repeat)) * ff_c_bpvl_exponent_bound)) /\ exists ff_q_bpvl_exponent_bound_repeat_decoded. ff_b_bpvl_exponent_bound = ff_q_bpvl_exponent_bound_repeat_decoded * S ((S (ff_i_bpvl_exponent_bound_repeat)) * ff_c_bpvl_exponent_bound) + (p)))) /\ (exists ff_u_bpvl_exponent_bound_product ff_v_bpvl_exponent_bound_product. ((((exists ff_h_bpvl_exponent_bound_product_start. ff_h_bpvl_exponent_bound_product_start + S (1) = S ((S (0)) * ff_v_bpvl_exponent_bound_product)) /\ exists ff_q_bpvl_exponent_bound_product_start. ff_u_bpvl_exponent_bound_product = ff_q_bpvl_exponent_bound_product_start * S ((S (0)) * ff_v_bpvl_exponent_bound_product) + (1))) /\ ((((exists ff_h_bpvl_exponent_bound_product_terminal. ff_h_bpvl_exponent_bound_product_terminal + S (x) = S ((S (e)) * ff_v_bpvl_exponent_bound_product)) /\ exists ff_q_bpvl_exponent_bound_product_terminal. ff_u_bpvl_exponent_bound_product = ff_q_bpvl_exponent_bound_product_terminal * S ((S (e)) * ff_v_bpvl_exponent_bound_product) + (x))) /\ forall ff_i_bpvl_exponent_bound_product. (exists ff_lt_bpvl_exponent_bound_product_bound. ff_lt_bpvl_exponent_bound_product_bound + S ff_i_bpvl_exponent_bound_product = e) -> exists ff_p_bpvl_exponent_bound_product ff_r_bpvl_exponent_bound_product ff_s_bpvl_exponent_bound_product. ((((exists ff_h_bpvl_exponent_bound_product_factor. ff_h_bpvl_exponent_bound_product_factor + S (ff_p_bpvl_exponent_bound_product) = S ((S (ff_i_bpvl_exponent_bound_product)) * ff_c_bpvl_exponent_bound)) /\ exists ff_q_bpvl_exponent_bound_product_factor. ff_b_bpvl_exponent_bound = ff_q_bpvl_exponent_bound_product_factor * S ((S (ff_i_bpvl_exponent_bound_product)) * ff_c_bpvl_exponent_bound) + (ff_p_bpvl_exponent_bound_product))) /\ ((((exists ff_h_bpvl_exponent_bound_product_partial. ff_h_bpvl_exponent_bound_product_partial + S (ff_r_bpvl_exponent_bound_product) = S ((S (ff_i_bpvl_exponent_bound_product)) * ff_v_bpvl_exponent_bound_product)) /\ exists ff_q_bpvl_exponent_bound_product_partial. ff_u_bpvl_exponent_bound_product = ff_q_bpvl_exponent_bound_product_partial * S ((S (ff_i_bpvl_exponent_bound_product)) * ff_v_bpvl_exponent_bound_product) + (ff_r_bpvl_exponent_bound_product))) /\ ((((exists ff_h_bpvl_exponent_bound_product_successor. ff_h_bpvl_exponent_bound_product_successor + S (ff_s_bpvl_exponent_bound_product) = S ((S (S ff_i_bpvl_exponent_bound_product)) * ff_v_bpvl_exponent_bound_product)) /\ exists ff_q_bpvl_exponent_bound_product_successor. ff_u_bpvl_exponent_bound_product = ff_q_bpvl_exponent_bound_product_successor * S ((S (S ff_i_bpvl_exponent_bound_product)) * ff_v_bpvl_exponent_bound_product) + (ff_s_bpvl_exponent_bound_product))) /\ ff_s_bpvl_exponent_bound_product = ff_r_bpvl_exponent_bound_product * ff_p_bpvl_exponent_bound_product)))))))) -> (exists bpv_gap_power_exponent. bpv_gap_power_exponent + e = x)

Structural proof guide

The exponent of a relational power at a prime base is bounded by its value.

Direct prerequisites: pow_successor_decompose, zero_le, prime_nonzero, one_le_of_ne_zero, pow_nonzero_of_one_le, prime_two_le, succ_le_succ, succ_le_mul_of_two_le_right, le_trans. The authored body proceeds by structural induction (1), case analysis (2), intermediate claims (8), equality transport (1).

Proof neighborhood

Direct dependencies

BT0083 pow_successor_decompose BT000W zero_le BT003G prime_nonzero BT0010 one_le_of_ne_zero BT00Q1 pow_nonzero_of_one_le BT00QD prime_two_le BT0016 succ_le_succ BT00QE succ_le_mul_of_two_le_right BT000F le_trans

Direct dependents

BT00QG prime_power_divides_exponent_le_value BT00SA prime_power_quotient_tail_zero BT00XO prime_power_quotient_zero_of_exponent_gt

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 e
  3. 0003induction e
  4. 0004intro x
  5. 0005intro hp
  6. 0006intro hx
  7. 0007specialize zero_le x
  8. 0008exact zero_le
  9. 0009intro x
  10. 0010intro hp
  11. 0011intro hx
  12. 0012have hstep : exists r. (exists ff_b_bpvl_prefix ff_c_bpvl_prefix. ((forall ff_i_bpvl_prefix_repeat. (exists ff_lt_bpvl_prefix_repeat_bound. ff_lt_bpvl_prefix_repeat_bound + S ff_i_bpvl_prefix_repeat = e) -> (((exists ff_h_bpvl_prefix_repeat_decoded. ff_h_bpvl_prefix_repeat_decoded + S (p) = S ((S (ff_i_bpvl_prefix_repeat)) * ff_c_bpvl_prefix)) /\ exists ff_q_bpvl_prefix_repeat_decoded. ff_b_bpvl_prefix = ff_q_bpvl_prefix_repeat_decoded * S ((S (ff_i_bpvl_prefix_repeat)) * ff_c_bpvl_prefix) + (p)))) /\ (exists ff_u_bpvl_prefix_product ff_v_bpvl_prefix_product. ((((exists ff_h_bpvl_prefix_product_start. ff_h_bpvl_prefix_product_start + S (1) = S ((S (0)) * ff_v_bpvl_prefix_product)) /\ exists ff_q_bpvl_prefix_product_start. ff_u_bpvl_prefix_product = ff_q_bpvl_prefix_product_start * S ((S (0)) * ff_v_bpvl_prefix_product) + (1))) /\ ((((exists ff_h_bpvl_prefix_product_terminal. ff_h_bpvl_prefix_product_terminal + S (r) = S ((S (e)) * ff_v_bpvl_prefix_product)) /\ exists ff_q_bpvl_prefix_product_terminal. ff_u_bpvl_prefix_product = ff_q_bpvl_prefix_product_terminal * S ((S (e)) * ff_v_bpvl_prefix_product) + (r))) /\ forall ff_i_bpvl_prefix_product. (exists ff_lt_bpvl_prefix_product_bound. ff_lt_bpvl_prefix_product_bound + S ff_i_bpvl_prefix_product = e) -> exists ff_p_bpvl_prefix_product ff_r_bpvl_prefix_product ff_s_bpvl_prefix_product. ((((exists ff_h_bpvl_prefix_product_factor. ff_h_bpvl_prefix_product_factor + S (ff_p_bpvl_prefix_product) = S ((S (ff_i_bpvl_prefix_product)) * ff_c_bpvl_prefix)) /\ exists ff_q_bpvl_prefix_product_factor. ff_b_bpvl_prefix = ff_q_bpvl_prefix_product_factor * S ((S (ff_i_bpvl_prefix_product)) * ff_c_bpvl_prefix) + (ff_p_bpvl_prefix_product))) /\ ((((exists ff_h_bpvl_prefix_product_partial. ff_h_bpvl_prefix_product_partial + S (ff_r_bpvl_prefix_product) = S ((S (ff_i_bpvl_prefix_product)) * ff_v_bpvl_prefix_product)) /\ exists ff_q_bpvl_prefix_product_partial. ff_u_bpvl_prefix_product = ff_q_bpvl_prefix_product_partial * S ((S (ff_i_bpvl_prefix_product)) * ff_v_bpvl_prefix_product) + (ff_r_bpvl_prefix_product))) /\ ((((exists ff_h_bpvl_prefix_product_successor. ff_h_bpvl_prefix_product_successor + S (ff_s_bpvl_prefix_product) = S ((S (S ff_i_bpvl_prefix_product)) * ff_v_bpvl_prefix_product)) /\ exists ff_q_bpvl_prefix_product_successor. ff_u_bpvl_prefix_product = ff_q_bpvl_prefix_product_successor * S ((S (S ff_i_bpvl_prefix_product)) * ff_v_bpvl_prefix_product) + (ff_s_bpvl_prefix_product))) /\ ff_s_bpvl_prefix_product = ff_r_bpvl_prefix_product * ff_p_bpvl_prefix_product)))))))) /\ x = r * p
  13. 0013specialize pow_successor_decompose p
  14. 0014specialize pow_successor_decompose e
  15. 0015specialize pow_successor_decompose (S e)
  16. 0016specialize pow_successor_decompose x
  17. 0017apply pow_successor_decompose
  18. 0018refl
  19. 0019exact hx
  20. 0020cases hstep
  21. 0021cases hstep_witness
  22. 0022have he_prefix : exists k. k + e = x1
  23. 0023specialize IH x1
  24. 0024apply IH
  25. 0025exact hp
  26. 0026exact hstep_witness_left
  27. 0027have hp0 : ~(p = 0)
  28. 0028intro hpzero
  29. 0029specialize prime_nonzero p
  30. 0030apply prime_nonzero
  31. 0031exact hp
  32. 0032exact hpzero
  33. 0033have hp1 : exists k. k + 1 = p
  34. 0034specialize one_le_of_ne_zero p
  35. 0035apply one_le_of_ne_zero
  36. 0036exact hp0
  37. 0037have hprefix0 : ~(x1 = 0)
  38. 0038intro hprefixzero
  39. 0039specialize pow_nonzero_of_one_le p
  40. 0040specialize pow_nonzero_of_one_le e
  41. 0041specialize pow_nonzero_of_one_le x1
  42. 0042apply pow_nonzero_of_one_le
  43. 0043exact hp1
  44. 0044exact hstep_witness_left
  45. 0045exact hprefixzero
  46. 0046have hp2 : exists k. k + 2 = p
  47. 0047specialize prime_two_le p
  48. 0048apply prime_two_le
  49. 0049exact hp
  50. 0050have hprefix_step : exists k. k + S x1 = x1 * p
  51. 0051specialize succ_le_mul_of_two_le_right x1
  52. 0052specialize succ_le_mul_of_two_le_right p
  53. 0053apply succ_le_mul_of_two_le_right
  54. 0054exact hprefix0
  55. 0055exact hp2
  56. 0056have he_step : exists k. k + S e = S x1
  57. 0057specialize succ_le_succ e
  58. 0058specialize succ_le_succ x1
  59. 0059apply succ_le_succ
  60. 0060exact he_prefix
  61. 0061rewrite hstep_witness_right
  62. 0062specialize le_trans (S e)
  63. 0063specialize le_trans (S x1)
  64. 0064specialize le_trans (x1 * p)
  65. 0065apply le_trans
  66. 0066exact he_step
  67. 0067exact hprefix_step