Metamath Proof Explorer

Theorem sylow1lem1

Description: Lemma for sylow1 . The p-adic valuation of the size of S is equal to the number of excess powers of P in ( #X ) / ( P ^ N ) . (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses sylow1.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
sylow1.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
sylow1.f ⊢ ( 𝜑 → 𝑋 ∈ Fin )
sylow1.p ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
sylow1.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
sylow1.d ⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
sylow1lem.a ⊢ + = ( +g ‘ 𝐺 )
sylow1lem.s ⊢ 𝑆 = { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) }
Assertion sylow1lem1 ( 𝜑 → ( ( ♯ ‘ 𝑆 ) ∈ ℕ ∧ ( 𝑃 pCnt ( ♯ ‘ 𝑆 ) ) = ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 sylow1.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 sylow1.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
3 sylow1.f ⊢ ( 𝜑 → 𝑋 ∈ Fin )
4 sylow1.p ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 sylow1.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6 sylow1.d ⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
7 sylow1lem.a ⊢ + = ( +g ‘ 𝐺 )
8 sylow1lem.s ⊢ 𝑆 = { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) }
9 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
10 4 9 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
11 10 5 nnexpcld ⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∈ ℕ )
12 11 nnzd ⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∈ ℤ )
13 hashbc ⊢ ( ( 𝑋 ∈ Fin ∧ ( 𝑃 ↑ 𝑁 ) ∈ ℤ ) → ( ( ♯ ‘ 𝑋 ) C ( 𝑃 ↑ 𝑁 ) ) = ( ♯ ‘ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ) )
14 3 12 13 syl2anc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) C ( 𝑃 ↑ 𝑁 ) ) = ( ♯ ‘ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ) )
15 8 fveq2i ⊢ ( ♯ ‘ 𝑆 ) = ( ♯ ‘ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } )
16 14 15 eqtr4di ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) C ( 𝑃 ↑ 𝑁 ) ) = ( ♯ ‘ 𝑆 ) )
17 1 grpbn0 ⊢ ( 𝐺 ∈ Grp → 𝑋 ≠ ∅ )
18 2 17 syl ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
19 hasheq0 ⊢ ( 𝑋 ∈ Fin → ( ( ♯ ‘ 𝑋 ) = 0 ↔ 𝑋 = ∅ ) )
20 3 19 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) = 0 ↔ 𝑋 = ∅ ) )
21 20 necon3bbid ⊢ ( 𝜑 → ( ¬ ( ♯ ‘ 𝑋 ) = 0 ↔ 𝑋 ≠ ∅ ) )
22 18 21 mpbird ⊢ ( 𝜑 → ¬ ( ♯ ‘ 𝑋 ) = 0 )
23 hashcl ⊢ ( 𝑋 ∈ Fin → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
24 3 23 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
25 elnn0 ⊢ ( ( ♯ ‘ 𝑋 ) ∈ ℕ0 ↔ ( ( ♯ ‘ 𝑋 ) ∈ ℕ ∨ ( ♯ ‘ 𝑋 ) = 0 ) )
26 24 25 sylib ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ∨ ( ♯ ‘ 𝑋 ) = 0 ) )
27 26 ord ⊢ ( 𝜑 → ( ¬ ( ♯ ‘ 𝑋 ) ∈ ℕ → ( ♯ ‘ 𝑋 ) = 0 ) )
28 22 27 mt3d ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℕ )
29 dvdsle ⊢ ( ( ( 𝑃 ↑ 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑋 ) ∈ ℕ ) → ( ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) → ( 𝑃 ↑ 𝑁 ) ≤ ( ♯ ‘ 𝑋 ) ) )
30 12 28 29 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) → ( 𝑃 ↑ 𝑁 ) ≤ ( ♯ ‘ 𝑋 ) ) )
31 6 30 mpd ⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ≤ ( ♯ ‘ 𝑋 ) )
32 11 nnnn0d ⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∈ ℕ0 )
33 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
34 32 33 eleqtrdi ⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∈ ( ℤ≥ ‘ 0 ) )
35 24 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℤ )
36 elfz5 ⊢ ( ( ( 𝑃 ↑ 𝑁 ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( ♯ ‘ 𝑋 ) ∈ ℤ ) → ( ( 𝑃 ↑ 𝑁 ) ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ↔ ( 𝑃 ↑ 𝑁 ) ≤ ( ♯ ‘ 𝑋 ) ) )
37 34 35 36 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑁 ) ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ↔ ( 𝑃 ↑ 𝑁 ) ≤ ( ♯ ‘ 𝑋 ) ) )
38 31 37 mpbird ⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) )
39 bccl2 ⊢ ( ( 𝑃 ↑ 𝑁 ) ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) → ( ( ♯ ‘ 𝑋 ) C ( 𝑃 ↑ 𝑁 ) ) ∈ ℕ )
40 38 39 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) C ( 𝑃 ↑ 𝑁 ) ) ∈ ℕ )
41 16 40 eqeltrrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ℕ )
42 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
43 11 42 eleqtrdi ⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) )
44 elfz5 ⊢ ( ( ( 𝑃 ↑ 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( ♯ ‘ 𝑋 ) ∈ ℤ ) → ( ( 𝑃 ↑ 𝑁 ) ∈ ( 1 ... ( ♯ ‘ 𝑋 ) ) ↔ ( 𝑃 ↑ 𝑁 ) ≤ ( ♯ ‘ 𝑋 ) ) )
45 43 35 44 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑁 ) ∈ ( 1 ... ( ♯ ‘ 𝑋 ) ) ↔ ( 𝑃 ↑ 𝑁 ) ≤ ( ♯ ‘ 𝑋 ) ) )
46 31 45 mpbird ⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∈ ( 1 ... ( ♯ ‘ 𝑋 ) ) )
47 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
48 fzsubel ⊢ ( ( ( 1 ∈ ℤ ∧ ( ♯ ‘ 𝑋 ) ∈ ℤ ) ∧ ( ( 𝑃 ↑ 𝑁 ) ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( ( 𝑃 ↑ 𝑁 ) ∈ ( 1 ... ( ♯ ‘ 𝑋 ) ) ↔ ( ( 𝑃 ↑ 𝑁 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( ( ♯ ‘ 𝑋 ) − 1 ) ) ) )
49 47 35 12 47 48 syl22anc ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑁 ) ∈ ( 1 ... ( ♯ ‘ 𝑋 ) ) ↔ ( ( 𝑃 ↑ 𝑁 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( ( ♯ ‘ 𝑋 ) − 1 ) ) ) )
50 46 49 mpbid ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑁 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( ( ♯ ‘ 𝑋 ) − 1 ) ) )
51 1m1e0 ⊢ ( 1 − 1 ) = 0
52 51 oveq1i ⊢ ( ( 1 − 1 ) ... ( ( ♯ ‘ 𝑋 ) − 1 ) ) = ( 0 ... ( ( ♯ ‘ 𝑋 ) − 1 ) )
53 50 52 eleqtrdi ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑁 ) − 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑋 ) − 1 ) ) )
54 bcp1nk ⊢ ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑋 ) − 1 ) ) → ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) + 1 ) C ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) + 1 ) ) = ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) · ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) + 1 ) / ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) + 1 ) ) ) )
55 53 54 syl ⊢ ( 𝜑 → ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) + 1 ) C ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) + 1 ) ) = ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) · ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) + 1 ) / ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) + 1 ) ) ) )
56 24 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℂ )
57 ax-1cn ⊢ 1 ∈ ℂ
58 npcan ⊢ ( ( ( ♯ ‘ 𝑋 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ♯ ‘ 𝑋 ) − 1 ) + 1 ) = ( ♯ ‘ 𝑋 ) )
59 56 57 58 sylancl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑋 ) − 1 ) + 1 ) = ( ♯ ‘ 𝑋 ) )
60 11 nncnd ⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∈ ℂ )
61 npcan ⊢ ( ( ( 𝑃 ↑ 𝑁 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) + 1 ) = ( 𝑃 ↑ 𝑁 ) )
62 60 57 61 sylancl ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) + 1 ) = ( 𝑃 ↑ 𝑁 ) )
63 59 62 oveq12d ⊢ ( 𝜑 → ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) + 1 ) C ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) + 1 ) ) = ( ( ♯ ‘ 𝑋 ) C ( 𝑃 ↑ 𝑁 ) ) )
64 59 62 oveq12d ⊢ ( 𝜑 → ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) + 1 ) / ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) + 1 ) ) = ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) )
65 64 oveq2d ⊢ ( 𝜑 → ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) · ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) + 1 ) / ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) + 1 ) ) ) = ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) · ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ) )
66 55 63 65 3eqtr3d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) C ( 𝑃 ↑ 𝑁 ) ) = ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) · ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ) )
67 66 oveq2d ⊢ ( 𝜑 → ( 𝑃 pCnt ( ( ♯ ‘ 𝑋 ) C ( 𝑃 ↑ 𝑁 ) ) ) = ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) · ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ) ) )
68 16 oveq2d ⊢ ( 𝜑 → ( 𝑃 pCnt ( ( ♯ ‘ 𝑋 ) C ( 𝑃 ↑ 𝑁 ) ) ) = ( 𝑃 pCnt ( ♯ ‘ 𝑆 ) ) )
69 bccl2 ⊢ ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑋 ) − 1 ) ) → ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ∈ ℕ )
70 53 69 syl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ∈ ℕ )
71 70 nnzd ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ∈ ℤ )
72 70 nnne0d ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ≠ 0 )
73 11 nnne0d ⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ≠ 0 )
74 dvdsval2 ⊢ ( ( ( 𝑃 ↑ 𝑁 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑁 ) ≠ 0 ∧ ( ♯ ‘ 𝑋 ) ∈ ℤ ) → ( ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) ↔ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ∈ ℤ ) )
75 12 73 35 74 syl3anc ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) ↔ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ∈ ℤ ) )
76 6 75 mpbid ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ∈ ℤ )
77 28 nnne0d ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ≠ 0 )
78 56 60 77 73 divne0d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ≠ 0 )
79 pcmul ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ∈ ℤ ∧ ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ≠ 0 ) ∧ ( ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) · ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ) ) = ( ( 𝑃 pCnt ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ) + ( 𝑃 pCnt ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ) ) )
80 4 71 72 76 78 79 syl122anc ⊢ ( 𝜑 → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) · ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ) ) = ( ( 𝑃 pCnt ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ) + ( 𝑃 pCnt ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ) ) )
81 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
82 56 60 81 npncand ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) = ( ( ♯ ‘ 𝑋 ) − 1 ) )
83 82 oveq1d ⊢ ( 𝜑 → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) = ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) )
84 83 oveq2d ⊢ ( 𝜑 → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ) = ( 𝑃 pCnt ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ) )
85 11 nnred ⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∈ ℝ )
86 85 ltm1d ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑁 ) − 1 ) < ( 𝑃 ↑ 𝑁 ) )
87 nnm1nn0 ⊢ ( ( 𝑃 ↑ 𝑁 ) ∈ ℕ → ( ( 𝑃 ↑ 𝑁 ) − 1 ) ∈ ℕ0 )
88 11 87 syl ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑁 ) − 1 ) ∈ ℕ0 )
89 breq1 ⊢ ( 𝑥 = 0 → ( 𝑥 < ( 𝑃 ↑ 𝑁 ) ↔ 0 < ( 𝑃 ↑ 𝑁 ) ) )
90 bcxmaslem1 ⊢ ( 𝑥 = 0 → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) = ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 0 ) C 0 ) )
91 90 oveq2d ⊢ ( 𝑥 = 0 → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 0 ) C 0 ) ) )
92 91 eqeq1d ⊢ ( 𝑥 = 0 → ( ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = 0 ↔ ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 0 ) C 0 ) ) = 0 ) )
93 89 92 imbi12d ⊢ ( 𝑥 = 0 → ( ( 𝑥 < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = 0 ) ↔ ( 0 < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 0 ) C 0 ) ) = 0 ) ) )
94 93 imbi2d ⊢ ( 𝑥 = 0 → ( ( 𝜑 → ( 𝑥 < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = 0 ) ) ↔ ( 𝜑 → ( 0 < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 0 ) C 0 ) ) = 0 ) ) ) )
95 breq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 < ( 𝑃 ↑ 𝑁 ) ↔ 𝑛 < ( 𝑃 ↑ 𝑁 ) ) )
96 bcxmaslem1 ⊢ ( 𝑥 = 𝑛 → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) = ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) )
97 96 oveq2d ⊢ ( 𝑥 = 𝑛 → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ) )
98 97 eqeq1d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = 0 ↔ ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ) = 0 ) )
99 95 98 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = 0 ) ↔ ( 𝑛 < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ) = 0 ) ) )
100 99 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝜑 → ( 𝑥 < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = 0 ) ) ↔ ( 𝜑 → ( 𝑛 < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ) = 0 ) ) ) )
101 breq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 < ( 𝑃 ↑ 𝑁 ) ↔ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) )
102 bcxmaslem1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) = ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) )
103 102 oveq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) )
104 103 eqeq1d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = 0 ↔ ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) = 0 ) )
105 101 104 imbi12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑥 < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = 0 ) ↔ ( ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) = 0 ) ) )
106 105 imbi2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝑥 < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = 0 ) ) ↔ ( 𝜑 → ( ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) = 0 ) ) ) )
107 breq1 ⊢ ( 𝑥 = ( ( 𝑃 ↑ 𝑁 ) − 1 ) → ( 𝑥 < ( 𝑃 ↑ 𝑁 ) ↔ ( ( 𝑃 ↑ 𝑁 ) − 1 ) < ( 𝑃 ↑ 𝑁 ) ) )
108 bcxmaslem1 ⊢ ( 𝑥 = ( ( 𝑃 ↑ 𝑁 ) − 1 ) → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) = ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) )
109 108 oveq2d ⊢ ( 𝑥 = ( ( 𝑃 ↑ 𝑁 ) − 1 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ) )
110 109 eqeq1d ⊢ ( 𝑥 = ( ( 𝑃 ↑ 𝑁 ) − 1 ) → ( ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = 0 ↔ ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ) = 0 ) )
111 107 110 imbi12d ⊢ ( 𝑥 = ( ( 𝑃 ↑ 𝑁 ) − 1 ) → ( ( 𝑥 < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = 0 ) ↔ ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ) = 0 ) ) )
112 111 imbi2d ⊢ ( 𝑥 = ( ( 𝑃 ↑ 𝑁 ) − 1 ) → ( ( 𝜑 → ( 𝑥 < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑥 ) C 𝑥 ) ) = 0 ) ) ↔ ( 𝜑 → ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ) = 0 ) ) ) )
113 znn0sub ⊢ ( ( ( 𝑃 ↑ 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑋 ) ∈ ℤ ) → ( ( 𝑃 ↑ 𝑁 ) ≤ ( ♯ ‘ 𝑋 ) ↔ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℕ0 ) )
114 12 35 113 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑁 ) ≤ ( ♯ ‘ 𝑋 ) ↔ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℕ0 ) )
115 31 114 mpbid ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℕ0 )
116 0nn0 ⊢ 0 ∈ ℕ0
117 nn0addcl ⊢ ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 0 ) ∈ ℕ0 )
118 115 116 117 sylancl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 0 ) ∈ ℕ0 )
119 bcn0 ⊢ ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 0 ) ∈ ℕ0 → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 0 ) C 0 ) = 1 )
120 118 119 syl ⊢ ( 𝜑 → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 0 ) C 0 ) = 1 )
121 120 oveq2d ⊢ ( 𝜑 → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 0 ) C 0 ) ) = ( 𝑃 pCnt 1 ) )
122 pc1 ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 1 ) = 0 )
123 4 122 syl ⊢ ( 𝜑 → ( 𝑃 pCnt 1 ) = 0 )
124 121 123 eqtrd ⊢ ( 𝜑 → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 0 ) C 0 ) ) = 0 )
125 124 a1d ⊢ ( 𝜑 → ( 0 < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 0 ) C 0 ) ) = 0 ) )
126 nn0re ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℝ )
127 126 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → 𝑛 ∈ ℝ )
128 nn0p1nn ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℕ )
129 128 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ℕ )
130 129 nnred ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ℝ )
131 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 ↑ 𝑁 ) ∈ ℕ )
132 131 nnred ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 ↑ 𝑁 ) ∈ ℝ )
133 127 ltp1d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → 𝑛 < ( 𝑛 + 1 ) )
134 simprr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) )
135 127 130 132 133 134 lttrd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → 𝑛 < ( 𝑃 ↑ 𝑁 ) )
136 135 expr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) → 𝑛 < ( 𝑃 ↑ 𝑁 ) ) )
137 136 imim1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ) = 0 ) → ( ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ) = 0 ) ) )
138 oveq1 ⊢ ( ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ) = 0 → ( ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ) + ( 𝑃 pCnt ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) = ( 0 + ( 𝑃 pCnt ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) )
139 115 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℕ0 )
140 139 nn0cnd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℂ )
141 nn0cn ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ )
142 141 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → 𝑛 ∈ ℂ )
143 1cnd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → 1 ∈ ℂ )
144 140 142 143 addassd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) = ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( 𝑛 + 1 ) ) )
145 144 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) C ( 𝑛 + 1 ) ) = ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) )
146 nn0addge2 ⊢ ( ( 𝑛 ∈ ℝ ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℕ0 ) → 𝑛 ≤ ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) )
147 127 139 146 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → 𝑛 ≤ ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) )
148 simprl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → 𝑛 ∈ ℕ0 )
149 148 33 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 0 ) )
150 139 148 nn0addcld ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) ∈ ℕ0 )
151 150 nn0zd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) ∈ ℤ )
152 elfz5 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 0 ) ∧ ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) ∈ ℤ ) → ( 𝑛 ∈ ( 0 ... ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) ) ↔ 𝑛 ≤ ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) ) )
153 149 151 152 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑛 ∈ ( 0 ... ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) ) ↔ 𝑛 ≤ ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) ) )
154 147 153 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → 𝑛 ∈ ( 0 ... ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) ) )
155 bcp1nk ⊢ ( 𝑛 ∈ ( 0 ... ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) ) → ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) C ( 𝑛 + 1 ) ) = ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) · ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) )
156 154 155 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) C ( 𝑛 + 1 ) ) = ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) · ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) )
157 145 156 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) = ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) · ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) )
158 157 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) = ( 𝑃 pCnt ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) · ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) )
159 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → 𝑃 ∈ ℙ )
160 bccl2 ⊢ ( 𝑛 ∈ ( 0 ... ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) ) → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ∈ ℕ )
161 154 160 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ∈ ℕ )
162 nnq ⊢ ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ∈ ℕ → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ∈ ℚ )
163 161 162 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ∈ ℚ )
164 161 nnne0d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ≠ 0 )
165 151 peano2zd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ∈ ℤ )
166 znq ⊢ ( ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ∈ ℤ ∧ ( 𝑛 + 1 ) ∈ ℕ ) → ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ∈ ℚ )
167 165 129 166 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ∈ ℚ )
168 nn0p1nn ⊢ ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) ∈ ℕ0 → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ∈ ℕ )
169 150 168 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ∈ ℕ )
170 nnrp ⊢ ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ∈ ℕ → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ∈ ℝ+ )
171 nnrp ⊢ ( ( 𝑛 + 1 ) ∈ ℕ → ( 𝑛 + 1 ) ∈ ℝ+ )
172 rpdivcl ⊢ ( ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ∈ ℝ+ ∧ ( 𝑛 + 1 ) ∈ ℝ+ ) → ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ∈ ℝ+ )
173 170 171 172 syl2an ⊢ ( ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ∈ ℕ ∧ ( 𝑛 + 1 ) ∈ ℕ ) → ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ∈ ℝ+ )
174 169 129 173 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ∈ ℝ+ )
175 174 rpne0d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ≠ 0 )
176 pcqmul ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ∈ ℚ ∧ ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ≠ 0 ) ∧ ( ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ∈ ℚ ∧ ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ≠ 0 ) ) → ( 𝑃 pCnt ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) · ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) = ( ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ) + ( 𝑃 pCnt ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) )
177 159 163 164 167 175 176 syl122anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 pCnt ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) · ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) = ( ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ) + ( 𝑃 pCnt ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) )
178 158 177 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) = ( ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ) + ( 𝑃 pCnt ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) )
179 169 nnne0d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ≠ 0 )
180 pcdiv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ∈ ℤ ∧ ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ≠ 0 ) ∧ ( 𝑛 + 1 ) ∈ ℕ ) → ( 𝑃 pCnt ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) = ( ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ) − ( 𝑃 pCnt ( 𝑛 + 1 ) ) ) )
181 159 165 179 129 180 syl121anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 pCnt ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) = ( ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ) − ( 𝑃 pCnt ( 𝑛 + 1 ) ) ) )
182 129 nncnd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ℂ )
183 140 182 144 comraddd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) = ( ( 𝑛 + 1 ) + ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) )
184 183 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ) = ( 𝑃 pCnt ( ( 𝑛 + 1 ) + ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) ) )
185 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) = 0 ) → ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) = 0 )
186 185 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) = 0 ) → ( ( 𝑛 + 1 ) + ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) = ( ( 𝑛 + 1 ) + 0 ) )
187 182 addridd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( 𝑛 + 1 ) + 0 ) = ( 𝑛 + 1 ) )
188 187 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) = 0 ) → ( ( 𝑛 + 1 ) + 0 ) = ( 𝑛 + 1 ) )
189 186 188 eqtr2d ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) = 0 ) → ( 𝑛 + 1 ) = ( ( 𝑛 + 1 ) + ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) )
190 189 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) = 0 ) → ( 𝑃 pCnt ( 𝑛 + 1 ) ) = ( 𝑃 pCnt ( ( 𝑛 + 1 ) + ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) ) )
191 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → 𝑃 ∈ ℙ )
192 nnq ⊢ ( ( 𝑛 + 1 ) ∈ ℕ → ( 𝑛 + 1 ) ∈ ℚ )
193 129 192 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ℚ )
194 193 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( 𝑛 + 1 ) ∈ ℚ )
195 139 nn0zd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℤ )
196 zq ⊢ ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℤ → ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℚ )
197 195 196 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℚ )
198 197 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℚ )
199 159 129 pccld ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 pCnt ( 𝑛 + 1 ) ) ∈ ℕ0 )
200 199 nn0red ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 pCnt ( 𝑛 + 1 ) ) ∈ ℝ )
201 200 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( 𝑃 pCnt ( 𝑛 + 1 ) ) ∈ ℝ )
202 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
203 202 nn0red ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → 𝑁 ∈ ℝ )
204 203 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → 𝑁 ∈ ℝ )
205 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 )
206 205 neneqd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ¬ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) = 0 )
207 115 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℕ0 )
208 elnn0 ⊢ ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℕ0 ↔ ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℕ ∨ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) = 0 ) )
209 207 208 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℕ ∨ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) = 0 ) )
210 209 ord ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( ¬ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℕ → ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) = 0 ) )
211 206 210 mt3d ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℕ )
212 191 211 pccld ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( 𝑃 pCnt ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) ∈ ℕ0 )
213 212 nn0red ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( 𝑃 pCnt ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) ∈ ℝ )
214 129 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ℤ )
215 pcdvdsb ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑛 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ≤ ( 𝑃 pCnt ( 𝑛 + 1 ) ) ↔ ( 𝑃 ↑ 𝑁 ) ∥ ( 𝑛 + 1 ) ) )
216 159 214 202 215 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑁 ≤ ( 𝑃 pCnt ( 𝑛 + 1 ) ) ↔ ( 𝑃 ↑ 𝑁 ) ∥ ( 𝑛 + 1 ) ) )
217 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 ↑ 𝑁 ) ∈ ℤ )
218 dvdsle ⊢ ( ( ( 𝑃 ↑ 𝑁 ) ∈ ℤ ∧ ( 𝑛 + 1 ) ∈ ℕ ) → ( ( 𝑃 ↑ 𝑁 ) ∥ ( 𝑛 + 1 ) → ( 𝑃 ↑ 𝑁 ) ≤ ( 𝑛 + 1 ) ) )
219 217 129 218 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( 𝑃 ↑ 𝑁 ) ∥ ( 𝑛 + 1 ) → ( 𝑃 ↑ 𝑁 ) ≤ ( 𝑛 + 1 ) ) )
220 216 219 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑁 ≤ ( 𝑃 pCnt ( 𝑛 + 1 ) ) → ( 𝑃 ↑ 𝑁 ) ≤ ( 𝑛 + 1 ) ) )
221 203 200 lenltd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑁 ≤ ( 𝑃 pCnt ( 𝑛 + 1 ) ) ↔ ¬ ( 𝑃 pCnt ( 𝑛 + 1 ) ) < 𝑁 ) )
222 132 130 lenltd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( 𝑃 ↑ 𝑁 ) ≤ ( 𝑛 + 1 ) ↔ ¬ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) )
223 220 221 222 3imtr3d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ¬ ( 𝑃 pCnt ( 𝑛 + 1 ) ) < 𝑁 → ¬ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) )
224 134 223 mt4d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 pCnt ( 𝑛 + 1 ) ) < 𝑁 )
225 224 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( 𝑃 pCnt ( 𝑛 + 1 ) ) < 𝑁 )
226 dvdssubr ⊢ ( ( ( 𝑃 ↑ 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑋 ) ∈ ℤ ) → ( ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) ↔ ( 𝑃 ↑ 𝑁 ) ∥ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) )
227 12 35 226 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) ↔ ( 𝑃 ↑ 𝑁 ) ∥ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) )
228 6 227 mpbid ⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∥ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) )
229 228 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( 𝑃 ↑ 𝑁 ) ∥ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) )
230 207 nn0zd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℤ )
231 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → 𝑁 ∈ ℕ0 )
232 pcdvdsb ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ≤ ( 𝑃 pCnt ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) ↔ ( 𝑃 ↑ 𝑁 ) ∥ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) )
233 191 230 231 232 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( 𝑁 ≤ ( 𝑃 pCnt ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) ↔ ( 𝑃 ↑ 𝑁 ) ∥ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) )
234 229 233 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → 𝑁 ≤ ( 𝑃 pCnt ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) )
235 201 204 213 225 234 ltletrd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( 𝑃 pCnt ( 𝑛 + 1 ) ) < ( 𝑃 pCnt ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) )
236 191 194 198 235 pcadd2 ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) ∧ ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ≠ 0 ) → ( 𝑃 pCnt ( 𝑛 + 1 ) ) = ( 𝑃 pCnt ( ( 𝑛 + 1 ) + ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) ) )
237 190 236 pm2.61dane ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 pCnt ( 𝑛 + 1 ) ) = ( 𝑃 pCnt ( ( 𝑛 + 1 ) + ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) ) ) )
238 184 237 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ) = ( 𝑃 pCnt ( 𝑛 + 1 ) ) )
239 199 nn0cnd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 pCnt ( 𝑛 + 1 ) ) ∈ ℂ )
240 238 239 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ) ∈ ℂ )
241 240 238 subeq0bd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) ) − ( 𝑃 pCnt ( 𝑛 + 1 ) ) ) = 0 )
242 181 241 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 𝑃 pCnt ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) = 0 )
243 242 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( 0 + ( 𝑃 pCnt ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) = ( 0 + 0 ) )
244 00id ⊢ ( 0 + 0 ) = 0
245 243 244 eqtr2di ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → 0 = ( 0 + ( 𝑃 pCnt ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) )
246 178 245 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) = 0 ↔ ( ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ) + ( 𝑃 pCnt ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) = ( 0 + ( 𝑃 pCnt ( ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) ) )
247 138 246 imbitrrid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) ) ) → ( ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ) = 0 → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) = 0 ) )
248 137 247 animpimp2impd ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝜑 → ( 𝑛 < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + 𝑛 ) C 𝑛 ) ) = 0 ) ) → ( 𝜑 → ( ( 𝑛 + 1 ) < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) = 0 ) ) ) )
249 94 100 106 112 125 248 nn0ind ⊢ ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) ∈ ℕ0 → ( 𝜑 → ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ) = 0 ) ) )
250 88 249 mpcom ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ 𝑁 ) − 1 ) < ( 𝑃 ↑ 𝑁 ) → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ) = 0 ) )
251 86 250 mpd ⊢ ( 𝜑 → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − ( 𝑃 ↑ 𝑁 ) ) + ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ) = 0 )
252 84 251 eqtr3d ⊢ ( 𝜑 → ( 𝑃 pCnt ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ) = 0 )
253 pcdiv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( ♯ ‘ 𝑋 ) ∈ ℤ ∧ ( ♯ ‘ 𝑋 ) ≠ 0 ) ∧ ( 𝑃 ↑ 𝑁 ) ∈ ℕ ) → ( 𝑃 pCnt ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ) = ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − ( 𝑃 pCnt ( 𝑃 ↑ 𝑁 ) ) ) )
254 4 35 77 11 253 syl121anc ⊢ ( 𝜑 → ( 𝑃 pCnt ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ) = ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − ( 𝑃 pCnt ( 𝑃 ↑ 𝑁 ) ) ) )
255 5 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
256 pcid ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝑁 ) ) = 𝑁 )
257 4 255 256 syl2anc ⊢ ( 𝜑 → ( 𝑃 pCnt ( 𝑃 ↑ 𝑁 ) ) = 𝑁 )
258 257 oveq2d ⊢ ( 𝜑 → ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − ( 𝑃 pCnt ( 𝑃 ↑ 𝑁 ) ) ) = ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
259 254 258 eqtrd ⊢ ( 𝜑 → ( 𝑃 pCnt ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ) = ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
260 252 259 oveq12d ⊢ ( 𝜑 → ( ( 𝑃 pCnt ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) ) + ( 𝑃 pCnt ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ) ) = ( 0 + ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )
261 4 28 pccld ⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℕ0 )
262 261 nn0zd ⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℤ )
263 262 255 zsubcld ⊢ ( 𝜑 → ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ∈ ℤ )
264 263 zcnd ⊢ ( 𝜑 → ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ∈ ℂ )
265 264 addlidd ⊢ ( 𝜑 → ( 0 + ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) = ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
266 80 260 265 3eqtrd ⊢ ( 𝜑 → ( 𝑃 pCnt ( ( ( ( ♯ ‘ 𝑋 ) − 1 ) C ( ( 𝑃 ↑ 𝑁 ) − 1 ) ) · ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ 𝑁 ) ) ) ) = ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
267 67 68 266 3eqtr3d ⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝑆 ) ) = ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
268 41 267 jca ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑆 ) ∈ ℕ ∧ ( 𝑃 pCnt ( ♯ ‘ 𝑆 ) ) = ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )