BT0116

fixed_nontrivial_factor_not_prime

Alpha body-checked · checked-use disabled

A displayed nontrivial factorization refutes primality.

Exact expanded PA statement

forall n a b. n = a * b -> ~(a = 1) -> ~(b = 1) -> ((~(n = 1) /\ forall bpr_left_bb8fnfp_prime bpr_right_bb8fnfp_prime. n = bpr_left_bb8fnfp_prime * bpr_right_bb8fnfp_prime -> bpr_left_bb8fnfp_prime = 1 \/ bpr_right_bb8fnfp_prime = 1)) -> false

Structural proof guide

A displayed nontrivial factorization refutes primality.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

BT011A prime_le_twenty_two_cases BT0126 bertrand_upper_endpoint_factorization

Formal native tactic body

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

  1. 0001intro n
  2. 0002intro a
  3. 0003intro b
  4. 0004intro hfactor
  5. 0005intro ha
  6. 0006intro hb
  7. 0007intro hprime
  8. 0008cases hprime
  9. 0009specialize hprime_right a
  10. 0010specialize hprime_right b
  11. 0011have hunit : a = 1 \/ b = 1
  12. 0012apply hprime_right
  13. 0013exact hfactor
  14. 0014cases hunit
  15. 0015apply ha
  16. 0016exact hunit_left
  17. 0017apply hb
  18. 0018exact hunit_right