| Step | Hyp | Ref
| Expression |
| 1 | | eldifi 4131 |
. . . . . 6
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
| 2 | | 2nn 12339 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
| 3 | 2 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 2 ∈
ℕ) |
| 4 | | 2nn0 12543 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
| 5 | 4 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 2 ∈
ℕ0) |
| 6 | | peano2nn 12278 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
| 7 | 6 | nnnn0d 12587 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ0) |
| 8 | 5, 7 | nn0expcld 14285 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(2↑(𝑁 + 1)) ∈
ℕ0) |
| 9 | 3, 8 | nnexpcld 14284 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(2↑(2↑(𝑁 + 1)))
∈ ℕ) |
| 10 | 9 | nnzd 12640 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(2↑(2↑(𝑁 + 1)))
∈ ℤ) |
| 11 | | modprm1div 16835 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧
(2↑(2↑(𝑁 + 1)))
∈ ℤ) → (((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1 ↔ 𝑃 ∥ ((2↑(2↑(𝑁 + 1))) − 1))) |
| 12 | 1, 10, 11 | syl2anr 597 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((2↑(2↑(𝑁
+ 1))) mod 𝑃) = 1 ↔
𝑃 ∥
((2↑(2↑(𝑁 + 1)))
− 1))) |
| 13 | | prmnn 16711 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 14 | 1, 13 | syl 17 |
. . . . . . . 8
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℕ) |
| 15 | 14 | adantl 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 𝑃 ∈
ℕ) |
| 16 | | 2z 12649 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
| 17 | 16 | a1i 11 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 2 ∈ ℤ) |
| 18 | | eldifsn 4786 |
. . . . . . . . . 10
⊢ (𝑃 ∈ (ℙ ∖ {2})
↔ (𝑃 ∈ ℙ
∧ 𝑃 ≠
2)) |
| 19 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) → 𝑃 ≠ 2) |
| 20 | 19 | necomd 2996 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) → 2 ≠ 𝑃) |
| 21 | 18, 20 | sylbi 217 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 2 ≠ 𝑃) |
| 22 | | 2prm 16729 |
. . . . . . . . . 10
⊢ 2 ∈
ℙ |
| 23 | | prmrp 16749 |
. . . . . . . . . 10
⊢ ((2
∈ ℙ ∧ 𝑃
∈ ℙ) → ((2 gcd 𝑃) = 1 ↔ 2 ≠ 𝑃)) |
| 24 | 22, 1, 23 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((2 gcd 𝑃) = 1
↔ 2 ≠ 𝑃)) |
| 25 | 21, 24 | mpbird 257 |
. . . . . . . 8
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (2 gcd 𝑃) =
1) |
| 26 | 25 | adantl 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (2 gcd 𝑃) =
1) |
| 27 | 15, 17, 26 | 3jca 1129 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑃 ∈ ℕ
∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1)) |
| 28 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (2↑(𝑁 + 1))
∈ ℕ0) |
| 29 | | odzdvds 16833 |
. . . . . 6
⊢ (((𝑃 ∈ ℕ ∧ 2 ∈
ℤ ∧ (2 gcd 𝑃) =
1) ∧ (2↑(𝑁 + 1))
∈ ℕ0) → (𝑃 ∥ ((2↑(2↑(𝑁 + 1))) − 1) ↔
((odℤ‘𝑃)‘2) ∥ (2↑(𝑁 + 1)))) |
| 30 | 27, 28, 29 | syl2anc 584 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑃 ∥
((2↑(2↑(𝑁 + 1)))
− 1) ↔ ((odℤ‘𝑃)‘2) ∥ (2↑(𝑁 + 1)))) |
| 31 | 12, 30 | bitrd 279 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((2↑(2↑(𝑁
+ 1))) mod 𝑃) = 1 ↔
((odℤ‘𝑃)‘2) ∥ (2↑(𝑁 + 1)))) |
| 32 | | nnnn0 12533 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
| 33 | 5, 32 | nn0expcld 14285 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(2↑𝑁) ∈
ℕ0) |
| 34 | 3, 33 | nnexpcld 14284 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(2↑(2↑𝑁)) ∈
ℕ) |
| 35 | 34 | nnzd 12640 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(2↑(2↑𝑁)) ∈
ℤ) |
| 36 | | modprm1div 16835 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧
(2↑(2↑𝑁)) ∈
ℤ) → (((2↑(2↑𝑁)) mod 𝑃) = 1 ↔ 𝑃 ∥ ((2↑(2↑𝑁)) − 1))) |
| 37 | 1, 35, 36 | syl2anr 597 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((2↑(2↑𝑁)) mod 𝑃) = 1 ↔ 𝑃 ∥ ((2↑(2↑𝑁)) − 1))) |
| 38 | 33 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (2↑𝑁) ∈
ℕ0) |
| 39 | | odzdvds 16833 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℕ ∧ 2 ∈
ℤ ∧ (2 gcd 𝑃) =
1) ∧ (2↑𝑁) ∈
ℕ0) → (𝑃 ∥ ((2↑(2↑𝑁)) − 1) ↔
((odℤ‘𝑃)‘2) ∥ (2↑𝑁))) |
| 40 | 27, 38, 39 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑃 ∥
((2↑(2↑𝑁))
− 1) ↔ ((odℤ‘𝑃)‘2) ∥ (2↑𝑁))) |
| 41 | 37, 40 | bitrd 279 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((2↑(2↑𝑁)) mod 𝑃) = 1 ↔
((odℤ‘𝑃)‘2) ∥ (2↑𝑁))) |
| 42 | 41 | necon3abid 2977 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((2↑(2↑𝑁)) mod 𝑃) ≠ 1 ↔ ¬
((odℤ‘𝑃)‘2) ∥ (2↑𝑁))) |
| 43 | | odzcl 16831 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℕ ∧ 2 ∈
ℤ ∧ (2 gcd 𝑃) =
1) → ((odℤ‘𝑃)‘2) ∈ ℕ) |
| 44 | 27, 43 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((odℤ‘𝑃)‘2) ∈ ℕ) |
| 45 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑁 + 1) ∈
ℕ0) |
| 46 | | dvdsprmpweqle 16924 |
. . . . . . . . 9
⊢ ((2
∈ ℙ ∧ ((odℤ‘𝑃)‘2) ∈ ℕ ∧ (𝑁 + 1) ∈
ℕ0) → (((odℤ‘𝑃)‘2) ∥ (2↑(𝑁 + 1)) → ∃𝑛 ∈ ℕ0
(𝑛 ≤ (𝑁 + 1) ∧
((odℤ‘𝑃)‘2) = (2↑𝑛)))) |
| 47 | 22, 44, 45, 46 | mp3an2i 1468 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((odℤ‘𝑃)‘2) ∥ (2↑(𝑁 + 1)) → ∃𝑛 ∈ ℕ0
(𝑛 ≤ (𝑁 + 1) ∧
((odℤ‘𝑃)‘2) = (2↑𝑛)))) |
| 48 | | breq1 5146 |
. . . . . . . . . . . . 13
⊢
(((odℤ‘𝑃)‘2) = (2↑𝑛) → (((odℤ‘𝑃)‘2) ∥ (2↑𝑁) ↔ (2↑𝑛) ∥ (2↑𝑁))) |
| 49 | 48 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ 𝑃 ∈
(ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧
((odℤ‘𝑃)‘2) = (2↑𝑛)) → (((odℤ‘𝑃)‘2) ∥ (2↑𝑁) ↔ (2↑𝑛) ∥ (2↑𝑁))) |
| 50 | 49 | notbid 318 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ 𝑃 ∈
(ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧
((odℤ‘𝑃)‘2) = (2↑𝑛)) → (¬
((odℤ‘𝑃)‘2) ∥ (2↑𝑁) ↔ ¬ (2↑𝑛) ∥ (2↑𝑁))) |
| 51 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈
ℕ ∧ 𝑃 ∈
(ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧
((odℤ‘𝑃)‘2) = (2↑𝑛)) → ((odℤ‘𝑃)‘2) = (2↑𝑛)) |
| 52 | 51 | adantr 480 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈
ℕ ∧ 𝑃 ∈
(ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧
((odℤ‘𝑃)‘2) = (2↑𝑛)) ∧ ¬ (2↑𝑛) ∥ (2↑𝑁)) → ((odℤ‘𝑃)‘2) = (2↑𝑛)) |
| 53 | | nn0re 12535 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℝ) |
| 54 | 6 | nnred 12281 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℝ) |
| 55 | 54 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑁 + 1) ∈
ℝ) |
| 56 | | leloe 11347 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℝ ∧ (𝑁 + 1) ∈ ℝ) →
(𝑛 ≤ (𝑁 + 1) ↔ (𝑛 < (𝑁 + 1) ∨ 𝑛 = (𝑁 + 1)))) |
| 57 | 53, 55, 56 | syl2anr 597 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑛 ∈
ℕ0) → (𝑛 ≤ (𝑁 + 1) ↔ (𝑛 < (𝑁 + 1) ∨ 𝑛 = (𝑁 + 1)))) |
| 58 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑛 ∈
ℕ0) → 𝑛 ∈ ℕ0) |
| 59 | | nn0z 12638 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) |
| 60 | 59 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑛 ∈
ℕ0) → 𝑛 ∈ ℤ) |
| 61 | 60 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑛 ∈
ℕ0) ∧ 𝑛 < (𝑁 + 1)) → 𝑛 ∈ ℤ) |
| 62 | | nnz 12634 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
| 63 | 62 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 𝑁 ∈
ℤ) |
| 64 | 63 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑛 ∈
ℕ0) → 𝑁 ∈ ℤ) |
| 65 | 64 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑛 ∈
ℕ0) ∧ 𝑛 < (𝑁 + 1)) → 𝑁 ∈ ℤ) |
| 66 | | zleltp1 12668 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑛 ≤ 𝑁 ↔ 𝑛 < (𝑁 + 1))) |
| 67 | 59, 63, 66 | syl2anr 597 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑛 ∈
ℕ0) → (𝑛 ≤ 𝑁 ↔ 𝑛 < (𝑁 + 1))) |
| 68 | 67 | biimpar 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑛 ∈
ℕ0) ∧ 𝑛 < (𝑁 + 1)) → 𝑛 ≤ 𝑁) |
| 69 | | eluz2 12884 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘𝑛) ↔ (𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑛 ≤ 𝑁)) |
| 70 | 61, 65, 68, 69 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑛 ∈
ℕ0) ∧ 𝑛 < (𝑁 + 1)) → 𝑁 ∈ (ℤ≥‘𝑛)) |
| 71 | | dvdsexp 16365 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2
∈ ℤ ∧ 𝑛
∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑛)) → (2↑𝑛) ∥ (2↑𝑁)) |
| 72 | 16, 58, 70, 71 | mp3an2ani 1470 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑛 ∈
ℕ0) ∧ 𝑛 < (𝑁 + 1)) → (2↑𝑛) ∥ (2↑𝑁)) |
| 73 | 72 | pm2.24d 151 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑛 ∈
ℕ0) ∧ 𝑛 < (𝑁 + 1)) → (¬ (2↑𝑛) ∥ (2↑𝑁) → (2↑𝑛) = (2↑(𝑁 + 1)))) |
| 74 | 73 | expcom 413 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 < (𝑁 + 1) → (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0)
→ (¬ (2↑𝑛)
∥ (2↑𝑁) →
(2↑𝑛) = (2↑(𝑁 + 1))))) |
| 75 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (𝑁 + 1) → (2↑𝑛) = (2↑(𝑁 + 1))) |
| 76 | 75 | 2a1d 26 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = (𝑁 + 1) → (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0)
→ (¬ (2↑𝑛)
∥ (2↑𝑁) →
(2↑𝑛) = (2↑(𝑁 + 1))))) |
| 77 | 74, 76 | jaoi 858 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 < (𝑁 + 1) ∨ 𝑛 = (𝑁 + 1)) → (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0)
→ (¬ (2↑𝑛)
∥ (2↑𝑁) →
(2↑𝑛) = (2↑(𝑁 + 1))))) |
| 78 | 77 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑛 ∈
ℕ0) → ((𝑛 < (𝑁 + 1) ∨ 𝑛 = (𝑁 + 1)) → (¬ (2↑𝑛) ∥ (2↑𝑁) → (2↑𝑛) = (2↑(𝑁 + 1))))) |
| 79 | 57, 78 | sylbid 240 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑛 ∈
ℕ0) → (𝑛 ≤ (𝑁 + 1) → (¬ (2↑𝑛) ∥ (2↑𝑁) → (2↑𝑛) = (2↑(𝑁 + 1))))) |
| 80 | 79 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑛 ∈
ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) → (¬ (2↑𝑛) ∥ (2↑𝑁) → (2↑𝑛) = (2↑(𝑁 + 1)))) |
| 81 | 80 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈
ℕ ∧ 𝑃 ∈
(ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧
((odℤ‘𝑃)‘2) = (2↑𝑛)) → (¬ (2↑𝑛) ∥ (2↑𝑁) → (2↑𝑛) = (2↑(𝑁 + 1)))) |
| 82 | 81 | imp 406 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈
ℕ ∧ 𝑃 ∈
(ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧
((odℤ‘𝑃)‘2) = (2↑𝑛)) ∧ ¬ (2↑𝑛) ∥ (2↑𝑁)) → (2↑𝑛) = (2↑(𝑁 + 1))) |
| 83 | 52, 82 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈
ℕ ∧ 𝑃 ∈
(ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧
((odℤ‘𝑃)‘2) = (2↑𝑛)) ∧ ¬ (2↑𝑛) ∥ (2↑𝑁)) → ((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))) |
| 84 | 83 | ex 412 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ 𝑃 ∈
(ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧
((odℤ‘𝑃)‘2) = (2↑𝑛)) → (¬ (2↑𝑛) ∥ (2↑𝑁) → ((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))) |
| 85 | 50, 84 | sylbid 240 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ 𝑃 ∈
(ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧
((odℤ‘𝑃)‘2) = (2↑𝑛)) → (¬
((odℤ‘𝑃)‘2) ∥ (2↑𝑁) → ((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))) |
| 86 | 85 | expl 457 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ 𝑛 ∈
ℕ0) → ((𝑛 ≤ (𝑁 + 1) ∧
((odℤ‘𝑃)‘2) = (2↑𝑛)) → (¬
((odℤ‘𝑃)‘2) ∥ (2↑𝑁) → ((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))) |
| 87 | 86 | rexlimdva 3155 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (∃𝑛 ∈
ℕ0 (𝑛 ≤
(𝑁 + 1) ∧
((odℤ‘𝑃)‘2) = (2↑𝑛)) → (¬
((odℤ‘𝑃)‘2) ∥ (2↑𝑁) → ((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))) |
| 88 | 47, 87 | syld 47 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((odℤ‘𝑃)‘2) ∥ (2↑(𝑁 + 1)) → (¬
((odℤ‘𝑃)‘2) ∥ (2↑𝑁) → ((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))) |
| 89 | 88 | com23 86 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (¬ ((odℤ‘𝑃)‘2) ∥ (2↑𝑁) → (((odℤ‘𝑃)‘2) ∥
(2↑(𝑁 + 1)) →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))) |
| 90 | 42, 89 | sylbid 240 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((2↑(2↑𝑁)) mod 𝑃) ≠ 1 →
(((odℤ‘𝑃)‘2) ∥ (2↑(𝑁 + 1)) →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))) |
| 91 | 90 | com23 86 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((odℤ‘𝑃)‘2) ∥ (2↑(𝑁 + 1)) →
(((2↑(2↑𝑁)) mod
𝑃) ≠ 1 →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))) |
| 92 | 31, 91 | sylbid 240 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((2↑(2↑(𝑁
+ 1))) mod 𝑃) = 1 →
(((2↑(2↑𝑁)) mod
𝑃) ≠ 1 →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))) |
| 93 | 92 | com23 86 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((2↑(2↑𝑁)) mod 𝑃) ≠ 1 → (((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1 →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))) |
| 94 | 93 | imp32 418 |
1
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (((2↑(2↑𝑁))
mod 𝑃) ≠ 1 ∧
((2↑(2↑(𝑁 + 1)))
mod 𝑃) = 1)) →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))) |