BT00QO

prime_nondivisor_mul

Alpha body-checked · checked-use disabled

A prime dividing neither factor does not divide their product.

Exact expanded PA statement

forall p a b. ((~(p = 1) /\ forall frm_prime_left_bpd_prime frm_prime_right_bpd_prime. p = frm_prime_left_bpd_prime * frm_prime_right_bpd_prime -> frm_prime_left_bpd_prime = 1 \/ frm_prime_right_bpd_prime = 1)) -> ~(exists bpd_factor_nondivisor_left. a = (p) * bpd_factor_nondivisor_left) -> ~(exists bpd_factor_nondivisor_right. b = (p) * bpd_factor_nondivisor_right) -> ~(exists bpd_factor_nondivisor_product. a * b = (p) * bpd_factor_nondivisor_product)

Structural proof guide

A prime dividing neither factor does not divide their product.

Direct prerequisites: euclid_prime_dvd_product. The authored body proceeds by case analysis (1), intermediate claims (1).

Proof neighborhood

Direct dependencies

BT003N euclid_prime_dvd_product

Direct dependents

BT00QQ power_valuation_mul_successor_not_divides

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 b
  4. 0004intro hp
  5. 0005intro ha
  6. 0006intro hb
  7. 0007intro hab
  8. 0008have hsplit : (exists u. a = p * u) \/ exists v. b = p * v
  9. 0009specialize euclid_prime_dvd_product p
  10. 0010specialize euclid_prime_dvd_product a
  11. 0011specialize euclid_prime_dvd_product b
  12. 0012apply euclid_prime_dvd_product
  13. 0013exact hp
  14. 0014exact hab
  15. 0015cases hsplit
  16. 0016apply ha
  17. 0017exact hsplit_left
  18. 0018apply hb
  19. 0019exact hsplit_right