BT00U5

primorial_factor_choice_exists

Alpha body-checked · checked-use disabled

Every index has its exact prime-or-one selector factor.

Exact expanded PA statement

forall i. exists a. (((((~(S (i) = 1) /\ forall bpr_left_bpfc_exists_prime bpr_right_bpfc_exists_prime. S (i) = bpr_left_bpfc_exists_prime * bpr_right_bpfc_exists_prime -> bpr_left_bpfc_exists_prime = 1 \/ bpr_right_bpfc_exists_prime = 1)) /\ a = S (i)) \/ (~((~(S (i) = 1) /\ forall bpr_left_bpfc_exists_prime bpr_right_bpfc_exists_prime. S (i) = bpr_left_bpfc_exists_prime * bpr_right_bpfc_exists_prime -> bpr_left_bpfc_exists_prime = 1 \/ bpr_right_bpfc_exists_prime = 1)) /\ a = 1)))

Structural proof guide

Every index has its exact prime-or-one selector factor.

Direct prerequisites: prime_decidable. The authored body proceeds by case analysis (1).

Proof neighborhood

Direct dependencies

BT003H prime_decidable

Direct dependents

BT00U7 primorial_factor_prefix_extend BT00UR primorial_interval_factor_prefix_extend

Formal native tactic body

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

  1. 0001intro i
  2. 0002specialize prime_decidable (S i)
  3. 0003cases prime_decidable
  4. 0004exists S i
  5. 0005left
  6. 0006split
  7. 0007exact prime_decidable_left
  8. 0008refl
  9. 0009exists 1
  10. 0010right
  11. 0011split
  12. 0012exact prime_decidable_right
  13. 0013refl