Step |
Hyp |
Ref |
Expression |
1 |
|
eldifi |
⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ ) |
2 |
1
|
adantl |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 𝑃 ∈ ℙ ) |
3 |
|
prmz |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ ) |
4 |
2 3
|
syl |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 𝑃 ∈ ℤ ) |
5 |
|
simpl |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 𝐴 ∈ ℤ ) |
6 |
4 5
|
gcdcomd |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑃 gcd 𝐴 ) = ( 𝐴 gcd 𝑃 ) ) |
7 |
6
|
eqeq1d |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝑃 gcd 𝐴 ) = 1 ↔ ( 𝐴 gcd 𝑃 ) = 1 ) ) |
8 |
|
coprm |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝐴 ↔ ( 𝑃 gcd 𝐴 ) = 1 ) ) |
9 |
2 5 8
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ¬ 𝑃 ∥ 𝐴 ↔ ( 𝑃 gcd 𝐴 ) = 1 ) ) |
10 |
|
lgsne0 |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝐴 /L 𝑃 ) ≠ 0 ↔ ( 𝐴 gcd 𝑃 ) = 1 ) ) |
11 |
5 4 10
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) ≠ 0 ↔ ( 𝐴 gcd 𝑃 ) = 1 ) ) |
12 |
7 9 11
|
3bitr4d |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ¬ 𝑃 ∥ 𝐴 ↔ ( 𝐴 /L 𝑃 ) ≠ 0 ) ) |
13 |
12
|
necon4bbid |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑃 ∥ 𝐴 ↔ ( 𝐴 /L 𝑃 ) = 0 ) ) |
14 |
|
0ne1 |
⊢ 0 ≠ 1 |
15 |
|
neeq1 |
⊢ ( ( 𝐴 /L 𝑃 ) = 0 → ( ( 𝐴 /L 𝑃 ) ≠ 1 ↔ 0 ≠ 1 ) ) |
16 |
14 15
|
mpbiri |
⊢ ( ( 𝐴 /L 𝑃 ) = 0 → ( 𝐴 /L 𝑃 ) ≠ 1 ) |
17 |
13 16
|
syl6bi |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑃 ∥ 𝐴 → ( 𝐴 /L 𝑃 ) ≠ 1 ) ) |
18 |
17
|
necon2bd |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 1 → ¬ 𝑃 ∥ 𝐴 ) ) |
19 |
|
lgsqrlem5 |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) → ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) |
20 |
19
|
3expia |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 1 → ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) |
21 |
18 20
|
jcad |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 1 → ( ¬ 𝑃 ∥ 𝐴 ∧ ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) ) |
22 |
|
simprl |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑥 ∈ ℤ ) |
23 |
22
|
zred |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑥 ∈ ℝ ) |
24 |
|
absresq |
⊢ ( 𝑥 ∈ ℝ → ( ( abs ‘ 𝑥 ) ↑ 2 ) = ( 𝑥 ↑ 2 ) ) |
25 |
23 24
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ 2 ) = ( 𝑥 ↑ 2 ) ) |
26 |
25
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( ( abs ‘ 𝑥 ) ↑ 2 ) /L 𝑃 ) = ( ( 𝑥 ↑ 2 ) /L 𝑃 ) ) |
27 |
|
simplr |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ¬ 𝑃 ∥ 𝐴 ) |
28 |
1
|
ad3antlr |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑃 ∈ ℙ ) |
29 |
28 3
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑃 ∈ ℤ ) |
30 |
|
zsqcl |
⊢ ( 𝑥 ∈ ℤ → ( 𝑥 ↑ 2 ) ∈ ℤ ) |
31 |
22 30
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( 𝑥 ↑ 2 ) ∈ ℤ ) |
32 |
|
simplll |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝐴 ∈ ℤ ) |
33 |
|
simprr |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) |
34 |
|
dvdssub2 |
⊢ ( ( ( 𝑃 ∈ ℤ ∧ ( 𝑥 ↑ 2 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) → ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ↔ 𝑃 ∥ 𝐴 ) ) |
35 |
29 31 32 33 34
|
syl31anc |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ↔ 𝑃 ∥ 𝐴 ) ) |
36 |
27 35
|
mtbird |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ¬ 𝑃 ∥ ( 𝑥 ↑ 2 ) ) |
37 |
|
2nn |
⊢ 2 ∈ ℕ |
38 |
37
|
a1i |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 2 ∈ ℕ ) |
39 |
|
prmdvdsexp |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ∧ 2 ∈ ℕ ) → ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ↔ 𝑃 ∥ 𝑥 ) ) |
40 |
28 22 38 39
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ↔ 𝑃 ∥ 𝑥 ) ) |
41 |
36 40
|
mtbid |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ¬ 𝑃 ∥ 𝑥 ) |
42 |
|
dvds0 |
⊢ ( 𝑃 ∈ ℤ → 𝑃 ∥ 0 ) |
43 |
29 42
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑃 ∥ 0 ) |
44 |
|
breq2 |
⊢ ( 𝑥 = 0 → ( 𝑃 ∥ 𝑥 ↔ 𝑃 ∥ 0 ) ) |
45 |
43 44
|
syl5ibrcom |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( 𝑥 = 0 → 𝑃 ∥ 𝑥 ) ) |
46 |
45
|
necon3bd |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ¬ 𝑃 ∥ 𝑥 → 𝑥 ≠ 0 ) ) |
47 |
41 46
|
mpd |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑥 ≠ 0 ) |
48 |
|
nnabscl |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) → ( abs ‘ 𝑥 ) ∈ ℕ ) |
49 |
22 47 48
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℕ ) |
50 |
49
|
nnzd |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℤ ) |
51 |
49
|
nnne0d |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( abs ‘ 𝑥 ) ≠ 0 ) |
52 |
50 29
|
gcdcomd |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( abs ‘ 𝑥 ) gcd 𝑃 ) = ( 𝑃 gcd ( abs ‘ 𝑥 ) ) ) |
53 |
|
dvdsabsb |
⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑃 ∥ 𝑥 ↔ 𝑃 ∥ ( abs ‘ 𝑥 ) ) ) |
54 |
29 22 53
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( 𝑃 ∥ 𝑥 ↔ 𝑃 ∥ ( abs ‘ 𝑥 ) ) ) |
55 |
41 54
|
mtbid |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ¬ 𝑃 ∥ ( abs ‘ 𝑥 ) ) |
56 |
|
coprm |
⊢ ( ( 𝑃 ∈ ℙ ∧ ( abs ‘ 𝑥 ) ∈ ℤ ) → ( ¬ 𝑃 ∥ ( abs ‘ 𝑥 ) ↔ ( 𝑃 gcd ( abs ‘ 𝑥 ) ) = 1 ) ) |
57 |
28 50 56
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ¬ 𝑃 ∥ ( abs ‘ 𝑥 ) ↔ ( 𝑃 gcd ( abs ‘ 𝑥 ) ) = 1 ) ) |
58 |
55 57
|
mpbid |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( 𝑃 gcd ( abs ‘ 𝑥 ) ) = 1 ) |
59 |
52 58
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( abs ‘ 𝑥 ) gcd 𝑃 ) = 1 ) |
60 |
|
lgssq |
⊢ ( ( ( ( abs ‘ 𝑥 ) ∈ ℤ ∧ ( abs ‘ 𝑥 ) ≠ 0 ) ∧ 𝑃 ∈ ℤ ∧ ( ( abs ‘ 𝑥 ) gcd 𝑃 ) = 1 ) → ( ( ( abs ‘ 𝑥 ) ↑ 2 ) /L 𝑃 ) = 1 ) |
61 |
50 51 29 59 60
|
syl211anc |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( ( abs ‘ 𝑥 ) ↑ 2 ) /L 𝑃 ) = 1 ) |
62 |
|
prmnn |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ ) |
63 |
28 62
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑃 ∈ ℕ ) |
64 |
|
moddvds |
⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑥 ↑ 2 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) |
65 |
63 31 32 64
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) |
66 |
33 65
|
mpbird |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ) |
67 |
66
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) /L 𝑃 ) = ( ( 𝐴 mod 𝑃 ) /L 𝑃 ) ) |
68 |
|
eldifsni |
⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ≠ 2 ) |
69 |
68
|
ad3antlr |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑃 ≠ 2 ) |
70 |
69
|
necomd |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 2 ≠ 𝑃 ) |
71 |
|
2z |
⊢ 2 ∈ ℤ |
72 |
|
uzid |
⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) ) |
73 |
71 72
|
ax-mp |
⊢ 2 ∈ ( ℤ≥ ‘ 2 ) |
74 |
|
dvdsprm |
⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( 2 ∥ 𝑃 ↔ 2 = 𝑃 ) ) |
75 |
74
|
necon3bbid |
⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( ¬ 2 ∥ 𝑃 ↔ 2 ≠ 𝑃 ) ) |
76 |
73 28 75
|
sylancr |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ¬ 2 ∥ 𝑃 ↔ 2 ≠ 𝑃 ) ) |
77 |
70 76
|
mpbird |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ¬ 2 ∥ 𝑃 ) |
78 |
|
lgsmod |
⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℤ ∧ 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) /L 𝑃 ) = ( ( 𝑥 ↑ 2 ) /L 𝑃 ) ) |
79 |
31 63 77 78
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) /L 𝑃 ) = ( ( 𝑥 ↑ 2 ) /L 𝑃 ) ) |
80 |
|
lgsmod |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( ( 𝐴 mod 𝑃 ) /L 𝑃 ) = ( 𝐴 /L 𝑃 ) ) |
81 |
32 63 77 80
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( 𝐴 mod 𝑃 ) /L 𝑃 ) = ( 𝐴 /L 𝑃 ) ) |
82 |
67 79 81
|
3eqtr3d |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( 𝑥 ↑ 2 ) /L 𝑃 ) = ( 𝐴 /L 𝑃 ) ) |
83 |
26 61 82
|
3eqtr3rd |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( 𝐴 /L 𝑃 ) = 1 ) |
84 |
83
|
rexlimdvaa |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) → ( 𝐴 /L 𝑃 ) = 1 ) ) |
85 |
84
|
expimpd |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ¬ 𝑃 ∥ 𝐴 ∧ ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) → ( 𝐴 /L 𝑃 ) = 1 ) ) |
86 |
21 85
|
impbid |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 1 ↔ ( ¬ 𝑃 ∥ 𝐴 ∧ ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) ) |