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

Proof

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