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 addid1d ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ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 syl5ibr ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ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 addid2d ( 𝜑 → ( 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 ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )