This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gexexlem

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

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