Proof of Theorem dvdsprmpweqle
Step | Hyp | Ref
| Expression |
1 | | dvdsprmpweq 15426 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛))) |
2 | 1 | imp 444 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ∥ (𝑃↑𝑁)) → ∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛)) |
3 | | nn0re 11178 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
4 | 3 | 3ad2ant3 1077 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℝ) |
5 | 4 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ∥ (𝑃↑𝑁)) → 𝑁 ∈ ℝ) |
6 | | nn0re 11178 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℝ) |
7 | 5, 6 | anim12i 588 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) → (𝑁 ∈ ℝ ∧ 𝑛 ∈
ℝ)) |
8 | 7 | ancomd 466 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) → (𝑛 ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
9 | 8 | adantr 480 |
. . . . . . . 8
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ ∧ 𝑁 ∈
ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → (𝑛 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
10 | | lelttric 10023 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑛 ≤ 𝑁 ∨ 𝑁 < 𝑛)) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ ∧ 𝑁 ∈
ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → (𝑛 ≤ 𝑁 ∨ 𝑁 < 𝑛)) |
12 | | breq1 4586 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 = (𝑃↑𝑛) → (𝐴 ∥ (𝑃↑𝑁) ↔ (𝑃↑𝑛) ∥ (𝑃↑𝑁))) |
13 | 12 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → (𝐴 ∥ (𝑃↑𝑁) ↔ (𝑃↑𝑛) ∥ (𝑃↑𝑁))) |
14 | | prmnn 15226 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
15 | 14 | nnnn0d 11228 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ0) |
16 | 15 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑃 ∈
ℕ0) |
17 | 16 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑃 ∈
ℕ0) |
18 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑛 ∈ ℕ0) |
19 | 17, 18 | nn0expcld 12893 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑃↑𝑛) ∈
ℕ0) |
20 | 19 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑃↑𝑛) ∈ ℤ) |
21 | 14 | nncnd 10913 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
22 | 21 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑃 ∈
ℂ) |
23 | 22 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑃 ∈ ℂ) |
24 | 14 | nnne0d 10942 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℙ → 𝑃 ≠ 0) |
25 | 24 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑃 ≠
0) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑃 ≠ 0) |
27 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) |
28 | 27 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑛 ∈ ℤ) |
29 | 23, 26, 28 | expne0d 12876 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑃↑𝑛) ≠ 0) |
30 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) |
31 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑁 ∈
ℕ0) |
32 | 17, 31 | nn0expcld 12893 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑃↑𝑁) ∈
ℕ0) |
33 | 32 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑃↑𝑁) ∈ ℤ) |
34 | | dvdsval2 14824 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0 ∧ (𝑃↑𝑁) ∈ ℤ) → ((𝑃↑𝑛) ∥ (𝑃↑𝑁) ↔ ((𝑃↑𝑁) / (𝑃↑𝑛)) ∈ ℤ)) |
35 | 20, 29, 33, 34 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → ((𝑃↑𝑛) ∥ (𝑃↑𝑁) ↔ ((𝑃↑𝑁) / (𝑃↑𝑛)) ∈ ℤ)) |
36 | 21, 24 | jca 553 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℙ → (𝑃 ∈ ℂ ∧ 𝑃 ≠ 0)) |
37 | 36 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝑃 ∈ ℂ
∧ 𝑃 ≠
0)) |
38 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
39 | 38 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℤ) |
40 | 39, 27 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ)) |
41 | | expsub 12770 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℂ ∧ 𝑃 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝑃↑(𝑁 − 𝑛)) = ((𝑃↑𝑁) / (𝑃↑𝑛))) |
42 | 41 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℂ ∧ 𝑃 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → ((𝑃↑𝑁) / (𝑃↑𝑛)) = (𝑃↑(𝑁 − 𝑛))) |
43 | 37, 40, 42 | syl2an2r 872 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → ((𝑃↑𝑁) / (𝑃↑𝑛)) = (𝑃↑(𝑁 − 𝑛))) |
44 | 43 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (((𝑃↑𝑁) / (𝑃↑𝑛)) ∈ ℤ ↔ (𝑃↑(𝑁 − 𝑛)) ∈ ℤ)) |
45 | 23 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → 𝑃 ∈ ℂ) |
46 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
47 | 46 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℂ) |
48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑁 ∈ ℂ) |
49 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℂ) |
50 | 49 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑛 ∈ ℂ) |
51 | 48, 50 | subcld 10271 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑁 − 𝑛) ∈ ℂ) |
52 | 51 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → (𝑁 − 𝑛) ∈ ℂ) |
53 | 47, 49 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑁 ∈ ℂ ∧ 𝑛 ∈ ℂ)) |
54 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → (𝑁 ∈ ℂ ∧ 𝑛 ∈ ℂ)) |
55 | | negsubdi2 10219 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℂ ∧ 𝑛 ∈ ℂ) → -(𝑁 − 𝑛) = (𝑛 − 𝑁)) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → -(𝑁 − 𝑛) = (𝑛 − 𝑁)) |
57 | 30 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑁 ∈ ℕ0 ∧ 𝑛 ∈
ℕ0)) |
58 | 57 | ancomd 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑛 ∈ ℕ0 ∧ 𝑁 ∈
ℕ0)) |
59 | | ltsubnn0 11221 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑛 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 < 𝑛 → (𝑛 − 𝑁) ∈
ℕ0)) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑁 < 𝑛 → (𝑛 − 𝑁) ∈
ℕ0)) |
61 | 60 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → (𝑛 − 𝑁) ∈
ℕ0) |
62 | 56, 61 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → -(𝑁 − 𝑛) ∈
ℕ0) |
63 | | expneg2 12731 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ ℂ ∧ (𝑁 − 𝑛) ∈ ℂ ∧ -(𝑁 − 𝑛) ∈ ℕ0) → (𝑃↑(𝑁 − 𝑛)) = (1 / (𝑃↑-(𝑁 − 𝑛)))) |
64 | 45, 52, 62, 63 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → (𝑃↑(𝑁 − 𝑛)) = (1 / (𝑃↑-(𝑁 − 𝑛)))) |
65 | 64 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → ((𝑃↑(𝑁 − 𝑛)) ∈ ℤ ↔ (1 / (𝑃↑-(𝑁 − 𝑛))) ∈ ℤ)) |
66 | 14 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ) |
67 | 66 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑃 ∈
ℝ) |
68 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑃 ∈ ℝ) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → 𝑃 ∈ ℝ) |
70 | 69, 61 | reexpcld 12887 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → (𝑃↑(𝑛 − 𝑁)) ∈ ℝ) |
71 | | znnsub 11300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑁 < 𝑛 ↔ (𝑛 − 𝑁) ∈ ℕ)) |
72 | 40, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑁 < 𝑛 ↔ (𝑛 − 𝑁) ∈ ℕ)) |
73 | 72 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → (𝑛 − 𝑁) ∈ ℕ) |
74 | | prmgt1 15247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℙ → 1 <
𝑃) |
75 | 74 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 1 < 𝑃) |
76 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 1 < 𝑃) |
77 | 76 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → 1 < 𝑃) |
78 | | expgt1 12760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℝ ∧ (𝑛 − 𝑁) ∈ ℕ ∧ 1 < 𝑃) → 1 < (𝑃↑(𝑛 − 𝑁))) |
79 | 69, 73, 77, 78 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → 1 < (𝑃↑(𝑛 − 𝑁))) |
80 | 70, 79 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → ((𝑃↑(𝑛 − 𝑁)) ∈ ℝ ∧ 1 < (𝑃↑(𝑛 − 𝑁)))) |
81 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (-(𝑁 − 𝑛) = (𝑛 − 𝑁) → (𝑃↑-(𝑁 − 𝑛)) = (𝑃↑(𝑛 − 𝑁))) |
82 | 81 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (-(𝑁 − 𝑛) = (𝑛 − 𝑁) → ((𝑃↑-(𝑁 − 𝑛)) ∈ ℝ ↔ (𝑃↑(𝑛 − 𝑁)) ∈ ℝ)) |
83 | 81 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (-(𝑁 − 𝑛) = (𝑛 − 𝑁) → (1 < (𝑃↑-(𝑁 − 𝑛)) ↔ 1 < (𝑃↑(𝑛 − 𝑁)))) |
84 | 82, 83 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (-(𝑁 − 𝑛) = (𝑛 − 𝑁) → (((𝑃↑-(𝑁 − 𝑛)) ∈ ℝ ∧ 1 < (𝑃↑-(𝑁 − 𝑛))) ↔ ((𝑃↑(𝑛 − 𝑁)) ∈ ℝ ∧ 1 < (𝑃↑(𝑛 − 𝑁))))) |
85 | 80, 84 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → (-(𝑁 − 𝑛) = (𝑛 − 𝑁) → ((𝑃↑-(𝑁 − 𝑛)) ∈ ℝ ∧ 1 < (𝑃↑-(𝑁 − 𝑛))))) |
86 | 56, 85 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → ((𝑃↑-(𝑁 − 𝑛)) ∈ ℝ ∧ 1 < (𝑃↑-(𝑁 − 𝑛)))) |
87 | | recnz 11328 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃↑-(𝑁 − 𝑛)) ∈ ℝ ∧ 1 < (𝑃↑-(𝑁 − 𝑛))) → ¬ (1 / (𝑃↑-(𝑁 − 𝑛))) ∈ ℤ) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → ¬ (1 / (𝑃↑-(𝑁 − 𝑛))) ∈ ℤ) |
89 | 88 | pm2.21d 117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → ((1 / (𝑃↑-(𝑁 − 𝑛))) ∈ ℤ → 𝑛 ≤ 𝑁)) |
90 | 65, 89 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → ((𝑃↑(𝑁 − 𝑛)) ∈ ℤ → 𝑛 ≤ 𝑁)) |
91 | 90 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑁 < 𝑛 → ((𝑃↑(𝑁 − 𝑛)) ∈ ℤ → 𝑛 ≤ 𝑁))) |
92 | 91 | com23 84 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → ((𝑃↑(𝑁 − 𝑛)) ∈ ℤ → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁))) |
93 | 44, 92 | sylbid 229 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (((𝑃↑𝑁) / (𝑃↑𝑛)) ∈ ℤ → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁))) |
94 | 35, 93 | sylbid 229 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → ((𝑃↑𝑛) ∥ (𝑃↑𝑁) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁))) |
95 | 94 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → ((𝑃↑𝑛) ∥ (𝑃↑𝑁) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁))) |
96 | 13, 95 | sylbid 229 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → (𝐴 ∥ (𝑃↑𝑁) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁))) |
97 | 96 | ex 449 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝐴 = (𝑃↑𝑛) → (𝐴 ∥ (𝑃↑𝑁) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁)))) |
98 | 97 | com23 84 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → (𝐴 = (𝑃↑𝑛) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁)))) |
99 | 98 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝑛 ∈
ℕ0 → (𝐴 ∥ (𝑃↑𝑁) → (𝐴 = (𝑃↑𝑛) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁))))) |
100 | 99 | com23 84 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 ∥ (𝑃↑𝑁) → (𝑛 ∈ ℕ0 → (𝐴 = (𝑃↑𝑛) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁))))) |
101 | 100 | imp41 617 |
. . . . . . . . 9
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ ∧ 𝑁 ∈
ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁)) |
102 | 101 | com12 32 |
. . . . . . . 8
⊢ (𝑁 < 𝑛 → (((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → 𝑛 ≤ 𝑁)) |
103 | 102 | jao1i 821 |
. . . . . . 7
⊢ ((𝑛 ≤ 𝑁 ∨ 𝑁 < 𝑛) → (((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → 𝑛 ≤ 𝑁)) |
104 | 11, 103 | mpcom 37 |
. . . . . 6
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ ∧ 𝑁 ∈
ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → 𝑛 ≤ 𝑁) |
105 | | simpr 476 |
. . . . . 6
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ ∧ 𝑁 ∈
ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → 𝐴 = (𝑃↑𝑛)) |
106 | 104, 105 | jca 553 |
. . . . 5
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ ∧ 𝑁 ∈
ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → (𝑛 ≤ 𝑁 ∧ 𝐴 = (𝑃↑𝑛))) |
107 | 106 | ex 449 |
. . . 4
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) → (𝐴 = (𝑃↑𝑛) → (𝑛 ≤ 𝑁 ∧ 𝐴 = (𝑃↑𝑛)))) |
108 | 107 | reximdva 3000 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ∥ (𝑃↑𝑁)) → (∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛) → ∃𝑛 ∈ ℕ0 (𝑛 ≤ 𝑁 ∧ 𝐴 = (𝑃↑𝑛)))) |
109 | 2, 108 | mpd 15 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ∥ (𝑃↑𝑁)) → ∃𝑛 ∈ ℕ0 (𝑛 ≤ 𝑁 ∧ 𝐴 = (𝑃↑𝑛))) |
110 | 109 | ex 449 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ0 (𝑛 ≤ 𝑁 ∧ 𝐴 = (𝑃↑𝑛)))) |