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	85 71	gcdcomd	$⊢ ((φ \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)}})$
87		pcndvds2	$⊢ (p \in ℙ \land O (A) \in ℕ) \to \neg p ∥ (\frac{O (A)}{p^{p pCnt O (A)}})$
88	19 23 87	syl2anc	$⊢ ((φ \land x \in X) \land p \in ℙ) \to \neg p ∥ (\frac{O (A)}{p^{p pCnt O (A)}})$
89		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)$
90	19 85 89	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)$
91	88 90	mpbid	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p \gcd (\frac{O (A)}{p^{p pCnt O (A)}}) = 1$
92		prmz	$⊢ p \in ℙ \to p \in ℤ$
93	92	adantl	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p \in ℤ$
94		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)$
95	93 85 35 94	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)$
96	91 95	mpd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (x)} \gcd (\frac{O (A)}{p^{p pCnt O (A)}}) = 1$
97	81 86 96	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$
98		eqid	$⊢ +_{G} = +_{G}$
99	3 1 98	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)$
100	15 29 42 97 99	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)$
101	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)}$
102	100 101	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)}$
103		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))$
104	103	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))$
105	7	ralrimiva	$⊢ φ \to \forall y \in X O (y) \leq O (A)$
106	105	ad2antrr	$⊢ ((φ \land x \in X) \land p \in ℙ) \to \forall y \in X O (y) \leq O (A)$
107	1 98	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$
108	16 29 42 107	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$
109	104 106 108	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)$
110	102 109	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)$
111	84	nnred	$⊢ ((φ \land x \in X) \land p \in ℙ) \to \frac{O (A)}{p^{p pCnt O (A)}} \in ℝ$
112	23	nnred	$⊢ ((φ \land x \in X) \land p \in ℙ) \to O (A) \in ℝ$
113	36	nnrpd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (x)} \in ℝ^{+}$
114	111 112 113	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)}})$
115	110 114	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)}}$
116		nnrp	$⊢ p^{p pCnt O (x)} \in ℕ \to p^{p pCnt O (x)} \in ℝ^{+}$
117		nnrp	$⊢ p^{p pCnt O (A)} \in ℕ \to p^{p pCnt O (A)} \in ℝ^{+}$
118		nnrp	$⊢ O (A) \in ℕ \to O (A) \in ℝ^{+}$
119		rpregt0	$⊢ p^{p pCnt O (x)} \in ℝ^{+} \to (p^{p pCnt O (x)} \in ℝ \land 0 < p^{p pCnt O (x)})$
120		rpregt0	$⊢ p^{p pCnt O (A)} \in ℝ^{+} \to (p^{p pCnt O (A)} \in ℝ \land 0 < p^{p pCnt O (A)})$
121		rpregt0	$⊢ O (A) \in ℝ^{+} \to (O (A) \in ℝ \land 0 < O (A))$
122		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)}})$
123	119 120 121 122	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)}})$
124	116 117 118 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	36 25 23 124	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)}})$
126	115 125	mpbird	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p^{p pCnt O (x)} \leq p^{p pCnt O (A)}$
127	18	nnred	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p \in ℝ$
128	35	nn0zd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p pCnt O (x) \in ℤ$
129	24	nn0zd	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p pCnt O (A) \in ℤ$
130		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
131	130	adantl	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p \in ℤ_{\geq 2}$
132		eluz2gt1	$⊢ p \in ℤ_{\geq 2} \to 1 < p$
133	131 132	syl	$⊢ ((φ \land x \in X) \land p \in ℙ) \to 1 < p$
134	127 128 129 133	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)})$
135	126 134	mpbird	$⊢ ((φ \land x \in X) \land p \in ℙ) \to p pCnt O (x) \leq p pCnt O (A)$
136	135	ralrimiva	$⊢ (φ \land x \in X) \to \forall p \in ℙ p pCnt O (x) \leq p pCnt O (A)$
137	1 3	odcl	$⊢ x \in X \to O (x) \in ℕ_{0}$
138	137	adantl	$⊢ (φ \land x \in X) \to O (x) \in ℕ_{0}$
139	138	nn0zd	$⊢ (φ \land x \in X) \to O (x) \in ℤ$
140	9	nn0zd	$⊢ φ \to O (A) \in ℤ$
141	140	adantr	$⊢ (φ \land x \in X) \to O (A) \in ℤ$
142		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))$
143	139 141 142	syl2anc	$⊢ (φ \land x \in X) \to (O (x) ∥ O (A) \leftrightarrow \forall p \in ℙ p pCnt O (x) \leq p pCnt O (A))$
144	136 143	mpbird	$⊢ (φ \land x \in X) \to O (x) ∥ O (A)$
145	144	ralrimiva	$⊢ φ \to \forall x \in X O (x) ∥ O (A)$
146	1 2 3	gexdvds2	$⊢ (G \in Grp \land O (A) \in ℤ) \to (E ∥ O (A) \leftrightarrow \forall x \in X O (x) ∥ O (A))$
147	12 140 146	syl2anc	$⊢ φ \to (E ∥ O (A) \leftrightarrow \forall x \in X O (x) ∥ O (A))$
148	145 147	mpbird	$⊢ φ \to E ∥ O (A)$
149		dvdseq	$⊢ ((O (A) \in ℕ_{0} \land E \in ℕ_{0}) \land (O (A) ∥ E \land E ∥ O (A))) \to O (A) = E$
150	9 10 14 148 149	syl22anc	$⊢ φ \to O (A) = E$

Metamath Proof Explorer

Theorem gexexlem

Proof