BT010U

beta_product_all_one_exact

Alpha body-checked · checked-use disabled

A Product whose decoded factors are all one is exactly one.

Exact expanded PA statement

forall b c l z. (forall i a. (exists bcf_lt_gap_b5bpao_bound. bcf_lt_gap_b5bpao_bound + S (i) = l) -> (((exists bpr_height_b5bpao_entry. bpr_height_b5bpao_entry + S (a) = S ((S (i)) * c)) /\ exists bpr_quotient_b5bpao_entry. b = bpr_quotient_b5bpao_entry * S ((S (i)) * c) + (a))) -> a = 1) -> (exists ff_u_b5bpao_product ff_v_b5bpao_product. ((((exists ff_h_b5bpao_product_start. ff_h_b5bpao_product_start + S (1) = S ((S (0)) * ff_v_b5bpao_product)) /\ exists ff_q_b5bpao_product_start. ff_u_b5bpao_product = ff_q_b5bpao_product_start * S ((S (0)) * ff_v_b5bpao_product) + (1))) /\ ((((exists ff_h_b5bpao_product_terminal. ff_h_b5bpao_product_terminal + S (z) = S ((S (l)) * ff_v_b5bpao_product)) /\ exists ff_q_b5bpao_product_terminal. ff_u_b5bpao_product = ff_q_b5bpao_product_terminal * S ((S (l)) * ff_v_b5bpao_product) + (z))) /\ forall ff_i_b5bpao_product. (exists ff_lt_b5bpao_product_bound. ff_lt_b5bpao_product_bound + S ff_i_b5bpao_product = l) -> exists ff_p_b5bpao_product ff_r_b5bpao_product ff_s_b5bpao_product. ((((exists ff_h_b5bpao_product_factor. ff_h_b5bpao_product_factor + S (ff_p_b5bpao_product) = S ((S (ff_i_b5bpao_product)) * c)) /\ exists ff_q_b5bpao_product_factor. b = ff_q_b5bpao_product_factor * S ((S (ff_i_b5bpao_product)) * c) + (ff_p_b5bpao_product))) /\ ((((exists ff_h_b5bpao_product_partial. ff_h_b5bpao_product_partial + S (ff_r_b5bpao_product) = S ((S (ff_i_b5bpao_product)) * ff_v_b5bpao_product)) /\ exists ff_q_b5bpao_product_partial. ff_u_b5bpao_product = ff_q_b5bpao_product_partial * S ((S (ff_i_b5bpao_product)) * ff_v_b5bpao_product) + (ff_r_b5bpao_product))) /\ ((((exists ff_h_b5bpao_product_successor. ff_h_b5bpao_product_successor + S (ff_s_b5bpao_product) = S ((S (S ff_i_b5bpao_product)) * ff_v_b5bpao_product)) /\ exists ff_q_b5bpao_product_successor. ff_u_b5bpao_product = ff_q_b5bpao_product_successor * S ((S (S ff_i_b5bpao_product)) * ff_v_b5bpao_product) + (ff_s_b5bpao_product))) /\ ff_s_b5bpao_product = ff_r_b5bpao_product * ff_p_b5bpao_product)))))) -> z = 1

Structural proof guide

A Product whose decoded factors are all one is exactly one.

Direct prerequisites: beta_product_zero, beta_product_succ_decompose, le_succ, le_refl, mul_one. The authored body proceeds by structural induction (1), case analysis (4), intermediate claims (4), equality transport (3).

Proof neighborhood

Direct dependencies

BT005I beta_product_zero BT005J beta_product_succ_decompose BT0018 le_succ BT000E le_refl BT000A mul_one

Direct dependents

BT0112 no_bertrand_high_contribution_interval_eq_one

Formal native tactic body

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

  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004intro z
  5. 0005intro hall
  6. 0006intro hproduct
  7. 0007specialize beta_product_zero b
  8. 0008specialize beta_product_zero c
  9. 0009specialize beta_product_zero z
  10. 0010apply beta_product_zero
  11. 0011exact hproduct
  12. 0012intro z
  13. 0013intro hall
  14. 0014intro hproduct
  15. 0015have hdecomposition : exists a r. (((exists bpr_height_b5bpao_decomposition_entry. bpr_height_b5bpao_decomposition_entry + S (a) = S ((S (l)) * c)) /\ exists bpr_quotient_b5bpao_decomposition_entry. b = bpr_quotient_b5bpao_decomposition_entry * S ((S (l)) * c) + (a))) /\ ((exists ff_u_b5bpao_decomposition_product ff_v_b5bpao_decomposition_product. ((((exists ff_h_b5bpao_decomposition_product_start. ff_h_b5bpao_decomposition_product_start + S (1) = S ((S (0)) * ff_v_b5bpao_decomposition_product)) /\ exists ff_q_b5bpao_decomposition_product_start. ff_u_b5bpao_decomposition_product = ff_q_b5bpao_decomposition_product_start * S ((S (0)) * ff_v_b5bpao_decomposition_product) + (1))) /\ ((((exists ff_h_b5bpao_decomposition_product_terminal. ff_h_b5bpao_decomposition_product_terminal + S (r) = S ((S (l)) * ff_v_b5bpao_decomposition_product)) /\ exists ff_q_b5bpao_decomposition_product_terminal. ff_u_b5bpao_decomposition_product = ff_q_b5bpao_decomposition_product_terminal * S ((S (l)) * ff_v_b5bpao_decomposition_product) + (r))) /\ forall ff_i_b5bpao_decomposition_product. (exists ff_lt_b5bpao_decomposition_product_bound. ff_lt_b5bpao_decomposition_product_bound + S ff_i_b5bpao_decomposition_product = l) -> exists ff_p_b5bpao_decomposition_product ff_r_b5bpao_decomposition_product ff_s_b5bpao_decomposition_product. ((((exists ff_h_b5bpao_decomposition_product_factor. ff_h_b5bpao_decomposition_product_factor + S (ff_p_b5bpao_decomposition_product) = S ((S (ff_i_b5bpao_decomposition_product)) * c)) /\ exists ff_q_b5bpao_decomposition_product_factor. b = ff_q_b5bpao_decomposition_product_factor * S ((S (ff_i_b5bpao_decomposition_product)) * c) + (ff_p_b5bpao_decomposition_product))) /\ ((((exists ff_h_b5bpao_decomposition_product_partial. ff_h_b5bpao_decomposition_product_partial + S (ff_r_b5bpao_decomposition_product) = S ((S (ff_i_b5bpao_decomposition_product)) * ff_v_b5bpao_decomposition_product)) /\ exists ff_q_b5bpao_decomposition_product_partial. ff_u_b5bpao_decomposition_product = ff_q_b5bpao_decomposition_product_partial * S ((S (ff_i_b5bpao_decomposition_product)) * ff_v_b5bpao_decomposition_product) + (ff_r_b5bpao_decomposition_product))) /\ ((((exists ff_h_b5bpao_decomposition_product_successor. ff_h_b5bpao_decomposition_product_successor + S (ff_s_b5bpao_decomposition_product) = S ((S (S ff_i_b5bpao_decomposition_product)) * ff_v_b5bpao_decomposition_product)) /\ exists ff_q_b5bpao_decomposition_product_successor. ff_u_b5bpao_decomposition_product = ff_q_b5bpao_decomposition_product_successor * S ((S (S ff_i_b5bpao_decomposition_product)) * ff_v_b5bpao_decomposition_product) + (ff_s_b5bpao_decomposition_product))) /\ ff_s_b5bpao_decomposition_product = ff_r_b5bpao_decomposition_product * ff_p_b5bpao_decomposition_product)))))) /\ z = r * a)
  16. 0016specialize beta_product_succ_decompose b
  17. 0017specialize beta_product_succ_decompose c
  18. 0018specialize beta_product_succ_decompose l
  19. 0019specialize beta_product_succ_decompose z
  20. 0020apply beta_product_succ_decompose
  21. 0021exact hproduct
  22. 0022cases hdecomposition
  23. 0023cases hdecomposition_witness
  24. 0024cases hdecomposition_witness_witness
  25. 0025cases hdecomposition_witness_witness_right
  26. 0026have hprevious : forall i a. (exists bcf_lt_gap_b5bpao_previous_bound. bcf_lt_gap_b5bpao_previous_bound + S (i) = l) -> (((exists bpr_height_b5bpao_previous_entry. bpr_height_b5bpao_previous_entry + S (a) = S ((S (i)) * c)) /\ exists bpr_quotient_b5bpao_previous_entry. b = bpr_quotient_b5bpao_previous_entry * S ((S (i)) * c) + (a))) -> a = 1
  27. 0027intro i
  28. 0028intro a
  29. 0029intro hi
  30. 0030intro ha
  31. 0031specialize hall i
  32. 0032specialize hall a
  33. 0033apply hall
  34. 0034specialize le_succ (S i)
  35. 0035specialize le_succ l
  36. 0036apply le_succ
  37. 0037exact hi
  38. 0038exact ha
  39. 0039have hprefix_one : x1 = 1
  40. 0040specialize IH x1
  41. 0041apply IH
  42. 0042exact hprevious
  43. 0043exact hdecomposition_witness_witness_right_left
  44. 0044have hfactor_one : x = 1
  45. 0045specialize hall l
  46. 0046specialize hall x
  47. 0047apply hall
  48. 0048specialize le_refl (S l)
  49. 0049exact le_refl
  50. 0050exact hdecomposition_witness_witness_left
  51. 0051rewrite hdecomposition_witness_witness_right_right
  52. 0052rewrite hprefix_one
  53. 0053rewrite hfactor_one
  54. 0054specialize mul_one 1
  55. 0055exact mul_one