MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gexexlem Structured version   Visualization version   GIF version

Theorem gexexlem 18176
Description: Lemma for gexex 18177. (Contributed by Mario Carneiro, 24-Apr-2016.)
Hypotheses
Ref Expression
gexex.1 𝑋 = (Base‘𝐺)
gexex.2 𝐸 = (gEx‘𝐺)
gexex.3 𝑂 = (od‘𝐺)
gexexlem.1 (𝜑𝐺 ∈ Abel)
gexexlem.2 (𝜑𝐸 ∈ ℕ)
gexexlem.3 (𝜑𝐴𝑋)
gexexlem.4 ((𝜑𝑦𝑋) → (𝑂𝑦) ≤ (𝑂𝐴))
Assertion
Ref Expression
gexexlem (𝜑 → (𝑂𝐴) = 𝐸)
Distinct variable groups:   𝑦,𝐴   𝑦,𝐸   𝑦,𝐺   𝑦,𝑂   𝜑,𝑦   𝑦,𝑋

Proof of Theorem gexexlem
Dummy variables 𝑥 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gexexlem.3 . . 3 (𝜑𝐴𝑋)
2 gexex.1 . . . 4 𝑋 = (Base‘𝐺)
3 gexex.3 . . . 4 𝑂 = (od‘𝐺)
42, 3odcl 17876 . . 3 (𝐴𝑋 → (𝑂𝐴) ∈ ℕ0)
51, 4syl 17 . 2 (𝜑 → (𝑂𝐴) ∈ ℕ0)
6 gexexlem.2 . . 3 (𝜑𝐸 ∈ ℕ)
76nnnn0d 11295 . 2 (𝜑𝐸 ∈ ℕ0)
8 gexexlem.1 . . . 4 (𝜑𝐺 ∈ Abel)
9 ablgrp 18119 . . . 4 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
108, 9syl 17 . . 3 (𝜑𝐺 ∈ Grp)
11 gexex.2 . . . 4 𝐸 = (gEx‘𝐺)
122, 11, 3gexod 17922 . . 3 ((𝐺 ∈ Grp ∧ 𝐴𝑋) → (𝑂𝐴) ∥ 𝐸)
1310, 1, 12syl2anc 692 . 2 (𝜑 → (𝑂𝐴) ∥ 𝐸)
148ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → 𝐺 ∈ Abel)
1510ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → 𝐺 ∈ Grp)
16 prmnn 15312 . . . . . . . . . . . . . . . 16 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
1716adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℕ)
18 simpr 477 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
196ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → 𝐸 ∈ ℕ)
201ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → 𝐴𝑋)
212, 11, 3gexnnod 17924 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴𝑋) → (𝑂𝐴) ∈ ℕ)
2215, 19, 20, 21syl3anc 1323 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂𝐴) ∈ ℕ)
2318, 22pccld 15479 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (𝑂𝐴)) ∈ ℕ0)
2417, 23nnexpcld 12970 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt (𝑂𝐴))) ∈ ℕ)
2524nnzd 11425 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt (𝑂𝐴))) ∈ ℤ)
26 eqid 2621 . . . . . . . . . . . . . 14 (.g𝐺) = (.g𝐺)
272, 26mulgcl 17480 . . . . . . . . . . . . 13 ((𝐺 ∈ Grp ∧ (𝑝↑(𝑝 pCnt (𝑂𝐴))) ∈ ℤ ∧ 𝐴𝑋) → ((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴) ∈ 𝑋)
2815, 25, 20, 27syl3anc 1323 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴) ∈ 𝑋)
29 simplr 791 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → 𝑥𝑋)
302, 11, 3gexnnod 17924 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝑥𝑋) → (𝑂𝑥) ∈ ℕ)
3115, 19, 29, 30syl3anc 1323 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂𝑥) ∈ ℕ)
32 pcdvds 15492 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ ℙ ∧ (𝑂𝑥) ∈ ℕ) → (𝑝↑(𝑝 pCnt (𝑂𝑥))) ∥ (𝑂𝑥))
3318, 31, 32syl2anc 692 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt (𝑂𝑥))) ∥ (𝑂𝑥))
3418, 31pccld 15479 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (𝑂𝑥)) ∈ ℕ0)
3517, 34nnexpcld 12970 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt (𝑂𝑥))) ∈ ℕ)
36 nndivdvds 14913 . . . . . . . . . . . . . . . 16 (((𝑂𝑥) ∈ ℕ ∧ (𝑝↑(𝑝 pCnt (𝑂𝑥))) ∈ ℕ) → ((𝑝↑(𝑝 pCnt (𝑂𝑥))) ∥ (𝑂𝑥) ↔ ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ∈ ℕ))
3731, 35, 36syl2anc 692 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑝↑(𝑝 pCnt (𝑂𝑥))) ∥ (𝑂𝑥) ↔ ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ∈ ℕ))
3833, 37mpbid 222 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ∈ ℕ)
3938nnzd 11425 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ∈ ℤ)
402, 26mulgcl 17480 . . . . . . . . . . . . 13 ((𝐺 ∈ Grp ∧ ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ∈ ℤ ∧ 𝑥𝑋) → (((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥) ∈ 𝑋)
4115, 39, 29, 40syl3anc 1323 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥) ∈ 𝑋)
422, 3, 26odmulg 17894 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ 𝐴𝑋 ∧ (𝑝↑(𝑝 pCnt (𝑂𝐴))) ∈ ℤ) → (𝑂𝐴) = (((𝑝↑(𝑝 pCnt (𝑂𝐴))) gcd (𝑂𝐴)) · (𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴))))
4315, 20, 25, 42syl3anc 1323 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂𝐴) = (((𝑝↑(𝑝 pCnt (𝑂𝐴))) gcd (𝑂𝐴)) · (𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴))))
44 pcdvds 15492 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ ℙ ∧ (𝑂𝐴) ∈ ℕ) → (𝑝↑(𝑝 pCnt (𝑂𝐴))) ∥ (𝑂𝐴))
4518, 22, 44syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt (𝑂𝐴))) ∥ (𝑂𝐴))
46 gcdeq 15196 . . . . . . . . . . . . . . . . . . . 20 (((𝑝↑(𝑝 pCnt (𝑂𝐴))) ∈ ℕ ∧ (𝑂𝐴) ∈ ℕ) → (((𝑝↑(𝑝 pCnt (𝑂𝐴))) gcd (𝑂𝐴)) = (𝑝↑(𝑝 pCnt (𝑂𝐴))) ↔ (𝑝↑(𝑝 pCnt (𝑂𝐴))) ∥ (𝑂𝐴)))
4724, 22, 46syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (((𝑝↑(𝑝 pCnt (𝑂𝐴))) gcd (𝑂𝐴)) = (𝑝↑(𝑝 pCnt (𝑂𝐴))) ↔ (𝑝↑(𝑝 pCnt (𝑂𝐴))) ∥ (𝑂𝐴)))
4845, 47mpbird 247 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑝↑(𝑝 pCnt (𝑂𝐴))) gcd (𝑂𝐴)) = (𝑝↑(𝑝 pCnt (𝑂𝐴))))
4948oveq1d 6619 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (((𝑝↑(𝑝 pCnt (𝑂𝐴))) gcd (𝑂𝐴)) · (𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴))) = ((𝑝↑(𝑝 pCnt (𝑂𝐴))) · (𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴))))
5043, 49eqtrd 2655 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂𝐴) = ((𝑝↑(𝑝 pCnt (𝑂𝐴))) · (𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴))))
5150oveq1d 6619 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) = (((𝑝↑(𝑝 pCnt (𝑂𝐴))) · (𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴))) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))))
522, 11, 3gexnnod 17924 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ ((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴) ∈ 𝑋) → (𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)) ∈ ℕ)
5315, 19, 28, 52syl3anc 1323 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)) ∈ ℕ)
5453nncnd 10980 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)) ∈ ℂ)
5524nncnd 10980 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt (𝑂𝐴))) ∈ ℂ)
5624nnne0d 11009 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt (𝑂𝐴))) ≠ 0)
5754, 55, 56divcan3d 10750 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (((𝑝↑(𝑝 pCnt (𝑂𝐴))) · (𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴))) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) = (𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)))
5851, 57eqtr2d 2656 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)) = ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))))
592, 11, 3gexnnod 17924 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ (((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥) ∈ 𝑋) → (𝑂‘(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥)) ∈ ℕ)
6015, 19, 41, 59syl3anc 1323 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂‘(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥)) ∈ ℕ)
6160nncnd 10980 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂‘(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥)) ∈ ℂ)
6235nncnd 10980 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt (𝑂𝑥))) ∈ ℂ)
6338nncnd 10980 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ∈ ℂ)
6438nnne0d 11009 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ≠ 0)
6531nncnd 10980 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂𝑥) ∈ ℂ)
6635nnne0d 11009 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt (𝑂𝑥))) ≠ 0)
6765, 62, 66divcan1d 10746 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) · (𝑝↑(𝑝 pCnt (𝑂𝑥)))) = (𝑂𝑥))
682, 3, 26odmulg 17894 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ 𝑥𝑋 ∧ ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ∈ ℤ) → (𝑂𝑥) = ((((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) gcd (𝑂𝑥)) · (𝑂‘(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))))
6915, 29, 39, 68syl3anc 1323 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂𝑥) = ((((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) gcd (𝑂𝑥)) · (𝑂‘(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))))
7035nnzd 11425 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt (𝑂𝑥))) ∈ ℤ)
71 dvdsmul1 14927 . . . . . . . . . . . . . . . . . . . 20 ((((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt (𝑂𝑥))) ∈ ℤ) → ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ∥ (((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) · (𝑝↑(𝑝 pCnt (𝑂𝑥)))))
7239, 70, 71syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ∥ (((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) · (𝑝↑(𝑝 pCnt (𝑂𝑥)))))
7372, 67breqtrd 4639 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ∥ (𝑂𝑥))
74 gcdeq 15196 . . . . . . . . . . . . . . . . . . 19 ((((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ∈ ℕ ∧ (𝑂𝑥) ∈ ℕ) → ((((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) gcd (𝑂𝑥)) = ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ↔ ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ∥ (𝑂𝑥)))
7538, 31, 74syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) gcd (𝑂𝑥)) = ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ↔ ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ∥ (𝑂𝑥)))
7673, 75mpbird 247 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) gcd (𝑂𝑥)) = ((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))))
7776oveq1d 6619 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) gcd (𝑂𝑥)) · (𝑂‘(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))) = (((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) · (𝑂‘(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))))
7867, 69, 773eqtrrd 2660 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) · (𝑂‘(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))) = (((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))) · (𝑝↑(𝑝 pCnt (𝑂𝑥)))))
7961, 62, 63, 64, 78mulcanad 10606 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂‘(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥)) = (𝑝↑(𝑝 pCnt (𝑂𝑥))))
8058, 79oveq12d 6622 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)) gcd (𝑂‘(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))) = (((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) gcd (𝑝↑(𝑝 pCnt (𝑂𝑥)))))
81 nndivdvds 14913 . . . . . . . . . . . . . . . . 17 (((𝑂𝐴) ∈ ℕ ∧ (𝑝↑(𝑝 pCnt (𝑂𝐴))) ∈ ℕ) → ((𝑝↑(𝑝 pCnt (𝑂𝐴))) ∥ (𝑂𝐴) ↔ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ∈ ℕ))
8222, 24, 81syl2anc 692 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑝↑(𝑝 pCnt (𝑂𝐴))) ∥ (𝑂𝐴) ↔ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ∈ ℕ))
8345, 82mpbid 222 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ∈ ℕ)
8483nnzd 11425 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ∈ ℤ)
85 gcdcom 15159 . . . . . . . . . . . . . 14 ((((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt (𝑂𝑥))) ∈ ℤ) → (((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) gcd (𝑝↑(𝑝 pCnt (𝑂𝑥)))) = ((𝑝↑(𝑝 pCnt (𝑂𝑥))) gcd ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴))))))
8684, 70, 85syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) gcd (𝑝↑(𝑝 pCnt (𝑂𝑥)))) = ((𝑝↑(𝑝 pCnt (𝑂𝑥))) gcd ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴))))))
87 pcndvds2 15496 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ ℙ ∧ (𝑂𝐴) ∈ ℕ) → ¬ 𝑝 ∥ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))))
8818, 22, 87syl2anc 692 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ¬ 𝑝 ∥ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))))
89 coprm 15347 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ ℙ ∧ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ∈ ℤ) → (¬ 𝑝 ∥ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ↔ (𝑝 gcd ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴))))) = 1))
9018, 84, 89syl2anc 692 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (¬ 𝑝 ∥ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ↔ (𝑝 gcd ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴))))) = 1))
9188, 90mpbid 222 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝 gcd ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴))))) = 1)
92 prmz 15313 . . . . . . . . . . . . . . . 16 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
9392adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ)
94 rpexp1i 15357 . . . . . . . . . . . . . . 15 ((𝑝 ∈ ℤ ∧ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ∈ ℤ ∧ (𝑝 pCnt (𝑂𝑥)) ∈ ℕ0) → ((𝑝 gcd ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴))))) = 1 → ((𝑝↑(𝑝 pCnt (𝑂𝑥))) gcd ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴))))) = 1))
9593, 84, 34, 94syl3anc 1323 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑝 gcd ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴))))) = 1 → ((𝑝↑(𝑝 pCnt (𝑂𝑥))) gcd ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴))))) = 1))
9691, 95mpd 15 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑝↑(𝑝 pCnt (𝑂𝑥))) gcd ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴))))) = 1)
9780, 86, 963eqtrd 2659 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)) gcd (𝑂‘(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))) = 1)
98 eqid 2621 . . . . . . . . . . . . 13 (+g𝐺) = (+g𝐺)
993, 2, 98odadd 18174 . . . . . . . . . . . 12 (((𝐺 ∈ Abel ∧ ((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴) ∈ 𝑋 ∧ (((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥) ∈ 𝑋) ∧ ((𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)) gcd (𝑂‘(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))) = 1) → (𝑂‘(((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)(+g𝐺)(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))) = ((𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)) · (𝑂‘(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))))
10014, 28, 41, 97, 99syl31anc 1326 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂‘(((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)(+g𝐺)(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))) = ((𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)) · (𝑂‘(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))))
10158, 79oveq12d 6622 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑂‘((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)) · (𝑂‘(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))) = (((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) · (𝑝↑(𝑝 pCnt (𝑂𝑥)))))
102100, 101eqtrd 2655 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂‘(((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)(+g𝐺)(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))) = (((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) · (𝑝↑(𝑝 pCnt (𝑂𝑥)))))
1032, 98grpcl 17351 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ ((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴) ∈ 𝑋 ∧ (((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥) ∈ 𝑋) → (((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)(+g𝐺)(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥)) ∈ 𝑋)
10415, 28, 41, 103syl3anc 1323 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)(+g𝐺)(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥)) ∈ 𝑋)
105 gexexlem.4 . . . . . . . . . . . . 13 ((𝜑𝑦𝑋) → (𝑂𝑦) ≤ (𝑂𝐴))
106105ralrimiva 2960 . . . . . . . . . . . 12 (𝜑 → ∀𝑦𝑋 (𝑂𝑦) ≤ (𝑂𝐴))
107106ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ∀𝑦𝑋 (𝑂𝑦) ≤ (𝑂𝐴))
108 fveq2 6148 . . . . . . . . . . . . 13 (𝑦 = (((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)(+g𝐺)(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥)) → (𝑂𝑦) = (𝑂‘(((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)(+g𝐺)(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))))
109108breq1d 4623 . . . . . . . . . . . 12 (𝑦 = (((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)(+g𝐺)(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥)) → ((𝑂𝑦) ≤ (𝑂𝐴) ↔ (𝑂‘(((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)(+g𝐺)(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))) ≤ (𝑂𝐴)))
110109rspcv 3291 . . . . . . . . . . 11 ((((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)(+g𝐺)(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥)) ∈ 𝑋 → (∀𝑦𝑋 (𝑂𝑦) ≤ (𝑂𝐴) → (𝑂‘(((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)(+g𝐺)(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))) ≤ (𝑂𝐴)))
111104, 107, 110sylc 65 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂‘(((𝑝↑(𝑝 pCnt (𝑂𝐴)))(.g𝐺)𝐴)(+g𝐺)(((𝑂𝑥) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))(.g𝐺)𝑥))) ≤ (𝑂𝐴))
112102, 111eqbrtrrd 4637 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) · (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ≤ (𝑂𝐴))
11383nnred 10979 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ∈ ℝ)
11422nnred 10979 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑂𝐴) ∈ ℝ)
11535nnrpd 11814 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt (𝑂𝑥))) ∈ ℝ+)
116113, 114, 115lemuldivd 11865 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) · (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ≤ (𝑂𝐴) ↔ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ≤ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))))
117112, 116mpbid 222 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ≤ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝑥)))))
118 nnrp 11786 . . . . . . . . . 10 ((𝑝↑(𝑝 pCnt (𝑂𝑥))) ∈ ℕ → (𝑝↑(𝑝 pCnt (𝑂𝑥))) ∈ ℝ+)
119 nnrp 11786 . . . . . . . . . 10 ((𝑝↑(𝑝 pCnt (𝑂𝐴))) ∈ ℕ → (𝑝↑(𝑝 pCnt (𝑂𝐴))) ∈ ℝ+)
120 nnrp 11786 . . . . . . . . . 10 ((𝑂𝐴) ∈ ℕ → (𝑂𝐴) ∈ ℝ+)
121 rpregt0 11790 . . . . . . . . . . 11 ((𝑝↑(𝑝 pCnt (𝑂𝑥))) ∈ ℝ+ → ((𝑝↑(𝑝 pCnt (𝑂𝑥))) ∈ ℝ ∧ 0 < (𝑝↑(𝑝 pCnt (𝑂𝑥)))))
122 rpregt0 11790 . . . . . . . . . . 11 ((𝑝↑(𝑝 pCnt (𝑂𝐴))) ∈ ℝ+ → ((𝑝↑(𝑝 pCnt (𝑂𝐴))) ∈ ℝ ∧ 0 < (𝑝↑(𝑝 pCnt (𝑂𝐴)))))
123 rpregt0 11790 . . . . . . . . . . 11 ((𝑂𝐴) ∈ ℝ+ → ((𝑂𝐴) ∈ ℝ ∧ 0 < (𝑂𝐴)))
124 lediv2 10857 . . . . . . . . . . 11 ((((𝑝↑(𝑝 pCnt (𝑂𝑥))) ∈ ℝ ∧ 0 < (𝑝↑(𝑝 pCnt (𝑂𝑥)))) ∧ ((𝑝↑(𝑝 pCnt (𝑂𝐴))) ∈ ℝ ∧ 0 < (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ∧ ((𝑂𝐴) ∈ ℝ ∧ 0 < (𝑂𝐴))) → ((𝑝↑(𝑝 pCnt (𝑂𝑥))) ≤ (𝑝↑(𝑝 pCnt (𝑂𝐴))) ↔ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ≤ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))))
125121, 122, 123, 124syl3an 1365 . . . . . . . . . 10 (((𝑝↑(𝑝 pCnt (𝑂𝑥))) ∈ ℝ+ ∧ (𝑝↑(𝑝 pCnt (𝑂𝐴))) ∈ ℝ+ ∧ (𝑂𝐴) ∈ ℝ+) → ((𝑝↑(𝑝 pCnt (𝑂𝑥))) ≤ (𝑝↑(𝑝 pCnt (𝑂𝐴))) ↔ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ≤ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))))
126118, 119, 120, 125syl3an 1365 . . . . . . . . 9 (((𝑝↑(𝑝 pCnt (𝑂𝑥))) ∈ ℕ ∧ (𝑝↑(𝑝 pCnt (𝑂𝐴))) ∈ ℕ ∧ (𝑂𝐴) ∈ ℕ) → ((𝑝↑(𝑝 pCnt (𝑂𝑥))) ≤ (𝑝↑(𝑝 pCnt (𝑂𝐴))) ↔ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ≤ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))))
12735, 24, 22, 126syl3anc 1323 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑝↑(𝑝 pCnt (𝑂𝑥))) ≤ (𝑝↑(𝑝 pCnt (𝑂𝐴))) ↔ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝐴)))) ≤ ((𝑂𝐴) / (𝑝↑(𝑝 pCnt (𝑂𝑥))))))
128117, 127mpbird 247 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt (𝑂𝑥))) ≤ (𝑝↑(𝑝 pCnt (𝑂𝐴))))
12917nnred 10979 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ)
13034nn0zd 11424 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (𝑂𝑥)) ∈ ℤ)
13123nn0zd 11424 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (𝑂𝐴)) ∈ ℤ)
132 prmuz2 15332 . . . . . . . . . 10 (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ‘2))
133132adantl 482 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ (ℤ‘2))
134 eluz2b2 11705 . . . . . . . . . 10 (𝑝 ∈ (ℤ‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝))
135134simprbi 480 . . . . . . . . 9 (𝑝 ∈ (ℤ‘2) → 1 < 𝑝)
136133, 135syl 17 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → 1 < 𝑝)
137129, 130, 131, 136leexp2d 12979 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (𝑂𝑥)) ≤ (𝑝 pCnt (𝑂𝐴)) ↔ (𝑝↑(𝑝 pCnt (𝑂𝑥))) ≤ (𝑝↑(𝑝 pCnt (𝑂𝐴)))))
138128, 137mpbird 247 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (𝑂𝑥)) ≤ (𝑝 pCnt (𝑂𝐴)))
139138ralrimiva 2960 . . . . 5 ((𝜑𝑥𝑋) → ∀𝑝 ∈ ℙ (𝑝 pCnt (𝑂𝑥)) ≤ (𝑝 pCnt (𝑂𝐴)))
1402, 3odcl 17876 . . . . . . . 8 (𝑥𝑋 → (𝑂𝑥) ∈ ℕ0)
141140adantl 482 . . . . . . 7 ((𝜑𝑥𝑋) → (𝑂𝑥) ∈ ℕ0)
142141nn0zd 11424 . . . . . 6 ((𝜑𝑥𝑋) → (𝑂𝑥) ∈ ℤ)
1435nn0zd 11424 . . . . . . 7 (𝜑 → (𝑂𝐴) ∈ ℤ)
144143adantr 481 . . . . . 6 ((𝜑𝑥𝑋) → (𝑂𝐴) ∈ ℤ)
145 pc2dvds 15507 . . . . . 6 (((𝑂𝑥) ∈ ℤ ∧ (𝑂𝐴) ∈ ℤ) → ((𝑂𝑥) ∥ (𝑂𝐴) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (𝑂𝑥)) ≤ (𝑝 pCnt (𝑂𝐴))))
146142, 144, 145syl2anc 692 . . . . 5 ((𝜑𝑥𝑋) → ((𝑂𝑥) ∥ (𝑂𝐴) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (𝑂𝑥)) ≤ (𝑝 pCnt (𝑂𝐴))))
147139, 146mpbird 247 . . . 4 ((𝜑𝑥𝑋) → (𝑂𝑥) ∥ (𝑂𝐴))
148147ralrimiva 2960 . . 3 (𝜑 → ∀𝑥𝑋 (𝑂𝑥) ∥ (𝑂𝐴))
1492, 11, 3gexdvds2 17921 . . . 4 ((𝐺 ∈ Grp ∧ (𝑂𝐴) ∈ ℤ) → (𝐸 ∥ (𝑂𝐴) ↔ ∀𝑥𝑋 (𝑂𝑥) ∥ (𝑂𝐴)))
15010, 143, 149syl2anc 692 . . 3 (𝜑 → (𝐸 ∥ (𝑂𝐴) ↔ ∀𝑥𝑋 (𝑂𝑥) ∥ (𝑂𝐴)))
151148, 150mpbird 247 . 2 (𝜑𝐸 ∥ (𝑂𝐴))
152 dvdseq 14960 . 2 ((((𝑂𝐴) ∈ ℕ0𝐸 ∈ ℕ0) ∧ ((𝑂𝐴) ∥ 𝐸𝐸 ∥ (𝑂𝐴))) → (𝑂𝐴) = 𝐸)
1535, 7, 13, 151, 152syl22anc 1324 1 (𝜑 → (𝑂𝐴) = 𝐸)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2907   class class class wbr 4613  cfv 5847  (class class class)co 6604  cr 9879  0cc0 9880  1c1 9881   · cmul 9885   < clt 10018  cle 10019   / cdiv 10628  cn 10964  2c2 11014  0cn0 11236  cz 11321  cuz 11631  +crp 11776  cexp 12800  cdvds 14907   gcd cgcd 15140  cprime 15309   pCnt cpc 15465  Basecbs 15781  +gcplusg 15862  Grpcgrp 17343  .gcmg 17461  odcod 17865  gExcgex 17866  Abelcabl 18115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-sup 8292  df-inf 8293  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-n0 11237  df-z 11322  df-uz 11632  df-q 11733  df-rp 11777  df-fz 12269  df-fzo 12407  df-fl 12533  df-mod 12609  df-seq 12742  df-exp 12801  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-dvds 14908  df-gcd 15141  df-prm 15310  df-pc 15466  df-0g 16023  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-grp 17346  df-minusg 17347  df-sbg 17348  df-mulg 17462  df-od 17869  df-gex 17870  df-cmn 18116  df-abl 18117
This theorem is referenced by:  gexex  18177
  Copyright terms: Public domain W3C validator