Proof of Theorem dvdsprmpweqle
Step | Hyp | Ref
| Expression |
1 | | dvdsprmpweq 12281 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛))) |
2 | 1 | imp 123 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ∥ (𝑃↑𝑁)) → ∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛)) |
3 | | simplr 525 |
. . . . . . . . 9
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ ∧ 𝑁 ∈
ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → 𝑛 ∈ ℕ0) |
4 | 3 | nn0zd 9325 |
. . . . . . . 8
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ ∧ 𝑁 ∈
ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → 𝑛 ∈ ℤ) |
5 | | simp3 994 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) |
6 | 5 | ad3antrrr 489 |
. . . . . . . . 9
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ ∧ 𝑁 ∈
ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → 𝑁 ∈
ℕ0) |
7 | 6 | nn0zd 9325 |
. . . . . . . 8
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ ∧ 𝑁 ∈
ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → 𝑁 ∈ ℤ) |
8 | | zlelttric 9250 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑛 ≤ 𝑁 ∨ 𝑁 < 𝑛)) |
9 | 4, 7, 8 | syl2anc 409 |
. . . . . . 7
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ ∧ 𝑁 ∈
ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → (𝑛 ≤ 𝑁 ∨ 𝑁 < 𝑛)) |
10 | | breq1 3990 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 = (𝑃↑𝑛) → (𝐴 ∥ (𝑃↑𝑁) ↔ (𝑃↑𝑛) ∥ (𝑃↑𝑁))) |
11 | 10 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → (𝐴 ∥ (𝑃↑𝑁) ↔ (𝑃↑𝑛) ∥ (𝑃↑𝑁))) |
12 | | prmnn 12057 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
13 | 12 | nnnn0d 9181 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ0) |
14 | 13 | 3ad2ant1 1013 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑃 ∈
ℕ0) |
15 | 14 | adantr 274 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑃 ∈
ℕ0) |
16 | | simpr 109 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑛 ∈ ℕ0) |
17 | 15, 16 | nn0expcld 10625 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑃↑𝑛) ∈
ℕ0) |
18 | 17 | nn0zd 9325 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑃↑𝑛) ∈ ℤ) |
19 | 12 | nncnd 8885 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
20 | 19 | 3ad2ant1 1013 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑃 ∈
ℂ) |
21 | 20 | adantr 274 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑃 ∈ ℂ) |
22 | 12 | nnap0d 8917 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℙ → 𝑃 # 0) |
23 | 22 | 3ad2ant1 1013 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑃 #
0) |
24 | 23 | adantr 274 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑃 # 0) |
25 | | nn0z 9225 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) |
26 | 25 | adantl 275 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑛 ∈ ℤ) |
27 | 21, 24, 26 | expap0d 10608 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑃↑𝑛) # 0) |
28 | | 0zd 9217 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 0 ∈ ℤ) |
29 | | zapne 9279 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃↑𝑛) ∈ ℤ ∧ 0 ∈ ℤ)
→ ((𝑃↑𝑛) # 0 ↔ (𝑃↑𝑛) ≠ 0)) |
30 | 18, 28, 29 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → ((𝑃↑𝑛) # 0 ↔ (𝑃↑𝑛) ≠ 0)) |
31 | 27, 30 | mpbid 146 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑃↑𝑛) ≠ 0) |
32 | 5 | adantr 274 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑁 ∈
ℕ0) |
33 | 15, 32 | nn0expcld 10625 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑃↑𝑁) ∈
ℕ0) |
34 | 33 | nn0zd 9325 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑃↑𝑁) ∈ ℤ) |
35 | | dvdsval2 11745 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0 ∧ (𝑃↑𝑁) ∈ ℤ) → ((𝑃↑𝑛) ∥ (𝑃↑𝑁) ↔ ((𝑃↑𝑁) / (𝑃↑𝑛)) ∈ ℤ)) |
36 | 18, 31, 34, 35 | syl3anc 1233 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → ((𝑃↑𝑛) ∥ (𝑃↑𝑁) ↔ ((𝑃↑𝑁) / (𝑃↑𝑛)) ∈ ℤ)) |
37 | 32 | nn0zd 9325 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑁 ∈ ℤ) |
38 | 21, 24, 26, 37 | expsubapd 10613 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑃↑(𝑁 − 𝑛)) = ((𝑃↑𝑁) / (𝑃↑𝑛))) |
39 | 38 | eqcomd 2176 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → ((𝑃↑𝑁) / (𝑃↑𝑛)) = (𝑃↑(𝑁 − 𝑛))) |
40 | 39 | eleq1d 2239 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (((𝑃↑𝑁) / (𝑃↑𝑛)) ∈ ℤ ↔ (𝑃↑(𝑁 − 𝑛)) ∈ ℤ)) |
41 | 21 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → 𝑃 ∈ ℂ) |
42 | 24 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → 𝑃 # 0) |
43 | | nn0cn 9138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
44 | 43 | 3ad2ant3 1015 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℂ) |
45 | 44 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑁 ∈ ℂ) |
46 | | nn0cn 9138 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℂ) |
47 | 46 | adantl 275 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑛 ∈ ℂ) |
48 | 45, 47 | subcld 8223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑁 − 𝑛) ∈ ℂ) |
49 | 48 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → (𝑁 − 𝑛) ∈ ℂ) |
50 | 44, 46 | anim12i 336 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑁 ∈ ℂ ∧ 𝑛 ∈ ℂ)) |
51 | 50 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → (𝑁 ∈ ℂ ∧ 𝑛 ∈ ℂ)) |
52 | | negsubdi2 8171 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℂ ∧ 𝑛 ∈ ℂ) → -(𝑁 − 𝑛) = (𝑛 − 𝑁)) |
53 | 51, 52 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → -(𝑁 − 𝑛) = (𝑛 − 𝑁)) |
54 | 5 | anim1ci 339 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑛 ∈ ℕ0 ∧ 𝑁 ∈
ℕ0)) |
55 | | ltsubnn0 9272 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑛 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 < 𝑛 → (𝑛 − 𝑁) ∈
ℕ0)) |
56 | 54, 55 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑁 < 𝑛 → (𝑛 − 𝑁) ∈
ℕ0)) |
57 | 56 | imp 123 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → (𝑛 − 𝑁) ∈
ℕ0) |
58 | 53, 57 | eqeltrd 2247 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → -(𝑁 − 𝑛) ∈
ℕ0) |
59 | | expineg2 10478 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃 ∈ ℂ ∧ 𝑃 # 0) ∧ ((𝑁 − 𝑛) ∈ ℂ ∧ -(𝑁 − 𝑛) ∈ ℕ0)) → (𝑃↑(𝑁 − 𝑛)) = (1 / (𝑃↑-(𝑁 − 𝑛)))) |
60 | 41, 42, 49, 58, 59 | syl22anc 1234 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → (𝑃↑(𝑁 − 𝑛)) = (1 / (𝑃↑-(𝑁 − 𝑛)))) |
61 | 60 | eleq1d 2239 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → ((𝑃↑(𝑁 − 𝑛)) ∈ ℤ ↔ (1 / (𝑃↑-(𝑁 − 𝑛))) ∈ ℤ)) |
62 | 12 | nnred 8884 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ) |
63 | 62 | 3ad2ant1 1013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑃 ∈
ℝ) |
64 | 63 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑃 ∈ ℝ) |
65 | 64 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → 𝑃 ∈ ℝ) |
66 | 65, 57 | reexpcld 10619 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → (𝑃↑(𝑛 − 𝑁)) ∈ ℝ) |
67 | | nn0z 9225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
68 | 67 | 3ad2ant3 1015 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℤ) |
69 | 68, 25 | anim12i 336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ)) |
70 | | znnsub 9256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑁 < 𝑛 ↔ (𝑛 − 𝑁) ∈ ℕ)) |
71 | 69, 70 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑁 < 𝑛 ↔ (𝑛 − 𝑁) ∈ ℕ)) |
72 | 71 | biimpa 294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → (𝑛 − 𝑁) ∈ ℕ) |
73 | | prmgt1 12079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℙ → 1 <
𝑃) |
74 | 73 | 3ad2ant1 1013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 1 < 𝑃) |
75 | 74 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 1 < 𝑃) |
76 | 75 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → 1 < 𝑃) |
77 | | expgt1 10507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℝ ∧ (𝑛 − 𝑁) ∈ ℕ ∧ 1 < 𝑃) → 1 < (𝑃↑(𝑛 − 𝑁))) |
78 | 65, 72, 76, 77 | syl3anc 1233 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → 1 < (𝑃↑(𝑛 − 𝑁))) |
79 | 66, 78 | jca 304 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → ((𝑃↑(𝑛 − 𝑁)) ∈ ℝ ∧ 1 < (𝑃↑(𝑛 − 𝑁)))) |
80 | | oveq2 5859 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (-(𝑁 − 𝑛) = (𝑛 − 𝑁) → (𝑃↑-(𝑁 − 𝑛)) = (𝑃↑(𝑛 − 𝑁))) |
81 | 80 | eleq1d 2239 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (-(𝑁 − 𝑛) = (𝑛 − 𝑁) → ((𝑃↑-(𝑁 − 𝑛)) ∈ ℝ ↔ (𝑃↑(𝑛 − 𝑁)) ∈ ℝ)) |
82 | 80 | breq2d 3999 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (-(𝑁 − 𝑛) = (𝑛 − 𝑁) → (1 < (𝑃↑-(𝑁 − 𝑛)) ↔ 1 < (𝑃↑(𝑛 − 𝑁)))) |
83 | 81, 82 | anbi12d 470 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (-(𝑁 − 𝑛) = (𝑛 − 𝑁) → (((𝑃↑-(𝑁 − 𝑛)) ∈ ℝ ∧ 1 < (𝑃↑-(𝑁 − 𝑛))) ↔ ((𝑃↑(𝑛 − 𝑁)) ∈ ℝ ∧ 1 < (𝑃↑(𝑛 − 𝑁))))) |
84 | 79, 83 | syl5ibrcom 156 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → (-(𝑁 − 𝑛) = (𝑛 − 𝑁) → ((𝑃↑-(𝑁 − 𝑛)) ∈ ℝ ∧ 1 < (𝑃↑-(𝑁 − 𝑛))))) |
85 | 53, 84 | mpd 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → ((𝑃↑-(𝑁 − 𝑛)) ∈ ℝ ∧ 1 < (𝑃↑-(𝑁 − 𝑛)))) |
86 | | recnz 9298 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃↑-(𝑁 − 𝑛)) ∈ ℝ ∧ 1 < (𝑃↑-(𝑁 − 𝑛))) → ¬ (1 / (𝑃↑-(𝑁 − 𝑛))) ∈ ℤ) |
87 | 85, 86 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → ¬ (1 / (𝑃↑-(𝑁 − 𝑛))) ∈ ℤ) |
88 | 87 | pm2.21d 614 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → ((1 / (𝑃↑-(𝑁 − 𝑛))) ∈ ℤ → 𝑛 ≤ 𝑁)) |
89 | 61, 88 | sylbid 149 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑁 < 𝑛) → ((𝑃↑(𝑁 − 𝑛)) ∈ ℤ → 𝑛 ≤ 𝑁)) |
90 | 89 | ex 114 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑁 < 𝑛 → ((𝑃↑(𝑁 − 𝑛)) ∈ ℤ → 𝑛 ≤ 𝑁))) |
91 | 90 | com23 78 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → ((𝑃↑(𝑁 − 𝑛)) ∈ ℤ → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁))) |
92 | 40, 91 | sylbid 149 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (((𝑃↑𝑁) / (𝑃↑𝑛)) ∈ ℤ → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁))) |
93 | 36, 92 | sylbid 149 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → ((𝑃↑𝑛) ∥ (𝑃↑𝑁) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁))) |
94 | 93 | adantr 274 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → ((𝑃↑𝑛) ∥ (𝑃↑𝑁) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁))) |
95 | 11, 94 | sylbid 149 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → (𝐴 ∥ (𝑃↑𝑁) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁))) |
96 | 95 | ex 114 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝐴 = (𝑃↑𝑛) → (𝐴 ∥ (𝑃↑𝑁) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁)))) |
97 | 96 | com23 78 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → (𝐴 = (𝑃↑𝑛) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁)))) |
98 | 97 | ex 114 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝑛 ∈
ℕ0 → (𝐴 ∥ (𝑃↑𝑁) → (𝐴 = (𝑃↑𝑛) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁))))) |
99 | 98 | com23 78 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 ∥ (𝑃↑𝑁) → (𝑛 ∈ ℕ0 → (𝐴 = (𝑃↑𝑛) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁))))) |
100 | 99 | imp41 351 |
. . . . . . . . 9
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ ∧ 𝑁 ∈
ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → (𝑁 < 𝑛 → 𝑛 ≤ 𝑁)) |
101 | 100 | com12 30 |
. . . . . . . 8
⊢ (𝑁 < 𝑛 → (((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → 𝑛 ≤ 𝑁)) |
102 | 101 | jao1i 791 |
. . . . . . 7
⊢ ((𝑛 ≤ 𝑁 ∨ 𝑁 < 𝑛) → (((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → 𝑛 ≤ 𝑁)) |
103 | 9, 102 | mpcom 36 |
. . . . . 6
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ ∧ 𝑁 ∈
ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → 𝑛 ≤ 𝑁) |
104 | | simpr 109 |
. . . . . 6
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ ∧ 𝑁 ∈
ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → 𝐴 = (𝑃↑𝑛)) |
105 | 103, 104 | jca 304 |
. . . . 5
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ ∧ 𝑁 ∈
ℕ0) ∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) ∧ 𝐴 = (𝑃↑𝑛)) → (𝑛 ≤ 𝑁 ∧ 𝐴 = (𝑃↑𝑛))) |
106 | 105 | ex 114 |
. . . 4
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ∥ (𝑃↑𝑁)) ∧ 𝑛 ∈ ℕ0) → (𝐴 = (𝑃↑𝑛) → (𝑛 ≤ 𝑁 ∧ 𝐴 = (𝑃↑𝑛)))) |
107 | 106 | reximdva 2572 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ∥ (𝑃↑𝑁)) → (∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛) → ∃𝑛 ∈ ℕ0 (𝑛 ≤ 𝑁 ∧ 𝐴 = (𝑃↑𝑛)))) |
108 | 2, 107 | mpd 13 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ∥ (𝑃↑𝑁)) → ∃𝑛 ∈ ℕ0 (𝑛 ≤ 𝑁 ∧ 𝐴 = (𝑃↑𝑛))) |
109 | 108 | ex 114 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ0 (𝑛 ≤ 𝑁 ∧ 𝐴 = (𝑃↑𝑛)))) |