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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
fincygsubgodexd.2 ⊢ ( 𝜑 → 𝐺 ∈ CycGrp )
fincygsubgodexd.3 ⊢ ( 𝜑 → 𝐶 ∥ ( ♯ ‘ 𝐵 ) )
fincygsubgodexd.4 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
fincygsubgodexd.5 ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
Assertion fincygsubgodexd ( 𝜑 → ∃ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 fincygsubgodexd.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 fincygsubgodexd.2 ⊢ ( 𝜑 → 𝐺 ∈ CycGrp )
3 fincygsubgodexd.3 ⊢ ( 𝜑 → 𝐶 ∥ ( ♯ ‘ 𝐵 ) )
4 fincygsubgodexd.4 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
5 fincygsubgodexd.5 ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
6 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
7 1 6 iscyg ⊢ ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ ∃ 𝑦 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 ) )
8 7 simprbi ⊢ ( 𝐺 ∈ CycGrp → ∃ 𝑦 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 )
9 2 8 syl ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 )
10 eqid ⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ( .g ‘ 𝐺 ) 𝑦 ) ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ( .g ‘ 𝐺 ) 𝑦 ) ) )
11 cyggrp ⊢ ( 𝐺 ∈ CycGrp → 𝐺 ∈ Grp )
12 2 11 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
13 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 ) ) → 𝐺 ∈ Grp )
14 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 ) ) → 𝑦 ∈ 𝐵 )
15 1 12 4 hashfingrpnn ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ )
16 nndivdvds ⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 ∥ ( ♯ ‘ 𝐵 ) ↔ ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ∈ ℕ ) )
17 15 5 16 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∥ ( ♯ ‘ 𝐵 ) ↔ ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ∈ ℕ ) )
18 3 17 mpbid ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ∈ ℕ )
19 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ∈ ℕ )
20 1 6 10 13 14 19 fincygsubgd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 ) ) → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ( .g ‘ 𝐺 ) 𝑦 ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
21 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 ) ) ∧ 𝑥 = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ( .g ‘ 𝐺 ) 𝑦 ) ) ) ) → 𝑥 = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ( .g ‘ 𝐺 ) 𝑦 ) ) ) )
22 21 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 ) ) ∧ 𝑥 = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ( .g ‘ 𝐺 ) 𝑦 ) ) ) ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ( .g ‘ 𝐺 ) 𝑦 ) ) ) ) )
23 eqid ⊢ ( ( ♯ ‘ 𝐵 ) / ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ) = ( ( ♯ ‘ 𝐵 ) / ( ( ♯ ‘ 𝐵 ) / 𝐶 ) )
24 eqid ⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) )
25 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 ) ) → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 )
26 5 nnne0d ⊢ ( 𝜑 → 𝐶 ≠ 0 )
27 divconjdvds ⊢ ( ( 𝐶 ∥ ( ♯ ‘ 𝐵 ) ∧ 𝐶 ≠ 0 ) → ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ∥ ( ♯ ‘ 𝐵 ) )
28 3 26 27 syl2anc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ∥ ( ♯ ‘ 𝐵 ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ∥ ( ♯ ‘ 𝐵 ) )
30 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 ) ) → 𝐵 ∈ Fin )
31 1 6 23 24 10 13 14 25 29 30 19 fincygsubgodd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 ) ) → ( ♯ ‘ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ( .g ‘ 𝐺 ) 𝑦 ) ) ) ) = ( ( ♯ ‘ 𝐵 ) / ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ) )
32 31 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 ) ) ∧ 𝑥 = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ( .g ‘ 𝐺 ) 𝑦 ) ) ) ) → ( ♯ ‘ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ( .g ‘ 𝐺 ) 𝑦 ) ) ) ) = ( ( ♯ ‘ 𝐵 ) / ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ) )
33 15 nncnd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℂ )
34 5 nncnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
35 15 nnne0d ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ≠ 0 )
36 33 34 35 26 ddcand ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) / ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ) = 𝐶 )
37 36 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 ) ) ∧ 𝑥 = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ( .g ‘ 𝐺 ) 𝑦 ) ) ) ) → ( ( ♯ ‘ 𝐵 ) / ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ) = 𝐶 )
38 22 32 37 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 ) ) ∧ 𝑥 = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ( .g ‘ 𝐺 ) 𝑦 ) ) ) ) → ( ♯ ‘ 𝑥 ) = 𝐶 )
39 20 38 rspcedeqvd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑦 ) ) = 𝐵 ) ) → ∃ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) = 𝐶 )
40 9 39 rexlimddv ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) = 𝐶 )