Step | Hyp | Ref
| Expression |
1 | | 2prm 15243 |
. . . 4
⊢ 2 ∈
ℙ |
2 | | pcndvds2 15410 |
. . . 4
⊢ ((2
∈ ℙ ∧ 𝐾
∈ ℕ) → ¬ 2 ∥ (𝐾 / (2↑(2 pCnt 𝐾)))) |
3 | 1, 2 | mpan 702 |
. . 3
⊢ (𝐾 ∈ ℕ → ¬ 2
∥ (𝐾 / (2↑(2
pCnt 𝐾)))) |
4 | | pcdvds 15406 |
. . . 4
⊢ ((2
∈ ℙ ∧ 𝐾
∈ ℕ) → (2↑(2 pCnt 𝐾)) ∥ 𝐾) |
5 | 1, 4 | mpan 702 |
. . 3
⊢ (𝐾 ∈ ℕ →
(2↑(2 pCnt 𝐾)) ∥
𝐾) |
6 | | id 22 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ) |
7 | | 2nn 11062 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ → 2 ∈
ℕ) |
9 | 1 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ → 2 ∈
ℙ) |
10 | 9, 6 | pccld 15393 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ → (2 pCnt
𝐾) ∈
ℕ0) |
11 | 8, 10 | nnexpcld 12892 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ →
(2↑(2 pCnt 𝐾)) ∈
ℕ) |
12 | 6, 11 | jca 553 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ → (𝐾 ∈ ℕ ∧ (2↑(2
pCnt 𝐾)) ∈
ℕ)) |
13 | | nndivdvds 14827 |
. . . . . . 7
⊢ ((𝐾 ∈ ℕ ∧ (2↑(2
pCnt 𝐾)) ∈ ℕ)
→ ((2↑(2 pCnt 𝐾))
∥ 𝐾 ↔ (𝐾 / (2↑(2 pCnt 𝐾))) ∈
ℕ)) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (𝐾 ∈ ℕ →
((2↑(2 pCnt 𝐾))
∥ 𝐾 ↔ (𝐾 / (2↑(2 pCnt 𝐾))) ∈
ℕ)) |
15 | 14 | adantr 480 |
. . . . 5
⊢ ((𝐾 ∈ ℕ ∧ ¬ 2
∥ (𝐾 / (2↑(2
pCnt 𝐾)))) →
((2↑(2 pCnt 𝐾))
∥ 𝐾 ↔ (𝐾 / (2↑(2 pCnt 𝐾))) ∈
ℕ)) |
16 | | elnn1uz2 11641 |
. . . . . . 7
⊢ ((𝐾 / (2↑(2 pCnt 𝐾))) ∈ ℕ ↔
((𝐾 / (2↑(2 pCnt 𝐾))) = 1 ∨ (𝐾 / (2↑(2 pCnt 𝐾))) ∈
(ℤ≥‘2))) |
17 | | nncn 10905 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℂ) |
18 | | nncn 10905 |
. . . . . . . . . . . . . . 15
⊢
((2↑(2 pCnt 𝐾))
∈ ℕ → (2↑(2 pCnt 𝐾)) ∈ ℂ) |
19 | | nnne0 10930 |
. . . . . . . . . . . . . . 15
⊢
((2↑(2 pCnt 𝐾))
∈ ℕ → (2↑(2 pCnt 𝐾)) ≠ 0) |
20 | 18, 19 | jca 553 |
. . . . . . . . . . . . . 14
⊢
((2↑(2 pCnt 𝐾))
∈ ℕ → ((2↑(2 pCnt 𝐾)) ∈ ℂ ∧ (2↑(2 pCnt
𝐾)) ≠
0)) |
21 | 11, 20 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ →
((2↑(2 pCnt 𝐾)) ∈
ℂ ∧ (2↑(2 pCnt 𝐾)) ≠ 0)) |
22 | | 3anass 1035 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℂ ∧ (2↑(2
pCnt 𝐾)) ∈ ℂ
∧ (2↑(2 pCnt 𝐾))
≠ 0) ↔ (𝐾 ∈
ℂ ∧ ((2↑(2 pCnt 𝐾)) ∈ ℂ ∧ (2↑(2 pCnt
𝐾)) ≠
0))) |
23 | 17, 21, 22 | sylanbrc 695 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ → (𝐾 ∈ ℂ ∧ (2↑(2
pCnt 𝐾)) ∈ ℂ
∧ (2↑(2 pCnt 𝐾))
≠ 0)) |
24 | 23 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ ∧ ¬ 2
∥ (𝐾 / (2↑(2
pCnt 𝐾)))) → (𝐾 ∈ ℂ ∧ (2↑(2
pCnt 𝐾)) ∈ ℂ
∧ (2↑(2 pCnt 𝐾))
≠ 0)) |
25 | | diveq1 10597 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℂ ∧ (2↑(2
pCnt 𝐾)) ∈ ℂ
∧ (2↑(2 pCnt 𝐾))
≠ 0) → ((𝐾 /
(2↑(2 pCnt 𝐾))) = 1
↔ 𝐾 = (2↑(2 pCnt
𝐾)))) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ ∧ ¬ 2
∥ (𝐾 / (2↑(2
pCnt 𝐾)))) → ((𝐾 / (2↑(2 pCnt 𝐾))) = 1 ↔ 𝐾 = (2↑(2 pCnt 𝐾)))) |
27 | 10 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ ∧ 𝐾 = (2↑(2 pCnt 𝐾))) → (2 pCnt 𝐾) ∈
ℕ0) |
28 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (2 pCnt 𝐾) → (2↑𝑛) = (2↑(2 pCnt 𝐾))) |
29 | 28 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (2 pCnt 𝐾) → (𝐾 = (2↑𝑛) ↔ 𝐾 = (2↑(2 pCnt 𝐾)))) |
30 | 29 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ ℕ ∧ 𝐾 = (2↑(2 pCnt 𝐾))) ∧ 𝑛 = (2 pCnt 𝐾)) → (𝐾 = (2↑𝑛) ↔ 𝐾 = (2↑(2 pCnt 𝐾)))) |
31 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ ∧ 𝐾 = (2↑(2 pCnt 𝐾))) → 𝐾 = (2↑(2 pCnt 𝐾))) |
32 | 27, 30, 31 | rspcedvd 3289 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ ∧ 𝐾 = (2↑(2 pCnt 𝐾))) → ∃𝑛 ∈ ℕ0
𝐾 = (2↑𝑛)) |
33 | 32 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ → (𝐾 = (2↑(2 pCnt 𝐾)) → ∃𝑛 ∈ ℕ0
𝐾 = (2↑𝑛))) |
34 | | pm2.24 120 |
. . . . . . . . . . . 12
⊢
(∃𝑛 ∈
ℕ0 𝐾 =
(2↑𝑛) → (¬
∃𝑛 ∈
ℕ0 𝐾 =
(2↑𝑛) →
∃𝑝 ∈ (ℙ
∖ {2})𝑝 ∥ 𝐾)) |
35 | 33, 34 | syl6 34 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ → (𝐾 = (2↑(2 pCnt 𝐾)) → (¬ ∃𝑛 ∈ ℕ0
𝐾 = (2↑𝑛) → ∃𝑝 ∈ (ℙ ∖
{2})𝑝 ∥ 𝐾))) |
36 | 35 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ ∧ ¬ 2
∥ (𝐾 / (2↑(2
pCnt 𝐾)))) → (𝐾 = (2↑(2 pCnt 𝐾)) → (¬ ∃𝑛 ∈ ℕ0
𝐾 = (2↑𝑛) → ∃𝑝 ∈ (ℙ ∖
{2})𝑝 ∥ 𝐾))) |
37 | 26, 36 | sylbid 229 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ ∧ ¬ 2
∥ (𝐾 / (2↑(2
pCnt 𝐾)))) → ((𝐾 / (2↑(2 pCnt 𝐾))) = 1 → (¬
∃𝑛 ∈
ℕ0 𝐾 =
(2↑𝑛) →
∃𝑝 ∈ (ℙ
∖ {2})𝑝 ∥ 𝐾))) |
38 | 37 | com12 32 |
. . . . . . . 8
⊢ ((𝐾 / (2↑(2 pCnt 𝐾))) = 1 → ((𝐾 ∈ ℕ ∧ ¬ 2
∥ (𝐾 / (2↑(2
pCnt 𝐾)))) → (¬
∃𝑛 ∈
ℕ0 𝐾 =
(2↑𝑛) →
∃𝑝 ∈ (ℙ
∖ {2})𝑝 ∥ 𝐾))) |
39 | | exprmfct 15254 |
. . . . . . . . 9
⊢ ((𝐾 / (2↑(2 pCnt 𝐾))) ∈
(ℤ≥‘2) → ∃𝑞 ∈ ℙ 𝑞 ∥ (𝐾 / (2↑(2 pCnt 𝐾)))) |
40 | | breq1 4586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 = 2 → (𝑞 ∥ (𝐾 / (2↑(2 pCnt 𝐾))) ↔ 2 ∥ (𝐾 / (2↑(2 pCnt 𝐾))))) |
41 | 40 | biimpcd 238 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞 ∥ (𝐾 / (2↑(2 pCnt 𝐾))) → (𝑞 = 2 → 2 ∥ (𝐾 / (2↑(2 pCnt 𝐾))))) |
42 | 41 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑞 ∥ (𝐾 / (2↑(2 pCnt 𝐾)))) → (𝑞 = 2 → 2 ∥ (𝐾 / (2↑(2 pCnt 𝐾))))) |
43 | 42 | necon3bd 2796 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑞 ∥ (𝐾 / (2↑(2 pCnt 𝐾)))) → (¬ 2 ∥ (𝐾 / (2↑(2 pCnt 𝐾))) → 𝑞 ≠ 2)) |
44 | 43 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ (𝐾 / (2↑(2 pCnt 𝐾))) → (¬ 2 ∥ (𝐾 / (2↑(2 pCnt 𝐾))) → 𝑞 ≠ 2))) |
45 | | prmnn 15226 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℕ) |
46 | 5, 14 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ℕ → (𝐾 / (2↑(2 pCnt 𝐾))) ∈
ℕ) |
47 | | nndivides 14828 |
. . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℕ ∧ (𝐾 / (2↑(2 pCnt 𝐾))) ∈ ℕ) →
(𝑞 ∥ (𝐾 / (2↑(2 pCnt 𝐾))) ↔ ∃𝑚 ∈ ℕ (𝑚 · 𝑞) = (𝐾 / (2↑(2 pCnt 𝐾))))) |
48 | 45, 46, 47 | syl2anr 494 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ (𝐾 / (2↑(2 pCnt 𝐾))) ↔ ∃𝑚 ∈ ℕ (𝑚 · 𝑞) = (𝐾 / (2↑(2 pCnt 𝐾))))) |
49 | | eqcom 2617 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 · 𝑞) = (𝐾 / (2↑(2 pCnt 𝐾))) ↔ (𝐾 / (2↑(2 pCnt 𝐾))) = (𝑚 · 𝑞)) |
50 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) → 𝐾 ∈
ℂ) |
51 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) → 𝐾 ∈
ℂ) |
52 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈
ℕ) |
53 | 45 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) → 𝑞 ∈
ℕ) |
54 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) → 𝑞 ∈
ℕ) |
55 | 52, 54 | nnmulcld 10945 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) → (𝑚 · 𝑞) ∈ ℕ) |
56 | 55 | nncnd 10913 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) → (𝑚 · 𝑞) ∈ ℂ) |
57 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) →
(2↑(2 pCnt 𝐾)) ∈
ℕ) |
58 | 57 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) →
(2↑(2 pCnt 𝐾)) ∈
ℕ) |
59 | 58, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) →
((2↑(2 pCnt 𝐾)) ∈
ℂ ∧ (2↑(2 pCnt 𝐾)) ≠ 0)) |
60 | 51, 56, 59 | 3jca 1235 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) → (𝐾 ∈ ℂ ∧ (𝑚 · 𝑞) ∈ ℂ ∧ ((2↑(2 pCnt 𝐾)) ∈ ℂ ∧
(2↑(2 pCnt 𝐾)) ≠
0))) |
61 | | divmul 10567 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℂ ∧ (𝑚 · 𝑞) ∈ ℂ ∧ ((2↑(2 pCnt 𝐾)) ∈ ℂ ∧
(2↑(2 pCnt 𝐾)) ≠
0)) → ((𝐾 / (2↑(2
pCnt 𝐾))) = (𝑚 · 𝑞) ↔ ((2↑(2 pCnt 𝐾)) · (𝑚 · 𝑞)) = 𝐾)) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) → ((𝐾 / (2↑(2 pCnt 𝐾))) = (𝑚 · 𝑞) ↔ ((2↑(2 pCnt 𝐾)) · (𝑚 · 𝑞)) = 𝐾)) |
63 | 49, 62 | syl5bb 271 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) → ((𝑚 · 𝑞) = (𝐾 / (2↑(2 pCnt 𝐾))) ↔ ((2↑(2 pCnt 𝐾)) · (𝑚 · 𝑞)) = 𝐾)) |
64 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) → 𝑞 ∈
ℙ) |
65 | 64 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) → 𝑞 ∈
ℙ) |
66 | 65 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) ∧ 𝑞 ≠ 2) → (𝑞 ∈ ℙ ∧ 𝑞 ≠ 2)) |
67 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 ∈ (ℙ ∖ {2})
↔ (𝑞 ∈ ℙ
∧ 𝑞 ≠
2)) |
68 | 66, 67 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) ∧ 𝑞 ≠ 2) → 𝑞 ∈ (ℙ ∖
{2})) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐾 ∈
ℕ ∧ 𝑞 ∈
ℙ) ∧ 𝑚 ∈
ℕ) ∧ 𝑞 ≠ 2)
∧ ((2↑(2 pCnt 𝐾))
· (𝑚 · 𝑞)) = 𝐾) → 𝑞 ∈ (ℙ ∖
{2})) |
70 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = 𝑞 → (𝑝 ∥ 𝐾 ↔ 𝑞 ∥ 𝐾)) |
71 | 70 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐾 ∈
ℕ ∧ 𝑞 ∈
ℙ) ∧ 𝑚 ∈
ℕ) ∧ 𝑞 ≠ 2)
∧ ((2↑(2 pCnt 𝐾))
· (𝑚 · 𝑞)) = 𝐾) ∧ 𝑝 = 𝑞) → (𝑝 ∥ 𝐾 ↔ 𝑞 ∥ 𝐾)) |
72 | 58, 52 | nnmulcld 10945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) →
((2↑(2 pCnt 𝐾))
· 𝑚) ∈
ℕ) |
73 | 72 | nnzd 11357 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) →
((2↑(2 pCnt 𝐾))
· 𝑚) ∈
ℤ) |
74 | 45 | nnzd 11357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℤ) |
75 | 74 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) → 𝑞 ∈
ℤ) |
76 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) → 𝑞 ∈
ℤ) |
77 | 73, 76 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) →
(((2↑(2 pCnt 𝐾))
· 𝑚) ∈ ℤ
∧ 𝑞 ∈
ℤ)) |
78 | 77 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) ∧ 𝑞 ≠ 2) → (((2↑(2
pCnt 𝐾)) · 𝑚) ∈ ℤ ∧ 𝑞 ∈
ℤ)) |
79 | | dvdsmul2 14842 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((2↑(2 pCnt 𝐾)) · 𝑚) ∈ ℤ ∧ 𝑞 ∈ ℤ) → 𝑞 ∥ (((2↑(2 pCnt 𝐾)) · 𝑚) · 𝑞)) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) ∧ 𝑞 ≠ 2) → 𝑞 ∥ (((2↑(2 pCnt 𝐾)) · 𝑚) · 𝑞)) |
81 | | 2nn0 11186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 2 ∈
ℕ0 |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐾 ∈ ℕ → 2 ∈
ℕ0) |
83 | 82, 10 | nn0expcld 12893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐾 ∈ ℕ →
(2↑(2 pCnt 𝐾)) ∈
ℕ0) |
84 | 83 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) →
(2↑(2 pCnt 𝐾)) ∈
ℕ0) |
85 | 84 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) →
(2↑(2 pCnt 𝐾)) ∈
ℕ0) |
86 | 85 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) →
(2↑(2 pCnt 𝐾)) ∈
ℂ) |
87 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
88 | 87 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈
ℂ) |
89 | 45 | nncnd 10913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℂ) |
90 | 89 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) → 𝑞 ∈
ℂ) |
91 | 90 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) → 𝑞 ∈
ℂ) |
92 | 86, 88, 91 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) →
((2↑(2 pCnt 𝐾)) ∈
ℂ ∧ 𝑚 ∈
ℂ ∧ 𝑞 ∈
ℂ)) |
93 | 92 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) ∧ 𝑞 ≠ 2) → ((2↑(2 pCnt
𝐾)) ∈ ℂ ∧
𝑚 ∈ ℂ ∧
𝑞 ∈
ℂ)) |
94 | | mulass 9903 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((2↑(2 pCnt 𝐾)) ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑞 ∈ ℂ) → (((2↑(2 pCnt
𝐾)) · 𝑚) · 𝑞) = ((2↑(2 pCnt 𝐾)) · (𝑚 · 𝑞))) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) ∧ 𝑞 ≠ 2) → (((2↑(2
pCnt 𝐾)) · 𝑚) · 𝑞) = ((2↑(2 pCnt 𝐾)) · (𝑚 · 𝑞))) |
96 | 80, 95 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) ∧ 𝑞 ≠ 2) → 𝑞 ∥ ((2↑(2 pCnt 𝐾)) · (𝑚 · 𝑞))) |
97 | 96 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐾 ∈
ℕ ∧ 𝑞 ∈
ℙ) ∧ 𝑚 ∈
ℕ) ∧ 𝑞 ≠ 2)
∧ ((2↑(2 pCnt 𝐾))
· (𝑚 · 𝑞)) = 𝐾) → 𝑞 ∥ ((2↑(2 pCnt 𝐾)) · (𝑚 · 𝑞))) |
98 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((2↑(2 pCnt 𝐾)) · (𝑚 · 𝑞)) = 𝐾 → (𝑞 ∥ ((2↑(2 pCnt 𝐾)) · (𝑚 · 𝑞)) ↔ 𝑞 ∥ 𝐾)) |
99 | 98 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐾 ∈
ℕ ∧ 𝑞 ∈
ℙ) ∧ 𝑚 ∈
ℕ) ∧ 𝑞 ≠ 2)
∧ ((2↑(2 pCnt 𝐾))
· (𝑚 · 𝑞)) = 𝐾) → (𝑞 ∥ ((2↑(2 pCnt 𝐾)) · (𝑚 · 𝑞)) ↔ 𝑞 ∥ 𝐾)) |
100 | 97, 99 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐾 ∈
ℕ ∧ 𝑞 ∈
ℙ) ∧ 𝑚 ∈
ℕ) ∧ 𝑞 ≠ 2)
∧ ((2↑(2 pCnt 𝐾))
· (𝑚 · 𝑞)) = 𝐾) → 𝑞 ∥ 𝐾) |
101 | 69, 71, 100 | rspcedvd 3289 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐾 ∈
ℕ ∧ 𝑞 ∈
ℙ) ∧ 𝑚 ∈
ℕ) ∧ 𝑞 ≠ 2)
∧ ((2↑(2 pCnt 𝐾))
· (𝑚 · 𝑞)) = 𝐾) → ∃𝑝 ∈ (ℙ ∖ {2})𝑝 ∥ 𝐾) |
102 | 101 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐾 ∈
ℕ ∧ 𝑞 ∈
ℙ) ∧ 𝑚 ∈
ℕ) ∧ 𝑞 ≠ 2)
∧ ((2↑(2 pCnt 𝐾))
· (𝑚 · 𝑞)) = 𝐾) → (¬ ∃𝑛 ∈ ℕ0 𝐾 = (2↑𝑛) → ∃𝑝 ∈ (ℙ ∖ {2})𝑝 ∥ 𝐾)) |
103 | 102 | exp31 628 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) → (𝑞 ≠ 2 → (((2↑(2 pCnt
𝐾)) · (𝑚 · 𝑞)) = 𝐾 → (¬ ∃𝑛 ∈ ℕ0 𝐾 = (2↑𝑛) → ∃𝑝 ∈ (ℙ ∖ {2})𝑝 ∥ 𝐾)))) |
104 | 103 | com23 84 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) →
(((2↑(2 pCnt 𝐾))
· (𝑚 · 𝑞)) = 𝐾 → (𝑞 ≠ 2 → (¬ ∃𝑛 ∈ ℕ0
𝐾 = (2↑𝑛) → ∃𝑝 ∈ (ℙ ∖
{2})𝑝 ∥ 𝐾)))) |
105 | 63, 104 | sylbid 229 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) ∧ 𝑚 ∈ ℕ) → ((𝑚 · 𝑞) = (𝐾 / (2↑(2 pCnt 𝐾))) → (𝑞 ≠ 2 → (¬ ∃𝑛 ∈ ℕ0
𝐾 = (2↑𝑛) → ∃𝑝 ∈ (ℙ ∖
{2})𝑝 ∥ 𝐾)))) |
106 | 105 | rexlimdva 3013 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) →
(∃𝑚 ∈ ℕ
(𝑚 · 𝑞) = (𝐾 / (2↑(2 pCnt 𝐾))) → (𝑞 ≠ 2 → (¬ ∃𝑛 ∈ ℕ0
𝐾 = (2↑𝑛) → ∃𝑝 ∈ (ℙ ∖
{2})𝑝 ∥ 𝐾)))) |
107 | 48, 106 | sylbid 229 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ (𝐾 / (2↑(2 pCnt 𝐾))) → (𝑞 ≠ 2 → (¬ ∃𝑛 ∈ ℕ0
𝐾 = (2↑𝑛) → ∃𝑝 ∈ (ℙ ∖
{2})𝑝 ∥ 𝐾)))) |
108 | 44, 107 | syldd 70 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ (𝐾 / (2↑(2 pCnt 𝐾))) → (¬ 2 ∥ (𝐾 / (2↑(2 pCnt 𝐾))) → (¬ ∃𝑛 ∈ ℕ0
𝐾 = (2↑𝑛) → ∃𝑝 ∈ (ℙ ∖
{2})𝑝 ∥ 𝐾)))) |
109 | 108 | rexlimdva 3013 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ →
(∃𝑞 ∈ ℙ
𝑞 ∥ (𝐾 / (2↑(2 pCnt 𝐾))) → (¬ 2 ∥
(𝐾 / (2↑(2 pCnt 𝐾))) → (¬ ∃𝑛 ∈ ℕ0
𝐾 = (2↑𝑛) → ∃𝑝 ∈ (ℙ ∖
{2})𝑝 ∥ 𝐾)))) |
110 | 109 | com12 32 |
. . . . . . . . . 10
⊢
(∃𝑞 ∈
ℙ 𝑞 ∥ (𝐾 / (2↑(2 pCnt 𝐾))) → (𝐾 ∈ ℕ → (¬ 2 ∥
(𝐾 / (2↑(2 pCnt 𝐾))) → (¬ ∃𝑛 ∈ ℕ0
𝐾 = (2↑𝑛) → ∃𝑝 ∈ (ℙ ∖
{2})𝑝 ∥ 𝐾)))) |
111 | 110 | impd 446 |
. . . . . . . . 9
⊢
(∃𝑞 ∈
ℙ 𝑞 ∥ (𝐾 / (2↑(2 pCnt 𝐾))) → ((𝐾 ∈ ℕ ∧ ¬ 2 ∥ (𝐾 / (2↑(2 pCnt 𝐾)))) → (¬ ∃𝑛 ∈ ℕ0
𝐾 = (2↑𝑛) → ∃𝑝 ∈ (ℙ ∖
{2})𝑝 ∥ 𝐾))) |
112 | 39, 111 | syl 17 |
. . . . . . . 8
⊢ ((𝐾 / (2↑(2 pCnt 𝐾))) ∈
(ℤ≥‘2) → ((𝐾 ∈ ℕ ∧ ¬ 2 ∥ (𝐾 / (2↑(2 pCnt 𝐾)))) → (¬ ∃𝑛 ∈ ℕ0
𝐾 = (2↑𝑛) → ∃𝑝 ∈ (ℙ ∖
{2})𝑝 ∥ 𝐾))) |
113 | 38, 112 | jaoi 393 |
. . . . . . 7
⊢ (((𝐾 / (2↑(2 pCnt 𝐾))) = 1 ∨ (𝐾 / (2↑(2 pCnt 𝐾))) ∈ (ℤ≥‘2))
→ ((𝐾 ∈ ℕ
∧ ¬ 2 ∥ (𝐾 /
(2↑(2 pCnt 𝐾))))
→ (¬ ∃𝑛
∈ ℕ0 𝐾 = (2↑𝑛) → ∃𝑝 ∈ (ℙ ∖ {2})𝑝 ∥ 𝐾))) |
114 | 16, 113 | sylbi 206 |
. . . . . 6
⊢ ((𝐾 / (2↑(2 pCnt 𝐾))) ∈ ℕ →
((𝐾 ∈ ℕ ∧
¬ 2 ∥ (𝐾 /
(2↑(2 pCnt 𝐾))))
→ (¬ ∃𝑛
∈ ℕ0 𝐾 = (2↑𝑛) → ∃𝑝 ∈ (ℙ ∖ {2})𝑝 ∥ 𝐾))) |
115 | 114 | com12 32 |
. . . . 5
⊢ ((𝐾 ∈ ℕ ∧ ¬ 2
∥ (𝐾 / (2↑(2
pCnt 𝐾)))) → ((𝐾 / (2↑(2 pCnt 𝐾))) ∈ ℕ → (¬
∃𝑛 ∈
ℕ0 𝐾 =
(2↑𝑛) →
∃𝑝 ∈ (ℙ
∖ {2})𝑝 ∥ 𝐾))) |
116 | 15, 115 | sylbid 229 |
. . . 4
⊢ ((𝐾 ∈ ℕ ∧ ¬ 2
∥ (𝐾 / (2↑(2
pCnt 𝐾)))) →
((2↑(2 pCnt 𝐾))
∥ 𝐾 → (¬
∃𝑛 ∈
ℕ0 𝐾 =
(2↑𝑛) →
∃𝑝 ∈ (ℙ
∖ {2})𝑝 ∥ 𝐾))) |
117 | 116 | ex 449 |
. . 3
⊢ (𝐾 ∈ ℕ → (¬ 2
∥ (𝐾 / (2↑(2
pCnt 𝐾))) →
((2↑(2 pCnt 𝐾))
∥ 𝐾 → (¬
∃𝑛 ∈
ℕ0 𝐾 =
(2↑𝑛) →
∃𝑝 ∈ (ℙ
∖ {2})𝑝 ∥ 𝐾)))) |
118 | 3, 5, 117 | mp2d 47 |
. 2
⊢ (𝐾 ∈ ℕ → (¬
∃𝑛 ∈
ℕ0 𝐾 =
(2↑𝑛) →
∃𝑝 ∈ (ℙ
∖ {2})𝑝 ∥ 𝐾)) |
119 | 118 | imp 444 |
1
⊢ ((𝐾 ∈ ℕ ∧ ¬
∃𝑛 ∈
ℕ0 𝐾 =
(2↑𝑛)) →
∃𝑝 ∈ (ℙ
∖ {2})𝑝 ∥ 𝐾) |