bertrand_floor_power_product_le_h_from_total

Proof neighborhood

Direct dependencies

Direct dependents

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 s
3. 0003intro A
4. 0004intro H
5. 0005intro htotal
6. 0006intro hfloor
7. 0007intro hA
8. 0008intro hH
9. 0009have hstrict : exists k. k + S (2 * n) = S s * S s
10. 0010specialize floor_sqrt_strict_upper_bound (2 * n)
11. 0011specialize floor_sqrt_strict_upper_bound s
12. 0012apply floor_sqrt_strict_upper_bound
13. 0013exact hfloor
14. 0014have hweak : exists k. k + 2 * n = S s * S s
15. 0015specialize lt_to_le (2 * n)
16. 0016specialize lt_to_le (S s * S s)
17. 0017apply lt_to_le
18. 0018exact hstrict
19. 0019have hsucc : s + 1 = S s
20. 0020rewrite PA4
21. 0021congr
22. 0022apply PA3
23. 0023have hv_exists : exists v. (exists pa_b_b6_floor_product_square pa_c_b6_floor_product_square. ((forall pa_i_b6_floor_product_square_repeat. (exists pa_lt_b6_floor_product_square_repeat_bound. pa_lt_b6_floor_product_square_repeat_bound + S pa_i_b6_floor_product_square_repeat = 2) -> (((exists pa_h_b6_floor_product_square_repeat_decoded. pa_h_b6_floor_product_square_repeat_decoded + S (s + 1) = S ((S (pa_i_b6_floor_product_square_repeat)) * pa_c_b6_floor_product_square)) /\ exists pa_q_b6_floor_product_square_repeat_decoded. pa_b_b6_floor_product_square = pa_q_b6_floor_product_square_repeat_decoded * S ((S (pa_i_b6_floor_product_square_repeat)) * pa_c_b6_floor_product_square) + (s + 1)))) /\ (exists pa_u_b6_floor_product_square_product pa_v_b6_floor_product_square_product. ((((exists pa_h_b6_floor_product_square_product_start. pa_h_b6_floor_product_square_product_start + S (1) = S ((S (0)) * pa_v_b6_floor_product_square_product)) /\ exists pa_q_b6_floor_product_square_product_start. pa_u_b6_floor_product_square_product = pa_q_b6_floor_product_square_product_start * S ((S (0)) * pa_v_b6_floor_product_square_product) + (1))) /\ ((((exists pa_h_b6_floor_product_square_product_terminal. pa_h_b6_floor_product_square_product_terminal + S (v) = S ((S (2)) * pa_v_b6_floor_product_square_product)) /\ exists pa_q_b6_floor_product_square_product_terminal. pa_u_b6_floor_product_square_product = pa_q_b6_floor_product_square_product_terminal * S ((S (2)) * pa_v_b6_floor_product_square_product) + (v))) /\ forall pa_i_b6_floor_product_square_product. (exists pa_lt_b6_floor_product_square_product_bound. pa_lt_b6_floor_product_square_product_bound + S pa_i_b6_floor_product_square_product = 2) -> exists pa_p_b6_floor_product_square_product pa_r_b6_floor_product_square_product pa_s_b6_floor_product_square_product. ((((exists pa_h_b6_floor_product_square_product_factor. pa_h_b6_floor_product_square_product_factor + S (pa_p_b6_floor_product_square_product) = S ((S (pa_i_b6_floor_product_square_product)) * pa_c_b6_floor_product_square)) /\ exists pa_q_b6_floor_product_square_product_factor. pa_b_b6_floor_product_square = pa_q_b6_floor_product_square_product_factor * S ((S (pa_i_b6_floor_product_square_product)) * pa_c_b6_floor_product_square) + (pa_p_b6_floor_product_square_product))) /\ ((((exists pa_h_b6_floor_product_square_product_partial. pa_h_b6_floor_product_square_product_partial + S (pa_r_b6_floor_product_square_product) = S ((S (pa_i_b6_floor_product_square_product)) * pa_v_b6_floor_product_square_product)) /\ exists pa_q_b6_floor_product_square_product_partial. pa_u_b6_floor_product_square_product = pa_q_b6_floor_product_square_product_partial * S ((S (pa_i_b6_floor_product_square_product)) * pa_v_b6_floor_product_square_product) + (pa_r_b6_floor_product_square_product))) /\ ((((exists pa_h_b6_floor_product_square_product_successor. pa_h_b6_floor_product_square_product_successor + S (pa_s_b6_floor_product_square_product) = S ((S (S pa_i_b6_floor_product_square_product)) * pa_v_b6_floor_product_square_product)) /\ exists pa_q_b6_floor_product_square_product_successor. pa_u_b6_floor_product_square_product = pa_q_b6_floor_product_square_product_successor * S ((S (S pa_i_b6_floor_product_square_product)) * pa_v_b6_floor_product_square_product) + (pa_s_b6_floor_product_square_product))) /\ pa_s_b6_floor_product_square_product = pa_r_b6_floor_product_square_product * pa_p_b6_floor_product_square_product))))))))
24. 0024specialize htotal (s + 1)
25. 0025specialize htotal 2
26. 0026exact htotal
27. 0027cases hv_exists
28. 0028have hv_square : x = (s + 1) * (s + 1)
29. 0029specialize pow_two (s + 1)
30. 0030specialize pow_two 2
31. 0031specialize pow_two x
32. 0032apply pow_two
33. 0033refl
34. 0034exact hv_exists_witness
35. 0035have hbase : exists bqb_le_gap_b6_floor_product_base_order. bqb_le_gap_b6_floor_product_base_order + (2 * n) = (x)
36. 0036rewrite hv_square
37. 0037rewrite hsucc
38. 0038rewrite hsucc
39. 0039exact hweak
40. 0040have hu_exists : exists u. (exists pa_b_b6_floor_product_square_outer pa_c_b6_floor_product_square_outer. ((forall pa_i_b6_floor_product_square_outer_repeat. (exists pa_lt_b6_floor_product_square_outer_repeat_bound. pa_lt_b6_floor_product_square_outer_repeat_bound + S pa_i_b6_floor_product_square_outer_repeat = s) -> (((exists pa_h_b6_floor_product_square_outer_repeat_decoded. pa_h_b6_floor_product_square_outer_repeat_decoded + S (x) = S ((S (pa_i_b6_floor_product_square_outer_repeat)) * pa_c_b6_floor_product_square_outer)) /\ exists pa_q_b6_floor_product_square_outer_repeat_decoded. pa_b_b6_floor_product_square_outer = pa_q_b6_floor_product_square_outer_repeat_decoded * S ((S (pa_i_b6_floor_product_square_outer_repeat)) * pa_c_b6_floor_product_square_outer) + (x)))) /\ (exists pa_u_b6_floor_product_square_outer_product pa_v_b6_floor_product_square_outer_product. ((((exists pa_h_b6_floor_product_square_outer_product_start. pa_h_b6_floor_product_square_outer_product_start + S (1) = S ((S (0)) * pa_v_b6_floor_product_square_outer_product)) /\ exists pa_q_b6_floor_product_square_outer_product_start. pa_u_b6_floor_product_square_outer_product = pa_q_b6_floor_product_square_outer_product_start * S ((S (0)) * pa_v_b6_floor_product_square_outer_product) + (1))) /\ ((((exists pa_h_b6_floor_product_square_outer_product_terminal. pa_h_b6_floor_product_square_outer_product_terminal + S (u) = S ((S (s)) * pa_v_b6_floor_product_square_outer_product)) /\ exists pa_q_b6_floor_product_square_outer_product_terminal. pa_u_b6_floor_product_square_outer_product = pa_q_b6_floor_product_square_outer_product_terminal * S ((S (s)) * pa_v_b6_floor_product_square_outer_product) + (u))) /\ forall pa_i_b6_floor_product_square_outer_product. (exists pa_lt_b6_floor_product_square_outer_product_bound. pa_lt_b6_floor_product_square_outer_product_bound + S pa_i_b6_floor_product_square_outer_product = s) -> exists pa_p_b6_floor_product_square_outer_product pa_r_b6_floor_product_square_outer_product pa_s_b6_floor_product_square_outer_product. ((((exists pa_h_b6_floor_product_square_outer_product_factor. pa_h_b6_floor_product_square_outer_product_factor + S (pa_p_b6_floor_product_square_outer_product) = S ((S (pa_i_b6_floor_product_square_outer_product)) * pa_c_b6_floor_product_square_outer)) /\ exists pa_q_b6_floor_product_square_outer_product_factor. pa_b_b6_floor_product_square_outer = pa_q_b6_floor_product_square_outer_product_factor * S ((S (pa_i_b6_floor_product_square_outer_product)) * pa_c_b6_floor_product_square_outer) + (pa_p_b6_floor_product_square_outer_product))) /\ ((((exists pa_h_b6_floor_product_square_outer_product_partial. pa_h_b6_floor_product_square_outer_product_partial + S (pa_r_b6_floor_product_square_outer_product) = S ((S (pa_i_b6_floor_product_square_outer_product)) * pa_v_b6_floor_product_square_outer_product)) /\ exists pa_q_b6_floor_product_square_outer_product_partial. pa_u_b6_floor_product_square_outer_product = pa_q_b6_floor_product_square_outer_product_partial * S ((S (pa_i_b6_floor_product_square_outer_product)) * pa_v_b6_floor_product_square_outer_product) + (pa_r_b6_floor_product_square_outer_product))) /\ ((((exists pa_h_b6_floor_product_square_outer_product_successor. pa_h_b6_floor_product_square_outer_product_successor + S (pa_s_b6_floor_product_square_outer_product) = S ((S (S pa_i_b6_floor_product_square_outer_product)) * pa_v_b6_floor_product_square_outer_product)) /\ exists pa_q_b6_floor_product_square_outer_product_successor. pa_u_b6_floor_product_square_outer_product = pa_q_b6_floor_product_square_outer_product_successor * S ((S (S pa_i_b6_floor_product_square_outer_product)) * pa_v_b6_floor_product_square_outer_product) + (pa_s_b6_floor_product_square_outer_product))) /\ pa_s_b6_floor_product_square_outer_product = pa_r_b6_floor_product_square_outer_product * pa_p_b6_floor_product_square_outer_product))))))))
41. 0041specialize htotal x
42. 0042specialize htotal s
43. 0043exact htotal
44. 0044cases hu_exists
45. 0045have hpower : exists bqb_le_gap_b6_floor_product_power_order. bqb_le_gap_b6_floor_product_power_order + (A) = (x1)
46. 0046specialize pow_base_monotone (2 * n)
47. 0047specialize pow_base_monotone x
48. 0048specialize pow_base_monotone s
49. 0049specialize pow_base_monotone A
50. 0050specialize pow_base_monotone x1
51. 0051apply pow_base_monotone
52. 0052exact hbase
53. 0053exact hA
54. 0054exact hu_exists_witness
55. 0055have hz_exists : exists z. (exists pa_b_b6_floor_product_square_flat pa_c_b6_floor_product_square_flat. ((forall pa_i_b6_floor_product_square_flat_repeat. (exists pa_lt_b6_floor_product_square_flat_repeat_bound. pa_lt_b6_floor_product_square_flat_repeat_bound + S pa_i_b6_floor_product_square_flat_repeat = 2 * s) -> (((exists pa_h_b6_floor_product_square_flat_repeat_decoded. pa_h_b6_floor_product_square_flat_repeat_decoded + S (s + 1) = S ((S (pa_i_b6_floor_product_square_flat_repeat)) * pa_c_b6_floor_product_square_flat)) /\ exists pa_q_b6_floor_product_square_flat_repeat_decoded. pa_b_b6_floor_product_square_flat = pa_q_b6_floor_product_square_flat_repeat_decoded * S ((S (pa_i_b6_floor_product_square_flat_repeat)) * pa_c_b6_floor_product_square_flat) + (s + 1)))) /\ (exists pa_u_b6_floor_product_square_flat_product pa_v_b6_floor_product_square_flat_product. ((((exists pa_h_b6_floor_product_square_flat_product_start. pa_h_b6_floor_product_square_flat_product_start + S (1) = S ((S (0)) * pa_v_b6_floor_product_square_flat_product)) /\ exists pa_q_b6_floor_product_square_flat_product_start. pa_u_b6_floor_product_square_flat_product = pa_q_b6_floor_product_square_flat_product_start * S ((S (0)) * pa_v_b6_floor_product_square_flat_product) + (1))) /\ ((((exists pa_h_b6_floor_product_square_flat_product_terminal. pa_h_b6_floor_product_square_flat_product_terminal + S (z) = S ((S (2 * s)) * pa_v_b6_floor_product_square_flat_product)) /\ exists pa_q_b6_floor_product_square_flat_product_terminal. pa_u_b6_floor_product_square_flat_product = pa_q_b6_floor_product_square_flat_product_terminal * S ((S (2 * s)) * pa_v_b6_floor_product_square_flat_product) + (z))) /\ forall pa_i_b6_floor_product_square_flat_product. (exists pa_lt_b6_floor_product_square_flat_product_bound. pa_lt_b6_floor_product_square_flat_product_bound + S pa_i_b6_floor_product_square_flat_product = 2 * s) -> exists pa_p_b6_floor_product_square_flat_product pa_r_b6_floor_product_square_flat_product pa_s_b6_floor_product_square_flat_product. ((((exists pa_h_b6_floor_product_square_flat_product_factor. pa_h_b6_floor_product_square_flat_product_factor + S (pa_p_b6_floor_product_square_flat_product) = S ((S (pa_i_b6_floor_product_square_flat_product)) * pa_c_b6_floor_product_square_flat)) /\ exists pa_q_b6_floor_product_square_flat_product_factor. pa_b_b6_floor_product_square_flat = pa_q_b6_floor_product_square_flat_product_factor * S ((S (pa_i_b6_floor_product_square_flat_product)) * pa_c_b6_floor_product_square_flat) + (pa_p_b6_floor_product_square_flat_product))) /\ ((((exists pa_h_b6_floor_product_square_flat_product_partial. pa_h_b6_floor_product_square_flat_product_partial + S (pa_r_b6_floor_product_square_flat_product) = S ((S (pa_i_b6_floor_product_square_flat_product)) * pa_v_b6_floor_product_square_flat_product)) /\ exists pa_q_b6_floor_product_square_flat_product_partial. pa_u_b6_floor_product_square_flat_product = pa_q_b6_floor_product_square_flat_product_partial * S ((S (pa_i_b6_floor_product_square_flat_product)) * pa_v_b6_floor_product_square_flat_product) + (pa_r_b6_floor_product_square_flat_product))) /\ ((((exists pa_h_b6_floor_product_square_flat_product_successor. pa_h_b6_floor_product_square_flat_product_successor + S (pa_s_b6_floor_product_square_flat_product) = S ((S (S pa_i_b6_floor_product_square_flat_product)) * pa_v_b6_floor_product_square_flat_product)) /\ exists pa_q_b6_floor_product_square_flat_product_successor. pa_u_b6_floor_product_square_flat_product = pa_q_b6_floor_product_square_flat_product_successor * S ((S (S pa_i_b6_floor_product_square_flat_product)) * pa_v_b6_floor_product_square_flat_product) + (pa_s_b6_floor_product_square_flat_product))) /\ pa_s_b6_floor_product_square_flat_product = pa_r_b6_floor_product_square_flat_product * pa_p_b6_floor_product_square_flat_product))))))))
56. 0056specialize htotal (s + 1)
57. 0057specialize htotal (2 * s)
58. 0058exact htotal
59. 0059cases hz_exists
60. 0060have huz : x1 = x2
61. 0061specialize pow_mul_exp_from_total (s + 1)
62. 0062specialize pow_mul_exp_from_total 2
63. 0063specialize pow_mul_exp_from_total s
64. 0064specialize pow_mul_exp_from_total (2 * s)
65. 0065specialize pow_mul_exp_from_total x
66. 0066specialize pow_mul_exp_from_total x1
67. 0067specialize pow_mul_exp_from_total x2
68. 0068apply pow_mul_exp_from_total
69. 0069exact htotal
70. 0070refl
71. 0071exact hv_exists_witness
72. 0072exact hu_exists_witness
73. 0073exact hz_exists_witness
74. 0074have hfactor : H = x2 * x
75. 0075specialize pow_add (s + 1)
76. 0076specialize pow_add (2 * s)
77. 0077specialize pow_add 2
78. 0078specialize pow_add (2 * s + 2)
79. 0079specialize pow_add x2
80. 0080specialize pow_add x
81. 0081specialize pow_add H
82. 0082apply pow_add
83. 0083refl
84. 0084exact hz_exists_witness
85. 0085exact hv_exists_witness
86. 0086exact hH
87. 0087have hn_double_sum : exists k. k + n = n + n
88. 0088specialize le_add_right n
89. 0089specialize le_add_right n
90. 0090exact le_add_right
91. 0091have hdouble : 2 * n = n + n
92. 0092specialize two_mul_eq_add_self n
93. 0093exact two_mul_eq_add_self
94. 0094have hn_double : exists bqb_le_gap_b6_floor_product_n_double. bqb_le_gap_b6_floor_product_n_double + (n) = (2 * n)
95. 0095rewrite hdouble
96. 0096exact hn_double_sum
97. 0097have hn_square : exists bqb_le_gap_b6_floor_product_n_square. bqb_le_gap_b6_floor_product_n_square + (n) = (x)
98. 0098specialize le_trans n
99. 0099specialize le_trans (2 * n)
100. 0100specialize le_trans x
101. 0101apply le_trans
102. 0102exact hn_double
103. 0103exact hbase
104. 0104have hAz : exists k. k + A = x2
105. 0105rewrite <- huz
106. 0106exact hpower
107. 0107have hproduct : exists bqb_le_gap_b6_floor_product_intermediate. bqb_le_gap_b6_floor_product_intermediate + (n * A) = (x * x2)
108. 0108specialize mul_le_mul n
109. 0109specialize mul_le_mul x
110. 0110specialize mul_le_mul A
111. 0111specialize mul_le_mul x2
112. 0112apply mul_le_mul
113. 0113exact hn_square
114. 0114exact hAz
115. 0115have hcomm : x * x2 = x2 * x
116. 0116specialize mul_comm x
117. 0117specialize mul_comm x2
118. 0118exact mul_comm
119. 0119rewrite hcomm at hproduct
120. 0120rewrite <- hfactor at hproduct
121. 0121exact hproduct