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