ablfacrplem

	Ref	Expression
Hypotheses	ablfacrp.b	$⊢ B = {Base}_{G}$
	ablfacrp.o	$⊢ O = od (G)$
	ablfacrp.k	$⊢ K = \{x \in B \| O (x) ∥ M\}$
	ablfacrp.l	$⊢ L = \{x \in B \| O (x) ∥ N\}$
	ablfacrp.g	$⊢ φ \to G \in Abel$
	ablfacrp.m	$⊢ φ \to M \in ℕ$
	ablfacrp.n	$⊢ φ \to N \in ℕ$
	ablfacrp.1	$⊢ φ \to M \gcd N = 1$
	ablfacrp.2	$⊢ φ \to \|B\| = M \cdot N$
Assertion	ablfacrplem	$⊢ φ \to \|K\| \gcd N = 1$

Proof

Step	Hyp	Ref	Expression
1		ablfacrp.b	$⊢ B = {Base}_{G}$
2		ablfacrp.o	$⊢ O = od (G)$
3		ablfacrp.k	$⊢ K = \{x \in B \| O (x) ∥ M\}$
4		ablfacrp.l	$⊢ L = \{x \in B \| O (x) ∥ N\}$
5		ablfacrp.g	$⊢ φ \to G \in Abel$
6		ablfacrp.m	$⊢ φ \to M \in ℕ$
7		ablfacrp.n	$⊢ φ \to N \in ℕ$
8		ablfacrp.1	$⊢ φ \to M \gcd N = 1$
9		ablfacrp.2	$⊢ φ \to \|B\| = M \cdot N$
10		nprmdvds1	$⊢ p \in ℙ \to \neg p ∥ 1$
11	10	adantl	$⊢ (φ \land p \in ℙ) \to \neg p ∥ 1$
12	8	adantr	$⊢ (φ \land p \in ℙ) \to M \gcd N = 1$
13	12	breq2d	$⊢ (φ \land p \in ℙ) \to (p ∥ (M \gcd N) \leftrightarrow p ∥ 1)$
14	11 13	mtbird	$⊢ (φ \land p \in ℙ) \to \neg p ∥ (M \gcd N)$
15	6	nnzd	$⊢ φ \to M \in ℤ$
16	2 1	oddvdssubg	$⊢ (G \in Abel \land M \in ℤ) \to \{x \in B \| O (x) ∥ M\} \in SubGrp (G)$
17	5 15 16	syl2anc	$⊢ φ \to \{x \in B \| O (x) ∥ M\} \in SubGrp (G)$
18	3 17	eqeltrid	$⊢ φ \to K \in SubGrp (G)$
19	18	ad2antrr	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to K \in SubGrp (G)$
20		eqid	$⊢ G ↾_{𝑠} K = G ↾_{𝑠} K$
21	20	subggrp	$⊢ K \in SubGrp (G) \to G ↾_{𝑠} K \in Grp$
22	19 21	syl	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to G ↾_{𝑠} K \in Grp$
23	20	subgbas	$⊢ K \in SubGrp (G) \to K = {Base}_{(G ↾_{𝑠} K)}$
24	19 23	syl	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to K = {Base}_{(G ↾_{𝑠} K)}$
25	6	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
26	7	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
27	25 26	nn0mulcld	$⊢ φ \to M \cdot N \in ℕ_{0}$
28	9 27	eqeltrd	$⊢ φ \to \|B\| \in ℕ_{0}$
29	1	fvexi	$⊢ B \in V$
30		hashclb	$⊢ B \in V \to (B \in Fin \leftrightarrow \|B\| \in ℕ_{0})$
31	29 30	ax-mp	$⊢ B \in Fin \leftrightarrow \|B\| \in ℕ_{0}$
32	28 31	sylibr	$⊢ φ \to B \in Fin$
33	3	ssrab3	$⊢ K \subseteq B$
34		ssfi	$⊢ (B \in Fin \land K \subseteq B) \to K \in Fin$
35	32 33 34	sylancl	$⊢ φ \to K \in Fin$
36	35	ad2antrr	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to K \in Fin$
37	24 36	eqeltrrd	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to {Base}_{(G ↾_{𝑠} K)} \in Fin$
38		simplr	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to p \in ℙ$
39		simpr	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to p ∥ \|K\|$
40	24	fveq2d	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to \|K\| = \|{Base}_{(G ↾_{𝑠} K)}\|$
41	39 40	breqtrd	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to p ∥ \|{Base}_{(G ↾_{𝑠} K)}\|$
42		eqid	$⊢ {Base}_{(G ↾_{𝑠} K)} = {Base}_{(G ↾_{𝑠} K)}$
43		eqid	$⊢ od (G ↾_{𝑠} K) = od (G ↾_{𝑠} K)$
44	42 43	odcau	$⊢ ((G ↾_{𝑠} K \in Grp \land {Base}_{(G ↾_{𝑠} K)} \in Fin \land p \in ℙ) \land p ∥ \|{Base}_{(G ↾_{𝑠} K)}\|) \to \exists g \in {Base}_{(G ↾_{𝑠} K)} od (G ↾_{𝑠} K) (g) = p$
45	22 37 38 41 44	syl31anc	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to \exists g \in {Base}_{(G ↾_{𝑠} K)} od (G ↾_{𝑠} K) (g) = p$
46	45 24	rexeqtrrdv	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to \exists g \in K od (G ↾_{𝑠} K) (g) = p$
47	20 2 43	subgod	$⊢ (K \in SubGrp (G) \land g \in K) \to O (g) = od (G ↾_{𝑠} K) (g)$
48	19 47	sylan	$⊢ (((φ \land p \in ℙ) \land p ∥ \|K\|) \land g \in K) \to O (g) = od (G ↾_{𝑠} K) (g)$
49		fveq2	$⊢ x = g \to O (x) = O (g)$
50	49	breq1d	$⊢ x = g \to (O (x) ∥ M \leftrightarrow O (g) ∥ M)$
51	50 3	elrab2	$⊢ g \in K \leftrightarrow (g \in B \land O (g) ∥ M)$
52	51	simprbi	$⊢ g \in K \to O (g) ∥ M$
53	52	adantl	$⊢ (((φ \land p \in ℙ) \land p ∥ \|K\|) \land g \in K) \to O (g) ∥ M$
54	48 53	eqbrtrrd	$⊢ (((φ \land p \in ℙ) \land p ∥ \|K\|) \land g \in K) \to od (G ↾_{𝑠} K) (g) ∥ M$
55		breq1	$⊢ od (G ↾_{𝑠} K) (g) = p \to (od (G ↾_{𝑠} K) (g) ∥ M \leftrightarrow p ∥ M)$
56	54 55	syl5ibcom	$⊢ (((φ \land p \in ℙ) \land p ∥ \|K\|) \land g \in K) \to (od (G ↾_{𝑠} K) (g) = p \to p ∥ M)$
57	56	rexlimdva	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to (\exists g \in K od (G ↾_{𝑠} K) (g) = p \to p ∥ M)$
58	46 57	mpd	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to p ∥ M$
59	58	ex	$⊢ (φ \land p \in ℙ) \to (p ∥ \|K\| \to p ∥ M)$
60	59	anim1d	$⊢ (φ \land p \in ℙ) \to ((p ∥ \|K\| \land p ∥ N) \to (p ∥ M \land p ∥ N))$
61		prmz	$⊢ p \in ℙ \to p \in ℤ$
62	61	adantl	$⊢ (φ \land p \in ℙ) \to p \in ℤ$
63		hashcl	$⊢ K \in Fin \to \|K\| \in ℕ_{0}$
64	35 63	syl	$⊢ φ \to \|K\| \in ℕ_{0}$
65	64	nn0zd	$⊢ φ \to \|K\| \in ℤ$
66	65	adantr	$⊢ (φ \land p \in ℙ) \to \|K\| \in ℤ$
67	7	nnzd	$⊢ φ \to N \in ℤ$
68	67	adantr	$⊢ (φ \land p \in ℙ) \to N \in ℤ$
69		dvdsgcdb	$⊢ (p \in ℤ \land \|K\| \in ℤ \land N \in ℤ) \to ((p ∥ \|K\| \land p ∥ N) \leftrightarrow p ∥ (\|K\| \gcd N))$
70	62 66 68 69	syl3anc	$⊢ (φ \land p \in ℙ) \to ((p ∥ \|K\| \land p ∥ N) \leftrightarrow p ∥ (\|K\| \gcd N))$
71	15	adantr	$⊢ (φ \land p \in ℙ) \to M \in ℤ$
72		dvdsgcdb	$⊢ (p \in ℤ \land M \in ℤ \land N \in ℤ) \to ((p ∥ M \land p ∥ N) \leftrightarrow p ∥ (M \gcd N))$
73	62 71 68 72	syl3anc	$⊢ (φ \land p \in ℙ) \to ((p ∥ M \land p ∥ N) \leftrightarrow p ∥ (M \gcd N))$
74	60 70 73	3imtr3d	$⊢ (φ \land p \in ℙ) \to (p ∥ (\|K\| \gcd N) \to p ∥ (M \gcd N))$
75	14 74	mtod	$⊢ (φ \land p \in ℙ) \to \neg p ∥ (\|K\| \gcd N)$
76	75	nrexdv	$⊢ φ \to \neg \exists p \in ℙ p ∥ (\|K\| \gcd N)$
77		exprmfct	$⊢ \|K\| \gcd N \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ (\|K\| \gcd N)$
78	76 77	nsyl	$⊢ φ \to \neg \|K\| \gcd N \in ℤ_{\geq 2}$
79	7	nnne0d	$⊢ φ \to N \neq 0$
80		simpr	$⊢ (\|K\| = 0 \land N = 0) \to N = 0$
81	80	necon3ai	$⊢ N \neq 0 \to \neg (\|K\| = 0 \land N = 0)$
82	79 81	syl	$⊢ φ \to \neg (\|K\| = 0 \land N = 0)$
83		gcdn0cl	$⊢ ((\|K\| \in ℤ \land N \in ℤ) \land \neg (\|K\| = 0 \land N = 0)) \to \|K\| \gcd N \in ℕ$
84	65 67 82 83	syl21anc	$⊢ φ \to \|K\| \gcd N \in ℕ$
85		elnn1uz2	$⊢ \|K\| \gcd N \in ℕ \leftrightarrow (\|K\| \gcd N = 1 \lor \|K\| \gcd N \in ℤ_{\geq 2})$
86	84 85	sylib	$⊢ φ \to (\|K\| \gcd N = 1 \lor \|K\| \gcd N \in ℤ_{\geq 2})$
87	86	ord	$⊢ φ \to (\neg \|K\| \gcd N = 1 \to \|K\| \gcd N \in ℤ_{\geq 2})$
88	78 87	mt3d	$⊢ φ \to \|K\| \gcd N = 1$

Metamath Proof Explorer

Theorem ablfacrplem

Proof