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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	fincygsubgodd.2	⊢ · = ( .g ‘ 𝐺 )
	fincygsubgodd.3	⊢ 𝐷 = ( ( ♯ ‘ 𝐵 ) / 𝐶 )
	fincygsubgodd.4	⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) )
	fincygsubgodd.5	⊢ 𝐻 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝐶 · 𝐴 ) ) )
	fincygsubgodd.6	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	fincygsubgodd.7	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	fincygsubgodd.8	⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
	fincygsubgodd.9	⊢ ( 𝜑 → 𝐶 ∥ ( ♯ ‘ 𝐵 ) )
	fincygsubgodd.10	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	fincygsubgodd.11	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
Assertion	fincygsubgodd	⊢ ( 𝜑 → ( ♯ ‘ ran 𝐻 ) = 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		fincygsubgodd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		fincygsubgodd.2	⊢ · = ( .g ‘ 𝐺 )
3		fincygsubgodd.3	⊢ 𝐷 = ( ( ♯ ‘ 𝐵 ) / 𝐶 )
4		fincygsubgodd.4	⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) )
5		fincygsubgodd.5	⊢ 𝐻 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝐶 · 𝐴 ) ) )
6		fincygsubgodd.6	⊢ ( 𝜑 → 𝐺 ∈ Grp )
7		fincygsubgodd.7	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
8		fincygsubgodd.8	⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
9		fincygsubgodd.9	⊢ ( 𝜑 → 𝐶 ∥ ( ♯ ‘ 𝐵 ) )
10		fincygsubgodd.10	⊢ ( 𝜑 → 𝐵 ∈ Fin )
11		fincygsubgodd.11	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
12		eqid	⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
13	4	rneqi	⊢ ran 𝐹 = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) )
14	8 13	eqtr3di	⊢ ( 𝜑 → 𝐵 = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) ) )
15	1 2 12 6 7 14	cycsubggenodd	⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) )
16	10	iftrued	⊢ ( 𝜑 → if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) = ( ♯ ‘ 𝐵 ) )
17	15 16	eqtrd	⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )
18	17	oveq1d	⊢ ( 𝜑 → ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) / 𝐶 ) = ( ( ♯ ‘ 𝐵 ) / 𝐶 ) )
19	11	nnzd	⊢ ( 𝜑 → 𝐶 ∈ ℤ )
20	1 12 2	odmulg	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ ℤ ) → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = ( ( 𝐶 gcd ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) · ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ) )
21	6 7 19 20	syl3anc	⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = ( ( 𝐶 gcd ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) · ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ) )
22	1 12	odcl	⊢ ( 𝐴 ∈ 𝐵 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℕ0 )
23		nn0z	⊢ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℕ0 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℤ )
24	7 22 23	3syl	⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℤ )
25	9 17	breqtrrd	⊢ ( 𝜑 → 𝐶 ∥ ( ( od ‘ 𝐺 ) ‘ 𝐴 ) )
26	11 24 25	dvdsgcdidd	⊢ ( 𝜑 → ( 𝐶 gcd ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) = 𝐶 )
27	26	oveq1d	⊢ ( 𝜑 → ( ( 𝐶 gcd ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) · ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ) = ( 𝐶 · ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ) )
28	21 27	eqtrd	⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = ( 𝐶 · ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ) )
29	1 12 7	odcld	⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℕ0 )
30	29	nn0cnd	⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℂ )
31	1 2 6 19 7	mulgcld	⊢ ( 𝜑 → ( 𝐶 · 𝐴 ) ∈ 𝐵 )
32	1 12 31	odcld	⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ∈ ℕ0 )
33	32	nn0cnd	⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ∈ ℂ )
34	19	zcnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
35	11	nnne0d	⊢ ( 𝜑 → 𝐶 ≠ 0 )
36	30 33 34 35	divmul2d	⊢ ( 𝜑 → ( ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) / 𝐶 ) = ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ↔ ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = ( 𝐶 · ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ) ) )
37	28 36	mpbird	⊢ ( 𝜑 → ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) / 𝐶 ) = ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) )
38	18 37	eqtr3d	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) / 𝐶 ) = ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) )
39	3 38	eqtrid	⊢ ( 𝜑 → 𝐷 = ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) )
40	5	rneqi	⊢ ran 𝐻 = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝐶 · 𝐴 ) ) )
41	40	a1i	⊢ ( 𝜑 → ran 𝐻 = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝐶 · 𝐴 ) ) ) )
42	1 2 12 6 31 41	cycsubggenodd	⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) = if ( ran 𝐻 ∈ Fin , ( ♯ ‘ ran 𝐻 ) , 0 ) )
43	39 42	eqtrd	⊢ ( 𝜑 → 𝐷 = if ( ran 𝐻 ∈ Fin , ( ♯ ‘ ran 𝐻 ) , 0 ) )
44		iffalse	⊢ ( ¬ ran 𝐻 ∈ Fin → if ( ran 𝐻 ∈ Fin , ( ♯ ‘ ran 𝐻 ) , 0 ) = 0 )
45	43 44	sylan9eq	⊢ ( ( 𝜑 ∧ ¬ ran 𝐻 ∈ Fin ) → 𝐷 = 0 )
46	3	a1i	⊢ ( 𝜑 → 𝐷 = ( ( ♯ ‘ 𝐵 ) / 𝐶 ) )
47		hashcl	⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
48		nn0cn	⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 → ( ♯ ‘ 𝐵 ) ∈ ℂ )
49	10 47 48	3syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℂ )
50	7 10	hashelne0d	⊢ ( 𝜑 → ¬ ( ♯ ‘ 𝐵 ) = 0 )
51	50	neqned	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ≠ 0 )
52	49 34 51 35	divne0d	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ≠ 0 )
53	46 52	eqnetrd	⊢ ( 𝜑 → 𝐷 ≠ 0 )
54	53	neneqd	⊢ ( 𝜑 → ¬ 𝐷 = 0 )
55	54	adantr	⊢ ( ( 𝜑 ∧ ¬ ran 𝐻 ∈ Fin ) → ¬ 𝐷 = 0 )
56	45 55	condan	⊢ ( 𝜑 → ran 𝐻 ∈ Fin )
57	56	iftrued	⊢ ( 𝜑 → if ( ran 𝐻 ∈ Fin , ( ♯ ‘ ran 𝐻 ) , 0 ) = ( ♯ ‘ ran 𝐻 ) )
58	39 42 57	3eqtrrd	⊢ ( 𝜑 → ( ♯ ‘ ran 𝐻 ) = 𝐷 )