Metamath Proof Explorer

Theorem pcdvdsb

Description: P ^ A divides N if and only if A is at most the count of P . (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion pcdvdsb ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → ( 𝐴 ≤ ( 𝑃 pCnt 𝑁 ) ↔ ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑁 = 0 → ( 𝑃 pCnt 𝑁 ) = ( 𝑃 pCnt 0 ) )
2 1 breq2d ⊢ ( 𝑁 = 0 → ( 𝐴 ≤ ( 𝑃 pCnt 𝑁 ) ↔ 𝐴 ≤ ( 𝑃 pCnt 0 ) ) )
3 breq2 ⊢ ( 𝑁 = 0 → ( ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ↔ ( 𝑃 ↑ 𝐴 ) ∥ 0 ) )
4 2 3 bibi12d ⊢ ( 𝑁 = 0 → ( ( 𝐴 ≤ ( 𝑃 pCnt 𝑁 ) ↔ ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) ↔ ( 𝐴 ≤ ( 𝑃 pCnt 0 ) ↔ ( 𝑃 ↑ 𝐴 ) ∥ 0 ) ) )
5 simpl3 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → 𝐴 ∈ ℕ0 )
6 5 nn0zd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → 𝐴 ∈ ℤ )
7 simpl1 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → 𝑃 ∈ ℙ )
8 simpl2 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → 𝑁 ∈ ℤ )
9 simpr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → 𝑁 ≠ 0 )
10 pczcl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 )
11 7 8 9 10 syl12anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 )
12 11 nn0zd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( 𝑃 pCnt 𝑁 ) ∈ ℤ )
13 eluz ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑃 pCnt 𝑁 ) ∈ ℤ ) → ( ( 𝑃 pCnt 𝑁 ) ∈ ( ℤ≥ ‘ 𝐴 ) ↔ 𝐴 ≤ ( 𝑃 pCnt 𝑁 ) ) )
14 6 12 13 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( ( 𝑃 pCnt 𝑁 ) ∈ ( ℤ≥ ‘ 𝐴 ) ↔ 𝐴 ≤ ( 𝑃 pCnt 𝑁 ) ) )
15 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
16 7 15 syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → 𝑃 ∈ ℕ )
17 16 nnzd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → 𝑃 ∈ ℤ )
18 dvdsexp ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ∧ ( 𝑃 pCnt 𝑁 ) ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝑃 ↑ 𝐴 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) )
19 18 3expia ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑃 pCnt 𝑁 ) ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝑃 ↑ 𝐴 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
20 17 5 19 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( ( 𝑃 pCnt 𝑁 ) ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝑃 ↑ 𝐴 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
21 14 20 sylbird ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( 𝐴 ≤ ( 𝑃 pCnt 𝑁 ) → ( 𝑃 ↑ 𝐴 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
22 pczdvds ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∥ 𝑁 )
23 7 8 9 22 syl12anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∥ 𝑁 )
24 nnexpcl ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 ↑ 𝐴 ) ∈ ℕ )
25 15 24 sylan ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 ↑ 𝐴 ) ∈ ℕ )
26 25 3adant2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 ↑ 𝐴 ) ∈ ℕ )
27 26 nnzd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 ↑ 𝐴 ) ∈ ℤ )
28 27 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( 𝑃 ↑ 𝐴 ) ∈ ℤ )
29 16 11 nnexpcld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∈ ℕ )
30 29 nnzd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∈ ℤ )
31 dvdstr ⊢ ( ( ( 𝑃 ↑ 𝐴 ) ∈ ℤ ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑃 ↑ 𝐴 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∥ 𝑁 ) → ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) )
32 28 30 8 31 syl3anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( ( ( 𝑃 ↑ 𝐴 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∥ 𝑁 ) → ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) )
33 23 32 mpan2d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( ( 𝑃 ↑ 𝐴 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) → ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) )
34 21 33 syld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( 𝐴 ≤ ( 𝑃 pCnt 𝑁 ) → ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) )
35 nn0re ⊢ ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 → ( 𝑃 pCnt 𝑁 ) ∈ ℝ )
36 nn0re ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
37 ltnle ⊢ ( ( ( 𝑃 pCnt 𝑁 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑃 pCnt 𝑁 ) < 𝐴 ↔ ¬ 𝐴 ≤ ( 𝑃 pCnt 𝑁 ) ) )
38 35 36 37 syl2an ⊢ ( ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑃 pCnt 𝑁 ) < 𝐴 ↔ ¬ 𝐴 ≤ ( 𝑃 pCnt 𝑁 ) ) )
39 nn0ltp1le ⊢ ( ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑃 pCnt 𝑁 ) < 𝐴 ↔ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ≤ 𝐴 ) )
40 38 39 bitr3d ⊢ ( ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ¬ 𝐴 ≤ ( 𝑃 pCnt 𝑁 ) ↔ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ≤ 𝐴 ) )
41 11 5 40 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( ¬ 𝐴 ≤ ( 𝑃 pCnt 𝑁 ) ↔ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ≤ 𝐴 ) )
42 peano2nn0 ⊢ ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 → ( ( 𝑃 pCnt 𝑁 ) + 1 ) ∈ ℕ0 )
43 11 42 syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( ( 𝑃 pCnt 𝑁 ) + 1 ) ∈ ℕ0 )
44 43 nn0zd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( ( 𝑃 pCnt 𝑁 ) + 1 ) ∈ ℤ )
45 eluz ⊢ ( ( ( ( 𝑃 pCnt 𝑁 ) + 1 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ∈ ( ℤ≥ ‘ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ↔ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ≤ 𝐴 ) )
46 44 6 45 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( 𝐴 ∈ ( ℤ≥ ‘ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ↔ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ≤ 𝐴 ) )
47 dvdsexp ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ) → ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝐴 ) )
48 47 3expia ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ∈ ℕ0 ) → ( 𝐴 ∈ ( ℤ≥ ‘ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) → ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝐴 ) ) )
49 17 43 48 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( 𝐴 ∈ ( ℤ≥ ‘ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) → ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝐴 ) ) )
50 46 49 sylbird ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( ( ( 𝑃 pCnt 𝑁 ) + 1 ) ≤ 𝐴 → ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝐴 ) ) )
51 pczndvds ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∥ 𝑁 )
52 7 8 9 51 syl12anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ¬ ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∥ 𝑁 )
53 16 43 nnexpcld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∈ ℕ )
54 53 nnzd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∈ ℤ )
55 dvdstr ⊢ ( ( ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∈ ℤ ∧ ( 𝑃 ↑ 𝐴 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝐴 ) ∧ ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) → ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∥ 𝑁 ) )
56 54 28 8 55 syl3anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( ( ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝐴 ) ∧ ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) → ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∥ 𝑁 ) )
57 52 56 mtod ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ¬ ( ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝐴 ) ∧ ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) )
58 imnan ⊢ ( ( ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝐴 ) → ¬ ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) ↔ ¬ ( ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝐴 ) ∧ ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) )
59 57 58 sylibr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( ( 𝑃 ↑ ( ( 𝑃 pCnt 𝑁 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝐴 ) → ¬ ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) )
60 50 59 syld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( ( ( 𝑃 pCnt 𝑁 ) + 1 ) ≤ 𝐴 → ¬ ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) )
61 41 60 sylbid ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( ¬ 𝐴 ≤ ( 𝑃 pCnt 𝑁 ) → ¬ ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) )
62 34 61 impcon4bid ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑁 ≠ 0 ) → ( 𝐴 ≤ ( 𝑃 pCnt 𝑁 ) ↔ ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) )
63 36 3ad2ant3 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
64 63 rexrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → 𝐴 ∈ ℝ* )
65 pnfge ⊢ ( 𝐴 ∈ ℝ* → 𝐴 ≤ +∞ )
66 64 65 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → 𝐴 ≤ +∞ )
67 pc0 ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 0 ) = +∞ )
68 67 3ad2ant1 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 pCnt 0 ) = +∞ )
69 66 68 breqtrrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → 𝐴 ≤ ( 𝑃 pCnt 0 ) )
70 dvds0 ⊢ ( ( 𝑃 ↑ 𝐴 ) ∈ ℤ → ( 𝑃 ↑ 𝐴 ) ∥ 0 )
71 27 70 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 ↑ 𝐴 ) ∥ 0 )
72 69 71 2thd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → ( 𝐴 ≤ ( 𝑃 pCnt 0 ) ↔ ( 𝑃 ↑ 𝐴 ) ∥ 0 ) )
73 4 62 72 pm2.61ne ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → ( 𝐴 ≤ ( 𝑃 pCnt 𝑁 ) ↔ ( 𝑃 ↑ 𝐴 ) ∥ 𝑁 ) )