Theorem ablfac1lem

Description: Lemma for ablfac1b . Satisfy the assumptions of ablfacrp. (Contributed by Mario Carneiro, 26-Apr-2016)

	Ref	Expression
Hypotheses	ablfac1.b	$$⊢B={\mathrm{Base}}_G$$
	ablfac1.o	$$⊢O=\mathrm{od}\left(G\right)$$
	ablfac1.s	$$⊢S=\left(p\in A⟼\left\{x\in B|O\left(x\right)\parallel p^{p\mathrm{pCnt}\left|B\right|}\right\}\right)$$
	ablfac1.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	ablfac1.f	$$⊢\phi \to B\in \mathrm{Fin}$$
	ablfac1.1	$$⊢\phi \to A\subseteq \mathbb{P}$$
	ablfac1.m	$$⊢M=P^{P\mathrm{pCnt}\left|B\right|}$$
	ablfac1.n	$$⊢N=\frac{\left|B\right|}{M}$$
Assertion	ablfac1lem	$$⊢\left(\phi \wedge P\in A\right)\to \left(\left(M\in \mathbb{N}\wedge N\in \mathbb{N}\right)\wedge M\gcd N=1\wedge \left|B\right|=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ablfac1.b	$$⊢B={\mathrm{Base}}_G$$
2		ablfac1.o	$$⊢O=\mathrm{od}\left(G\right)$$
3		ablfac1.s	$$⊢S=\left(p\in A⟼\left\{x\in B|O\left(x\right)\parallel p^{p\mathrm{pCnt}\left|B\right|}\right\}\right)$$
4		ablfac1.g	$$⊢\phi \to G\in \mathrm{Abel}$$
5		ablfac1.f	$$⊢\phi \to B\in \mathrm{Fin}$$
6		ablfac1.1	$$⊢\phi \to A\subseteq \mathbb{P}$$
7		ablfac1.m	$$⊢M=P^{P\mathrm{pCnt}\left|B\right|}$$
8		ablfac1.n	$$⊢N=\frac{\left|B\right|}{M}$$
9	6	sselda	$$⊢\left(\phi \wedge P\in A\right)\to P\in \mathbb{P}$$
10		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
11	9 10	syl	$$⊢\left(\phi \wedge P\in A\right)\to P\in \mathbb{N}$$
12		ablgrp	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{Grp}$$
13	1	grpbn0	$$⊢G\in \mathrm{Grp}\to B\ne \varnothing$$
14	4 12 13	3syl	$$⊢\phi \to B\ne \varnothing$$
15		hashnncl	$$⊢B\in \mathrm{Fin}\to \left(\left|B\right|\in \mathbb{N}\leftrightarrow B\ne \varnothing \right)$$
16	5 15	syl	$$⊢\phi \to \left(\left|B\right|\in \mathbb{N}\leftrightarrow B\ne \varnothing \right)$$
17	14 16	mpbird	$$⊢\phi \to \left|B\right|\in \mathbb{N}$$
18	17	adantr	$$⊢\left(\phi \wedge P\in A\right)\to \left|B\right|\in \mathbb{N}$$
19	9 18	pccld	$$⊢\left(\phi \wedge P\in A\right)\to P\mathrm{pCnt}\left|B\right|\in {\mathbb{N}}_0$$
20	11 19	nnexpcld	$$⊢\left(\phi \wedge P\in A\right)\to P^{P\mathrm{pCnt}\left|B\right|}\in \mathbb{N}$$
21	7 20	eqeltrid	$$⊢\left(\phi \wedge P\in A\right)\to M\in \mathbb{N}$$
22		pcdvds	$$⊢\left(P\in \mathbb{P}\wedge \left|B\right|\in \mathbb{N}\right)\to P^{P\mathrm{pCnt}\left|B\right|}\parallel \left|B\right|$$
23	9 18 22	syl2anc	$$⊢\left(\phi \wedge P\in A\right)\to P^{P\mathrm{pCnt}\left|B\right|}\parallel \left|B\right|$$
24	7 23	eqbrtrid	$$⊢\left(\phi \wedge P\in A\right)\to M\parallel \left|B\right|$$
25		nndivdvds	$$⊢\left(\left|B\right|\in \mathbb{N}\wedge M\in \mathbb{N}\right)\to \left(M\parallel \left|B\right|\leftrightarrow \frac{\left|B\right|}{M}\in \mathbb{N}\right)$$
26	18 21 25	syl2anc	$$⊢\left(\phi \wedge P\in A\right)\to \left(M\parallel \left|B\right|\leftrightarrow \frac{\left|B\right|}{M}\in \mathbb{N}\right)$$
27	24 26	mpbid	$$⊢\left(\phi \wedge P\in A\right)\to \frac{\left|B\right|}{M}\in \mathbb{N}$$
28	8 27	eqeltrid	$$⊢\left(\phi \wedge P\in A\right)\to N\in \mathbb{N}$$
29	21 28	jca	$$⊢\left(\phi \wedge P\in A\right)\to \left(M\in \mathbb{N}\wedge N\in \mathbb{N}\right)$$
30	7	oveq1i	$$⊢M\gcd N=P^{P\mathrm{pCnt}\left|B\right|}\gcd N$$
31		pcndvds2	$$⊢\left(P\in \mathbb{P}\wedge \left|B\right|\in \mathbb{N}\right)\to \neg P\parallel \left(\frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}\right)$$
32	9 18 31	syl2anc	$$⊢\left(\phi \wedge P\in A\right)\to \neg P\parallel \left(\frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}\right)$$
33	7	oveq2i	$$⊢\frac{\left|B\right|}{M}=\frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}$$
34	8 33	eqtri	$$⊢N=\frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}$$
35	34	breq2i	$$⊢P\parallel N\leftrightarrow P\parallel \left(\frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}\right)$$
36	32 35	sylnibr	$$⊢\left(\phi \wedge P\in A\right)\to \neg P\parallel N$$
37	28	nnzd	$$⊢\left(\phi \wedge P\in A\right)\to N\in \mathbb{Z}$$
38		coprm	$$⊢\left(P\in \mathbb{P}\wedge N\in \mathbb{Z}\right)\to \left(\neg P\parallel N\leftrightarrow P\gcd N=1\right)$$
39	9 37 38	syl2anc	$$⊢\left(\phi \wedge P\in A\right)\to \left(\neg P\parallel N\leftrightarrow P\gcd N=1\right)$$
40	36 39	mpbid	$$⊢\left(\phi \wedge P\in A\right)\to P\gcd N=1$$
41		prmz	$$⊢P\in \mathbb{P}\to P\in \mathbb{Z}$$
42	9 41	syl	$$⊢\left(\phi \wedge P\in A\right)\to P\in \mathbb{Z}$$
43		rpexp1i	$$⊢\left(P\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge P\mathrm{pCnt}\left|B\right|\in {\mathbb{N}}_0\right)\to \left(P\gcd N=1\to P^{P\mathrm{pCnt}\left|B\right|}\gcd N=1\right)$$
44	42 37 19 43	syl3anc	$$⊢\left(\phi \wedge P\in A\right)\to \left(P\gcd N=1\to P^{P\mathrm{pCnt}\left|B\right|}\gcd N=1\right)$$
45	40 44	mpd	$$⊢\left(\phi \wedge P\in A\right)\to P^{P\mathrm{pCnt}\left|B\right|}\gcd N=1$$
46	30 45	syl5eq	$$⊢\left(\phi \wedge P\in A\right)\to M\gcd N=1$$
47	8	oveq2i	$$⊢\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=M\left(\frac{\left|B\right|}{M}\right)$$
48	18	nncnd	$$⊢\left(\phi \wedge P\in A\right)\to \left|B\right|\in ℂ$$
49	21	nncnd	$$⊢\left(\phi \wedge P\in A\right)\to M\in ℂ$$
50	21	nnne0d	$$⊢\left(\phi \wedge P\in A\right)\to M\ne 0$$
51	48 49 50	divcan2d	$$⊢\left(\phi \wedge P\in A\right)\to M\left(\frac{\left|B\right|}{M}\right)=\left|B\right|$$
52	47 51	syl5req	$$⊢\left(\phi \wedge P\in A\right)\to \left|B\right|=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
53	29 46 52	3jca	$$⊢\left(\phi \wedge P\in A\right)\to \left(\left(M\in \mathbb{N}\wedge N\in \mathbb{N}\right)\wedge M\gcd N=1\wedge \left|B\right|=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$