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
|- X = ( Base ` G )
sylow1.g
|- ( ph -> G e. Grp )
sylow1.f
|- ( ph -> X e. Fin )
sylow1.p
|- ( ph -> P e. Prime )
sylow1.n
|- ( ph -> N e. NN0 )
sylow1.d
|- ( ph -> ( P ^ N ) || ( # ` X ) )
sylow1lem.a
|- .+ = ( +g ` G )
sylow1lem.s
|- S = { s e. ~P X | ( # ` s ) = ( P ^ N ) }
Assertion sylow1lem1
|- ( ph -> ( ( # ` S ) e. NN /\ ( P pCnt ( # ` S ) ) = ( ( P pCnt ( # ` X ) ) - N ) ) )

Proof

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