gexexlem

	Ref	Expression
Hypotheses	gexex.1	$⊢ X = {Base}_{G}$
	gexex.2	$⊢ E = gEx (G)$
	gexex.3	$⊢ O = od (G)$
	gexexlem.1	$⊢ φ \to G \in Abel$
	gexexlem.2	$⊢ φ \to E \in ℕ$
	gexexlem.3	$⊢ φ \to A \in X$
	gexexlem.4	$⊢ (φ \land y \in X) \to O (y) \leq O (A)$
Assertion	gexexlem	$⊢ φ \to O (A) = E$

Proof

Step	Hyp	Ref	Expression
1		gexex.1	$⊢ X = {Base}_{G}$
2		gexex.2	$⊢ E = gEx (G)$
3		gexex.3	$⊢ O = od (G)$
4		gexexlem.1	$⊢ φ \to G \in Abel$
5		gexexlem.2	$⊢ φ \to E \in ℕ$
6		gexexlem.3	$⊢ φ \to A \in X$
7		gexexlem.4	$⊢ (φ \land y \in X) \to O (y) \leq O (A)$
8	1 3	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
9	6 8	syl	$⊢ φ \to O (A) \in ℕ_{0}$
10	5	nnnn0d	$⊢ φ \to E \in ℕ_{0}$
11		ablgrp	$⊢ G \in Abel \to G \in Grp$
12	4 11	syl	$⊢ φ \to G \in Grp$
13	1 2 3	gexod	$⊢ (G \in Grp \land A \in X) \to O (A) ∥ E$
14	12 6 13	syl2anc	$⊢ φ \to O (A) ∥ E$
15	4	ad2antrr	$⊢ ((φ \land x \in X) \land p \in ℙ) \to G \in Abel$
16	12	ad2antrr	$⊢ ((φ \land x \in X) \land p \in ℙ) \to G \in Grp$
17		prmnn	$⊢ p \in ℙ \to p \in ℕ$
18	17	adantl	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p \in ℕ$
19		simpr	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p \in ℙ$
20	5	ad2antrr	$⊢ ((φ \land x \in X) \land p \in ℙ) \to E \in ℕ$
21	6	ad2antrr	$⊢ ((φ \land x \in X) \land p \in ℙ) \to A \in X$
22	1 2 3	gexnnod	$⊢ (G \in Grp \land E \in ℕ \land A \in X) \to O (A) \in ℕ$
23	16 20 21 22	syl3anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O (A) \in ℕ$
24	19 23	pccld	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p pCnt O (A) \in ℕ_{0}$
25	18 24	nnexpcld	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (A)} \in ℕ$
26	25	nnzd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (A)} \in ℤ$
27		eqid	$⊢ \cdot_{G} = \cdot_{G}$
28	1 27	mulgcl	$⊢ (G \in Grp \land p^{p pCnt O (A)} \in ℤ \land A \in X) \to p^{p pCnt O (A)} \cdot_{G} A \in X$
29	16 26 21 28	syl3anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (A)} \cdot_{G} A \in X$
30		simplr	$⊢ ((φ \land x \in X) \land p \in ℙ) \to x \in X$
31	1 2 3	gexnnod	$⊢ (G \in Grp \land E \in ℕ \land x \in X) \to O (x) \in ℕ$
32	16 20 30 31	syl3anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O (x) \in ℕ$
33		pcdvds	$⊢ (p \in ℙ \land O (x) \in ℕ) \to p^{p pCnt O (x)} ∥ O (x)$
34	19 32 33	syl2anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (x)} ∥ O (x)$
35	19 32	pccld	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p pCnt O (x) \in ℕ_{0}$
36	18 35	nnexpcld	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (x)} \in ℕ$
37		nndivdvds	$⊢ (O (x) \in ℕ \land p^{p pCnt O (x)} \in ℕ) \to (p^{p pCnt O (x)} ∥ O (x) \leftrightarrow \frac{O (x)}{p^{p pCnt O (x)}} \in ℕ)$
38	32 36 37	syl2anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (p^{p pCnt O (x)} ∥ O (x) \leftrightarrow \frac{O (x)}{p^{p pCnt O (x)}} \in ℕ)$
39	34 38	mpbid	$⊢ ((φ \land x \in X) \land p \in ℙ) \to \frac{O (x)}{p^{p pCnt O (x)}} \in ℕ$
40	39	nnzd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to \frac{O (x)}{p^{p pCnt O (x)}} \in ℤ$
41	1 27	mulgcl	$⊢ (G \in Grp \land \frac{O (x)}{p^{p pCnt O (x)}} \in ℤ \land x \in X) \to (\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x \in X$
42	16 40 30 41	syl3anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x \in X$
43	1 3 27	odmulg	$⊢ (G \in Grp \land A \in X \land p^{p pCnt O (A)} \in ℤ) \to O (A) = (p^{p pCnt O (A)} \gcd O (A)) O (p^{p pCnt O (A)} \cdot_{G} A)$
44	16 21 26 43	syl3anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O (A) = (p^{p pCnt O (A)} \gcd O (A)) O (p^{p pCnt O (A)} \cdot_{G} A)$
45		pcdvds	$⊢ (p \in ℙ \land O (A) \in ℕ) \to p^{p pCnt O (A)} ∥ O (A)$
46	19 23 45	syl2anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (A)} ∥ O (A)$
47		gcdeq	$⊢ (p^{p pCnt O (A)} \in ℕ \land O (A) \in ℕ) \to (p^{p pCnt O (A)} \gcd O (A) = p^{p pCnt O (A)} \leftrightarrow p^{p pCnt O (A)} ∥ O (A))$
48	25 23 47	syl2anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (p^{p pCnt O (A)} \gcd O (A) = p^{p pCnt O (A)} \leftrightarrow p^{p pCnt O (A)} ∥ O (A))$
49	46 48	mpbird	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (A)} \gcd O (A) = p^{p pCnt O (A)}$
50	49	oveq1d	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (p^{p pCnt O (A)} \gcd O (A)) O (p^{p pCnt O (A)} \cdot_{G} A) = p^{p pCnt O (A)} O (p^{p pCnt O (A)} \cdot_{G} A)$
51	44 50	eqtrd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O (A) = p^{p pCnt O (A)} O (p^{p pCnt O (A)} \cdot_{G} A)$
52	51	oveq1d	$⊢ ((φ \land x \in X) \land p \in ℙ) \to \frac{O (A)}{p^{p pCnt O (A)}} = \frac{p^{p pCnt O (A)} O (p^{p pCnt O (A)} \cdot_{G} A)}{p^{p pCnt O (A)}}$
53	1 2 3	gexnnod	$⊢ (G \in Grp \land E \in ℕ \land p^{p pCnt O (A)} \cdot_{G} A \in X) \to O (p^{p pCnt O (A)} \cdot_{G} A) \in ℕ$
54	16 20 29 53	syl3anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O (p^{p pCnt O (A)} \cdot_{G} A) \in ℕ$
55	54	nncnd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O (p^{p pCnt O (A)} \cdot_{G} A) \in ℂ$
56	25	nncnd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (A)} \in ℂ$
57	25	nnne0d	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (A)} \neq 0$
58	55 56 57	divcan3d	$⊢ ((φ \land x \in X) \land p \in ℙ) \to \frac{p^{p pCnt O (A)} O (p^{p pCnt O (A)} \cdot_{G} A)}{p^{p pCnt O (A)}} = O (p^{p pCnt O (A)} \cdot_{G} A)$
59	52 58	eqtr2d	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O (p^{p pCnt O (A)} \cdot_{G} A) = \frac{O (A)}{p^{p pCnt O (A)}}$
60	1 2 3	gexnnod	$⊢ (G \in Grp \land E \in ℕ \land (\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x \in X) \to O ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x) \in ℕ$
61	16 20 42 60	syl3anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x) \in ℕ$
62	61	nncnd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x) \in ℂ$
63	36	nncnd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (x)} \in ℂ$
64	39	nncnd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to \frac{O (x)}{p^{p pCnt O (x)}} \in ℂ$
65	39	nnne0d	$⊢ ((φ \land x \in X) \land p \in ℙ) \to \frac{O (x)}{p^{p pCnt O (x)}} \neq 0$
66	32	nncnd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O (x) \in ℂ$
67	36	nnne0d	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (x)} \neq 0$
68	66 63 67	divcan1d	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (\frac{O (x)}{p^{p pCnt O (x)}}) p^{p pCnt O (x)} = O (x)$
69	1 3 27	odmulg	$⊢ (G \in Grp \land x \in X \land \frac{O (x)}{p^{p pCnt O (x)}} \in ℤ) \to O (x) = ((\frac{O (x)}{p^{p pCnt O (x)}}) \gcd O (x)) O ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x)$
70	16 30 40 69	syl3anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O (x) = ((\frac{O (x)}{p^{p pCnt O (x)}}) \gcd O (x)) O ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x)$
71	36	nnzd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (x)} \in ℤ$
72		dvdsmul1	$⊢ (\frac{O (x)}{p^{p pCnt O (x)}} \in ℤ \land p^{p pCnt O (x)} \in ℤ) \to (\frac{O (x)}{p^{p pCnt O (x)}}) ∥ (\frac{O (x)}{p^{p pCnt O (x)}}) p^{p pCnt O (x)}$
73	40 71 72	syl2anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (\frac{O (x)}{p^{p pCnt O (x)}}) ∥ (\frac{O (x)}{p^{p pCnt O (x)}}) p^{p pCnt O (x)}$
74	73 68	breqtrd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (\frac{O (x)}{p^{p pCnt O (x)}}) ∥ O (x)$
75		gcdeq	$⊢ (\frac{O (x)}{p^{p pCnt O (x)}} \in ℕ \land O (x) \in ℕ) \to ((\frac{O (x)}{p^{p pCnt O (x)}}) \gcd O (x) = \frac{O (x)}{p^{p pCnt O (x)}} \leftrightarrow (\frac{O (x)}{p^{p pCnt O (x)}}) ∥ O (x))$
76	39 32 75	syl2anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to ((\frac{O (x)}{p^{p pCnt O (x)}}) \gcd O (x) = \frac{O (x)}{p^{p pCnt O (x)}} \leftrightarrow (\frac{O (x)}{p^{p pCnt O (x)}}) ∥ O (x))$
77	74 76	mpbird	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (\frac{O (x)}{p^{p pCnt O (x)}}) \gcd O (x) = \frac{O (x)}{p^{p pCnt O (x)}}$
78	77	oveq1d	$⊢ ((φ \land x \in X) \land p \in ℙ) \to ((\frac{O (x)}{p^{p pCnt O (x)}}) \gcd O (x)) O ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x) = (\frac{O (x)}{p^{p pCnt O (x)}}) O ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x)$
79	68 70 78	3eqtrrd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (\frac{O (x)}{p^{p pCnt O (x)}}) O ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x) = (\frac{O (x)}{p^{p pCnt O (x)}}) p^{p pCnt O (x)}$
80	62 63 64 65 79	mulcanad	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x) = p^{p pCnt O (x)}$
81	59 80	oveq12d	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O (p^{p pCnt O (A)} \cdot_{G} A) \gcd O ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x) = (\frac{O (A)}{p^{p pCnt O (A)}}) \gcd p^{p pCnt O (x)}$
82		nndivdvds	$⊢ (O (A) \in ℕ \land p^{p pCnt O (A)} \in ℕ) \to (p^{p pCnt O (A)} ∥ O (A) \leftrightarrow \frac{O (A)}{p^{p pCnt O (A)}} \in ℕ)$
83	23 25 82	syl2anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (p^{p pCnt O (A)} ∥ O (A) \leftrightarrow \frac{O (A)}{p^{p pCnt O (A)}} \in ℕ)$
84	46 83	mpbid	$⊢ ((φ \land x \in X) \land p \in ℙ) \to \frac{O (A)}{p^{p pCnt O (A)}} \in ℕ$
85	84	nnzd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to \frac{O (A)}{p^{p pCnt O (A)}} \in ℤ$
86		gcdcom	$⊢ (\frac{O (A)}{p^{p pCnt O (A)}} \in ℤ \land p^{p pCnt O (x)} \in ℤ) \to (\frac{O (A)}{p^{p pCnt O (A)}}) \gcd p^{p pCnt O (x)} = p^{p pCnt O (x)} \gcd (\frac{O (A)}{p^{p pCnt O (A)}})$
87	85 71 86	syl2anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (\frac{O (A)}{p^{p pCnt O (A)}}) \gcd p^{p pCnt O (x)} = p^{p pCnt O (x)} \gcd (\frac{O (A)}{p^{p pCnt O (A)}})$
88		pcndvds2	$⊢ (p \in ℙ \land O (A) \in ℕ) \to \neg p ∥ (\frac{O (A)}{p^{p pCnt O (A)}})$
89	19 23 88	syl2anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to \neg p ∥ (\frac{O (A)}{p^{p pCnt O (A)}})$
90		coprm	$⊢ (p \in ℙ \land \frac{O (A)}{p^{p pCnt O (A)}} \in ℤ) \to (\neg p ∥ (\frac{O (A)}{p^{p pCnt O (A)}}) \leftrightarrow p \gcd (\frac{O (A)}{p^{p pCnt O (A)}}) = 1)$
91	19 85 90	syl2anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (\neg p ∥ (\frac{O (A)}{p^{p pCnt O (A)}}) \leftrightarrow p \gcd (\frac{O (A)}{p^{p pCnt O (A)}}) = 1)$
92	89 91	mpbid	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p \gcd (\frac{O (A)}{p^{p pCnt O (A)}}) = 1$
93		prmz	$⊢ p \in ℙ \to p \in ℤ$
94	93	adantl	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p \in ℤ$
95		rpexp1i	$⊢ (p \in ℤ \land \frac{O (A)}{p^{p pCnt O (A)}} \in ℤ \land p pCnt O (x) \in ℕ_{0}) \to (p \gcd (\frac{O (A)}{p^{p pCnt O (A)}}) = 1 \to p^{p pCnt O (x)} \gcd (\frac{O (A)}{p^{p pCnt O (A)}}) = 1)$
96	94 85 35 95	syl3anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (p \gcd (\frac{O (A)}{p^{p pCnt O (A)}}) = 1 \to p^{p pCnt O (x)} \gcd (\frac{O (A)}{p^{p pCnt O (A)}}) = 1)$
97	92 96	mpd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (x)} \gcd (\frac{O (A)}{p^{p pCnt O (A)}}) = 1$
98	81 87 97	3eqtrd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O (p^{p pCnt O (A)} \cdot_{G} A) \gcd O ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x) = 1$
99		eqid	$⊢ +_{G} = +_{G}$
100	3 1 99	odadd	$⊢ ((G \in Abel \land p^{p pCnt O (A)} \cdot_{G} A \in X \land (\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x \in X) \land O (p^{p pCnt O (A)} \cdot_{G} A) \gcd O ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x) = 1) \to O ((p^{p pCnt O (A)} \cdot_{G} A) +_{G} ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x)) = O (p^{p pCnt O (A)} \cdot_{G} A) O ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x)$
101	15 29 42 98 100	syl31anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O ((p^{p pCnt O (A)} \cdot_{G} A) +_{G} ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x)) = O (p^{p pCnt O (A)} \cdot_{G} A) O ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x)$
102	59 80	oveq12d	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O (p^{p pCnt O (A)} \cdot_{G} A) O ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x) = (\frac{O (A)}{p^{p pCnt O (A)}}) p^{p pCnt O (x)}$
103	101 102	eqtrd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O ((p^{p pCnt O (A)} \cdot_{G} A) +_{G} ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x)) = (\frac{O (A)}{p^{p pCnt O (A)}}) p^{p pCnt O (x)}$
104		fveq2	$⊢ y = (p^{p pCnt O (A)} \cdot_{G} A) +_{G} ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x) \to O (y) = O ((p^{p pCnt O (A)} \cdot_{G} A) +_{G} ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x))$
105	104	breq1d	$⊢ y = (p^{p pCnt O (A)} \cdot_{G} A) +_{G} ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x) \to (O (y) \leq O (A) \leftrightarrow O ((p^{p pCnt O (A)} \cdot_{G} A) +_{G} ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x)) \leq O (A))$
106	7	ralrimiva	$⊢ φ \to \forall y \in X O (y) \leq O (A)$
107	106	ad2antrr	$⊢ ((φ \land x \in X) \land p \in ℙ) \to \forall y \in X O (y) \leq O (A)$
108	1 99	grpcl	$⊢ (G \in Grp \land p^{p pCnt O (A)} \cdot_{G} A \in X \land (\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x \in X) \to (p^{p pCnt O (A)} \cdot_{G} A) +_{G} ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x) \in X$
109	16 29 42 108	syl3anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (p^{p pCnt O (A)} \cdot_{G} A) +_{G} ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x) \in X$
110	105 107 109	rspcdva	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O ((p^{p pCnt O (A)} \cdot_{G} A) +_{G} ((\frac{O (x)}{p^{p pCnt O (x)}}) \cdot_{G} x)) \leq O (A)$
111	103 110	eqbrtrrd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (\frac{O (A)}{p^{p pCnt O (A)}}) p^{p pCnt O (x)} \leq O (A)$
112	84	nnred	$⊢ ((φ \land x \in X) \land p \in ℙ) \to \frac{O (A)}{p^{p pCnt O (A)}} \in ℝ$
113	23	nnred	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O (A) \in ℝ$
114	36	nnrpd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (x)} \in ℝ^{+}$
115	112 113 114	lemuldivd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to ((\frac{O (A)}{p^{p pCnt O (A)}}) p^{p pCnt O (x)} \leq O (A) \leftrightarrow \frac{O (A)}{p^{p pCnt O (A)}} \leq \frac{O (A)}{p^{p pCnt O (x)}})$
116	111 115	mpbid	$⊢ ((φ \land x \in X) \land p \in ℙ) \to \frac{O (A)}{p^{p pCnt O (A)}} \leq \frac{O (A)}{p^{p pCnt O (x)}}$
117		nnrp	$⊢ p^{p pCnt O (x)} \in ℕ \to p^{p pCnt O (x)} \in ℝ^{+}$
118		nnrp	$⊢ p^{p pCnt O (A)} \in ℕ \to p^{p pCnt O (A)} \in ℝ^{+}$
119		nnrp	$⊢ O (A) \in ℕ \to O (A) \in ℝ^{+}$
120		rpregt0	$⊢ p^{p pCnt O (x)} \in ℝ^{+} \to (p^{p pCnt O (x)} \in ℝ \land 0 < p^{p pCnt O (x)})$
121		rpregt0	$⊢ p^{p pCnt O (A)} \in ℝ^{+} \to (p^{p pCnt O (A)} \in ℝ \land 0 < p^{p pCnt O (A)})$
122		rpregt0	$⊢ O (A) \in ℝ^{+} \to (O (A) \in ℝ \land 0 < O (A))$
123		lediv2	$⊢ ((p^{p pCnt O (x)} \in ℝ \land 0 < p^{p pCnt O (x)}) \land (p^{p pCnt O (A)} \in ℝ \land 0 < p^{p pCnt O (A)}) \land (O (A) \in ℝ \land 0 < O (A))) \to (p^{p pCnt O (x)} \leq p^{p pCnt O (A)} \leftrightarrow \frac{O (A)}{p^{p pCnt O (A)}} \leq \frac{O (A)}{p^{p pCnt O (x)}})$
124	120 121 122 123	syl3an	$⊢ (p^{p pCnt O (x)} \in ℝ^{+} \land p^{p pCnt O (A)} \in ℝ^{+} \land O (A) \in ℝ^{+}) \to (p^{p pCnt O (x)} \leq p^{p pCnt O (A)} \leftrightarrow \frac{O (A)}{p^{p pCnt O (A)}} \leq \frac{O (A)}{p^{p pCnt O (x)}})$
125	117 118 119 124	syl3an	$⊢ (p^{p pCnt O (x)} \in ℕ \land p^{p pCnt O (A)} \in ℕ \land O (A) \in ℕ) \to (p^{p pCnt O (x)} \leq p^{p pCnt O (A)} \leftrightarrow \frac{O (A)}{p^{p pCnt O (A)}} \leq \frac{O (A)}{p^{p pCnt O (x)}})$
126	36 25 23 125	syl3anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (p^{p pCnt O (x)} \leq p^{p pCnt O (A)} \leftrightarrow \frac{O (A)}{p^{p pCnt O (A)}} \leq \frac{O (A)}{p^{p pCnt O (x)}})$
127	116 126	mpbird	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (x)} \leq p^{p pCnt O (A)}$
128	18	nnred	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p \in ℝ$
129	35	nn0zd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p pCnt O (x) \in ℤ$
130	24	nn0zd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p pCnt O (A) \in ℤ$
131		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
132	131	adantl	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p \in ℤ_{\geq 2}$
133		eluz2gt1	$⊢ p \in ℤ_{\geq 2} \to 1 < p$
134	132 133	syl	$⊢ ((φ \land x \in X) \land p \in ℙ) \to 1 < p$
135	128 129 130 134	leexp2d	$⊢ ((φ \land x \in X) \land p \in ℙ) \to (p pCnt O (x) \leq p pCnt O (A) \leftrightarrow p^{p pCnt O (x)} \leq p^{p pCnt O (A)})$
136	127 135	mpbird	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p pCnt O (x) \leq p pCnt O (A)$
137	136	ralrimiva	$⊢ (φ \land x \in X) \to \forall p \in ℙ p pCnt O (x) \leq p pCnt O (A)$
138	1 3	odcl	$⊢ x \in X \to O (x) \in ℕ_{0}$
139	138	adantl	$⊢ (φ \land x \in X) \to O (x) \in ℕ_{0}$
140	139	nn0zd	$⊢ (φ \land x \in X) \to O (x) \in ℤ$
141	9	nn0zd	$⊢ φ \to O (A) \in ℤ$
142	141	adantr	$⊢ (φ \land x \in X) \to O (A) \in ℤ$
143		pc2dvds	$⊢ (O (x) \in ℤ \land O (A) \in ℤ) \to (O (x) ∥ O (A) \leftrightarrow \forall p \in ℙ p pCnt O (x) \leq p pCnt O (A))$
144	140 142 143	syl2anc	$⊢ (φ \land x \in X) \to (O (x) ∥ O (A) \leftrightarrow \forall p \in ℙ p pCnt O (x) \leq p pCnt O (A))$
145	137 144	mpbird	$⊢ (φ \land x \in X) \to O (x) ∥ O (A)$
146	145	ralrimiva	$⊢ φ \to \forall x \in X O (x) ∥ O (A)$
147	1 2 3	gexdvds2	$⊢ (G \in Grp \land O (A) \in ℤ) \to (E ∥ O (A) \leftrightarrow \forall x \in X O (x) ∥ O (A))$
148	12 141 147	syl2anc	$⊢ φ \to (E ∥ O (A) \leftrightarrow \forall x \in X O (x) ∥ O (A))$
149	146 148	mpbird	$⊢ φ \to E ∥ O (A)$
150		dvdseq	$⊢ ((O (A) \in ℕ_{0} \land E \in ℕ_{0}) \land (O (A) ∥ E \land E ∥ O (A))) \to O (A) = E$
151	9 10 14 149 150	syl22anc	$⊢ φ \to O (A) = E$

Metamath Proof Explorer

Theorem gexexlem

Proof