Proof of Theorem m1lgs
| Step | Hyp | Ref
| Expression |
| 1 | | neg1z 12653 |
. . . . . . . . 9
⊢ -1 ∈
ℤ |
| 2 | | oddprm 16848 |
. . . . . . . . . 10
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
| 3 | 2 | nnnn0d 12587 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ0) |
| 4 | | zexpcl 14117 |
. . . . . . . . 9
⊢ ((-1
∈ ℤ ∧ ((𝑃
− 1) / 2) ∈ ℕ0) → (-1↑((𝑃 − 1) / 2)) ∈
ℤ) |
| 5 | 1, 3, 4 | sylancr 587 |
. . . . . . . 8
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (-1↑((𝑃 −
1) / 2)) ∈ ℤ) |
| 6 | 5 | peano2zd 12725 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((-1↑((𝑃
− 1) / 2)) + 1) ∈ ℤ) |
| 7 | | eldifi 4131 |
. . . . . . . 8
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
| 8 | | prmnn 16711 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℕ) |
| 10 | 6, 9 | zmodcld 13932 |
. . . . . 6
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (((-1↑((𝑃
− 1) / 2)) + 1) mod 𝑃) ∈
ℕ0) |
| 11 | 10 | nn0cnd 12589 |
. . . . 5
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (((-1↑((𝑃
− 1) / 2)) + 1) mod 𝑃) ∈ ℂ) |
| 12 | | 1cnd 11256 |
. . . . 5
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 1 ∈ ℂ) |
| 13 | 11, 12, 12 | subaddd 11638 |
. . . 4
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (((((-1↑((𝑃
− 1) / 2)) + 1) mod 𝑃) − 1) = 1 ↔ (1 + 1) =
(((-1↑((𝑃 − 1) /
2)) + 1) mod 𝑃))) |
| 14 | | 2re 12340 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
| 15 | 14 | a1i 11 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 2 ∈ ℝ) |
| 16 | 9 | nnrpd 13075 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℝ+) |
| 17 | | 0le2 12368 |
. . . . . . . 8
⊢ 0 ≤
2 |
| 18 | 17 | a1i 11 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 0 ≤ 2) |
| 19 | | oddprmgt2 16736 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 2 < 𝑃) |
| 20 | | modid 13936 |
. . . . . . 7
⊢ (((2
∈ ℝ ∧ 𝑃
∈ ℝ+) ∧ (0 ≤ 2 ∧ 2 < 𝑃)) → (2 mod 𝑃) = 2) |
| 21 | 15, 16, 18, 19, 20 | syl22anc 839 |
. . . . . 6
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (2 mod 𝑃) =
2) |
| 22 | | df-2 12329 |
. . . . . 6
⊢ 2 = (1 +
1) |
| 23 | 21, 22 | eqtrdi 2793 |
. . . . 5
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (2 mod 𝑃) = (1 +
1)) |
| 24 | 23 | eqeq1d 2739 |
. . . 4
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((2 mod 𝑃) =
(((-1↑((𝑃 − 1) /
2)) + 1) mod 𝑃) ↔ (1 +
1) = (((-1↑((𝑃 −
1) / 2)) + 1) mod 𝑃))) |
| 25 | | eldifsni 4790 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ≠
2) |
| 26 | 25 | neneqd 2945 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ¬ 𝑃 =
2) |
| 27 | | prmuz2 16733 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
| 28 | 7, 27 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
(ℤ≥‘2)) |
| 29 | | 2prm 16729 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℙ |
| 30 | | dvdsprm 16740 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 2 ∈ ℙ) → (𝑃 ∥ 2 ↔ 𝑃 = 2)) |
| 31 | 28, 29, 30 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∥ 2 ↔
𝑃 = 2)) |
| 32 | 26, 31 | mtbird 325 |
. . . . . . . . . 10
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ¬ 𝑃 ∥
2) |
| 33 | 32 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ ((𝑃
− 1) / 2)) → ¬ 𝑃 ∥ 2) |
| 34 | | 1cnd 11256 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ ((𝑃
− 1) / 2)) → 1 ∈ ℂ) |
| 35 | 2 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ ((𝑃
− 1) / 2)) → ((𝑃
− 1) / 2) ∈ ℕ) |
| 36 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ ((𝑃
− 1) / 2)) → ¬ 2 ∥ ((𝑃 − 1) / 2)) |
| 37 | | oexpneg 16382 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ ((𝑃
− 1) / 2) ∈ ℕ ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) =
-(1↑((𝑃 − 1) /
2))) |
| 38 | 34, 35, 36, 37 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ ((𝑃
− 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -(1↑((𝑃 − 1) /
2))) |
| 39 | 35 | nnzd 12640 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ ((𝑃
− 1) / 2)) → ((𝑃
− 1) / 2) ∈ ℤ) |
| 40 | | 1exp 14132 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 − 1) / 2) ∈ ℤ
→ (1↑((𝑃 −
1) / 2)) = 1) |
| 41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ ((𝑃
− 1) / 2)) → (1↑((𝑃 − 1) / 2)) = 1) |
| 42 | 41 | negeqd 11502 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ ((𝑃
− 1) / 2)) → -(1↑((𝑃 − 1) / 2)) = -1) |
| 43 | 38, 42 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ ((𝑃
− 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -1) |
| 44 | 43 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ ((𝑃
− 1) / 2)) → ((-1↑((𝑃 − 1) / 2)) + 1) = (-1 +
1)) |
| 45 | | ax-1cn 11213 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
| 46 | | neg1cn 12380 |
. . . . . . . . . . . . . 14
⊢ -1 ∈
ℂ |
| 47 | | 1pneg1e0 12385 |
. . . . . . . . . . . . . 14
⊢ (1 + -1)
= 0 |
| 48 | 45, 46, 47 | addcomli 11453 |
. . . . . . . . . . . . 13
⊢ (-1 + 1)
= 0 |
| 49 | 44, 48 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ ((𝑃
− 1) / 2)) → ((-1↑((𝑃 − 1) / 2)) + 1) = 0) |
| 50 | 49 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ ((𝑃
− 1) / 2)) → (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) = (2 −
0)) |
| 51 | | 2cn 12341 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
| 52 | 51 | subid1i 11581 |
. . . . . . . . . . 11
⊢ (2
− 0) = 2 |
| 53 | 50, 52 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ ((𝑃
− 1) / 2)) → (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) =
2) |
| 54 | 53 | breq2d 5155 |
. . . . . . . . 9
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ ((𝑃
− 1) / 2)) → (𝑃
∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) ↔ 𝑃 ∥ 2)) |
| 55 | 33, 54 | mtbird 325 |
. . . . . . . 8
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ ((𝑃
− 1) / 2)) → ¬ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) +
1))) |
| 56 | 55 | ex 412 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (¬ 2 ∥ ((𝑃
− 1) / 2) → ¬ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) +
1)))) |
| 57 | 56 | con4d 115 |
. . . . . 6
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∥ (2
− ((-1↑((𝑃
− 1) / 2)) + 1)) → 2 ∥ ((𝑃 − 1) / 2))) |
| 58 | | 2z 12649 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
| 59 | 58 | a1i 11 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 2 ∈ ℤ) |
| 60 | | moddvds 16301 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ 2 ∈
ℤ ∧ ((-1↑((𝑃
− 1) / 2)) + 1) ∈ ℤ) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) +
1)))) |
| 61 | 9, 59, 6, 60 | syl3anc 1373 |
. . . . . 6
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((2 mod 𝑃) =
(((-1↑((𝑃 − 1) /
2)) + 1) mod 𝑃) ↔
𝑃 ∥ (2 −
((-1↑((𝑃 − 1) /
2)) + 1)))) |
| 62 | | 4z 12651 |
. . . . . . . . 9
⊢ 4 ∈
ℤ |
| 63 | | 4ne0 12374 |
. . . . . . . . 9
⊢ 4 ≠
0 |
| 64 | | nnm1nn0 12567 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
| 65 | 9, 64 | syl 17 |
. . . . . . . . . 10
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 − 1) ∈
ℕ0) |
| 66 | 65 | nn0zd 12639 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 − 1) ∈
ℤ) |
| 67 | | dvdsval2 16293 |
. . . . . . . . 9
⊢ ((4
∈ ℤ ∧ 4 ≠ 0 ∧ (𝑃 − 1) ∈ ℤ) → (4
∥ (𝑃 − 1)
↔ ((𝑃 − 1) / 4)
∈ ℤ)) |
| 68 | 62, 63, 66, 67 | mp3an12i 1467 |
. . . . . . . 8
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (4 ∥ (𝑃
− 1) ↔ ((𝑃
− 1) / 4) ∈ ℤ)) |
| 69 | 65 | nn0cnd 12589 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 − 1) ∈
ℂ) |
| 70 | 51 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 2 ∈ ℂ) |
| 71 | | 2ne0 12370 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
| 72 | 71 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 2 ≠ 0) |
| 73 | 69, 70, 70, 72, 72 | divdiv1d 12074 |
. . . . . . . . . 10
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (((𝑃 − 1) / 2)
/ 2) = ((𝑃 − 1) / (2
· 2))) |
| 74 | | 2t2e4 12430 |
. . . . . . . . . . 11
⊢ (2
· 2) = 4 |
| 75 | 74 | oveq2i 7442 |
. . . . . . . . . 10
⊢ ((𝑃 − 1) / (2 · 2)) =
((𝑃 − 1) /
4) |
| 76 | 73, 75 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (((𝑃 − 1) / 2)
/ 2) = ((𝑃 − 1) /
4)) |
| 77 | 76 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((((𝑃 − 1) /
2) / 2) ∈ ℤ ↔ ((𝑃 − 1) / 4) ∈
ℤ)) |
| 78 | 68, 77 | bitr4d 282 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (4 ∥ (𝑃
− 1) ↔ (((𝑃
− 1) / 2) / 2) ∈ ℤ)) |
| 79 | 2 | nnzd 12640 |
. . . . . . . 8
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℤ) |
| 80 | | dvdsval2 16293 |
. . . . . . . 8
⊢ ((2
∈ ℤ ∧ 2 ≠ 0 ∧ ((𝑃 − 1) / 2) ∈ ℤ) → (2
∥ ((𝑃 − 1) / 2)
↔ (((𝑃 − 1) / 2)
/ 2) ∈ ℤ)) |
| 81 | 58, 71, 79, 80 | mp3an12i 1467 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (2 ∥ ((𝑃
− 1) / 2) ↔ (((𝑃
− 1) / 2) / 2) ∈ ℤ)) |
| 82 | 78, 81 | bitr4d 282 |
. . . . . 6
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (4 ∥ (𝑃
− 1) ↔ 2 ∥ ((𝑃 − 1) / 2))) |
| 83 | 57, 61, 82 | 3imtr4d 294 |
. . . . 5
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((2 mod 𝑃) =
(((-1↑((𝑃 − 1) /
2)) + 1) mod 𝑃) → 4
∥ (𝑃 −
1))) |
| 84 | 46 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 4 ∥ (𝑃 −
1)) → -1 ∈ ℂ) |
| 85 | | neg1ne0 12382 |
. . . . . . . . . . . 12
⊢ -1 ≠
0 |
| 86 | 85 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 4 ∥ (𝑃 −
1)) → -1 ≠ 0) |
| 87 | 58 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 4 ∥ (𝑃 −
1)) → 2 ∈ ℤ) |
| 88 | 78 | biimpa 476 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 4 ∥ (𝑃 −
1)) → (((𝑃 − 1)
/ 2) / 2) ∈ ℤ) |
| 89 | | expmulz 14149 |
. . . . . . . . . . 11
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ (((𝑃 − 1) / 2) / 2) ∈
ℤ)) → (-1↑(2 · (((𝑃 − 1) / 2) / 2))) =
((-1↑2)↑(((𝑃
− 1) / 2) / 2))) |
| 90 | 84, 86, 87, 88, 89 | syl22anc 839 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 4 ∥ (𝑃 −
1)) → (-1↑(2 · (((𝑃 − 1) / 2) / 2))) =
((-1↑2)↑(((𝑃
− 1) / 2) / 2))) |
| 91 | 2 | nncnd 12282 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℂ) |
| 92 | 91, 70, 72 | divcan2d 12045 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (2 · (((𝑃
− 1) / 2) / 2)) = ((𝑃
− 1) / 2)) |
| 93 | 92 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 4 ∥ (𝑃 −
1)) → (2 · (((𝑃
− 1) / 2) / 2)) = ((𝑃
− 1) / 2)) |
| 94 | 93 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 4 ∥ (𝑃 −
1)) → (-1↑(2 · (((𝑃 − 1) / 2) / 2))) = (-1↑((𝑃 − 1) /
2))) |
| 95 | | neg1sqe1 14235 |
. . . . . . . . . . . 12
⊢
(-1↑2) = 1 |
| 96 | 95 | oveq1i 7441 |
. . . . . . . . . . 11
⊢
((-1↑2)↑(((𝑃 − 1) / 2) / 2)) = (1↑(((𝑃 − 1) / 2) /
2)) |
| 97 | | 1exp 14132 |
. . . . . . . . . . . 12
⊢ ((((𝑃 − 1) / 2) / 2) ∈
ℤ → (1↑(((𝑃
− 1) / 2) / 2)) = 1) |
| 98 | 88, 97 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 4 ∥ (𝑃 −
1)) → (1↑(((𝑃
− 1) / 2) / 2)) = 1) |
| 99 | 96, 98 | eqtrid 2789 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 4 ∥ (𝑃 −
1)) → ((-1↑2)↑(((𝑃 − 1) / 2) / 2)) = 1) |
| 100 | 90, 94, 99 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 4 ∥ (𝑃 −
1)) → (-1↑((𝑃
− 1) / 2)) = 1) |
| 101 | 100 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 4 ∥ (𝑃 −
1)) → ((-1↑((𝑃
− 1) / 2)) + 1) = (1 + 1)) |
| 102 | 22, 101 | eqtr4id 2796 |
. . . . . . 7
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 4 ∥ (𝑃 −
1)) → 2 = ((-1↑((𝑃 − 1) / 2)) + 1)) |
| 103 | 102 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 4 ∥ (𝑃 −
1)) → (2 mod 𝑃) =
(((-1↑((𝑃 − 1) /
2)) + 1) mod 𝑃)) |
| 104 | 103 | ex 412 |
. . . . 5
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (4 ∥ (𝑃
− 1) → (2 mod 𝑃)
= (((-1↑((𝑃 − 1)
/ 2)) + 1) mod 𝑃))) |
| 105 | 83, 104 | impbid 212 |
. . . 4
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((2 mod 𝑃) =
(((-1↑((𝑃 − 1) /
2)) + 1) mod 𝑃) ↔ 4
∥ (𝑃 −
1))) |
| 106 | 13, 24, 105 | 3bitr2d 307 |
. . 3
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (((((-1↑((𝑃
− 1) / 2)) + 1) mod 𝑃) − 1) = 1 ↔ 4 ∥ (𝑃 − 1))) |
| 107 | | lgsval3 27359 |
. . . . 5
⊢ ((-1
∈ ℤ ∧ 𝑃
∈ (ℙ ∖ {2})) → (-1 /L 𝑃) = ((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1)) |
| 108 | 1, 107 | mpan 690 |
. . . 4
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (-1 /L 𝑃) = ((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1)) |
| 109 | 108 | eqeq1d 2739 |
. . 3
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((-1 /L 𝑃) = 1 ↔ ((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1)) |
| 110 | | 4nn 12349 |
. . . . 5
⊢ 4 ∈
ℕ |
| 111 | 110 | a1i 11 |
. . . 4
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 4 ∈ ℕ) |
| 112 | | prmz 16712 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
| 113 | 7, 112 | syl 17 |
. . . 4
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℤ) |
| 114 | | 1zzd 12648 |
. . . 4
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 1 ∈ ℤ) |
| 115 | | moddvds 16301 |
. . . 4
⊢ ((4
∈ ℕ ∧ 𝑃
∈ ℤ ∧ 1 ∈ ℤ) → ((𝑃 mod 4) = (1 mod 4) ↔ 4 ∥ (𝑃 − 1))) |
| 116 | 111, 113,
114, 115 | syl3anc 1373 |
. . 3
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 mod 4) = (1 mod
4) ↔ 4 ∥ (𝑃
− 1))) |
| 117 | 106, 109,
116 | 3bitr4d 311 |
. 2
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((-1 /L 𝑃) = 1 ↔ (𝑃 mod 4) = (1 mod 4))) |
| 118 | | 1re 11261 |
. . . 4
⊢ 1 ∈
ℝ |
| 119 | | nnrp 13046 |
. . . . 5
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
| 120 | 110, 119 | ax-mp 5 |
. . . 4
⊢ 4 ∈
ℝ+ |
| 121 | | 0le1 11786 |
. . . 4
⊢ 0 ≤
1 |
| 122 | | 1lt4 12442 |
. . . 4
⊢ 1 <
4 |
| 123 | | modid 13936 |
. . . 4
⊢ (((1
∈ ℝ ∧ 4 ∈ ℝ+) ∧ (0 ≤ 1 ∧ 1 <
4)) → (1 mod 4) = 1) |
| 124 | 118, 120,
121, 122, 123 | mp4an 693 |
. . 3
⊢ (1 mod 4)
= 1 |
| 125 | 124 | eqeq2i 2750 |
. 2
⊢ ((𝑃 mod 4) = (1 mod 4) ↔
(𝑃 mod 4) =
1) |
| 126 | 117, 125 | bitrdi 287 |
1
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((-1 /L 𝑃) = 1 ↔ (𝑃 mod 4) = 1)) |