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=BaseG
fincygsubgodexd.2 ⊢φ→G∈CycGrp
fincygsubgodexd.3 ⊢φ→C∥B
fincygsubgodexd.4 ⊢φ→B∈Fin
fincygsubgodexd.5 ⊢φ→C∈ℕ
Assertion fincygsubgodexd ⊢φ→∃x∈SubGrp⁡Gx=C

Proof

Step Hyp Ref Expression
1 fincygsubgodexd.1 ⊢B=BaseG
2 fincygsubgodexd.2 ⊢φ→G∈CycGrp
3 fincygsubgodexd.3 ⊢φ→C∥B
4 fincygsubgodexd.4 ⊢φ→B∈Fin
5 fincygsubgodexd.5 ⊢φ→C∈ℕ
6 eqid ⊢⋅G=⋅G
7 1 6 iscyg ⊢G∈CycGrp↔G∈Grp∧∃y∈Bran⁡n∈ℤ⟼n⋅Gy=B
8 7 simprbi ⊢G∈CycGrp→∃y∈Bran⁡n∈ℤ⟼n⋅Gy=B
9 2 8 syl ⊢φ→∃y∈Bran⁡n∈ℤ⟼n⋅Gy=B
10 eqid ⊢n∈ℤ⟼n⋅GBC⋅Gy=n∈ℤ⟼n⋅GBC⋅Gy
11 cyggrp ⊢G∈CycGrp→G∈Grp
12 2 11 syl ⊢φ→G∈Grp
13 12 adantr ⊢φ∧y∈B∧ran⁡n∈ℤ⟼n⋅Gy=B→G∈Grp
14 simprl ⊢φ∧y∈B∧ran⁡n∈ℤ⟼n⋅Gy=B→y∈B
15 1 12 4 hashfingrpnn ⊢φ→B∈ℕ
16 nndivdvds ⊢B∈ℕ∧C∈ℕ→C∥B↔BC∈ℕ
17 15 5 16 syl2anc ⊢φ→C∥B↔BC∈ℕ
18 3 17 mpbid ⊢φ→BC∈ℕ
19 18 adantr ⊢φ∧y∈B∧ran⁡n∈ℤ⟼n⋅Gy=B→BC∈ℕ
20 1 6 10 13 14 19 fincygsubgd ⊢φ∧y∈B∧ran⁡n∈ℤ⟼n⋅Gy=B→ran⁡n∈ℤ⟼n⋅GBC⋅Gy∈SubGrp⁡G
21 simpr ⊢φ∧y∈B∧ran⁡n∈ℤ⟼n⋅Gy=B∧x=ran⁡n∈ℤ⟼n⋅GBC⋅Gy→x=ran⁡n∈ℤ⟼n⋅GBC⋅Gy
22 21 fveq2d ⊢φ∧y∈B∧ran⁡n∈ℤ⟼n⋅Gy=B∧x=ran⁡n∈ℤ⟼n⋅GBC⋅Gy→x=ran⁡n∈ℤ⟼n⋅GBC⋅Gy
23 eqid ⊢BBC=BBC
24 eqid ⊢n∈ℤ⟼n⋅Gy=n∈ℤ⟼n⋅Gy
25 simprr ⊢φ∧y∈B∧ran⁡n∈ℤ⟼n⋅Gy=B→ran⁡n∈ℤ⟼n⋅Gy=B
26 5 nnne0d ⊢φ→C≠0
27 divconjdvds ⊢C∥B∧C≠0→BC∥B
28 3 26 27 syl2anc ⊢φ→BC∥B
29 28 adantr ⊢φ∧y∈B∧ran⁡n∈ℤ⟼n⋅Gy=B→BC∥B
30 4 adantr ⊢φ∧y∈B∧ran⁡n∈ℤ⟼n⋅Gy=B→B∈Fin
31 1 6 23 24 10 13 14 25 29 30 19 fincygsubgodd ⊢φ∧y∈B∧ran⁡n∈ℤ⟼n⋅Gy=B→ran⁡n∈ℤ⟼n⋅GBC⋅Gy=BBC
32 31 adantr ⊢φ∧y∈B∧ran⁡n∈ℤ⟼n⋅Gy=B∧x=ran⁡n∈ℤ⟼n⋅GBC⋅Gy→ran⁡n∈ℤ⟼n⋅GBC⋅Gy=BBC
33 15 nncnd ⊢φ→B∈ℂ
34 5 nncnd ⊢φ→C∈ℂ
35 15 nnne0d ⊢φ→B≠0
36 33 34 35 26 ddcand ⊢φ→BBC=C
37 36 ad2antrr ⊢φ∧y∈B∧ran⁡n∈ℤ⟼n⋅Gy=B∧x=ran⁡n∈ℤ⟼n⋅GBC⋅Gy→BBC=C
38 22 32 37 3eqtrd ⊢φ∧y∈B∧ran⁡n∈ℤ⟼n⋅Gy=B∧x=ran⁡n∈ℤ⟼n⋅GBC⋅Gy→x=C
39 20 38 rspcedeq1vd ⊢φ∧y∈B∧ran⁡n∈ℤ⟼n⋅Gy=B→∃x∈SubGrp⁡Gx=C
40 9 39 rexlimddv ⊢φ→∃x∈SubGrp⁡Gx=C