# Metamath Proof Explorer

## Theorem fincygsubgodexd

Description: A finite cyclic group has subgroups of every possible order. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses fincygsubgodexd.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
fincygsubgodexd.2 ${⊢}{\phi }\to {G}\in \mathrm{CycGrp}$
fincygsubgodexd.3 ${⊢}{\phi }\to {C}\parallel \left|{B}\right|$
fincygsubgodexd.4 ${⊢}{\phi }\to {B}\in \mathrm{Fin}$
fincygsubgodexd.5 ${⊢}{\phi }\to {C}\in ℕ$
Assertion fincygsubgodexd ${⊢}{\phi }\to \exists {x}\in \mathrm{SubGrp}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left|{x}\right|={C}$

### Proof

Step Hyp Ref Expression
1 fincygsubgodexd.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 fincygsubgodexd.2 ${⊢}{\phi }\to {G}\in \mathrm{CycGrp}$
3 fincygsubgodexd.3 ${⊢}{\phi }\to {C}\parallel \left|{B}\right|$
4 fincygsubgodexd.4 ${⊢}{\phi }\to {B}\in \mathrm{Fin}$
5 fincygsubgodexd.5 ${⊢}{\phi }\to {C}\in ℕ$
6 eqid ${⊢}{\cdot }_{{G}}={\cdot }_{{G}}$
7 1 6 iscyg ${⊢}{G}\in \mathrm{CycGrp}↔\left({G}\in \mathrm{Grp}\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right)$
8 7 simprbi ${⊢}{G}\in \mathrm{CycGrp}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}$
9 2 8 syl ${⊢}{\phi }\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}$
10 eqid ${⊢}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}\left(\left(\frac{\left|{B}\right|}{{C}}\right){\cdot }_{{G}}{y}\right)\right)=\left({n}\in ℤ⟼{n}{\cdot }_{{G}}\left(\left(\frac{\left|{B}\right|}{{C}}\right){\cdot }_{{G}}{y}\right)\right)$
11 cyggrp ${⊢}{G}\in \mathrm{CycGrp}\to {G}\in \mathrm{Grp}$
12 2 11 syl ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
13 12 adantr ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right)\right)\to {G}\in \mathrm{Grp}$
14 simprl ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right)\right)\to {y}\in {B}$
15 1 12 4 hashfingrpnn ${⊢}{\phi }\to \left|{B}\right|\in ℕ$
16 nndivdvds ${⊢}\left(\left|{B}\right|\in ℕ\wedge {C}\in ℕ\right)\to \left({C}\parallel \left|{B}\right|↔\frac{\left|{B}\right|}{{C}}\in ℕ\right)$
17 15 5 16 syl2anc ${⊢}{\phi }\to \left({C}\parallel \left|{B}\right|↔\frac{\left|{B}\right|}{{C}}\in ℕ\right)$
18 3 17 mpbid ${⊢}{\phi }\to \frac{\left|{B}\right|}{{C}}\in ℕ$
19 18 adantr ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right)\right)\to \frac{\left|{B}\right|}{{C}}\in ℕ$
20 1 6 10 13 14 19 fincygsubgd ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right)\right)\to \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}\left(\left(\frac{\left|{B}\right|}{{C}}\right){\cdot }_{{G}}{y}\right)\right)\in \mathrm{SubGrp}\left({G}\right)$
21 simpr ${⊢}\left(\left({\phi }\wedge \left({y}\in {B}\wedge \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right)\right)\wedge {x}=\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}\left(\left(\frac{\left|{B}\right|}{{C}}\right){\cdot }_{{G}}{y}\right)\right)\right)\to {x}=\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}\left(\left(\frac{\left|{B}\right|}{{C}}\right){\cdot }_{{G}}{y}\right)\right)$
22 21 fveq2d ${⊢}\left(\left({\phi }\wedge \left({y}\in {B}\wedge \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right)\right)\wedge {x}=\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}\left(\left(\frac{\left|{B}\right|}{{C}}\right){\cdot }_{{G}}{y}\right)\right)\right)\to \left|{x}\right|=\left|\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}\left(\left(\frac{\left|{B}\right|}{{C}}\right){\cdot }_{{G}}{y}\right)\right)\right|$
23 eqid ${⊢}\frac{\left|{B}\right|}{\frac{\left|{B}\right|}{{C}}}=\frac{\left|{B}\right|}{\frac{\left|{B}\right|}{{C}}}$
24 eqid ${⊢}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)=\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)$
25 simprr ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right)\right)\to \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}$
26 5 nnne0d ${⊢}{\phi }\to {C}\ne 0$
27 divconjdvds ${⊢}\left({C}\parallel \left|{B}\right|\wedge {C}\ne 0\right)\to \left(\frac{\left|{B}\right|}{{C}}\right)\parallel \left|{B}\right|$
28 3 26 27 syl2anc ${⊢}{\phi }\to \left(\frac{\left|{B}\right|}{{C}}\right)\parallel \left|{B}\right|$
29 28 adantr ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right)\right)\to \left(\frac{\left|{B}\right|}{{C}}\right)\parallel \left|{B}\right|$
30 4 adantr ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right)\right)\to {B}\in \mathrm{Fin}$
31 1 6 23 24 10 13 14 25 29 30 19 fincygsubgodd ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right)\right)\to \left|\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}\left(\left(\frac{\left|{B}\right|}{{C}}\right){\cdot }_{{G}}{y}\right)\right)\right|=\frac{\left|{B}\right|}{\frac{\left|{B}\right|}{{C}}}$
32 31 adantr ${⊢}\left(\left({\phi }\wedge \left({y}\in {B}\wedge \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right)\right)\wedge {x}=\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}\left(\left(\frac{\left|{B}\right|}{{C}}\right){\cdot }_{{G}}{y}\right)\right)\right)\to \left|\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}\left(\left(\frac{\left|{B}\right|}{{C}}\right){\cdot }_{{G}}{y}\right)\right)\right|=\frac{\left|{B}\right|}{\frac{\left|{B}\right|}{{C}}}$
33 15 nncnd ${⊢}{\phi }\to \left|{B}\right|\in ℂ$
34 5 nncnd ${⊢}{\phi }\to {C}\in ℂ$
35 15 nnne0d ${⊢}{\phi }\to \left|{B}\right|\ne 0$
36 33 34 35 26 ddcand ${⊢}{\phi }\to \frac{\left|{B}\right|}{\frac{\left|{B}\right|}{{C}}}={C}$
37 36 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({y}\in {B}\wedge \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right)\right)\wedge {x}=\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}\left(\left(\frac{\left|{B}\right|}{{C}}\right){\cdot }_{{G}}{y}\right)\right)\right)\to \frac{\left|{B}\right|}{\frac{\left|{B}\right|}{{C}}}={C}$
38 22 32 37 3eqtrd ${⊢}\left(\left({\phi }\wedge \left({y}\in {B}\wedge \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right)\right)\wedge {x}=\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}\left(\left(\frac{\left|{B}\right|}{{C}}\right){\cdot }_{{G}}{y}\right)\right)\right)\to \left|{x}\right|={C}$
39 20 38 rspcedeq1vd ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge \mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right)\right)\to \exists {x}\in \mathrm{SubGrp}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left|{x}\right|={C}$
40 9 39 rexlimddv ${⊢}{\phi }\to \exists {x}\in \mathrm{SubGrp}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left|{x}\right|={C}$