quadratic_residue_half_power_mod_one

Proof neighborhood

Direct dependencies

Direct dependents

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

1. 0001intro p
2. 0002intro h
3. 0003intro a
4. 0004intro A
5. 0005intro hshape
6. 0006intro hp
7. 0007intro hnonzero
8. 0008intro hresidue
9. 0009intro hA
10. 0010cases hresidue
11. 0011have hp0 : ~(p = 0)
12. 0012intro hpzero
13. 0013specialize prime_nonzero p
14. 0014apply prime_nonzero
15. 0015exact hp
16. 0016exact hpzero
17. 0017have hroot_nonzero : ~(exists k. x = p * k)
18. 0018intro hroot_divides
19. 0019have hsquare_divides : exists k. x * x = p * k
20. 0020specialize multiple_mul_right p
21. 0021specialize multiple_mul_right x
22. 0022specialize multiple_mul_right x
23. 0023apply multiple_mul_right
24. 0024exact hroot_divides
25. 0025have hsquare_zero : exists wpp_mod_left_euler_root_square_zero wpp_mod_right_euler_root_square_zero. (x * x) + p * wpp_mod_left_euler_root_square_zero = (0) + p * wpp_mod_right_euler_root_square_zero
26. 0026specialize dvd_to_mod_zero p
27. 0027specialize dvd_to_mod_zero (x * x)
28. 0028apply dvd_to_mod_zero
29. 0029exact hsquare_divides
30. 0030have hvalue_square : exists wpp_mod_left_euler_value_square wpp_mod_right_euler_value_square. (a) + p * wpp_mod_left_euler_value_square = (x * x) + p * wpp_mod_right_euler_value_square
31. 0031specialize mod_eq_symm p
32. 0032specialize mod_eq_symm (x * x)
33. 0033specialize mod_eq_symm a
34. 0034apply mod_eq_symm
35. 0035exact hresidue_witness
36. 0036have hvalue_zero : exists wpp_mod_left_euler_value_zero wpp_mod_right_euler_value_zero. (a) + p * wpp_mod_left_euler_value_zero = (0) + p * wpp_mod_right_euler_value_zero
37. 0037specialize mod_eq_trans p
38. 0038specialize mod_eq_trans a
39. 0039specialize mod_eq_trans (x * x)
40. 0040specialize mod_eq_trans 0
41. 0041apply mod_eq_trans
42. 0042exact hvalue_square
43. 0043exact hsquare_zero
44. 0044have hvalue_divides : exists k. a = p * k
45. 0045specialize mod_eq_zero_to_dvd_nonzero p
46. 0046specialize mod_eq_zero_to_dvd_nonzero a
47. 0047apply mod_eq_zero_to_dvd_nonzero
48. 0048exact hp0
49. 0049exact hvalue_zero
50. 0050apply hnonzero
51. 0051exact hvalue_divides
52. 0052have hroot_two_exists : exists R. (exists pa_b_euler_root_two_exists pa_c_euler_root_two_exists. ((forall pa_i_euler_root_two_exists_repeat. (exists pa_lt_euler_root_two_exists_repeat_bound. pa_lt_euler_root_two_exists_repeat_bound + S pa_i_euler_root_two_exists_repeat = 2) -> (((exists pa_h_euler_root_two_exists_repeat_decoded. pa_h_euler_root_two_exists_repeat_decoded + S (x) = S ((S (pa_i_euler_root_two_exists_repeat)) * pa_c_euler_root_two_exists)) /\ exists pa_q_euler_root_two_exists_repeat_decoded. pa_b_euler_root_two_exists = pa_q_euler_root_two_exists_repeat_decoded * S ((S (pa_i_euler_root_two_exists_repeat)) * pa_c_euler_root_two_exists) + (x)))) /\ (exists pa_u_euler_root_two_exists_product pa_v_euler_root_two_exists_product. ((((exists pa_h_euler_root_two_exists_product_start. pa_h_euler_root_two_exists_product_start + S (1) = S ((S (0)) * pa_v_euler_root_two_exists_product)) /\ exists pa_q_euler_root_two_exists_product_start. pa_u_euler_root_two_exists_product = pa_q_euler_root_two_exists_product_start * S ((S (0)) * pa_v_euler_root_two_exists_product) + (1))) /\ ((((exists pa_h_euler_root_two_exists_product_terminal. pa_h_euler_root_two_exists_product_terminal + S (R) = S ((S (2)) * pa_v_euler_root_two_exists_product)) /\ exists pa_q_euler_root_two_exists_product_terminal. pa_u_euler_root_two_exists_product = pa_q_euler_root_two_exists_product_terminal * S ((S (2)) * pa_v_euler_root_two_exists_product) + (R))) /\ forall pa_i_euler_root_two_exists_product. (exists pa_lt_euler_root_two_exists_product_bound. pa_lt_euler_root_two_exists_product_bound + S pa_i_euler_root_two_exists_product = 2) -> exists pa_p_euler_root_two_exists_product pa_r_euler_root_two_exists_product pa_s_euler_root_two_exists_product. ((((exists pa_h_euler_root_two_exists_product_factor. pa_h_euler_root_two_exists_product_factor + S (pa_p_euler_root_two_exists_product) = S ((S (pa_i_euler_root_two_exists_product)) * pa_c_euler_root_two_exists)) /\ exists pa_q_euler_root_two_exists_product_factor. pa_b_euler_root_two_exists = pa_q_euler_root_two_exists_product_factor * S ((S (pa_i_euler_root_two_exists_product)) * pa_c_euler_root_two_exists) + (pa_p_euler_root_two_exists_product))) /\ ((((exists pa_h_euler_root_two_exists_product_partial. pa_h_euler_root_two_exists_product_partial + S (pa_r_euler_root_two_exists_product) = S ((S (pa_i_euler_root_two_exists_product)) * pa_v_euler_root_two_exists_product)) /\ exists pa_q_euler_root_two_exists_product_partial. pa_u_euler_root_two_exists_product = pa_q_euler_root_two_exists_product_partial * S ((S (pa_i_euler_root_two_exists_product)) * pa_v_euler_root_two_exists_product) + (pa_r_euler_root_two_exists_product))) /\ ((((exists pa_h_euler_root_two_exists_product_successor. pa_h_euler_root_two_exists_product_successor + S (pa_s_euler_root_two_exists_product) = S ((S (S pa_i_euler_root_two_exists_product)) * pa_v_euler_root_two_exists_product)) /\ exists pa_q_euler_root_two_exists_product_successor. pa_u_euler_root_two_exists_product = pa_q_euler_root_two_exists_product_successor * S ((S (S pa_i_euler_root_two_exists_product)) * pa_v_euler_root_two_exists_product) + (pa_s_euler_root_two_exists_product))) /\ pa_s_euler_root_two_exists_product = pa_r_euler_root_two_exists_product * pa_p_euler_root_two_exists_product))))))))
53. 0053specialize pow_exists x
54. 0054specialize pow_exists 2
55. 0055exact pow_exists
56. 0056cases hroot_two_exists
57. 0057have hroot_two : exists pa_b_euler_root_two pa_c_euler_root_two. ((forall pa_i_euler_root_two_repeat. (exists pa_lt_euler_root_two_repeat_bound. pa_lt_euler_root_two_repeat_bound + S pa_i_euler_root_two_repeat = 2) -> (((exists pa_h_euler_root_two_repeat_decoded. pa_h_euler_root_two_repeat_decoded + S (x) = S ((S (pa_i_euler_root_two_repeat)) * pa_c_euler_root_two)) /\ exists pa_q_euler_root_two_repeat_decoded. pa_b_euler_root_two = pa_q_euler_root_two_repeat_decoded * S ((S (pa_i_euler_root_two_repeat)) * pa_c_euler_root_two) + (x)))) /\ (exists pa_u_euler_root_two_product pa_v_euler_root_two_product. ((((exists pa_h_euler_root_two_product_start. pa_h_euler_root_two_product_start + S (1) = S ((S (0)) * pa_v_euler_root_two_product)) /\ exists pa_q_euler_root_two_product_start. pa_u_euler_root_two_product = pa_q_euler_root_two_product_start * S ((S (0)) * pa_v_euler_root_two_product) + (1))) /\ ((((exists pa_h_euler_root_two_product_terminal. pa_h_euler_root_two_product_terminal + S (x1) = S ((S (2)) * pa_v_euler_root_two_product)) /\ exists pa_q_euler_root_two_product_terminal. pa_u_euler_root_two_product = pa_q_euler_root_two_product_terminal * S ((S (2)) * pa_v_euler_root_two_product) + (x1))) /\ forall pa_i_euler_root_two_product. (exists pa_lt_euler_root_two_product_bound. pa_lt_euler_root_two_product_bound + S pa_i_euler_root_two_product = 2) -> exists pa_p_euler_root_two_product pa_r_euler_root_two_product pa_s_euler_root_two_product. ((((exists pa_h_euler_root_two_product_factor. pa_h_euler_root_two_product_factor + S (pa_p_euler_root_two_product) = S ((S (pa_i_euler_root_two_product)) * pa_c_euler_root_two)) /\ exists pa_q_euler_root_two_product_factor. pa_b_euler_root_two = pa_q_euler_root_two_product_factor * S ((S (pa_i_euler_root_two_product)) * pa_c_euler_root_two) + (pa_p_euler_root_two_product))) /\ ((((exists pa_h_euler_root_two_product_partial. pa_h_euler_root_two_product_partial + S (pa_r_euler_root_two_product) = S ((S (pa_i_euler_root_two_product)) * pa_v_euler_root_two_product)) /\ exists pa_q_euler_root_two_product_partial. pa_u_euler_root_two_product = pa_q_euler_root_two_product_partial * S ((S (pa_i_euler_root_two_product)) * pa_v_euler_root_two_product) + (pa_r_euler_root_two_product))) /\ ((((exists pa_h_euler_root_two_product_successor. pa_h_euler_root_two_product_successor + S (pa_s_euler_root_two_product) = S ((S (S pa_i_euler_root_two_product)) * pa_v_euler_root_two_product)) /\ exists pa_q_euler_root_two_product_successor. pa_u_euler_root_two_product = pa_q_euler_root_two_product_successor * S ((S (S pa_i_euler_root_two_product)) * pa_v_euler_root_two_product) + (pa_s_euler_root_two_product))) /\ pa_s_euler_root_two_product = pa_r_euler_root_two_product * pa_p_euler_root_two_product)))))))
58. 0058exact hroot_two_exists_witness
59. 0059have hroot_two_eq : x1 = x * x
60. 0060specialize pow_two x
61. 0061specialize pow_two 2
62. 0062specialize pow_two x1
63. 0063apply pow_two
64. 0064refl
65. 0065exact hroot_two
66. 0066have hsquare_half_exists : exists R. (exists ff_b_euler_square_half_exists ff_c_euler_square_half_exists. ((forall ff_i_euler_square_half_exists_repeat. (exists ff_lt_euler_square_half_exists_repeat_bound. ff_lt_euler_square_half_exists_repeat_bound + S ff_i_euler_square_half_exists_repeat = h) -> (((exists ff_h_euler_square_half_exists_repeat_decoded. ff_h_euler_square_half_exists_repeat_decoded + S (x1) = S ((S (ff_i_euler_square_half_exists_repeat)) * ff_c_euler_square_half_exists)) /\ exists ff_q_euler_square_half_exists_repeat_decoded. ff_b_euler_square_half_exists = ff_q_euler_square_half_exists_repeat_decoded * S ((S (ff_i_euler_square_half_exists_repeat)) * ff_c_euler_square_half_exists) + (x1)))) /\ (exists ff_u_euler_square_half_exists_product ff_v_euler_square_half_exists_product. ((((exists ff_h_euler_square_half_exists_product_start. ff_h_euler_square_half_exists_product_start + S (1) = S ((S (0)) * ff_v_euler_square_half_exists_product)) /\ exists ff_q_euler_square_half_exists_product_start. ff_u_euler_square_half_exists_product = ff_q_euler_square_half_exists_product_start * S ((S (0)) * ff_v_euler_square_half_exists_product) + (1))) /\ ((((exists ff_h_euler_square_half_exists_product_terminal. ff_h_euler_square_half_exists_product_terminal + S (R) = S ((S (h)) * ff_v_euler_square_half_exists_product)) /\ exists ff_q_euler_square_half_exists_product_terminal. ff_u_euler_square_half_exists_product = ff_q_euler_square_half_exists_product_terminal * S ((S (h)) * ff_v_euler_square_half_exists_product) + (R))) /\ forall ff_i_euler_square_half_exists_product. (exists ff_lt_euler_square_half_exists_product_bound. ff_lt_euler_square_half_exists_product_bound + S ff_i_euler_square_half_exists_product = h) -> exists ff_p_euler_square_half_exists_product ff_r_euler_square_half_exists_product ff_s_euler_square_half_exists_product. ((((exists ff_h_euler_square_half_exists_product_factor. ff_h_euler_square_half_exists_product_factor + S (ff_p_euler_square_half_exists_product) = S ((S (ff_i_euler_square_half_exists_product)) * ff_c_euler_square_half_exists)) /\ exists ff_q_euler_square_half_exists_product_factor. ff_b_euler_square_half_exists = ff_q_euler_square_half_exists_product_factor * S ((S (ff_i_euler_square_half_exists_product)) * ff_c_euler_square_half_exists) + (ff_p_euler_square_half_exists_product))) /\ ((((exists ff_h_euler_square_half_exists_product_partial. ff_h_euler_square_half_exists_product_partial + S (ff_r_euler_square_half_exists_product) = S ((S (ff_i_euler_square_half_exists_product)) * ff_v_euler_square_half_exists_product)) /\ exists ff_q_euler_square_half_exists_product_partial. ff_u_euler_square_half_exists_product = ff_q_euler_square_half_exists_product_partial * S ((S (ff_i_euler_square_half_exists_product)) * ff_v_euler_square_half_exists_product) + (ff_r_euler_square_half_exists_product))) /\ ((((exists ff_h_euler_square_half_exists_product_successor. ff_h_euler_square_half_exists_product_successor + S (ff_s_euler_square_half_exists_product) = S ((S (S ff_i_euler_square_half_exists_product)) * ff_v_euler_square_half_exists_product)) /\ exists ff_q_euler_square_half_exists_product_successor. ff_u_euler_square_half_exists_product = ff_q_euler_square_half_exists_product_successor * S ((S (S ff_i_euler_square_half_exists_product)) * ff_v_euler_square_half_exists_product) + (ff_s_euler_square_half_exists_product))) /\ ff_s_euler_square_half_exists_product = ff_r_euler_square_half_exists_product * ff_p_euler_square_half_exists_product))))))))
67. 0067specialize pow_exists x1
68. 0068specialize pow_exists h
69. 0069exact pow_exists
70. 0070cases hsquare_half_exists
71. 0071have hsquare_half : exists ff_b_euler_square_half ff_c_euler_square_half. ((forall ff_i_euler_square_half_repeat. (exists ff_lt_euler_square_half_repeat_bound. ff_lt_euler_square_half_repeat_bound + S ff_i_euler_square_half_repeat = h) -> (((exists ff_h_euler_square_half_repeat_decoded. ff_h_euler_square_half_repeat_decoded + S (x1) = S ((S (ff_i_euler_square_half_repeat)) * ff_c_euler_square_half)) /\ exists ff_q_euler_square_half_repeat_decoded. ff_b_euler_square_half = ff_q_euler_square_half_repeat_decoded * S ((S (ff_i_euler_square_half_repeat)) * ff_c_euler_square_half) + (x1)))) /\ (exists ff_u_euler_square_half_product ff_v_euler_square_half_product. ((((exists ff_h_euler_square_half_product_start. ff_h_euler_square_half_product_start + S (1) = S ((S (0)) * ff_v_euler_square_half_product)) /\ exists ff_q_euler_square_half_product_start. ff_u_euler_square_half_product = ff_q_euler_square_half_product_start * S ((S (0)) * ff_v_euler_square_half_product) + (1))) /\ ((((exists ff_h_euler_square_half_product_terminal. ff_h_euler_square_half_product_terminal + S (x2) = S ((S (h)) * ff_v_euler_square_half_product)) /\ exists ff_q_euler_square_half_product_terminal. ff_u_euler_square_half_product = ff_q_euler_square_half_product_terminal * S ((S (h)) * ff_v_euler_square_half_product) + (x2))) /\ forall ff_i_euler_square_half_product. (exists ff_lt_euler_square_half_product_bound. ff_lt_euler_square_half_product_bound + S ff_i_euler_square_half_product = h) -> exists ff_p_euler_square_half_product ff_r_euler_square_half_product ff_s_euler_square_half_product. ((((exists ff_h_euler_square_half_product_factor. ff_h_euler_square_half_product_factor + S (ff_p_euler_square_half_product) = S ((S (ff_i_euler_square_half_product)) * ff_c_euler_square_half)) /\ exists ff_q_euler_square_half_product_factor. ff_b_euler_square_half = ff_q_euler_square_half_product_factor * S ((S (ff_i_euler_square_half_product)) * ff_c_euler_square_half) + (ff_p_euler_square_half_product))) /\ ((((exists ff_h_euler_square_half_product_partial. ff_h_euler_square_half_product_partial + S (ff_r_euler_square_half_product) = S ((S (ff_i_euler_square_half_product)) * ff_v_euler_square_half_product)) /\ exists ff_q_euler_square_half_product_partial. ff_u_euler_square_half_product = ff_q_euler_square_half_product_partial * S ((S (ff_i_euler_square_half_product)) * ff_v_euler_square_half_product) + (ff_r_euler_square_half_product))) /\ ((((exists ff_h_euler_square_half_product_successor. ff_h_euler_square_half_product_successor + S (ff_s_euler_square_half_product) = S ((S (S ff_i_euler_square_half_product)) * ff_v_euler_square_half_product)) /\ exists ff_q_euler_square_half_product_successor. ff_u_euler_square_half_product = ff_q_euler_square_half_product_successor * S ((S (S ff_i_euler_square_half_product)) * ff_v_euler_square_half_product) + (ff_s_euler_square_half_product))) /\ ff_s_euler_square_half_product = ff_r_euler_square_half_product * ff_p_euler_square_half_product)))))))
72. 0072exact hsquare_half_exists_witness
73. 0073have hroot_total_exists : exists R. (exists pa_b_euler_root_total_exists pa_c_euler_root_total_exists. ((forall pa_i_euler_root_total_exists_repeat. (exists pa_lt_euler_root_total_exists_repeat_bound. pa_lt_euler_root_total_exists_repeat_bound + S pa_i_euler_root_total_exists_repeat = 2 * h) -> (((exists pa_h_euler_root_total_exists_repeat_decoded. pa_h_euler_root_total_exists_repeat_decoded + S (x) = S ((S (pa_i_euler_root_total_exists_repeat)) * pa_c_euler_root_total_exists)) /\ exists pa_q_euler_root_total_exists_repeat_decoded. pa_b_euler_root_total_exists = pa_q_euler_root_total_exists_repeat_decoded * S ((S (pa_i_euler_root_total_exists_repeat)) * pa_c_euler_root_total_exists) + (x)))) /\ (exists pa_u_euler_root_total_exists_product pa_v_euler_root_total_exists_product. ((((exists pa_h_euler_root_total_exists_product_start. pa_h_euler_root_total_exists_product_start + S (1) = S ((S (0)) * pa_v_euler_root_total_exists_product)) /\ exists pa_q_euler_root_total_exists_product_start. pa_u_euler_root_total_exists_product = pa_q_euler_root_total_exists_product_start * S ((S (0)) * pa_v_euler_root_total_exists_product) + (1))) /\ ((((exists pa_h_euler_root_total_exists_product_terminal. pa_h_euler_root_total_exists_product_terminal + S (R) = S ((S (2 * h)) * pa_v_euler_root_total_exists_product)) /\ exists pa_q_euler_root_total_exists_product_terminal. pa_u_euler_root_total_exists_product = pa_q_euler_root_total_exists_product_terminal * S ((S (2 * h)) * pa_v_euler_root_total_exists_product) + (R))) /\ forall pa_i_euler_root_total_exists_product. (exists pa_lt_euler_root_total_exists_product_bound. pa_lt_euler_root_total_exists_product_bound + S pa_i_euler_root_total_exists_product = 2 * h) -> exists pa_p_euler_root_total_exists_product pa_r_euler_root_total_exists_product pa_s_euler_root_total_exists_product. ((((exists pa_h_euler_root_total_exists_product_factor. pa_h_euler_root_total_exists_product_factor + S (pa_p_euler_root_total_exists_product) = S ((S (pa_i_euler_root_total_exists_product)) * pa_c_euler_root_total_exists)) /\ exists pa_q_euler_root_total_exists_product_factor. pa_b_euler_root_total_exists = pa_q_euler_root_total_exists_product_factor * S ((S (pa_i_euler_root_total_exists_product)) * pa_c_euler_root_total_exists) + (pa_p_euler_root_total_exists_product))) /\ ((((exists pa_h_euler_root_total_exists_product_partial. pa_h_euler_root_total_exists_product_partial + S (pa_r_euler_root_total_exists_product) = S ((S (pa_i_euler_root_total_exists_product)) * pa_v_euler_root_total_exists_product)) /\ exists pa_q_euler_root_total_exists_product_partial. pa_u_euler_root_total_exists_product = pa_q_euler_root_total_exists_product_partial * S ((S (pa_i_euler_root_total_exists_product)) * pa_v_euler_root_total_exists_product) + (pa_r_euler_root_total_exists_product))) /\ ((((exists pa_h_euler_root_total_exists_product_successor. pa_h_euler_root_total_exists_product_successor + S (pa_s_euler_root_total_exists_product) = S ((S (S pa_i_euler_root_total_exists_product)) * pa_v_euler_root_total_exists_product)) /\ exists pa_q_euler_root_total_exists_product_successor. pa_u_euler_root_total_exists_product = pa_q_euler_root_total_exists_product_successor * S ((S (S pa_i_euler_root_total_exists_product)) * pa_v_euler_root_total_exists_product) + (pa_s_euler_root_total_exists_product))) /\ pa_s_euler_root_total_exists_product = pa_r_euler_root_total_exists_product * pa_p_euler_root_total_exists_product))))))))
74. 0074specialize pow_exists x
75. 0075specialize pow_exists (2 * h)
76. 0076exact pow_exists
77. 0077cases hroot_total_exists
78. 0078have hroot_total : exists pa_b_euler_root_double_half pa_c_euler_root_double_half. ((forall pa_i_euler_root_double_half_repeat. (exists pa_lt_euler_root_double_half_repeat_bound. pa_lt_euler_root_double_half_repeat_bound + S pa_i_euler_root_double_half_repeat = 2 * h) -> (((exists pa_h_euler_root_double_half_repeat_decoded. pa_h_euler_root_double_half_repeat_decoded + S (x) = S ((S (pa_i_euler_root_double_half_repeat)) * pa_c_euler_root_double_half)) /\ exists pa_q_euler_root_double_half_repeat_decoded. pa_b_euler_root_double_half = pa_q_euler_root_double_half_repeat_decoded * S ((S (pa_i_euler_root_double_half_repeat)) * pa_c_euler_root_double_half) + (x)))) /\ (exists pa_u_euler_root_double_half_product pa_v_euler_root_double_half_product. ((((exists pa_h_euler_root_double_half_product_start. pa_h_euler_root_double_half_product_start + S (1) = S ((S (0)) * pa_v_euler_root_double_half_product)) /\ exists pa_q_euler_root_double_half_product_start. pa_u_euler_root_double_half_product = pa_q_euler_root_double_half_product_start * S ((S (0)) * pa_v_euler_root_double_half_product) + (1))) /\ ((((exists pa_h_euler_root_double_half_product_terminal. pa_h_euler_root_double_half_product_terminal + S (x3) = S ((S (2 * h)) * pa_v_euler_root_double_half_product)) /\ exists pa_q_euler_root_double_half_product_terminal. pa_u_euler_root_double_half_product = pa_q_euler_root_double_half_product_terminal * S ((S (2 * h)) * pa_v_euler_root_double_half_product) + (x3))) /\ forall pa_i_euler_root_double_half_product. (exists pa_lt_euler_root_double_half_product_bound. pa_lt_euler_root_double_half_product_bound + S pa_i_euler_root_double_half_product = 2 * h) -> exists pa_p_euler_root_double_half_product pa_r_euler_root_double_half_product pa_s_euler_root_double_half_product. ((((exists pa_h_euler_root_double_half_product_factor. pa_h_euler_root_double_half_product_factor + S (pa_p_euler_root_double_half_product) = S ((S (pa_i_euler_root_double_half_product)) * pa_c_euler_root_double_half)) /\ exists pa_q_euler_root_double_half_product_factor. pa_b_euler_root_double_half = pa_q_euler_root_double_half_product_factor * S ((S (pa_i_euler_root_double_half_product)) * pa_c_euler_root_double_half) + (pa_p_euler_root_double_half_product))) /\ ((((exists pa_h_euler_root_double_half_product_partial. pa_h_euler_root_double_half_product_partial + S (pa_r_euler_root_double_half_product) = S ((S (pa_i_euler_root_double_half_product)) * pa_v_euler_root_double_half_product)) /\ exists pa_q_euler_root_double_half_product_partial. pa_u_euler_root_double_half_product = pa_q_euler_root_double_half_product_partial * S ((S (pa_i_euler_root_double_half_product)) * pa_v_euler_root_double_half_product) + (pa_r_euler_root_double_half_product))) /\ ((((exists pa_h_euler_root_double_half_product_successor. pa_h_euler_root_double_half_product_successor + S (pa_s_euler_root_double_half_product) = S ((S (S pa_i_euler_root_double_half_product)) * pa_v_euler_root_double_half_product)) /\ exists pa_q_euler_root_double_half_product_successor. pa_u_euler_root_double_half_product = pa_q_euler_root_double_half_product_successor * S ((S (S pa_i_euler_root_double_half_product)) * pa_v_euler_root_double_half_product) + (pa_s_euler_root_double_half_product))) /\ pa_s_euler_root_double_half_product = pa_r_euler_root_double_half_product * pa_p_euler_root_double_half_product)))))))
79. 0079exact hroot_total_exists_witness
80. 0080have hiterated : x2 = x3
81. 0081specialize pow_mul_exp x
82. 0082specialize pow_mul_exp 2
83. 0083specialize pow_mul_exp h
84. 0084specialize pow_mul_exp (2 * h)
85. 0085specialize pow_mul_exp x1
86. 0086specialize pow_mul_exp x2
87. 0087specialize pow_mul_exp x3
88. 0088apply pow_mul_exp
89. 0089refl
90. 0090exact hroot_two
91. 0091exact hsquare_half
92. 0092exact hroot_total
93. 0093have hpredecessor : p = S (2 * h)
94. 0094trans 2 * h + 1
95. 0095exact hshape
96. 0096simp
97. 0097have hfermat : exists wpp_mod_left_euler_root_fermat wpp_mod_right_euler_root_fermat. (x3) + p * wpp_mod_left_euler_root_fermat = (1) + p * wpp_mod_right_euler_root_fermat
98. 0098specialize fermat_predecessor_exponent_mod_one p
99. 0099specialize fermat_predecessor_exponent_mod_one (2 * h)
100. 0100specialize fermat_predecessor_exponent_mod_one x
101. 0101specialize fermat_predecessor_exponent_mod_one x3
102. 0102apply fermat_predecessor_exponent_mod_one
103. 0103exact hpredecessor
104. 0104exact hp
105. 0105exact hroot_nonzero
106. 0106exact hroot_total
107. 0107have hsquare_value : exists wpp_mod_left_euler_square_value wpp_mod_right_euler_square_value. (x1) + p * wpp_mod_left_euler_square_value = (a) + p * wpp_mod_right_euler_square_value
108. 0108rewrite hroot_two_eq
109. 0109exact hresidue_witness
110. 0110have hpowers : exists wpp_mod_left_euler_powers_congruent wpp_mod_right_euler_powers_congruent. (x2) + p * wpp_mod_left_euler_powers_congruent = (A) + p * wpp_mod_right_euler_powers_congruent
111. 0111specialize pow_mod_congruent p
112. 0112specialize pow_mod_congruent x1
113. 0113specialize pow_mod_congruent a
114. 0114specialize pow_mod_congruent h
115. 0115specialize pow_mod_congruent x2
116. 0116specialize pow_mod_congruent A
117. 0117apply pow_mod_congruent
118. 0118exact hsquare_value
119. 0119exact hsquare_half
120. 0120exact hA
121. 0121have hback : exists wpp_mod_left_euler_value_power_back wpp_mod_right_euler_value_power_back. (A) + p * wpp_mod_left_euler_value_power_back = (x2) + p * wpp_mod_right_euler_value_power_back
122. 0122specialize mod_eq_symm p
123. 0123specialize mod_eq_symm x2
124. 0124specialize mod_eq_symm A
125. 0125apply mod_eq_symm
126. 0126exact hpowers
127. 0127have hhalf_one : exists wpp_mod_left_euler_root_half_one wpp_mod_right_euler_root_half_one. (x2) + p * wpp_mod_left_euler_root_half_one = (1) + p * wpp_mod_right_euler_root_half_one
128. 0128rewrite hiterated
129. 0129exact hfermat
130. 0130specialize mod_eq_trans p
131. 0131specialize mod_eq_trans A
132. 0132specialize mod_eq_trans x2
133. 0133specialize mod_eq_trans 1
134. 0134apply mod_eq_trans
135. 0135exact hback
136. 0136exact hhalf_one