Step | Hyp | Ref
| Expression |
1 | | fincygsubgodd.3 |
. . 3
β’ π· = ((β―βπ΅) / πΆ) |
2 | | fincygsubgodd.1 |
. . . . . . 7
β’ π΅ = (BaseβπΊ) |
3 | | fincygsubgodd.2 |
. . . . . . 7
β’ Β· =
(.gβπΊ) |
4 | | eqid 2732 |
. . . . . . 7
β’
(odβπΊ) =
(odβπΊ) |
5 | | fincygsubgodd.6 |
. . . . . . 7
β’ (π β πΊ β Grp) |
6 | | fincygsubgodd.7 |
. . . . . . 7
β’ (π β π΄ β π΅) |
7 | | fincygsubgodd.8 |
. . . . . . . 8
β’ (π β ran πΉ = π΅) |
8 | | fincygsubgodd.4 |
. . . . . . . . 9
β’ πΉ = (π β β€ β¦ (π Β· π΄)) |
9 | 8 | rneqi 5936 |
. . . . . . . 8
β’ ran πΉ = ran (π β β€ β¦ (π Β· π΄)) |
10 | 7, 9 | eqtr3di 2787 |
. . . . . . 7
β’ (π β π΅ = ran (π β β€ β¦ (π Β· π΄))) |
11 | 2, 3, 4, 5, 6, 10 | cycsubggenodd 19978 |
. . . . . 6
β’ (π β ((odβπΊ)βπ΄) = if(π΅ β Fin, (β―βπ΅), 0)) |
12 | | fincygsubgodd.10 |
. . . . . . 7
β’ (π β π΅ β Fin) |
13 | 12 | iftrued 4536 |
. . . . . 6
β’ (π β if(π΅ β Fin, (β―βπ΅), 0) = (β―βπ΅)) |
14 | 11, 13 | eqtrd 2772 |
. . . . 5
β’ (π β ((odβπΊ)βπ΄) = (β―βπ΅)) |
15 | 14 | oveq1d 7423 |
. . . 4
β’ (π β (((odβπΊ)βπ΄) / πΆ) = ((β―βπ΅) / πΆ)) |
16 | | fincygsubgodd.11 |
. . . . . . . 8
β’ (π β πΆ β β) |
17 | 16 | nnzd 12584 |
. . . . . . 7
β’ (π β πΆ β β€) |
18 | 2, 4, 3 | odmulg 19423 |
. . . . . . 7
β’ ((πΊ β Grp β§ π΄ β π΅ β§ πΆ β β€) β ((odβπΊ)βπ΄) = ((πΆ gcd ((odβπΊ)βπ΄)) Β· ((odβπΊ)β(πΆ Β· π΄)))) |
19 | 5, 6, 17, 18 | syl3anc 1371 |
. . . . . 6
β’ (π β ((odβπΊ)βπ΄) = ((πΆ gcd ((odβπΊ)βπ΄)) Β· ((odβπΊ)β(πΆ Β· π΄)))) |
20 | 2, 4 | odcl 19403 |
. . . . . . . . 9
β’ (π΄ β π΅ β ((odβπΊ)βπ΄) β
β0) |
21 | | nn0z 12582 |
. . . . . . . . 9
β’
(((odβπΊ)βπ΄) β β0 β
((odβπΊ)βπ΄) β
β€) |
22 | 6, 20, 21 | 3syl 18 |
. . . . . . . 8
β’ (π β ((odβπΊ)βπ΄) β β€) |
23 | | fincygsubgodd.9 |
. . . . . . . . 9
β’ (π β πΆ β₯ (β―βπ΅)) |
24 | 23, 14 | breqtrrd 5176 |
. . . . . . . 8
β’ (π β πΆ β₯ ((odβπΊ)βπ΄)) |
25 | 16, 22, 24 | dvdsgcdidd 16478 |
. . . . . . 7
β’ (π β (πΆ gcd ((odβπΊ)βπ΄)) = πΆ) |
26 | 25 | oveq1d 7423 |
. . . . . 6
β’ (π β ((πΆ gcd ((odβπΊ)βπ΄)) Β· ((odβπΊ)β(πΆ Β· π΄))) = (πΆ Β· ((odβπΊ)β(πΆ Β· π΄)))) |
27 | 19, 26 | eqtrd 2772 |
. . . . 5
β’ (π β ((odβπΊ)βπ΄) = (πΆ Β· ((odβπΊ)β(πΆ Β· π΄)))) |
28 | 2, 4, 6 | odcld 19419 |
. . . . . . 7
β’ (π β ((odβπΊ)βπ΄) β
β0) |
29 | 28 | nn0cnd 12533 |
. . . . . 6
β’ (π β ((odβπΊ)βπ΄) β β) |
30 | 2, 3, 5, 17, 6 | mulgcld 18975 |
. . . . . . . 8
β’ (π β (πΆ Β· π΄) β π΅) |
31 | 2, 4, 30 | odcld 19419 |
. . . . . . 7
β’ (π β ((odβπΊ)β(πΆ Β· π΄)) β
β0) |
32 | 31 | nn0cnd 12533 |
. . . . . 6
β’ (π β ((odβπΊ)β(πΆ Β· π΄)) β β) |
33 | 17 | zcnd 12666 |
. . . . . 6
β’ (π β πΆ β β) |
34 | 16 | nnne0d 12261 |
. . . . . 6
β’ (π β πΆ β 0) |
35 | 29, 32, 33, 34 | divmul2d 12022 |
. . . . 5
β’ (π β ((((odβπΊ)βπ΄) / πΆ) = ((odβπΊ)β(πΆ Β· π΄)) β ((odβπΊ)βπ΄) = (πΆ Β· ((odβπΊ)β(πΆ Β· π΄))))) |
36 | 27, 35 | mpbird 256 |
. . . 4
β’ (π β (((odβπΊ)βπ΄) / πΆ) = ((odβπΊ)β(πΆ Β· π΄))) |
37 | 15, 36 | eqtr3d 2774 |
. . 3
β’ (π β ((β―βπ΅) / πΆ) = ((odβπΊ)β(πΆ Β· π΄))) |
38 | 1, 37 | eqtrid 2784 |
. 2
β’ (π β π· = ((odβπΊ)β(πΆ Β· π΄))) |
39 | | fincygsubgodd.5 |
. . . . 5
β’ π» = (π β β€ β¦ (π Β· (πΆ Β· π΄))) |
40 | 39 | rneqi 5936 |
. . . 4
β’ ran π» = ran (π β β€ β¦ (π Β· (πΆ Β· π΄))) |
41 | 40 | a1i 11 |
. . 3
β’ (π β ran π» = ran (π β β€ β¦ (π Β· (πΆ Β· π΄)))) |
42 | 2, 3, 4, 5, 30, 41 | cycsubggenodd 19978 |
. 2
β’ (π β ((odβπΊ)β(πΆ Β· π΄)) = if(ran π» β Fin, (β―βran π»), 0)) |
43 | 38, 42 | eqtrd 2772 |
. . . . 5
β’ (π β π· = if(ran π» β Fin, (β―βran π»), 0)) |
44 | | iffalse 4537 |
. . . . 5
β’ (Β¬
ran π» β Fin β
if(ran π» β Fin,
(β―βran π»), 0) =
0) |
45 | 43, 44 | sylan9eq 2792 |
. . . 4
β’ ((π β§ Β¬ ran π» β Fin) β π· = 0) |
46 | 1 | a1i 11 |
. . . . . . 7
β’ (π β π· = ((β―βπ΅) / πΆ)) |
47 | | hashcl 14315 |
. . . . . . . . 9
β’ (π΅ β Fin β
(β―βπ΅) β
β0) |
48 | | nn0cn 12481 |
. . . . . . . . 9
β’
((β―βπ΅)
β β0 β (β―βπ΅) β β) |
49 | 12, 47, 48 | 3syl 18 |
. . . . . . . 8
β’ (π β (β―βπ΅) β
β) |
50 | 6, 12 | hashelne0d 14327 |
. . . . . . . . 9
β’ (π β Β¬ (β―βπ΅) = 0) |
51 | 50 | neqned 2947 |
. . . . . . . 8
β’ (π β (β―βπ΅) β 0) |
52 | 49, 33, 51, 34 | divne0d 12005 |
. . . . . . 7
β’ (π β ((β―βπ΅) / πΆ) β 0) |
53 | 46, 52 | eqnetrd 3008 |
. . . . . 6
β’ (π β π· β 0) |
54 | 53 | neneqd 2945 |
. . . . 5
β’ (π β Β¬ π· = 0) |
55 | 54 | adantr 481 |
. . . 4
β’ ((π β§ Β¬ ran π» β Fin) β Β¬ π· = 0) |
56 | 45, 55 | condan 816 |
. . 3
β’ (π β ran π» β Fin) |
57 | 56 | iftrued 4536 |
. 2
β’ (π β if(ran π» β Fin, (β―βran π»), 0) = (β―βran π»)) |
58 | 38, 42, 57 | 3eqtrrd 2777 |
1
β’ (π β (β―βran π») = π·) |