# Metamath Proof Explorer

## Theorem fincygsubgodd

Description: Calculate the order of a subgroup of a finite cyclic group. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses fincygsubgodd.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
fincygsubgodd.2
fincygsubgodd.3 ${⊢}{D}=\frac{\left|{B}\right|}{{C}}$
fincygsubgodd.4
fincygsubgodd.5
fincygsubgodd.6 ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
fincygsubgodd.7 ${⊢}{\phi }\to {A}\in {B}$
fincygsubgodd.8 ${⊢}{\phi }\to \mathrm{ran}{F}={B}$
fincygsubgodd.9 ${⊢}{\phi }\to {C}\parallel \left|{B}\right|$
fincygsubgodd.10 ${⊢}{\phi }\to {B}\in \mathrm{Fin}$
fincygsubgodd.11 ${⊢}{\phi }\to {C}\in ℕ$
Assertion fincygsubgodd ${⊢}{\phi }\to \left|\mathrm{ran}{H}\right|={D}$

### Proof

Step Hyp Ref Expression
1 fincygsubgodd.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 fincygsubgodd.2
3 fincygsubgodd.3 ${⊢}{D}=\frac{\left|{B}\right|}{{C}}$
4 fincygsubgodd.4
5 fincygsubgodd.5
6 fincygsubgodd.6 ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
7 fincygsubgodd.7 ${⊢}{\phi }\to {A}\in {B}$
8 fincygsubgodd.8 ${⊢}{\phi }\to \mathrm{ran}{F}={B}$
9 fincygsubgodd.9 ${⊢}{\phi }\to {C}\parallel \left|{B}\right|$
10 fincygsubgodd.10 ${⊢}{\phi }\to {B}\in \mathrm{Fin}$
11 fincygsubgodd.11 ${⊢}{\phi }\to {C}\in ℕ$
12 eqid ${⊢}\mathrm{od}\left({G}\right)=\mathrm{od}\left({G}\right)$
13 4 rneqi
14 13 8 syl5reqr
15 1 2 12 6 7 14 cycsubggenodd ${⊢}{\phi }\to \mathrm{od}\left({G}\right)\left({A}\right)=if\left({B}\in \mathrm{Fin},\left|{B}\right|,0\right)$
16 10 iftrued ${⊢}{\phi }\to if\left({B}\in \mathrm{Fin},\left|{B}\right|,0\right)=\left|{B}\right|$
17 15 16 eqtrd ${⊢}{\phi }\to \mathrm{od}\left({G}\right)\left({A}\right)=\left|{B}\right|$
18 17 oveq1d ${⊢}{\phi }\to \frac{\mathrm{od}\left({G}\right)\left({A}\right)}{{C}}=\frac{\left|{B}\right|}{{C}}$
19 11 nnzd ${⊢}{\phi }\to {C}\in ℤ$
20 1 12 2 odmulg
21 6 7 19 20 syl3anc
22 1 12 odcl ${⊢}{A}\in {B}\to \mathrm{od}\left({G}\right)\left({A}\right)\in {ℕ}_{0}$
23 nn0z ${⊢}\mathrm{od}\left({G}\right)\left({A}\right)\in {ℕ}_{0}\to \mathrm{od}\left({G}\right)\left({A}\right)\in ℤ$
24 7 22 23 3syl ${⊢}{\phi }\to \mathrm{od}\left({G}\right)\left({A}\right)\in ℤ$
25 9 17 breqtrrd ${⊢}{\phi }\to {C}\parallel \mathrm{od}\left({G}\right)\left({A}\right)$
26 11 24 25 dvdsgcdidd ${⊢}{\phi }\to {C}\mathrm{gcd}\mathrm{od}\left({G}\right)\left({A}\right)={C}$
27 26 oveq1d
28 21 27 eqtrd
29 1 12 7 odcld ${⊢}{\phi }\to \mathrm{od}\left({G}\right)\left({A}\right)\in {ℕ}_{0}$
30 29 nn0cnd ${⊢}{\phi }\to \mathrm{od}\left({G}\right)\left({A}\right)\in ℂ$
31 1 2 6 19 7 mulgcld
32 1 12 31 odcld
33 32 nn0cnd
34 19 zcnd ${⊢}{\phi }\to {C}\in ℂ$
35 11 nnne0d ${⊢}{\phi }\to {C}\ne 0$
36 30 33 34 35 divmul2d
37 28 36 mpbird
38 18 37 eqtr3d
39 3 38 syl5eq
40 5 rneqi
41 40 a1i
42 1 2 12 6 31 41 cycsubggenodd
43 39 42 eqtrd ${⊢}{\phi }\to {D}=if\left(\mathrm{ran}{H}\in \mathrm{Fin},\left|\mathrm{ran}{H}\right|,0\right)$
44 iffalse ${⊢}¬\mathrm{ran}{H}\in \mathrm{Fin}\to if\left(\mathrm{ran}{H}\in \mathrm{Fin},\left|\mathrm{ran}{H}\right|,0\right)=0$
45 43 44 sylan9eq ${⊢}\left({\phi }\wedge ¬\mathrm{ran}{H}\in \mathrm{Fin}\right)\to {D}=0$
46 3 a1i ${⊢}{\phi }\to {D}=\frac{\left|{B}\right|}{{C}}$
47 hashcl ${⊢}{B}\in \mathrm{Fin}\to \left|{B}\right|\in {ℕ}_{0}$
48 nn0cn ${⊢}\left|{B}\right|\in {ℕ}_{0}\to \left|{B}\right|\in ℂ$
49 10 47 48 3syl ${⊢}{\phi }\to \left|{B}\right|\in ℂ$
50 7 10 hashelne0d ${⊢}{\phi }\to ¬\left|{B}\right|=0$
51 50 neqned ${⊢}{\phi }\to \left|{B}\right|\ne 0$
52 49 34 51 35 divne0d ${⊢}{\phi }\to \frac{\left|{B}\right|}{{C}}\ne 0$
53 46 52 eqnetrd ${⊢}{\phi }\to {D}\ne 0$
54 53 neneqd ${⊢}{\phi }\to ¬{D}=0$
55 54 adantr ${⊢}\left({\phi }\wedge ¬\mathrm{ran}{H}\in \mathrm{Fin}\right)\to ¬{D}=0$
56 45 55 condan ${⊢}{\phi }\to \mathrm{ran}{H}\in \mathrm{Fin}$
57 56 iftrued ${⊢}{\phi }\to if\left(\mathrm{ran}{H}\in \mathrm{Fin},\left|\mathrm{ran}{H}\right|,0\right)=\left|\mathrm{ran}{H}\right|$
58 39 42 57 3eqtrrd ${⊢}{\phi }\to \left|\mathrm{ran}{H}\right|={D}$