# Metamath Proof Explorer

## Theorem gexexlem

Description: Lemma for gexex . (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gexex.1 ${⊢}{X}={\mathrm{Base}}_{{G}}$
gexex.2 ${⊢}{E}=\mathrm{gEx}\left({G}\right)$
gexex.3 ${⊢}{O}=\mathrm{od}\left({G}\right)$
gexexlem.1 ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
gexexlem.2 ${⊢}{\phi }\to {E}\in ℕ$
gexexlem.3 ${⊢}{\phi }\to {A}\in {X}$
gexexlem.4 ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to {O}\left({y}\right)\le {O}\left({A}\right)$
Assertion gexexlem ${⊢}{\phi }\to {O}\left({A}\right)={E}$

### Proof

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