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	24	rexeqdv	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to (\exists g \in K od (G ↾_{𝑠} K) (g) = p \leftrightarrow \exists g \in {Base}_{(G ↾_{𝑠} K)} od (G ↾_{𝑠} K) (g) = p)$
47	45 46	mpbird	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to \exists g \in K od (G ↾_{𝑠} K) (g) = p$
48	20 2 43	subgod	$⊢ (K \in SubGrp (G) \land g \in K) \to O (g) = od (G ↾_{𝑠} K) (g)$
49	19 48	sylan	$⊢ (((φ \land p \in ℙ) \land p ∥ \|K\|) \land g \in K) \to O (g) = od (G ↾_{𝑠} K) (g)$
50		fveq2	$⊢ x = g \to O (x) = O (g)$
51	50	breq1d	$⊢ x = g \to (O (x) ∥ M \leftrightarrow O (g) ∥ M)$
52	51 3	elrab2	$⊢ g \in K \leftrightarrow (g \in B \land O (g) ∥ M)$
53	52	simprbi	$⊢ g \in K \to O (g) ∥ M$
54	53	adantl	$⊢ (((φ \land p \in ℙ) \land p ∥ \|K\|) \land g \in K) \to O (g) ∥ M$
55	49 54	eqbrtrrd	$⊢ (((φ \land p \in ℙ) \land p ∥ \|K\|) \land g \in K) \to od (G ↾_{𝑠} K) (g) ∥ M$
56		breq1	$⊢ od (G ↾_{𝑠} K) (g) = p \to (od (G ↾_{𝑠} K) (g) ∥ M \leftrightarrow p ∥ M)$
57	55 56	syl5ibcom	$⊢ (((φ \land p \in ℙ) \land p ∥ \|K\|) \land g \in K) \to (od (G ↾_{𝑠} K) (g) = p \to p ∥ M)$
58	57	rexlimdva	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to (\exists g \in K od (G ↾_{𝑠} K) (g) = p \to p ∥ M)$
59	47 58	mpd	$⊢ ((φ \land p \in ℙ) \land p ∥ \|K\|) \to p ∥ M$
60	59	ex	$⊢ (φ \land p \in ℙ) \to (p ∥ \|K\| \to p ∥ M)$
61	60	anim1d	$⊢ (φ \land p \in ℙ) \to ((p ∥ \|K\| \land p ∥ N) \to (p ∥ M \land p ∥ N))$
62		prmz	$⊢ p \in ℙ \to p \in ℤ$
63	62	adantl	$⊢ (φ \land p \in ℙ) \to p \in ℤ$
64		hashcl	$⊢ K \in Fin \to \|K\| \in ℕ_{0}$
65	35 64	syl	$⊢ φ \to \|K\| \in ℕ_{0}$
66	65	nn0zd	$⊢ φ \to \|K\| \in ℤ$
67	66	adantr	$⊢ (φ \land p \in ℙ) \to \|K\| \in ℤ$
68	7	nnzd	$⊢ φ \to N \in ℤ$
69	68	adantr	$⊢ (φ \land p \in ℙ) \to N \in ℤ$
70		dvdsgcdb	$⊢ (p \in ℤ \land \|K\| \in ℤ \land N \in ℤ) \to ((p ∥ \|K\| \land p ∥ N) \leftrightarrow p ∥ (\|K\| \gcd N))$
71	63 67 69 70	syl3anc	$⊢ (φ \land p \in ℙ) \to ((p ∥ \|K\| \land p ∥ N) \leftrightarrow p ∥ (\|K\| \gcd N))$
72	15	adantr	$⊢ (φ \land p \in ℙ) \to M \in ℤ$
73		dvdsgcdb	$⊢ (p \in ℤ \land M \in ℤ \land N \in ℤ) \to ((p ∥ M \land p ∥ N) \leftrightarrow p ∥ (M \gcd N))$
74	63 72 69 73	syl3anc	$⊢ (φ \land p \in ℙ) \to ((p ∥ M \land p ∥ N) \leftrightarrow p ∥ (M \gcd N))$
75	61 71 74	3imtr3d	$⊢ (φ \land p \in ℙ) \to (p ∥ (\|K\| \gcd N) \to p ∥ (M \gcd N))$
76	14 75	mtod	$⊢ (φ \land p \in ℙ) \to \neg p ∥ (\|K\| \gcd N)$
77	76	nrexdv	$⊢ φ \to \neg \exists p \in ℙ p ∥ (\|K\| \gcd N)$
78		exprmfct	$⊢ \|K\| \gcd N \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ (\|K\| \gcd N)$
79	77 78	nsyl	$⊢ φ \to \neg \|K\| \gcd N \in ℤ_{\geq 2}$
80	7	nnne0d	$⊢ φ \to N \neq 0$
81		simpr	$⊢ (\|K\| = 0 \land N = 0) \to N = 0$
82	81	necon3ai	$⊢ N \neq 0 \to \neg (\|K\| = 0 \land N = 0)$
83	80 82	syl	$⊢ φ \to \neg (\|K\| = 0 \land N = 0)$
84		gcdn0cl	$⊢ ((\|K\| \in ℤ \land N \in ℤ) \land \neg (\|K\| = 0 \land N = 0)) \to \|K\| \gcd N \in ℕ$
85	66 68 83 84	syl21anc	$⊢ φ \to \|K\| \gcd N \in ℕ$
86		elnn1uz2	$⊢ \|K\| \gcd N \in ℕ \leftrightarrow (\|K\| \gcd N = 1 \lor \|K\| \gcd N \in ℤ_{\geq 2})$
87	85 86	sylib	$⊢ φ \to (\|K\| \gcd N = 1 \lor \|K\| \gcd N \in ℤ_{\geq 2})$
88	87	ord	$⊢ φ \to (\neg \|K\| \gcd N = 1 \to \|K\| \gcd N \in ℤ_{\geq 2})$
89	79 88	mt3d	$⊢ φ \to \|K\| \gcd N = 1$

Metamath Proof Explorer

Theorem ablfacrplem

Proof