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

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 addridd 
 |-  ( ( 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 imbitrrid 
 |-  ( ( 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 addlidd 
 |-  ( 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 ) ) )