Step | Hyp | Ref
| Expression |
1 | | simpl1 1064 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → 𝐴 ∈ ℤ) |
2 | | simpl2 1065 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → 𝐵 ∈ ℤ) |
3 | | lgsdir2 25055 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 · 𝐵) /L 2) = ((𝐴 /L 2)
· (𝐵
/L 2))) |
4 | 1, 2, 3 | syl2anc 693 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → ((𝐴 · 𝐵) /L 2) = ((𝐴 /L 2)
· (𝐵
/L 2))) |
5 | | simpr 477 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → 𝑃 = 2) |
6 | 5 | oveq2d 6666 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → ((𝐴 · 𝐵) /L 𝑃) = ((𝐴 · 𝐵) /L 2)) |
7 | 5 | oveq2d 6666 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → (𝐴 /L 𝑃) = (𝐴 /L 2)) |
8 | 5 | oveq2d 6666 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → (𝐵 /L 𝑃) = (𝐵 /L 2)) |
9 | 7, 8 | oveq12d 6668 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) = ((𝐴 /L 2) · (𝐵 /L
2))) |
10 | 4, 6, 9 | 3eqtr4d 2666 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → ((𝐴 · 𝐵) /L 𝑃) = ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) |
11 | | simpl1 1064 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝐴 ∈
ℤ) |
12 | | simpl2 1065 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝐵 ∈
ℤ) |
13 | 11, 12 | zmulcld 11488 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐴 · 𝐵) ∈ ℤ) |
14 | | simpl3 1066 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∈
ℙ) |
15 | | prmz 15389 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
16 | 14, 15 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∈
ℤ) |
17 | | lgscl 25036 |
. . . . 5
⊢ (((𝐴 · 𝐵) ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝐴 · 𝐵) /L 𝑃) ∈ ℤ) |
18 | 13, 16, 17 | syl2anc 693 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 · 𝐵) /L 𝑃) ∈ ℤ) |
19 | 18 | zcnd 11483 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 · 𝐵) /L 𝑃) ∈ ℂ) |
20 | | lgscl 25036 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝐴 /L 𝑃) ∈
ℤ) |
21 | 11, 16, 20 | syl2anc 693 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐴 /L 𝑃) ∈
ℤ) |
22 | | lgscl 25036 |
. . . . . 6
⊢ ((𝐵 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝐵 /L 𝑃) ∈
ℤ) |
23 | 12, 16, 22 | syl2anc 693 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐵 /L 𝑃) ∈
ℤ) |
24 | 21, 23 | zmulcld 11488 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ ℤ) |
25 | 24 | zcnd 11483 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ ℂ) |
26 | 19, 25 | subcld 10392 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ∈ ℂ) |
27 | 26 | abscld 14175 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
(abs‘(((𝐴 ·
𝐵) /L
𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ∈ ℝ) |
28 | | prmnn 15388 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
29 | 14, 28 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∈
ℕ) |
30 | 29 | nnrpd 11870 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∈
ℝ+) |
31 | 26 | absge0d 14183 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 0 ≤
(abs‘(((𝐴 ·
𝐵) /L
𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))))) |
32 | | 2re 11090 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
33 | 32 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 2 ∈
ℝ) |
34 | 29 | nnred 11035 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∈
ℝ) |
35 | 19 | abscld 14175 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
(abs‘((𝐴 ·
𝐵) /L
𝑃)) ∈
ℝ) |
36 | 25 | abscld 14175 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
(abs‘((𝐴
/L 𝑃)
· (𝐵
/L 𝑃)))
∈ ℝ) |
37 | 35, 36 | readdcld 10069 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
((abs‘((𝐴 ·
𝐵) /L
𝑃)) + (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ∈ ℝ) |
38 | 19, 25 | abs2dif2d 14197 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
(abs‘(((𝐴 ·
𝐵) /L
𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ≤ ((abs‘((𝐴 · 𝐵) /L 𝑃)) + (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃))))) |
39 | | 1red 10055 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 1 ∈
ℝ) |
40 | | lgsle1 25037 |
. . . . . . . . . . 11
⊢ (((𝐴 · 𝐵) ∈ ℤ ∧ 𝑃 ∈ ℤ) → (abs‘((𝐴 · 𝐵) /L 𝑃)) ≤ 1) |
41 | 13, 16, 40 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
(abs‘((𝐴 ·
𝐵) /L
𝑃)) ≤
1) |
42 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ {𝑥 ∈ ℤ ∣
(abs‘𝑥) ≤ 1} =
{𝑥 ∈ ℤ ∣
(abs‘𝑥) ≤
1} |
43 | 42 | lgscl2 25034 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝐴 /L 𝑃) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}) |
44 | 11, 16, 43 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐴 /L 𝑃) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}) |
45 | 42 | lgscl2 25034 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝐵 /L 𝑃) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}) |
46 | 12, 16, 45 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐵 /L 𝑃) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}) |
47 | 42 | lgslem3 25024 |
. . . . . . . . . . . 12
⊢ (((𝐴 /L 𝑃) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} ∧ (𝐵 /L 𝑃) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}) → ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}) |
48 | 44, 46, 47 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}) |
49 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) → (abs‘𝑥) = (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) |
50 | 49 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) → ((abs‘𝑥) ≤ 1 ↔ (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ≤ 1)) |
51 | 50 | elrab 3363 |
. . . . . . . . . . . 12
⊢ (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} ↔ (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ ℤ ∧ (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ≤ 1)) |
52 | 51 | simprbi 480 |
. . . . . . . . . . 11
⊢ (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} →
(abs‘((𝐴
/L 𝑃)
· (𝐵
/L 𝑃)))
≤ 1) |
53 | 48, 52 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
(abs‘((𝐴
/L 𝑃)
· (𝐵
/L 𝑃)))
≤ 1) |
54 | 35, 36, 39, 39, 41, 53 | le2addd 10646 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
((abs‘((𝐴 ·
𝐵) /L
𝑃)) + (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ≤ (1 + 1)) |
55 | | df-2 11079 |
. . . . . . . . 9
⊢ 2 = (1 +
1) |
56 | 54, 55 | syl6breqr 4695 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
((abs‘((𝐴 ·
𝐵) /L
𝑃)) + (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ≤ 2) |
57 | 27, 37, 33, 38, 56 | letrd 10194 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
(abs‘(((𝐴 ·
𝐵) /L
𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ≤ 2) |
58 | | prmuz2 15408 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
59 | | eluzle 11700 |
. . . . . . . . 9
⊢ (𝑃 ∈
(ℤ≥‘2) → 2 ≤ 𝑃) |
60 | 14, 58, 59 | 3syl 18 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 2 ≤ 𝑃) |
61 | | simpr 477 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ≠ 2) |
62 | | ltlen 10138 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ 𝑃
∈ ℝ) → (2 < 𝑃 ↔ (2 ≤ 𝑃 ∧ 𝑃 ≠ 2))) |
63 | 32, 34, 62 | sylancr 695 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (2 < 𝑃 ↔ (2 ≤ 𝑃 ∧ 𝑃 ≠ 2))) |
64 | 60, 61, 63 | mpbir2and 957 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 2 < 𝑃) |
65 | 27, 33, 34, 57, 64 | lelttrd 10195 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
(abs‘(((𝐴 ·
𝐵) /L
𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) < 𝑃) |
66 | | modid 12695 |
. . . . . 6
⊢
((((abs‘(((𝐴
· 𝐵)
/L 𝑃)
− ((𝐴
/L 𝑃)
· (𝐵
/L 𝑃))))
∈ ℝ ∧ 𝑃
∈ ℝ+) ∧ (0 ≤ (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ∧ (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) < 𝑃)) → ((abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) mod 𝑃) = (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))))) |
67 | 27, 30, 31, 65, 66 | syl22anc 1327 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
((abs‘(((𝐴 ·
𝐵) /L
𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) mod 𝑃) = (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))))) |
68 | 11 | zcnd 11483 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝐴 ∈
ℂ) |
69 | 12 | zcnd 11483 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝐵 ∈
ℂ) |
70 | | eldifsn 4317 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ (ℙ ∖ {2})
↔ (𝑃 ∈ ℙ
∧ 𝑃 ≠
2)) |
71 | 14, 61, 70 | sylanbrc 698 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∈ (ℙ ∖
{2})) |
72 | | oddprm 15515 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝑃 − 1) / 2) ∈
ℕ) |
74 | 73 | nnnn0d 11351 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝑃 − 1) / 2) ∈
ℕ0) |
75 | 68, 69, 74 | mulexpd 13023 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 · 𝐵)↑((𝑃 − 1) / 2)) = ((𝐴↑((𝑃 − 1) / 2)) · (𝐵↑((𝑃 − 1) / 2)))) |
76 | | zexpcl 12875 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈
ℕ0) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℤ) |
77 | 11, 74, 76 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℤ) |
78 | 77 | zcnd 11483 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℂ) |
79 | | zexpcl 12875 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈
ℕ0) → (𝐵↑((𝑃 − 1) / 2)) ∈
ℤ) |
80 | 12, 74, 79 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐵↑((𝑃 − 1) / 2)) ∈
ℤ) |
81 | 80 | zcnd 11483 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐵↑((𝑃 − 1) / 2)) ∈
ℂ) |
82 | 78, 81 | mulcomd 10061 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴↑((𝑃 − 1) / 2)) · (𝐵↑((𝑃 − 1) / 2))) = ((𝐵↑((𝑃 − 1) / 2)) · (𝐴↑((𝑃 − 1) / 2)))) |
83 | 75, 82 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 · 𝐵)↑((𝑃 − 1) / 2)) = ((𝐵↑((𝑃 − 1) / 2)) · (𝐴↑((𝑃 − 1) / 2)))) |
84 | 83 | oveq1d 6665 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 · 𝐵)↑((𝑃 − 1) / 2)) mod 𝑃) = (((𝐵↑((𝑃 − 1) / 2)) · (𝐴↑((𝑃 − 1) / 2))) mod 𝑃)) |
85 | | lgsvalmod 25041 |
. . . . . . . . . 10
⊢ (((𝐴 · 𝐵) ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) →
(((𝐴 · 𝐵) /L 𝑃) mod 𝑃) = (((𝐴 · 𝐵)↑((𝑃 − 1) / 2)) mod 𝑃)) |
86 | 13, 71, 85 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 · 𝐵) /L 𝑃) mod 𝑃) = (((𝐴 · 𝐵)↑((𝑃 − 1) / 2)) mod 𝑃)) |
87 | 21 | zred 11482 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐴 /L 𝑃) ∈
ℝ) |
88 | 77 | zred 11482 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℝ) |
89 | | lgsvalmod 25041 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴
/L 𝑃) mod
𝑃) = ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃)) |
90 | 11, 71, 89 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 /L 𝑃) mod 𝑃) = ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃)) |
91 | | modmul1 12723 |
. . . . . . . . . . 11
⊢ ((((𝐴 /L 𝑃) ∈ ℝ ∧ (𝐴↑((𝑃 − 1) / 2)) ∈ ℝ) ∧
((𝐵 /L
𝑃) ∈ ℤ ∧
𝑃 ∈
ℝ+) ∧ ((𝐴 /L 𝑃) mod 𝑃) = ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃)) → (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) mod 𝑃) = (((𝐴↑((𝑃 − 1) / 2)) · (𝐵 /L 𝑃)) mod 𝑃)) |
92 | 87, 88, 23, 30, 90, 91 | syl221anc 1337 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) mod 𝑃) = (((𝐴↑((𝑃 − 1) / 2)) · (𝐵 /L 𝑃)) mod 𝑃)) |
93 | 23 | zcnd 11483 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐵 /L 𝑃) ∈
ℂ) |
94 | 78, 93 | mulcomd 10061 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴↑((𝑃 − 1) / 2)) · (𝐵 /L 𝑃)) = ((𝐵 /L 𝑃) · (𝐴↑((𝑃 − 1) / 2)))) |
95 | 94 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴↑((𝑃 − 1) / 2)) · (𝐵 /L 𝑃)) mod 𝑃) = (((𝐵 /L 𝑃) · (𝐴↑((𝑃 − 1) / 2))) mod 𝑃)) |
96 | 23 | zred 11482 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐵 /L 𝑃) ∈
ℝ) |
97 | 80 | zred 11482 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐵↑((𝑃 − 1) / 2)) ∈
ℝ) |
98 | | lgsvalmod 25041 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐵
/L 𝑃) mod
𝑃) = ((𝐵↑((𝑃 − 1) / 2)) mod 𝑃)) |
99 | 12, 71, 98 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐵 /L 𝑃) mod 𝑃) = ((𝐵↑((𝑃 − 1) / 2)) mod 𝑃)) |
100 | | modmul1 12723 |
. . . . . . . . . . . 12
⊢ ((((𝐵 /L 𝑃) ∈ ℝ ∧ (𝐵↑((𝑃 − 1) / 2)) ∈ ℝ) ∧
((𝐴↑((𝑃 − 1) / 2)) ∈ ℤ
∧ 𝑃 ∈
ℝ+) ∧ ((𝐵 /L 𝑃) mod 𝑃) = ((𝐵↑((𝑃 − 1) / 2)) mod 𝑃)) → (((𝐵 /L 𝑃) · (𝐴↑((𝑃 − 1) / 2))) mod 𝑃) = (((𝐵↑((𝑃 − 1) / 2)) · (𝐴↑((𝑃 − 1) / 2))) mod 𝑃)) |
101 | 96, 97, 77, 30, 99, 100 | syl221anc 1337 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐵 /L 𝑃) · (𝐴↑((𝑃 − 1) / 2))) mod 𝑃) = (((𝐵↑((𝑃 − 1) / 2)) · (𝐴↑((𝑃 − 1) / 2))) mod 𝑃)) |
102 | 95, 101 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴↑((𝑃 − 1) / 2)) · (𝐵 /L 𝑃)) mod 𝑃) = (((𝐵↑((𝑃 − 1) / 2)) · (𝐴↑((𝑃 − 1) / 2))) mod 𝑃)) |
103 | 92, 102 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) mod 𝑃) = (((𝐵↑((𝑃 − 1) / 2)) · (𝐴↑((𝑃 − 1) / 2))) mod 𝑃)) |
104 | 84, 86, 103 | 3eqtr4d 2666 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 · 𝐵) /L 𝑃) mod 𝑃) = (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) mod 𝑃)) |
105 | | moddvds 14991 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℕ ∧ ((𝐴 · 𝐵) /L 𝑃) ∈ ℤ ∧ ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ ℤ) → ((((𝐴 · 𝐵) /L 𝑃) mod 𝑃) = (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) mod 𝑃) ↔ 𝑃 ∥ (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))))) |
106 | 29, 18, 24, 105 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((((𝐴 · 𝐵) /L 𝑃) mod 𝑃) = (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) mod 𝑃) ↔ 𝑃 ∥ (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))))) |
107 | 104, 106 | mpbid 222 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∥ (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) |
108 | 18, 24 | zsubcld 11487 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ∈ ℤ) |
109 | | dvdsabsb 15001 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ∈ ℤ) → (𝑃 ∥ (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ↔ 𝑃 ∥ (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))))) |
110 | 16, 108, 109 | syl2anc 693 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝑃 ∥ (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ↔ 𝑃 ∥ (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))))) |
111 | 107, 110 | mpbid 222 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∥ (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))))) |
112 | | nn0abscl 14052 |
. . . . . . . . 9
⊢ ((((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ∈ ℤ →
(abs‘(((𝐴 ·
𝐵) /L
𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ∈
ℕ0) |
113 | 108, 112 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
(abs‘(((𝐴 ·
𝐵) /L
𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ∈
ℕ0) |
114 | 113 | nn0zd 11480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
(abs‘(((𝐴 ·
𝐵) /L
𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ∈ ℤ) |
115 | | dvdsval3 14987 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧
(abs‘(((𝐴 ·
𝐵) /L
𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ∈ ℤ) → (𝑃 ∥ (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ↔ ((abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) mod 𝑃) = 0)) |
116 | 29, 114, 115 | syl2anc 693 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝑃 ∥ (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ↔ ((abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) mod 𝑃) = 0)) |
117 | 111, 116 | mpbid 222 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
((abs‘(((𝐴 ·
𝐵) /L
𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) mod 𝑃) = 0) |
118 | 67, 117 | eqtr3d 2658 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) →
(abs‘(((𝐴 ·
𝐵) /L
𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) = 0) |
119 | 26, 118 | abs00d 14185 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) = 0) |
120 | 19, 25, 119 | subeq0d 10400 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 · 𝐵) /L 𝑃) = ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) |
121 | 10, 120 | pm2.61dane 2881 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ((𝐴 · 𝐵) /L 𝑃) = ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) |