Proof of Theorem fincygsubgodd
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fincygsubgodd.3 | . . 3
⊢ 𝐷 = ((♯‘𝐵) / 𝐶) | 
| 2 |  | fincygsubgodd.1 | . . . . . . 7
⊢ 𝐵 = (Base‘𝐺) | 
| 3 |  | fincygsubgodd.2 | . . . . . . 7
⊢  · =
(.g‘𝐺) | 
| 4 |  | eqid 2737 | . . . . . . 7
⊢
(od‘𝐺) =
(od‘𝐺) | 
| 5 |  | fincygsubgodd.6 | . . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 6 |  | fincygsubgodd.7 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝐵) | 
| 7 |  | fincygsubgodd.8 | . . . . . . . 8
⊢ (𝜑 → ran 𝐹 = 𝐵) | 
| 8 |  | fincygsubgodd.4 | . . . . . . . . 9
⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴)) | 
| 9 | 8 | rneqi 5948 | . . . . . . . 8
⊢ ran 𝐹 = ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴)) | 
| 10 | 7, 9 | eqtr3di 2792 | . . . . . . 7
⊢ (𝜑 → 𝐵 = ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴))) | 
| 11 | 2, 3, 4, 5, 6, 10 | cycsubggenodd 20129 | . . . . . 6
⊢ (𝜑 → ((od‘𝐺)‘𝐴) = if(𝐵 ∈ Fin, (♯‘𝐵), 0)) | 
| 12 |  | fincygsubgodd.10 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ Fin) | 
| 13 | 12 | iftrued 4533 | . . . . . 6
⊢ (𝜑 → if(𝐵 ∈ Fin, (♯‘𝐵), 0) = (♯‘𝐵)) | 
| 14 | 11, 13 | eqtrd 2777 | . . . . 5
⊢ (𝜑 → ((od‘𝐺)‘𝐴) = (♯‘𝐵)) | 
| 15 | 14 | oveq1d 7446 | . . . 4
⊢ (𝜑 → (((od‘𝐺)‘𝐴) / 𝐶) = ((♯‘𝐵) / 𝐶)) | 
| 16 |  | fincygsubgodd.11 | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℕ) | 
| 17 | 16 | nnzd 12640 | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℤ) | 
| 18 | 2, 4, 3 | odmulg 19574 | . . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ ℤ) → ((od‘𝐺)‘𝐴) = ((𝐶 gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘(𝐶 · 𝐴)))) | 
| 19 | 5, 6, 17, 18 | syl3anc 1373 | . . . . . 6
⊢ (𝜑 → ((od‘𝐺)‘𝐴) = ((𝐶 gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘(𝐶 · 𝐴)))) | 
| 20 | 2, 4 | odcl 19554 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝐵 → ((od‘𝐺)‘𝐴) ∈
ℕ0) | 
| 21 |  | nn0z 12638 | . . . . . . . . 9
⊢
(((od‘𝐺)‘𝐴) ∈ ℕ0 →
((od‘𝐺)‘𝐴) ∈
ℤ) | 
| 22 | 6, 20, 21 | 3syl 18 | . . . . . . . 8
⊢ (𝜑 → ((od‘𝐺)‘𝐴) ∈ ℤ) | 
| 23 |  | fincygsubgodd.9 | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∥ (♯‘𝐵)) | 
| 24 | 23, 14 | breqtrrd 5171 | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∥ ((od‘𝐺)‘𝐴)) | 
| 25 | 16, 22, 24 | dvdsgcdidd 16574 | . . . . . . 7
⊢ (𝜑 → (𝐶 gcd ((od‘𝐺)‘𝐴)) = 𝐶) | 
| 26 | 25 | oveq1d 7446 | . . . . . 6
⊢ (𝜑 → ((𝐶 gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘(𝐶 · 𝐴))) = (𝐶 · ((od‘𝐺)‘(𝐶 · 𝐴)))) | 
| 27 | 19, 26 | eqtrd 2777 | . . . . 5
⊢ (𝜑 → ((od‘𝐺)‘𝐴) = (𝐶 · ((od‘𝐺)‘(𝐶 · 𝐴)))) | 
| 28 | 2, 4, 6 | odcld 19570 | . . . . . . 7
⊢ (𝜑 → ((od‘𝐺)‘𝐴) ∈
ℕ0) | 
| 29 | 28 | nn0cnd 12589 | . . . . . 6
⊢ (𝜑 → ((od‘𝐺)‘𝐴) ∈ ℂ) | 
| 30 | 2, 3, 5, 17, 6 | mulgcld 19114 | . . . . . . . 8
⊢ (𝜑 → (𝐶 · 𝐴) ∈ 𝐵) | 
| 31 | 2, 4, 30 | odcld 19570 | . . . . . . 7
⊢ (𝜑 → ((od‘𝐺)‘(𝐶 · 𝐴)) ∈
ℕ0) | 
| 32 | 31 | nn0cnd 12589 | . . . . . 6
⊢ (𝜑 → ((od‘𝐺)‘(𝐶 · 𝐴)) ∈ ℂ) | 
| 33 | 17 | zcnd 12723 | . . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 34 | 16 | nnne0d 12316 | . . . . . 6
⊢ (𝜑 → 𝐶 ≠ 0) | 
| 35 | 29, 32, 33, 34 | divmul2d 12076 | . . . . 5
⊢ (𝜑 → ((((od‘𝐺)‘𝐴) / 𝐶) = ((od‘𝐺)‘(𝐶 · 𝐴)) ↔ ((od‘𝐺)‘𝐴) = (𝐶 · ((od‘𝐺)‘(𝐶 · 𝐴))))) | 
| 36 | 27, 35 | mpbird 257 | . . . 4
⊢ (𝜑 → (((od‘𝐺)‘𝐴) / 𝐶) = ((od‘𝐺)‘(𝐶 · 𝐴))) | 
| 37 | 15, 36 | eqtr3d 2779 | . . 3
⊢ (𝜑 → ((♯‘𝐵) / 𝐶) = ((od‘𝐺)‘(𝐶 · 𝐴))) | 
| 38 | 1, 37 | eqtrid 2789 | . 2
⊢ (𝜑 → 𝐷 = ((od‘𝐺)‘(𝐶 · 𝐴))) | 
| 39 |  | fincygsubgodd.5 | . . . . 5
⊢ 𝐻 = (𝑛 ∈ ℤ ↦ (𝑛 · (𝐶 · 𝐴))) | 
| 40 | 39 | rneqi 5948 | . . . 4
⊢ ran 𝐻 = ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝐶 · 𝐴))) | 
| 41 | 40 | a1i 11 | . . 3
⊢ (𝜑 → ran 𝐻 = ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝐶 · 𝐴)))) | 
| 42 | 2, 3, 4, 5, 30, 41 | cycsubggenodd 20129 | . 2
⊢ (𝜑 → ((od‘𝐺)‘(𝐶 · 𝐴)) = if(ran 𝐻 ∈ Fin, (♯‘ran 𝐻), 0)) | 
| 43 | 38, 42 | eqtrd 2777 | . . . . 5
⊢ (𝜑 → 𝐷 = if(ran 𝐻 ∈ Fin, (♯‘ran 𝐻), 0)) | 
| 44 |  | iffalse 4534 | . . . . 5
⊢ (¬
ran 𝐻 ∈ Fin →
if(ran 𝐻 ∈ Fin,
(♯‘ran 𝐻), 0) =
0) | 
| 45 | 43, 44 | sylan9eq 2797 | . . . 4
⊢ ((𝜑 ∧ ¬ ran 𝐻 ∈ Fin) → 𝐷 = 0) | 
| 46 | 1 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 𝐷 = ((♯‘𝐵) / 𝐶)) | 
| 47 |  | hashcl 14395 | . . . . . . . . 9
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) | 
| 48 |  | nn0cn 12536 | . . . . . . . . 9
⊢
((♯‘𝐵)
∈ ℕ0 → (♯‘𝐵) ∈ ℂ) | 
| 49 | 12, 47, 48 | 3syl 18 | . . . . . . . 8
⊢ (𝜑 → (♯‘𝐵) ∈
ℂ) | 
| 50 | 6, 12 | hashelne0d 14407 | . . . . . . . . 9
⊢ (𝜑 → ¬ (♯‘𝐵) = 0) | 
| 51 | 50 | neqned 2947 | . . . . . . . 8
⊢ (𝜑 → (♯‘𝐵) ≠ 0) | 
| 52 | 49, 33, 51, 34 | divne0d 12059 | . . . . . . 7
⊢ (𝜑 → ((♯‘𝐵) / 𝐶) ≠ 0) | 
| 53 | 46, 52 | eqnetrd 3008 | . . . . . 6
⊢ (𝜑 → 𝐷 ≠ 0) | 
| 54 | 53 | neneqd 2945 | . . . . 5
⊢ (𝜑 → ¬ 𝐷 = 0) | 
| 55 | 54 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ¬ ran 𝐻 ∈ Fin) → ¬ 𝐷 = 0) | 
| 56 | 45, 55 | condan 818 | . . 3
⊢ (𝜑 → ran 𝐻 ∈ Fin) | 
| 57 | 56 | iftrued 4533 | . 2
⊢ (𝜑 → if(ran 𝐻 ∈ Fin, (♯‘ran 𝐻), 0) = (♯‘ran 𝐻)) | 
| 58 | 38, 42, 57 | 3eqtrrd 2782 | 1
⊢ (𝜑 → (♯‘ran 𝐻) = 𝐷) |