Step |
Hyp |
Ref |
Expression |
1 |
|
isnsqf |
⊢ ( 𝐴 ∈ ℕ → ( ( μ ‘ 𝐴 ) = 0 ↔ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) ) |
2 |
1
|
necon3abid |
⊢ ( 𝐴 ∈ ℕ → ( ( μ ‘ 𝐴 ) ≠ 0 ↔ ¬ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) ) |
3 |
|
ralnex |
⊢ ( ∀ 𝑝 ∈ ℙ ¬ ( 𝑝 ↑ 2 ) ∥ 𝐴 ↔ ¬ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) |
4 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
5 |
|
pccl |
⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 ) |
6 |
5
|
ancoms |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 ) |
7 |
|
nn0ltp1le |
⊢ ( ( 1 ∈ ℕ0 ∧ ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 ) → ( 1 < ( 𝑝 pCnt 𝐴 ) ↔ ( 1 + 1 ) ≤ ( 𝑝 pCnt 𝐴 ) ) ) |
8 |
4 6 7
|
sylancr |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 1 < ( 𝑝 pCnt 𝐴 ) ↔ ( 1 + 1 ) ≤ ( 𝑝 pCnt 𝐴 ) ) ) |
9 |
|
1re |
⊢ 1 ∈ ℝ |
10 |
6
|
nn0red |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℝ ) |
11 |
|
ltnle |
⊢ ( ( 1 ∈ ℝ ∧ ( 𝑝 pCnt 𝐴 ) ∈ ℝ ) → ( 1 < ( 𝑝 pCnt 𝐴 ) ↔ ¬ ( 𝑝 pCnt 𝐴 ) ≤ 1 ) ) |
12 |
9 10 11
|
sylancr |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 1 < ( 𝑝 pCnt 𝐴 ) ↔ ¬ ( 𝑝 pCnt 𝐴 ) ≤ 1 ) ) |
13 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
14 |
13
|
breq1i |
⊢ ( 2 ≤ ( 𝑝 pCnt 𝐴 ) ↔ ( 1 + 1 ) ≤ ( 𝑝 pCnt 𝐴 ) ) |
15 |
|
id |
⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℙ ) |
16 |
|
nnz |
⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ ) |
17 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
18 |
|
pcdvdsb |
⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 2 ∈ ℕ0 ) → ( 2 ≤ ( 𝑝 pCnt 𝐴 ) ↔ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) ) |
19 |
17 18
|
mp3an3 |
⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 2 ≤ ( 𝑝 pCnt 𝐴 ) ↔ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) ) |
20 |
15 16 19
|
syl2anr |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 2 ≤ ( 𝑝 pCnt 𝐴 ) ↔ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) ) |
21 |
14 20
|
bitr3id |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( 1 + 1 ) ≤ ( 𝑝 pCnt 𝐴 ) ↔ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) ) |
22 |
8 12 21
|
3bitr3d |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ¬ ( 𝑝 pCnt 𝐴 ) ≤ 1 ↔ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) ) |
23 |
22
|
con1bid |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ¬ ( 𝑝 ↑ 2 ) ∥ 𝐴 ↔ ( 𝑝 pCnt 𝐴 ) ≤ 1 ) ) |
24 |
23
|
ralbidva |
⊢ ( 𝐴 ∈ ℕ → ( ∀ 𝑝 ∈ ℙ ¬ ( 𝑝 ↑ 2 ) ∥ 𝐴 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ 1 ) ) |
25 |
3 24
|
bitr3id |
⊢ ( 𝐴 ∈ ℕ → ( ¬ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ 1 ) ) |
26 |
2 25
|
bitrd |
⊢ ( 𝐴 ∈ ℕ → ( ( μ ‘ 𝐴 ) ≠ 0 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ 1 ) ) |