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