Proof of Theorem lgsvalmod
| Step | Hyp | Ref
| Expression |
| 1 | | eldifi 4131 |
. . . . . . . 8
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
| 2 | 1 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 𝑃 ∈
ℙ) |
| 3 | | prmz 16712 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
| 4 | 2, 3 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 𝑃 ∈
ℤ) |
| 5 | | lgscl 27355 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝐴 /L 𝑃) ∈
ℤ) |
| 6 | 4, 5 | syldan 591 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝐴
/L 𝑃)
∈ ℤ) |
| 7 | 6 | zred 12722 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝐴
/L 𝑃)
∈ ℝ) |
| 8 | | peano2re 11434 |
. . . 4
⊢ ((𝐴 /L 𝑃) ∈ ℝ → ((𝐴 /L 𝑃) + 1) ∈
ℝ) |
| 9 | 7, 8 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴
/L 𝑃) +
1) ∈ ℝ) |
| 10 | | oddprm 16848 |
. . . . . . . 8
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
| 11 | 10 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝑃 − 1) / 2)
∈ ℕ) |
| 12 | 11 | nnnn0d 12587 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝑃 − 1) / 2)
∈ ℕ0) |
| 13 | | zexpcl 14117 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈
ℕ0) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℤ) |
| 14 | 12, 13 | syldan 591 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝐴↑((𝑃 − 1) / 2)) ∈
ℤ) |
| 15 | 14 | zred 12722 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝐴↑((𝑃 − 1) / 2)) ∈
ℝ) |
| 16 | | peano2re 11434 |
. . . 4
⊢ ((𝐴↑((𝑃 − 1) / 2)) ∈ ℝ →
((𝐴↑((𝑃 − 1) / 2)) + 1) ∈
ℝ) |
| 17 | 15, 16 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈
ℝ) |
| 18 | | neg1rr 12381 |
. . . 4
⊢ -1 ∈
ℝ |
| 19 | 18 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ -1 ∈ ℝ) |
| 20 | | prmnn 16711 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 21 | 2, 20 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 𝑃 ∈
ℕ) |
| 22 | 21 | nnrpd 13075 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 𝑃 ∈
ℝ+) |
| 23 | | lgsval3 27359 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝐴
/L 𝑃) =
((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1)) |
| 24 | 23 | eqcomd 2743 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = (𝐴 /L 𝑃)) |
| 25 | 17, 22 | modcld 13915 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈
ℝ) |
| 26 | 25 | recnd 11289 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈
ℂ) |
| 27 | | ax-1cn 11213 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
| 28 | 27 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 1 ∈ ℂ) |
| 29 | 7 | recnd 11289 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝐴
/L 𝑃)
∈ ℂ) |
| 30 | 26, 28, 29 | subadd2d 11639 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = (𝐴 /L 𝑃) ↔ ((𝐴 /L 𝑃) + 1) = (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃))) |
| 31 | 24, 30 | mpbid 232 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴
/L 𝑃) +
1) = (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃)) |
| 32 | 31 | oveq1d 7446 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((𝐴
/L 𝑃) +
1) mod 𝑃) = ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) mod 𝑃)) |
| 33 | | modabs2 13945 |
. . . . 5
⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℝ ∧
𝑃 ∈
ℝ+) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) mod 𝑃) = (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃)) |
| 34 | 17, 22, 33 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) mod 𝑃) = (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃)) |
| 35 | 32, 34 | eqtrd 2777 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((𝐴
/L 𝑃) +
1) mod 𝑃) = (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃)) |
| 36 | | modadd1 13948 |
. . 3
⊢
(((((𝐴
/L 𝑃) +
1) ∈ ℝ ∧ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℝ) ∧
(-1 ∈ ℝ ∧ 𝑃
∈ ℝ+) ∧ (((𝐴 /L 𝑃) + 1) mod 𝑃) = (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃)) → ((((𝐴 /L 𝑃) + 1) + -1) mod 𝑃) = ((((𝐴↑((𝑃 − 1) / 2)) + 1) + -1) mod 𝑃)) |
| 37 | 9, 17, 19, 22, 35, 36 | syl221anc 1383 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((((𝐴
/L 𝑃) +
1) + -1) mod 𝑃) = ((((𝐴↑((𝑃 − 1) / 2)) + 1) + -1) mod 𝑃)) |
| 38 | 9 | recnd 11289 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴
/L 𝑃) +
1) ∈ ℂ) |
| 39 | | negsub 11557 |
. . . . 5
⊢ ((((𝐴 /L 𝑃) + 1) ∈ ℂ ∧ 1
∈ ℂ) → (((𝐴
/L 𝑃) +
1) + -1) = (((𝐴
/L 𝑃) +
1) − 1)) |
| 40 | 38, 27, 39 | sylancl 586 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((𝐴
/L 𝑃) +
1) + -1) = (((𝐴
/L 𝑃) +
1) − 1)) |
| 41 | | pncan 11514 |
. . . . 5
⊢ (((𝐴 /L 𝑃) ∈ ℂ ∧ 1 ∈
ℂ) → (((𝐴
/L 𝑃) +
1) − 1) = (𝐴
/L 𝑃)) |
| 42 | 29, 27, 41 | sylancl 586 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((𝐴
/L 𝑃) +
1) − 1) = (𝐴
/L 𝑃)) |
| 43 | 40, 42 | eqtrd 2777 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((𝐴
/L 𝑃) +
1) + -1) = (𝐴
/L 𝑃)) |
| 44 | 43 | oveq1d 7446 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((((𝐴
/L 𝑃) +
1) + -1) mod 𝑃) = ((𝐴 /L 𝑃) mod 𝑃)) |
| 45 | 17 | recnd 11289 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈
ℂ) |
| 46 | | negsub 11557 |
. . . . 5
⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℂ ∧
1 ∈ ℂ) → (((𝐴↑((𝑃 − 1) / 2)) + 1) + -1) = (((𝐴↑((𝑃 − 1) / 2)) + 1) −
1)) |
| 47 | 45, 27, 46 | sylancl 586 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((𝐴↑((𝑃 − 1) / 2)) + 1) + -1) =
(((𝐴↑((𝑃 − 1) / 2)) + 1) −
1)) |
| 48 | 15 | recnd 11289 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝐴↑((𝑃 − 1) / 2)) ∈
ℂ) |
| 49 | | pncan 11514 |
. . . . 5
⊢ (((𝐴↑((𝑃 − 1) / 2)) ∈ ℂ ∧ 1
∈ ℂ) → (((𝐴↑((𝑃 − 1) / 2)) + 1) − 1) = (𝐴↑((𝑃 − 1) / 2))) |
| 50 | 48, 27, 49 | sylancl 586 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((𝐴↑((𝑃 − 1) / 2)) + 1) −
1) = (𝐴↑((𝑃 − 1) /
2))) |
| 51 | 47, 50 | eqtrd 2777 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((𝐴↑((𝑃 − 1) / 2)) + 1) + -1) =
(𝐴↑((𝑃 − 1) / 2))) |
| 52 | 51 | oveq1d 7446 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((((𝐴↑((𝑃 − 1) / 2)) + 1) + -1) mod
𝑃) = ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃)) |
| 53 | 37, 44, 52 | 3eqtr3d 2785 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴
/L 𝑃) mod
𝑃) = ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃)) |