Proof of Theorem lgslem4
Step | Hyp | Ref
| Expression |
1 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → 𝐴 ∈ ℤ) |
2 | | oddprm 15353 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
3 | 2 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → ((𝑃 − 1) / 2) ∈
ℕ) |
4 | 3 | nnnn0d 11228 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → ((𝑃 − 1) / 2) ∈
ℕ0) |
5 | | zexpcl 12737 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈
ℕ0) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℤ) |
6 | 1, 4, 5 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℤ) |
7 | 6 | zred 11358 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℝ) |
8 | | 0red 9920 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → 0 ∈
ℝ) |
9 | | 1red 9934 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → 1 ∈
ℝ) |
10 | | eldifi 3694 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
11 | 10 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℙ) |
12 | | prmuz2 15246 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → 𝑃 ∈
(ℤ≥‘2)) |
14 | | eluz2b2 11637 |
. . . . . . . . . 10
⊢ (𝑃 ∈
(ℤ≥‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃)) |
15 | 13, 14 | sylib 207 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → (𝑃 ∈ ℕ ∧ 1 < 𝑃)) |
16 | 15 | simpld 474 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℕ) |
17 | 16 | nnrpd 11746 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → 𝑃 ∈
ℝ+) |
18 | | 0zd 11266 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → 0 ∈
ℤ) |
19 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → 𝑃 ∥ 𝐴) |
20 | | dvdsval3 14825 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ) → (𝑃 ∥ 𝐴 ↔ (𝐴 mod 𝑃) = 0)) |
21 | 16, 1, 20 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → (𝑃 ∥ 𝐴 ↔ (𝐴 mod 𝑃) = 0)) |
22 | 19, 21 | mpbid 221 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → (𝐴 mod 𝑃) = 0) |
23 | | 0mod 12563 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℝ+
→ (0 mod 𝑃) =
0) |
24 | 17, 23 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → (0 mod 𝑃) = 0) |
25 | 22, 24 | eqtr4d 2647 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → (𝐴 mod 𝑃) = (0 mod 𝑃)) |
26 | | modexp 12861 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 0 ∈
ℤ) ∧ (((𝑃 −
1) / 2) ∈ ℕ0 ∧ 𝑃 ∈ ℝ+) ∧ (𝐴 mod 𝑃) = (0 mod 𝑃)) → ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃) = ((0↑((𝑃 − 1) / 2)) mod 𝑃)) |
27 | 1, 18, 4, 17, 25, 26 | syl221anc 1329 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃) = ((0↑((𝑃 − 1) / 2)) mod 𝑃)) |
28 | 3 | 0expd 12886 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → (0↑((𝑃 − 1) / 2)) =
0) |
29 | 28 | oveq1d 6564 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → ((0↑((𝑃 − 1) / 2)) mod 𝑃) = (0 mod 𝑃)) |
30 | 27, 29 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃) = (0 mod 𝑃)) |
31 | | modadd1 12569 |
. . . . . . 7
⊢ ((((𝐴↑((𝑃 − 1) / 2)) ∈ ℝ ∧ 0
∈ ℝ) ∧ (1 ∈ ℝ ∧ 𝑃 ∈ ℝ+) ∧ ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃) = (0 mod 𝑃)) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = ((0 + 1) mod 𝑃)) |
32 | 7, 8, 9, 17, 30, 31 | syl221anc 1329 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = ((0 + 1) mod 𝑃)) |
33 | | 0p1e1 11009 |
. . . . . . 7
⊢ (0 + 1) =
1 |
34 | 33 | oveq1i 6559 |
. . . . . 6
⊢ ((0 + 1)
mod 𝑃) = (1 mod 𝑃) |
35 | 32, 34 | syl6eq 2660 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (1 mod 𝑃)) |
36 | 16 | nnred 10912 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℝ) |
37 | 15 | simprd 478 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → 1 < 𝑃) |
38 | | 1mod 12564 |
. . . . . 6
⊢ ((𝑃 ∈ ℝ ∧ 1 <
𝑃) → (1 mod 𝑃) = 1) |
39 | 36, 37, 38 | syl2anc 691 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → (1 mod 𝑃) = 1) |
40 | 35, 39 | eqtrd 2644 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 1) |
41 | 40 | oveq1d 6564 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = (1 −
1)) |
42 | | 1m1e0 10966 |
. . . 4
⊢ (1
− 1) = 0 |
43 | | lgslem2.z |
. . . . . 6
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} |
44 | 43 | lgslem2 24823 |
. . . . 5
⊢ (-1
∈ 𝑍 ∧ 0 ∈
𝑍 ∧ 1 ∈ 𝑍) |
45 | 44 | simp2i 1064 |
. . . 4
⊢ 0 ∈
𝑍 |
46 | 42, 45 | eqeltri 2684 |
. . 3
⊢ (1
− 1) ∈ 𝑍 |
47 | 41, 46 | syl6eqel 2696 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍) |
48 | | lgslem1 24822 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2}) |
49 | | elpri 4145 |
. . . 4
⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2} → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
50 | | oveq1 6556 |
. . . . . 6
⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = (0 −
1)) |
51 | | df-neg 10148 |
. . . . . . 7
⊢ -1 = (0
− 1) |
52 | 44 | simp1i 1063 |
. . . . . . 7
⊢ -1 ∈
𝑍 |
53 | 51, 52 | eqeltrri 2685 |
. . . . . 6
⊢ (0
− 1) ∈ 𝑍 |
54 | 50, 53 | syl6eqel 2696 |
. . . . 5
⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍) |
55 | | oveq1 6556 |
. . . . . 6
⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2 → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = (2 −
1)) |
56 | | 2m1e1 11012 |
. . . . . . 7
⊢ (2
− 1) = 1 |
57 | 44 | simp3i 1065 |
. . . . . . 7
⊢ 1 ∈
𝑍 |
58 | 56, 57 | eqeltri 2684 |
. . . . . 6
⊢ (2
− 1) ∈ 𝑍 |
59 | 55, 58 | syl6eqel 2696 |
. . . . 5
⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2 → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍) |
60 | 54, 59 | jaoi 393 |
. . . 4
⊢
(((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍) |
61 | 48, 49, 60 | 3syl 18 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍) |
62 | 61 | 3expa 1257 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍) |
63 | 47, 62 | pm2.61dan 828 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍) |