This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pcprmpw2

Description: Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Assertion pcprmpw2 ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ↔ 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 simplr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → 𝐴 ∈ ℕ )
2 1 nnnn0d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → 𝐴 ∈ ℕ0 )
3 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
4 3 ad2antrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → 𝑃 ∈ ℕ )
5 pccl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 )
6 5 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 )
7 4 6 nnexpcld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℕ )
8 7 nnnn0d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℕ0 )
9 6 nn0red ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 pCnt 𝐴 ) ∈ ℝ )
10 9 leidd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐴 ) )
11 simpll ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → 𝑃 ∈ ℙ )
12 6 nn0zd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 pCnt 𝐴 ) ∈ ℤ )
13 pcid ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 pCnt 𝐴 ) ∈ ℤ ) → ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) = ( 𝑃 pCnt 𝐴 ) )
14 11 12 13 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) = ( 𝑃 pCnt 𝐴 ) )
15 10 14 breqtrrd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
16 15 ad2antrr ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 = 𝑃 ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
17 simpr ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 = 𝑃 ) → 𝑝 = 𝑃 )
18 17 oveq1d ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 = 𝑃 ) → ( 𝑝 pCnt 𝐴 ) = ( 𝑃 pCnt 𝐴 ) )
19 17 oveq1d ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 = 𝑃 ) → ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) = ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
20 16 18 19 3brtr4d ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 = 𝑃 ) → ( 𝑝 pCnt 𝐴 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
21 simplrr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) )
22 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
23 22 adantl ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℤ )
24 1 adantr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∈ ℕ )
25 24 nnzd ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∈ ℤ )
26 simprl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → 𝑛 ∈ ℕ0 )
27 4 26 nnexpcld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ 𝑛 ) ∈ ℕ )
28 27 adantr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑃 ↑ 𝑛 ) ∈ ℕ )
29 28 nnzd ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑃 ↑ 𝑛 ) ∈ ℤ )
30 dvdstr ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ( 𝑃 ↑ 𝑛 ) ∈ ℤ ) → ( ( 𝑝 ∥ 𝐴 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) → 𝑝 ∥ ( 𝑃 ↑ 𝑛 ) ) )
31 23 25 29 30 syl3anc ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ 𝐴 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) → 𝑝 ∥ ( 𝑃 ↑ 𝑛 ) ) )
32 21 31 mpan2d ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ 𝐴 → 𝑝 ∥ ( 𝑃 ↑ 𝑛 ) ) )
33 simpr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
34 11 adantr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) → 𝑃 ∈ ℙ )
35 simplrl ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) → 𝑛 ∈ ℕ0 )
36 prmdvdsexpr ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑝 ∥ ( 𝑃 ↑ 𝑛 ) → 𝑝 = 𝑃 ) )
37 33 34 35 36 syl3anc ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( 𝑃 ↑ 𝑛 ) → 𝑝 = 𝑃 ) )
38 32 37 syld ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ 𝐴 → 𝑝 = 𝑃 ) )
39 38 necon3ad ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ≠ 𝑃 → ¬ 𝑝 ∥ 𝐴 ) )
40 39 imp ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → ¬ 𝑝 ∥ 𝐴 )
41 simplr ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → 𝑝 ∈ ℙ )
42 1 ad2antrr ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → 𝐴 ∈ ℕ )
43 pceq0 ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ( 𝑝 pCnt 𝐴 ) = 0 ↔ ¬ 𝑝 ∥ 𝐴 ) )
44 41 42 43 syl2anc ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → ( ( 𝑝 pCnt 𝐴 ) = 0 ↔ ¬ 𝑝 ∥ 𝐴 ) )
45 40 44 mpbird ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → ( 𝑝 pCnt 𝐴 ) = 0 )
46 7 ad2antrr ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℕ )
47 41 46 pccld ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ0 )
48 47 nn0ge0d ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → 0 ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
49 45 48 eqbrtrd ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → ( 𝑝 pCnt 𝐴 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
50 20 49 pm2.61dane ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐴 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
51 50 ralrimiva ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
52 1 nnzd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → 𝐴 ∈ ℤ )
53 7 nnzd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℤ )
54 pc2dvds ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℤ ) → ( 𝐴 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
55 52 53 54 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝐴 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
56 51 55 mpbird ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → 𝐴 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
57 pcdvds ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 )
58 57 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 )
59 dvdseq ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℕ0 ) ∧ ( 𝐴 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 ) ) → 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
60 2 8 56 58 59 syl22anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) ) → 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
61 60 rexlimdvaa ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) → 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
62 3 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → 𝑃 ∈ ℕ )
63 62 5 nnexpcld ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℕ )
64 63 nnzd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℤ )
65 iddvds ⊢ ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℤ → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
66 64 65 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
67 oveq2 ⊢ ( 𝑛 = ( 𝑃 pCnt 𝐴 ) → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
68 67 breq2d ⊢ ( 𝑛 = ( 𝑃 pCnt 𝐴 ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ ( 𝑃 ↑ 𝑛 ) ↔ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
69 68 rspcev ⊢ ( ( ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) → ∃ 𝑛 ∈ ℕ0 ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ ( 𝑃 ↑ 𝑛 ) )
70 5 66 69 syl2anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ∃ 𝑛 ∈ ℕ0 ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ ( 𝑃 ↑ 𝑛 ) )
71 breq1 ⊢ ( 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) → ( 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ↔ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ ( 𝑃 ↑ 𝑛 ) ) )
72 71 rexbidv ⊢ ( 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) → ( ∃ 𝑛 ∈ ℕ0 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ0 ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ ( 𝑃 ↑ 𝑛 ) ) )
73 70 72 syl5ibrcom ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) → ∃ 𝑛 ∈ ℕ0 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) )
74 61 73 impbid ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ↔ 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )