BT00Q4

power_divides_zero

Alpha body-checked · checked-use disabled

The zeroth relational power divides every natural.

Exact expanded PA statement

forall p a z. z = 0 -> (exists bpv_result_zero. ((exists ff_b_zero_power ff_c_zero_power. ((forall ff_i_zero_power_repeat. (exists ff_lt_zero_power_repeat_bound. ff_lt_zero_power_repeat_bound + S ff_i_zero_power_repeat = z) -> (((exists ff_h_zero_power_repeat_decoded. ff_h_zero_power_repeat_decoded + S (p) = S ((S (ff_i_zero_power_repeat)) * ff_c_zero_power)) /\ exists ff_q_zero_power_repeat_decoded. ff_b_zero_power = ff_q_zero_power_repeat_decoded * S ((S (ff_i_zero_power_repeat)) * ff_c_zero_power) + (p)))) /\ (exists ff_u_zero_power_product ff_v_zero_power_product. ((((exists ff_h_zero_power_product_start. ff_h_zero_power_product_start + S (1) = S ((S (0)) * ff_v_zero_power_product)) /\ exists ff_q_zero_power_product_start. ff_u_zero_power_product = ff_q_zero_power_product_start * S ((S (0)) * ff_v_zero_power_product) + (1))) /\ ((((exists ff_h_zero_power_product_terminal. ff_h_zero_power_product_terminal + S (bpv_result_zero) = S ((S (z)) * ff_v_zero_power_product)) /\ exists ff_q_zero_power_product_terminal. ff_u_zero_power_product = ff_q_zero_power_product_terminal * S ((S (z)) * ff_v_zero_power_product) + (bpv_result_zero))) /\ forall ff_i_zero_power_product. (exists ff_lt_zero_power_product_bound. ff_lt_zero_power_product_bound + S ff_i_zero_power_product = z) -> exists ff_p_zero_power_product ff_r_zero_power_product ff_s_zero_power_product. ((((exists ff_h_zero_power_product_factor. ff_h_zero_power_product_factor + S (ff_p_zero_power_product) = S ((S (ff_i_zero_power_product)) * ff_c_zero_power)) /\ exists ff_q_zero_power_product_factor. ff_b_zero_power = ff_q_zero_power_product_factor * S ((S (ff_i_zero_power_product)) * ff_c_zero_power) + (ff_p_zero_power_product))) /\ ((((exists ff_h_zero_power_product_partial. ff_h_zero_power_product_partial + S (ff_r_zero_power_product) = S ((S (ff_i_zero_power_product)) * ff_v_zero_power_product)) /\ exists ff_q_zero_power_product_partial. ff_u_zero_power_product = ff_q_zero_power_product_partial * S ((S (ff_i_zero_power_product)) * ff_v_zero_power_product) + (ff_r_zero_power_product))) /\ ((((exists ff_h_zero_power_product_successor. ff_h_zero_power_product_successor + S (ff_s_zero_power_product) = S ((S (S ff_i_zero_power_product)) * ff_v_zero_power_product)) /\ exists ff_q_zero_power_product_successor. ff_u_zero_power_product = ff_q_zero_power_product_successor * S ((S (S ff_i_zero_power_product)) * ff_v_zero_power_product) + (ff_s_zero_power_product))) /\ ff_s_zero_power_product = ff_r_zero_power_product * ff_p_zero_power_product)))))))) /\ (exists bpv_factor_zero_divides. a = bpv_result_zero * bpv_factor_zero_divides)))

Structural proof guide

The zeroth relational power divides every natural.

Direct prerequisites: pow_exists, pow_zero, one_multiple. The authored body proceeds by case analysis (1), intermediate claims (2), equality transport (1).

Proof neighborhood

Direct dependencies

BT0080 pow_exists BT0081 pow_zero BT0027 one_multiple

Direct dependents

BT00Q6 bounded_power_valuation_exists

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 a
  3. 0003intro z
  4. 0004intro hz
  5. 0005have hpower : exists r. (exists ff_b_zero_witness ff_c_zero_witness. ((forall ff_i_zero_witness_repeat. (exists ff_lt_zero_witness_repeat_bound. ff_lt_zero_witness_repeat_bound + S ff_i_zero_witness_repeat = z) -> (((exists ff_h_zero_witness_repeat_decoded. ff_h_zero_witness_repeat_decoded + S (p) = S ((S (ff_i_zero_witness_repeat)) * ff_c_zero_witness)) /\ exists ff_q_zero_witness_repeat_decoded. ff_b_zero_witness = ff_q_zero_witness_repeat_decoded * S ((S (ff_i_zero_witness_repeat)) * ff_c_zero_witness) + (p)))) /\ (exists ff_u_zero_witness_product ff_v_zero_witness_product. ((((exists ff_h_zero_witness_product_start. ff_h_zero_witness_product_start + S (1) = S ((S (0)) * ff_v_zero_witness_product)) /\ exists ff_q_zero_witness_product_start. ff_u_zero_witness_product = ff_q_zero_witness_product_start * S ((S (0)) * ff_v_zero_witness_product) + (1))) /\ ((((exists ff_h_zero_witness_product_terminal. ff_h_zero_witness_product_terminal + S (r) = S ((S (z)) * ff_v_zero_witness_product)) /\ exists ff_q_zero_witness_product_terminal. ff_u_zero_witness_product = ff_q_zero_witness_product_terminal * S ((S (z)) * ff_v_zero_witness_product) + (r))) /\ forall ff_i_zero_witness_product. (exists ff_lt_zero_witness_product_bound. ff_lt_zero_witness_product_bound + S ff_i_zero_witness_product = z) -> exists ff_p_zero_witness_product ff_r_zero_witness_product ff_s_zero_witness_product. ((((exists ff_h_zero_witness_product_factor. ff_h_zero_witness_product_factor + S (ff_p_zero_witness_product) = S ((S (ff_i_zero_witness_product)) * ff_c_zero_witness)) /\ exists ff_q_zero_witness_product_factor. ff_b_zero_witness = ff_q_zero_witness_product_factor * S ((S (ff_i_zero_witness_product)) * ff_c_zero_witness) + (ff_p_zero_witness_product))) /\ ((((exists ff_h_zero_witness_product_partial. ff_h_zero_witness_product_partial + S (ff_r_zero_witness_product) = S ((S (ff_i_zero_witness_product)) * ff_v_zero_witness_product)) /\ exists ff_q_zero_witness_product_partial. ff_u_zero_witness_product = ff_q_zero_witness_product_partial * S ((S (ff_i_zero_witness_product)) * ff_v_zero_witness_product) + (ff_r_zero_witness_product))) /\ ((((exists ff_h_zero_witness_product_successor. ff_h_zero_witness_product_successor + S (ff_s_zero_witness_product) = S ((S (S ff_i_zero_witness_product)) * ff_v_zero_witness_product)) /\ exists ff_q_zero_witness_product_successor. ff_u_zero_witness_product = ff_q_zero_witness_product_successor * S ((S (S ff_i_zero_witness_product)) * ff_v_zero_witness_product) + (ff_s_zero_witness_product))) /\ ff_s_zero_witness_product = ff_r_zero_witness_product * ff_p_zero_witness_product))))))))
  6. 0006specialize pow_exists p
  7. 0007specialize pow_exists z
  8. 0008exact pow_exists
  9. 0009cases hpower
  10. 0010have hr : x = 1
  11. 0011specialize pow_zero p
  12. 0012specialize pow_zero z
  13. 0013specialize pow_zero x
  14. 0014apply pow_zero
  15. 0015exact hz
  16. 0016exact hpower_witness
  17. 0017exists x
  18. 0018split
  19. 0019exact hpower_witness
  20. 0020rewrite hr
  21. 0021specialize one_multiple a
  22. 0022exact one_multiple