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	$⊢ φ \to G \in Grp$
	sylow1.f	$⊢ φ \to X \in Fin$
	sylow1.p	$⊢ φ \to P \in ℙ$
	sylow1.n	$⊢ φ \to N \in ℕ_{0}$
	sylow1.d	$⊢ φ \to P^{N} ∥ \|X\|$
	sylow1lem.a	$⊢ \underset{˙}{+} = +_{G}$
	sylow1lem.s	$⊢ S = \{s \in 𝒫 X \| \|s\| = P^{N}\}$
Assertion	sylow1lem1	$⊢ φ \to (\|S\| \in ℕ \land P pCnt \|S\| = (P pCnt \|X\|) - N)$

Proof

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

Metamath Proof Explorer

Theorem sylow1lem1

Proof