Proof of Theorem lgsqrmodndvds
Step | Hyp | Ref
| Expression |
1 | | lgsqrmod 24877 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴
/L 𝑃) = 1
→ ∃𝑥 ∈
ℤ ((𝑥↑2) mod
𝑃) = (𝐴 mod 𝑃))) |
2 | 1 | imp 444 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) → ∃𝑥 ∈
ℤ ((𝑥↑2) mod
𝑃) = (𝐴 mod 𝑃)) |
3 | | eldifi 3694 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
4 | | prmnn 15226 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℕ) |
6 | 5 | ad3antlr 763 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) ∧ 𝑥 ∈ ℤ)
→ 𝑃 ∈
ℕ) |
7 | | zsqcl 12796 |
. . . . . . . 8
⊢ (𝑥 ∈ ℤ → (𝑥↑2) ∈
ℤ) |
8 | 7 | adantl 481 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) ∧ 𝑥 ∈ ℤ)
→ (𝑥↑2) ∈
ℤ) |
9 | | simplll 794 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) ∧ 𝑥 ∈ ℤ)
→ 𝐴 ∈
ℤ) |
10 | | moddvds 14829 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ (𝑥↑2) ∈ ℤ ∧
𝐴 ∈ ℤ) →
(((𝑥↑2) mod 𝑃) = (𝐴 mod 𝑃) ↔ 𝑃 ∥ ((𝑥↑2) − 𝐴))) |
11 | 6, 8, 9, 10 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) ∧ 𝑥 ∈ ℤ)
→ (((𝑥↑2) mod
𝑃) = (𝐴 mod 𝑃) ↔ 𝑃 ∥ ((𝑥↑2) − 𝐴))) |
12 | 5 | nnzd 11357 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℤ) |
13 | 12 | ad3antlr 763 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) ∧ 𝑥 ∈ ℤ)
→ 𝑃 ∈
ℤ) |
14 | 13, 8, 9 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) ∧ 𝑥 ∈ ℤ)
→ (𝑃 ∈ ℤ
∧ (𝑥↑2) ∈
ℤ ∧ 𝐴 ∈
ℤ)) |
15 | 14 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑃 ∥ 𝑥 ∧ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (𝐴 /L 𝑃) = 1) ∧ 𝑥 ∈ ℤ)) → (𝑃 ∈ ℤ ∧ (𝑥↑2) ∈ ℤ ∧ 𝐴 ∈
ℤ)) |
16 | | dvdssub2 14861 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℤ ∧ (𝑥↑2) ∈ ℤ ∧
𝐴 ∈ ℤ) ∧
𝑃 ∥ ((𝑥↑2) − 𝐴)) → (𝑃 ∥ (𝑥↑2) ↔ 𝑃 ∥ 𝐴)) |
17 | 15, 16 | sylan 487 |
. . . . . . . . . 10
⊢ (((𝑃 ∥ 𝑥 ∧ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (𝐴 /L 𝑃) = 1) ∧ 𝑥 ∈ ℤ)) ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴)) → (𝑃 ∥ (𝑥↑2) ↔ 𝑃 ∥ 𝐴)) |
18 | 17 | ex 449 |
. . . . . . . . 9
⊢ ((𝑃 ∥ 𝑥 ∧ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (𝐴 /L 𝑃) = 1) ∧ 𝑥 ∈ ℤ)) → (𝑃 ∥ ((𝑥↑2) − 𝐴) → (𝑃 ∥ (𝑥↑2) ↔ 𝑃 ∥ 𝐴))) |
19 | | bicom 211 |
. . . . . . . . . 10
⊢ ((𝑃 ∥ (𝑥↑2) ↔ 𝑃 ∥ 𝐴) ↔ (𝑃 ∥ 𝐴 ↔ 𝑃 ∥ (𝑥↑2))) |
20 | 3 | ad3antlr 763 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) ∧ 𝑥 ∈ ℤ)
→ 𝑃 ∈
ℙ) |
21 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) ∧ 𝑥 ∈ ℤ)
→ 𝑥 ∈
ℤ) |
22 | | 2nn 11062 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ |
23 | 22 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) ∧ 𝑥 ∈ ℤ)
→ 2 ∈ ℕ) |
24 | | prmdvdsexp 15265 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ∧ 2 ∈
ℕ) → (𝑃 ∥
(𝑥↑2) ↔ 𝑃 ∥ 𝑥)) |
25 | 20, 21, 23, 24 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) ∧ 𝑥 ∈ ℤ)
→ (𝑃 ∥ (𝑥↑2) ↔ 𝑃 ∥ 𝑥)) |
26 | 25 | biimparc 503 |
. . . . . . . . . . 11
⊢ ((𝑃 ∥ 𝑥 ∧ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (𝐴 /L 𝑃) = 1) ∧ 𝑥 ∈ ℤ)) → 𝑃 ∥ (𝑥↑2)) |
27 | | bianir 1001 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∥ (𝑥↑2) ∧ (𝑃 ∥ 𝐴 ↔ 𝑃 ∥ (𝑥↑2))) → 𝑃 ∥ 𝐴) |
28 | 5 | anim2i 591 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝐴 ∈ ℤ
∧ 𝑃 ∈
ℕ)) |
29 | 28 | ancomd 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑃 ∈ ℕ
∧ 𝐴 ∈
ℤ)) |
30 | | dvdsval3 14825 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ) → (𝑃 ∥ 𝐴 ↔ (𝐴 mod 𝑃) = 0)) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑃 ∥ 𝐴 ↔ (𝐴 mod 𝑃) = 0)) |
32 | | lgsprme0 24864 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ((𝐴 /L 𝑃) = 0 ↔ (𝐴 mod 𝑃) = 0)) |
33 | 3, 32 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴
/L 𝑃) = 0
↔ (𝐴 mod 𝑃) = 0)) |
34 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 /L 𝑃) = 0 → ((𝐴 /L 𝑃) = 1 ↔ 0 = 1)) |
35 | | 0ne1 10965 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ≠
1 |
36 | | eqneqall 2793 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0 = 1
→ (0 ≠ 1 → ¬ 𝑃 ∥ 𝑥)) |
37 | 35, 36 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 = 1
→ ¬ 𝑃 ∥
𝑥) |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 /L 𝑃) = 0 → (0 = 1 → ¬
𝑃 ∥ 𝑥)) |
39 | 34, 38 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 /L 𝑃) = 0 → ((𝐴 /L 𝑃) = 1 → ¬ 𝑃 ∥ 𝑥)) |
40 | 33, 39 | syl6bir 243 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴 mod 𝑃) = 0 → ((𝐴 /L 𝑃) = 1 → ¬ 𝑃 ∥ 𝑥))) |
41 | 31, 40 | sylbid 229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑃 ∥ 𝐴 → ((𝐴 /L 𝑃) = 1 → ¬ 𝑃 ∥ 𝑥))) |
42 | 41 | com23 84 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴
/L 𝑃) = 1
→ (𝑃 ∥ 𝐴 → ¬ 𝑃 ∥ 𝑥))) |
43 | 42 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) → (𝑃 ∥ 𝐴 → ¬ 𝑃 ∥ 𝑥)) |
44 | 43 | ad2antrl 760 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∥ 𝑥 ∧ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (𝐴 /L 𝑃) = 1) ∧ 𝑥 ∈ ℤ)) → (𝑃 ∥ 𝐴 → ¬ 𝑃 ∥ 𝑥)) |
45 | 44 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∥ 𝐴 → ((𝑃 ∥ 𝑥 ∧ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (𝐴 /L 𝑃) = 1) ∧ 𝑥 ∈ ℤ)) → ¬ 𝑃 ∥ 𝑥)) |
46 | 27, 45 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∥ (𝑥↑2) ∧ (𝑃 ∥ 𝐴 ↔ 𝑃 ∥ (𝑥↑2))) → ((𝑃 ∥ 𝑥 ∧ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (𝐴 /L 𝑃) = 1) ∧ 𝑥 ∈ ℤ)) → ¬ 𝑃 ∥ 𝑥)) |
47 | 46 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑃 ∥ (𝑥↑2) → ((𝑃 ∥ 𝐴 ↔ 𝑃 ∥ (𝑥↑2)) → ((𝑃 ∥ 𝑥 ∧ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (𝐴 /L 𝑃) = 1) ∧ 𝑥 ∈ ℤ)) → ¬ 𝑃 ∥ 𝑥))) |
48 | 47 | com23 84 |
. . . . . . . . . . 11
⊢ (𝑃 ∥ (𝑥↑2) → ((𝑃 ∥ 𝑥 ∧ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (𝐴 /L 𝑃) = 1) ∧ 𝑥 ∈ ℤ)) → ((𝑃 ∥ 𝐴 ↔ 𝑃 ∥ (𝑥↑2)) → ¬ 𝑃 ∥ 𝑥))) |
49 | 26, 48 | mpcom 37 |
. . . . . . . . . 10
⊢ ((𝑃 ∥ 𝑥 ∧ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (𝐴 /L 𝑃) = 1) ∧ 𝑥 ∈ ℤ)) → ((𝑃 ∥ 𝐴 ↔ 𝑃 ∥ (𝑥↑2)) → ¬ 𝑃 ∥ 𝑥)) |
50 | 19, 49 | syl5bi 231 |
. . . . . . . . 9
⊢ ((𝑃 ∥ 𝑥 ∧ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (𝐴 /L 𝑃) = 1) ∧ 𝑥 ∈ ℤ)) → ((𝑃 ∥ (𝑥↑2) ↔ 𝑃 ∥ 𝐴) → ¬ 𝑃 ∥ 𝑥)) |
51 | 18, 50 | syld 46 |
. . . . . . . 8
⊢ ((𝑃 ∥ 𝑥 ∧ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (𝐴 /L 𝑃) = 1) ∧ 𝑥 ∈ ℤ)) → (𝑃 ∥ ((𝑥↑2) − 𝐴) → ¬ 𝑃 ∥ 𝑥)) |
52 | 51 | ex 449 |
. . . . . . 7
⊢ (𝑃 ∥ 𝑥 → ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (𝐴 /L 𝑃) = 1) ∧ 𝑥 ∈ ℤ) → (𝑃 ∥ ((𝑥↑2) − 𝐴) → ¬ 𝑃 ∥ 𝑥))) |
53 | | 2a1 28 |
. . . . . . 7
⊢ (¬
𝑃 ∥ 𝑥 → ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (𝐴 /L 𝑃) = 1) ∧ 𝑥 ∈ ℤ) → (𝑃 ∥ ((𝑥↑2) − 𝐴) → ¬ 𝑃 ∥ 𝑥))) |
54 | 52, 53 | pm2.61i 175 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) ∧ 𝑥 ∈ ℤ)
→ (𝑃 ∥ ((𝑥↑2) − 𝐴) → ¬ 𝑃 ∥ 𝑥)) |
55 | 11, 54 | sylbid 229 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) ∧ 𝑥 ∈ ℤ)
→ (((𝑥↑2) mod
𝑃) = (𝐴 mod 𝑃) → ¬ 𝑃 ∥ 𝑥)) |
56 | 55 | ancld 574 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) ∧ 𝑥 ∈ ℤ)
→ (((𝑥↑2) mod
𝑃) = (𝐴 mod 𝑃) → (((𝑥↑2) mod 𝑃) = (𝐴 mod 𝑃) ∧ ¬ 𝑃 ∥ 𝑥))) |
57 | 56 | reximdva 3000 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) → (∃𝑥 ∈
ℤ ((𝑥↑2) mod
𝑃) = (𝐴 mod 𝑃) → ∃𝑥 ∈ ℤ (((𝑥↑2) mod 𝑃) = (𝐴 mod 𝑃) ∧ ¬ 𝑃 ∥ 𝑥))) |
58 | 2, 57 | mpd 15 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (𝐴
/L 𝑃) =
1) → ∃𝑥 ∈
ℤ (((𝑥↑2) mod
𝑃) = (𝐴 mod 𝑃) ∧ ¬ 𝑃 ∥ 𝑥)) |
59 | 58 | ex 449 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝐴
/L 𝑃) = 1
→ ∃𝑥 ∈
ℤ (((𝑥↑2) mod
𝑃) = (𝐴 mod 𝑃) ∧ ¬ 𝑃 ∥ 𝑥))) |