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 ) ) )