Proof of Theorem lgsqr
Step | Hyp | Ref
| Expression |
1 | | eldifi 3732 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
2 | 1 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 𝑃 ∈
ℙ) |
3 | | prmz 15389 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
4 | 2, 3 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 𝑃 ∈
ℤ) |
5 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 𝐴 ∈
ℤ) |
6 | | gcdcom 15235 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑃 gcd 𝐴) = (𝐴 gcd 𝑃)) |
7 | 4, 5, 6 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑃 gcd 𝐴) = (𝐴 gcd 𝑃)) |
8 | 7 | eqeq1d 2624 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝑃 gcd 𝐴) = 1 ↔ (𝐴 gcd 𝑃) = 1)) |
9 | | coprm 15423 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬
𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
10 | 2, 5, 9 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (¬ 𝑃 ∥
𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
11 | | lgsne0 25060 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝐴 /L 𝑃) ≠ 0 ↔ (𝐴 gcd 𝑃) = 1)) |
12 | 5, 4, 11 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴
/L 𝑃)
≠ 0 ↔ (𝐴 gcd 𝑃) = 1)) |
13 | 8, 10, 12 | 3bitr4d 300 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (¬ 𝑃 ∥
𝐴 ↔ (𝐴 /L 𝑃) ≠ 0)) |
14 | 13 | necon4bbid 2835 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑃 ∥ 𝐴 ↔ (𝐴 /L 𝑃) = 0)) |
15 | | 0ne1 11088 |
. . . . . 6
⊢ 0 ≠
1 |
16 | | neeq1 2856 |
. . . . . 6
⊢ ((𝐴 /L 𝑃) = 0 → ((𝐴 /L 𝑃) ≠ 1 ↔ 0 ≠ 1)) |
17 | 15, 16 | mpbiri 248 |
. . . . 5
⊢ ((𝐴 /L 𝑃) = 0 → (𝐴 /L 𝑃) ≠ 1) |
18 | 14, 17 | syl6bi 243 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑃 ∥ 𝐴 → (𝐴 /L 𝑃) ≠ 1)) |
19 | 18 | necon2bd 2810 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴
/L 𝑃) = 1
→ ¬ 𝑃 ∥
𝐴)) |
20 | | lgsqrlem5 25075 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ (𝐴
/L 𝑃) =
1) → ∃𝑥 ∈
ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴)) |
21 | 20 | 3expia 1267 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴
/L 𝑃) = 1
→ ∃𝑥 ∈
ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴))) |
22 | 19, 21 | jcad 555 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴
/L 𝑃) = 1
→ (¬ 𝑃 ∥
𝐴 ∧ ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴)))) |
23 | | simprl 794 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑥 ∈ ℤ) |
24 | 23 | zred 11482 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑥 ∈ ℝ) |
25 | | absresq 14042 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ →
((abs‘𝑥)↑2) =
(𝑥↑2)) |
26 | 24, 25 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ((abs‘𝑥)↑2) = (𝑥↑2)) |
27 | 26 | oveq1d 6665 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (((abs‘𝑥)↑2) /L 𝑃) = ((𝑥↑2) /L 𝑃)) |
28 | | simplr 792 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ¬ 𝑃 ∥ 𝐴) |
29 | 1 | ad3antlr 767 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑃 ∈ ℙ) |
30 | 29, 3 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑃 ∈ ℤ) |
31 | | zsqcl 12934 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℤ → (𝑥↑2) ∈
ℤ) |
32 | 23, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (𝑥↑2) ∈ ℤ) |
33 | | simplll 798 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝐴 ∈ ℤ) |
34 | | simprr 796 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑃 ∥ ((𝑥↑2) − 𝐴)) |
35 | | dvdssub2 15023 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℤ ∧ (𝑥↑2) ∈ ℤ ∧
𝐴 ∈ ℤ) ∧
𝑃 ∥ ((𝑥↑2) − 𝐴)) → (𝑃 ∥ (𝑥↑2) ↔ 𝑃 ∥ 𝐴)) |
36 | 30, 32, 33, 34, 35 | syl31anc 1329 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (𝑃 ∥ (𝑥↑2) ↔ 𝑃 ∥ 𝐴)) |
37 | 28, 36 | mtbird 315 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ¬ 𝑃 ∥ (𝑥↑2)) |
38 | | 2nn 11185 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
39 | 38 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 2 ∈
ℕ) |
40 | | prmdvdsexp 15427 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ∧ 2 ∈
ℕ) → (𝑃 ∥
(𝑥↑2) ↔ 𝑃 ∥ 𝑥)) |
41 | 29, 23, 39, 40 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (𝑃 ∥ (𝑥↑2) ↔ 𝑃 ∥ 𝑥)) |
42 | 37, 41 | mtbid 314 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ¬ 𝑃 ∥ 𝑥) |
43 | | dvds0 14997 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℤ → 𝑃 ∥ 0) |
44 | 30, 43 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑃 ∥ 0) |
45 | | breq2 4657 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (𝑃 ∥ 𝑥 ↔ 𝑃 ∥ 0)) |
46 | 44, 45 | syl5ibrcom 237 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (𝑥 = 0 → 𝑃 ∥ 𝑥)) |
47 | 46 | necon3bd 2808 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (¬ 𝑃 ∥ 𝑥 → 𝑥 ≠ 0)) |
48 | 42, 47 | mpd 15 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑥 ≠ 0) |
49 | | nnabscl 14065 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) → (abs‘𝑥) ∈
ℕ) |
50 | 23, 48, 49 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (abs‘𝑥) ∈ ℕ) |
51 | 50 | nnzd 11481 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (abs‘𝑥) ∈ ℤ) |
52 | 50 | nnne0d 11065 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (abs‘𝑥) ≠ 0) |
53 | | gcdcom 15235 |
. . . . . . . 8
⊢
(((abs‘𝑥)
∈ ℤ ∧ 𝑃
∈ ℤ) → ((abs‘𝑥) gcd 𝑃) = (𝑃 gcd (abs‘𝑥))) |
54 | 51, 30, 53 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ((abs‘𝑥) gcd 𝑃) = (𝑃 gcd (abs‘𝑥))) |
55 | | dvdsabsb 15001 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑃 ∥ 𝑥 ↔ 𝑃 ∥ (abs‘𝑥))) |
56 | 30, 23, 55 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (𝑃 ∥ 𝑥 ↔ 𝑃 ∥ (abs‘𝑥))) |
57 | 42, 56 | mtbid 314 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ¬ 𝑃 ∥ (abs‘𝑥)) |
58 | | coprm 15423 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧
(abs‘𝑥) ∈
ℤ) → (¬ 𝑃
∥ (abs‘𝑥)
↔ (𝑃 gcd
(abs‘𝑥)) =
1)) |
59 | 29, 51, 58 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (¬ 𝑃 ∥ (abs‘𝑥) ↔ (𝑃 gcd (abs‘𝑥)) = 1)) |
60 | 57, 59 | mpbid 222 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (𝑃 gcd (abs‘𝑥)) = 1) |
61 | 54, 60 | eqtrd 2656 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ((abs‘𝑥) gcd 𝑃) = 1) |
62 | | lgssq 25062 |
. . . . . 6
⊢
((((abs‘𝑥)
∈ ℤ ∧ (abs‘𝑥) ≠ 0) ∧ 𝑃 ∈ ℤ ∧ ((abs‘𝑥) gcd 𝑃) = 1) → (((abs‘𝑥)↑2) /L
𝑃) = 1) |
63 | 51, 52, 30, 61, 62 | syl211anc 1332 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (((abs‘𝑥)↑2) /L 𝑃) = 1) |
64 | | prmnn 15388 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
65 | 29, 64 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑃 ∈ ℕ) |
66 | | moddvds 14991 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℕ ∧ (𝑥↑2) ∈ ℤ ∧
𝐴 ∈ ℤ) →
(((𝑥↑2) mod 𝑃) = (𝐴 mod 𝑃) ↔ 𝑃 ∥ ((𝑥↑2) − 𝐴))) |
67 | 65, 32, 33, 66 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (((𝑥↑2) mod 𝑃) = (𝐴 mod 𝑃) ↔ 𝑃 ∥ ((𝑥↑2) − 𝐴))) |
68 | 34, 67 | mpbird 247 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ((𝑥↑2) mod 𝑃) = (𝐴 mod 𝑃)) |
69 | 68 | oveq1d 6665 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (((𝑥↑2) mod 𝑃) /L 𝑃) = ((𝐴 mod 𝑃) /L 𝑃)) |
70 | | eldifsni 4320 |
. . . . . . . . . 10
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ≠
2) |
71 | 70 | ad3antlr 767 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑃 ≠ 2) |
72 | 71 | necomd 2849 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 2 ≠ 𝑃) |
73 | | 2z 11409 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
74 | | uzid 11702 |
. . . . . . . . . 10
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
75 | 73, 74 | ax-mp 5 |
. . . . . . . . 9
⊢ 2 ∈
(ℤ≥‘2) |
76 | | dvdsprm 15415 |
. . . . . . . . . 10
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃)) |
77 | 76 | necon3bbid 2831 |
. . . . . . . . 9
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (¬ 2 ∥
𝑃 ↔ 2 ≠ 𝑃)) |
78 | 75, 29, 77 | sylancr 695 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (¬ 2 ∥ 𝑃 ↔ 2 ≠ 𝑃)) |
79 | 72, 78 | mpbird 247 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ¬ 2 ∥ 𝑃) |
80 | | lgsmod 25048 |
. . . . . . 7
⊢ (((𝑥↑2) ∈ ℤ ∧
𝑃 ∈ ℕ ∧
¬ 2 ∥ 𝑃) →
(((𝑥↑2) mod 𝑃) /L 𝑃) = ((𝑥↑2) /L 𝑃)) |
81 | 32, 65, 79, 80 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (((𝑥↑2) mod 𝑃) /L 𝑃) = ((𝑥↑2) /L 𝑃)) |
82 | | lgsmod 25048 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → ((𝐴 mod 𝑃) /L 𝑃) = (𝐴 /L 𝑃)) |
83 | 33, 65, 79, 82 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ((𝐴 mod 𝑃) /L 𝑃) = (𝐴 /L 𝑃)) |
84 | 69, 81, 83 | 3eqtr3d 2664 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ((𝑥↑2) /L 𝑃) = (𝐴 /L 𝑃)) |
85 | 27, 63, 84 | 3eqtr3rd 2665 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (𝐴 /L 𝑃) = 1) |
86 | 85 | rexlimdvaa 3032 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ¬ 𝑃 ∥ 𝐴) → (∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴) → (𝐴 /L 𝑃) = 1)) |
87 | 86 | expimpd 629 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((¬ 𝑃 ∥
𝐴 ∧ ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴)) → (𝐴 /L 𝑃) = 1)) |
88 | 22, 87 | impbid 202 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴
/L 𝑃) = 1
↔ (¬ 𝑃 ∥
𝐴 ∧ ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴)))) |