Step | Hyp | Ref
| Expression |
1 | | iotaex 6470 |
. . . . . 6
β’
(β©ββπ β β€ (π¦ = (πΏβπ) β§ β = (π /L π))) β V |
2 | 1 | a1i 11 |
. . . . 5
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π¦ β π΅) β (β©ββπ β β€ (π¦ = (πΏβπ) β§ β = (π /L π))) β V) |
3 | | lgsdchr.x |
. . . . . 6
β’ π = (π¦ β π΅ β¦ (β©ββπ β β€ (π¦ = (πΏβπ) β§ β = (π /L π)))) |
4 | 3 | a1i 11 |
. . . . 5
β’ ((π β β β§ Β¬ 2
β₯ π) β π = (π¦ β π΅ β¦ (β©ββπ β β€ (π¦ = (πΏβπ) β§ β = (π /L π))))) |
5 | | nnnn0 12421 |
. . . . . . . . 9
β’ (π β β β π β
β0) |
6 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β β β§ Β¬ 2
β₯ π) β π β
β0) |
7 | | lgsdchr.z |
. . . . . . . . 9
β’ π =
(β€/nβ€βπ) |
8 | | lgsdchr.b |
. . . . . . . . 9
β’ π΅ = (Baseβπ) |
9 | | lgsdchr.l |
. . . . . . . . 9
β’ πΏ = (β€RHomβπ) |
10 | 7, 8, 9 | znzrhfo 20957 |
. . . . . . . 8
β’ (π β β0
β πΏ:β€βontoβπ΅) |
11 | 6, 10 | syl 17 |
. . . . . . 7
β’ ((π β β β§ Β¬ 2
β₯ π) β πΏ:β€βontoβπ΅) |
12 | | foelrn 7057 |
. . . . . . 7
β’ ((πΏ:β€βontoβπ΅ β§ π₯ β π΅) β βπ β β€ π₯ = (πΏβπ)) |
13 | 11, 12 | sylan 581 |
. . . . . 6
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π₯ β π΅) β βπ β β€ π₯ = (πΏβπ)) |
14 | | lgsdchr.g |
. . . . . . . . . . 11
β’ πΊ = (DChrβπ) |
15 | | lgsdchr.d |
. . . . . . . . . . 11
β’ π· = (BaseβπΊ) |
16 | 14, 7, 15, 8, 9, 3 | lgsdchrval 26705 |
. . . . . . . . . 10
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π β β€) β (πβ(πΏβπ)) = (π /L π)) |
17 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π β β€) β π β
β€) |
18 | | nnz 12521 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β€) |
19 | 18 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π β β€) β π β
β€) |
20 | | lgscl 26662 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β€) β (π /L π) β
β€) |
21 | 17, 19, 20 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π β β€) β (π /L π) β
β€) |
22 | 21 | zred 12608 |
. . . . . . . . . 10
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π β β€) β (π /L π) β
β) |
23 | 16, 22 | eqeltrd 2838 |
. . . . . . . . 9
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π β β€) β (πβ(πΏβπ)) β β) |
24 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π₯ = (πΏβπ) β (πβπ₯) = (πβ(πΏβπ))) |
25 | 24 | eleq1d 2823 |
. . . . . . . . 9
β’ (π₯ = (πΏβπ) β ((πβπ₯) β β β (πβ(πΏβπ)) β β)) |
26 | 23, 25 | syl5ibrcom 247 |
. . . . . . . 8
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π β β€) β (π₯ = (πΏβπ) β (πβπ₯) β β)) |
27 | 26 | rexlimdva 3153 |
. . . . . . 7
β’ ((π β β β§ Β¬ 2
β₯ π) β
(βπ β β€
π₯ = (πΏβπ) β (πβπ₯) β β)) |
28 | 27 | imp 408 |
. . . . . 6
β’ (((π β β β§ Β¬ 2
β₯ π) β§
βπ β β€
π₯ = (πΏβπ)) β (πβπ₯) β β) |
29 | 13, 28 | syldan 592 |
. . . . 5
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π₯ β π΅) β (πβπ₯) β β) |
30 | 2, 4, 29 | fmpt2d 7072 |
. . . 4
β’ ((π β β β§ Β¬ 2
β₯ π) β π:π΅βΆβ) |
31 | | ax-resscn 11109 |
. . . 4
β’ β
β β |
32 | | fss 6686 |
. . . 4
β’ ((π:π΅βΆβ β§ β β
β) β π:π΅βΆβ) |
33 | 30, 31, 32 | sylancl 587 |
. . 3
β’ ((π β β β§ Β¬ 2
β₯ π) β π:π΅βΆβ) |
34 | | eqid 2737 |
. . . . . 6
β’
(Unitβπ) =
(Unitβπ) |
35 | 8, 34 | unitss 20090 |
. . . . 5
β’
(Unitβπ)
β π΅ |
36 | | foelrn 7057 |
. . . . . . . . 9
β’ ((πΏ:β€βontoβπ΅ β§ π¦ β π΅) β βπ β β€ π¦ = (πΏβπ)) |
37 | 11, 36 | sylan 581 |
. . . . . . . 8
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π¦ β π΅) β βπ β β€ π¦ = (πΏβπ)) |
38 | 13, 37 | anim12dan 620 |
. . . . . . 7
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π₯ β π΅ β§ π¦ β π΅)) β (βπ β β€ π₯ = (πΏβπ) β§ βπ β β€ π¦ = (πΏβπ))) |
39 | | reeanv 3218 |
. . . . . . . . 9
β’
(βπ β
β€ βπ β
β€ (π₯ = (πΏβπ) β§ π¦ = (πΏβπ)) β (βπ β β€ π₯ = (πΏβπ) β§ βπ β β€ π¦ = (πΏβπ))) |
40 | 17 | adantrr 716 |
. . . . . . . . . . . . 13
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π β β€ β§ π β β€)) β π β
β€) |
41 | | simprr 772 |
. . . . . . . . . . . . 13
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π β β€ β§ π β β€)) β π β
β€) |
42 | 6 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π β β€ β§ π β β€)) β π β
β0) |
43 | | lgsdirnn0 26695 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β€ β§ π β β0)
β ((π Β· π) /L π) = ((π /L π) Β· (π /L π))) |
44 | 40, 41, 42, 43 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π β β€ β§ π β β€)) β ((π Β· π) /L π) = ((π /L π) Β· (π /L π))) |
45 | 7 | zncrng 20954 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β π β
CRing) |
46 | 6, 45 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ Β¬ 2
β₯ π) β π β CRing) |
47 | | crngring 19977 |
. . . . . . . . . . . . . . . . . 18
β’ (π β CRing β π β Ring) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ Β¬ 2
β₯ π) β π β Ring) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π β β€ β§ π β β€)) β π β Ring) |
50 | 9 | zrhrhm 20915 |
. . . . . . . . . . . . . . . 16
β’ (π β Ring β πΏ β (β€ring
RingHom π)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π β β€ β§ π β β€)) β πΏ β (β€ring
RingHom π)) |
52 | | zringbas 20878 |
. . . . . . . . . . . . . . . 16
β’ β€ =
(Baseββ€ring) |
53 | | zringmulr 20881 |
. . . . . . . . . . . . . . . 16
β’ Β·
= (.rββ€ring) |
54 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’
(.rβπ) = (.rβπ) |
55 | 52, 53, 54 | rhmmul 20160 |
. . . . . . . . . . . . . . 15
β’ ((πΏ β (β€ring
RingHom π) β§ π β β€ β§ π β β€) β (πΏβ(π Β· π)) = ((πΏβπ)(.rβπ)(πΏβπ))) |
56 | 51, 40, 41, 55 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π β β€ β§ π β β€)) β (πΏβ(π Β· π)) = ((πΏβπ)(.rβπ)(πΏβπ))) |
57 | 56 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π β β€ β§ π β β€)) β (πβ(πΏβ(π Β· π))) = (πβ((πΏβπ)(.rβπ)(πΏβπ)))) |
58 | | zmulcl 12553 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β€) β (π Β· π) β β€) |
59 | 14, 7, 15, 8, 9, 3 | lgsdchrval 26705 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π Β· π) β β€) β (πβ(πΏβ(π Β· π))) = ((π Β· π) /L π)) |
60 | 58, 59 | sylan2 594 |
. . . . . . . . . . . . 13
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π β β€ β§ π β β€)) β (πβ(πΏβ(π Β· π))) = ((π Β· π) /L π)) |
61 | 57, 60 | eqtr3d 2779 |
. . . . . . . . . . . 12
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π β β€ β§ π β β€)) β (πβ((πΏβπ)(.rβπ)(πΏβπ))) = ((π Β· π) /L π)) |
62 | 16 | adantrr 716 |
. . . . . . . . . . . . 13
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π β β€ β§ π β β€)) β (πβ(πΏβπ)) = (π /L π)) |
63 | 14, 7, 15, 8, 9, 3 | lgsdchrval 26705 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π β β€) β (πβ(πΏβπ)) = (π /L π)) |
64 | 63 | adantrl 715 |
. . . . . . . . . . . . 13
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π β β€ β§ π β β€)) β (πβ(πΏβπ)) = (π /L π)) |
65 | 62, 64 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π β β€ β§ π β β€)) β ((πβ(πΏβπ)) Β· (πβ(πΏβπ))) = ((π /L π) Β· (π /L π))) |
66 | 44, 61, 65 | 3eqtr4d 2787 |
. . . . . . . . . . 11
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π β β€ β§ π β β€)) β (πβ((πΏβπ)(.rβπ)(πΏβπ))) = ((πβ(πΏβπ)) Β· (πβ(πΏβπ)))) |
67 | | oveq12 7367 |
. . . . . . . . . . . . 13
β’ ((π₯ = (πΏβπ) β§ π¦ = (πΏβπ)) β (π₯(.rβπ)π¦) = ((πΏβπ)(.rβπ)(πΏβπ))) |
68 | 67 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((π₯ = (πΏβπ) β§ π¦ = (πΏβπ)) β (πβ(π₯(.rβπ)π¦)) = (πβ((πΏβπ)(.rβπ)(πΏβπ)))) |
69 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π¦ = (πΏβπ) β (πβπ¦) = (πβ(πΏβπ))) |
70 | 24, 69 | oveqan12d 7377 |
. . . . . . . . . . . 12
β’ ((π₯ = (πΏβπ) β§ π¦ = (πΏβπ)) β ((πβπ₯) Β· (πβπ¦)) = ((πβ(πΏβπ)) Β· (πβ(πΏβπ)))) |
71 | 68, 70 | eqeq12d 2753 |
. . . . . . . . . . 11
β’ ((π₯ = (πΏβπ) β§ π¦ = (πΏβπ)) β ((πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β (πβ((πΏβπ)(.rβπ)(πΏβπ))) = ((πβ(πΏβπ)) Β· (πβ(πΏβπ))))) |
72 | 66, 71 | syl5ibrcom 247 |
. . . . . . . . . 10
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π β β€ β§ π β β€)) β ((π₯ = (πΏβπ) β§ π¦ = (πΏβπ)) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)))) |
73 | 72 | rexlimdvva 3206 |
. . . . . . . . 9
β’ ((π β β β§ Β¬ 2
β₯ π) β
(βπ β β€
βπ β β€
(π₯ = (πΏβπ) β§ π¦ = (πΏβπ)) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)))) |
74 | 39, 73 | biimtrrid 242 |
. . . . . . . 8
β’ ((π β β β§ Β¬ 2
β₯ π) β
((βπ β β€
π₯ = (πΏβπ) β§ βπ β β€ π¦ = (πΏβπ)) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)))) |
75 | 74 | imp 408 |
. . . . . . 7
β’ (((π β β β§ Β¬ 2
β₯ π) β§
(βπ β β€
π₯ = (πΏβπ) β§ βπ β β€ π¦ = (πΏβπ))) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦))) |
76 | 38, 75 | syldan 592 |
. . . . . 6
β’ (((π β β β§ Β¬ 2
β₯ π) β§ (π₯ β π΅ β§ π¦ β π΅)) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦))) |
77 | 76 | ralrimivva 3198 |
. . . . 5
β’ ((π β β β§ Β¬ 2
β₯ π) β
βπ₯ β π΅ βπ¦ β π΅ (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦))) |
78 | | ss2ralv 4013 |
. . . . 5
β’
((Unitβπ)
β π΅ β
(βπ₯ β π΅ βπ¦ β π΅ (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β βπ₯ β (Unitβπ)βπ¦ β (Unitβπ)(πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)))) |
79 | 35, 77, 78 | mpsyl 68 |
. . . 4
β’ ((π β β β§ Β¬ 2
β₯ π) β
βπ₯ β
(Unitβπ)βπ¦ β (Unitβπ)(πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦))) |
80 | | 1z 12534 |
. . . . . 6
β’ 1 β
β€ |
81 | 14, 7, 15, 8, 9, 3 | lgsdchrval 26705 |
. . . . . 6
β’ (((π β β β§ Β¬ 2
β₯ π) β§ 1 β
β€) β (πβ(πΏβ1)) = (1 /L π)) |
82 | 80, 81 | mpan2 690 |
. . . . 5
β’ ((π β β β§ Β¬ 2
β₯ π) β (πβ(πΏβ1)) = (1 /L π)) |
83 | | eqid 2737 |
. . . . . . . 8
β’
(1rβπ) = (1rβπ) |
84 | 9, 83 | zrh1 20916 |
. . . . . . 7
β’ (π β Ring β (πΏβ1) =
(1rβπ)) |
85 | 48, 84 | syl 17 |
. . . . . 6
β’ ((π β β β§ Β¬ 2
β₯ π) β (πΏβ1) =
(1rβπ)) |
86 | 85 | fveq2d 6847 |
. . . . 5
β’ ((π β β β§ Β¬ 2
β₯ π) β (πβ(πΏβ1)) = (πβ(1rβπ))) |
87 | 18 | adantr 482 |
. . . . . 6
β’ ((π β β β§ Β¬ 2
β₯ π) β π β
β€) |
88 | | 1lgs 26691 |
. . . . . 6
β’ (π β β€ β (1
/L π) =
1) |
89 | 87, 88 | syl 17 |
. . . . 5
β’ ((π β β β§ Β¬ 2
β₯ π) β (1
/L π) =
1) |
90 | 82, 86, 89 | 3eqtr3d 2785 |
. . . 4
β’ ((π β β β§ Β¬ 2
β₯ π) β (πβ(1rβπ)) = 1) |
91 | | lgsne0 26686 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β€) β ((π /L π) β 0 β (π gcd π) = 1)) |
92 | 17, 19, 91 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π β β€) β ((π /L π) β 0 β (π gcd π) = 1)) |
93 | 92 | biimpd 228 |
. . . . . . . . . 10
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π β β€) β ((π /L π) β 0 β (π gcd π) = 1)) |
94 | 16 | neeq1d 3004 |
. . . . . . . . . 10
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π β β€) β ((πβ(πΏβπ)) β 0 β (π /L π) β 0)) |
95 | 7, 34, 9 | znunit 20973 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π β β€)
β ((πΏβπ) β (Unitβπ) β (π gcd π) = 1)) |
96 | 6, 95 | sylan 581 |
. . . . . . . . . 10
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π β β€) β ((πΏβπ) β (Unitβπ) β (π gcd π) = 1)) |
97 | 93, 94, 96 | 3imtr4d 294 |
. . . . . . . . 9
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π β β€) β ((πβ(πΏβπ)) β 0 β (πΏβπ) β (Unitβπ))) |
98 | 24 | neeq1d 3004 |
. . . . . . . . . 10
β’ (π₯ = (πΏβπ) β ((πβπ₯) β 0 β (πβ(πΏβπ)) β 0)) |
99 | | eleq1 2826 |
. . . . . . . . . 10
β’ (π₯ = (πΏβπ) β (π₯ β (Unitβπ) β (πΏβπ) β (Unitβπ))) |
100 | 98, 99 | imbi12d 345 |
. . . . . . . . 9
β’ (π₯ = (πΏβπ) β (((πβπ₯) β 0 β π₯ β (Unitβπ)) β ((πβ(πΏβπ)) β 0 β (πΏβπ) β (Unitβπ)))) |
101 | 97, 100 | syl5ibrcom 247 |
. . . . . . . 8
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π β β€) β (π₯ = (πΏβπ) β ((πβπ₯) β 0 β π₯ β (Unitβπ)))) |
102 | 101 | rexlimdva 3153 |
. . . . . . 7
β’ ((π β β β§ Β¬ 2
β₯ π) β
(βπ β β€
π₯ = (πΏβπ) β ((πβπ₯) β 0 β π₯ β (Unitβπ)))) |
103 | 102 | imp 408 |
. . . . . 6
β’ (((π β β β§ Β¬ 2
β₯ π) β§
βπ β β€
π₯ = (πΏβπ)) β ((πβπ₯) β 0 β π₯ β (Unitβπ))) |
104 | 13, 103 | syldan 592 |
. . . . 5
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π₯ β π΅) β ((πβπ₯) β 0 β π₯ β (Unitβπ))) |
105 | 104 | ralrimiva 3144 |
. . . 4
β’ ((π β β β§ Β¬ 2
β₯ π) β
βπ₯ β π΅ ((πβπ₯) β 0 β π₯ β (Unitβπ))) |
106 | 79, 90, 105 | 3jca 1129 |
. . 3
β’ ((π β β β§ Β¬ 2
β₯ π) β
(βπ₯ β
(Unitβπ)βπ¦ β (Unitβπ)(πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(1rβπ)) = 1 β§ βπ₯ β π΅ ((πβπ₯) β 0 β π₯ β (Unitβπ)))) |
107 | | simpl 484 |
. . . 4
β’ ((π β β β§ Β¬ 2
β₯ π) β π β
β) |
108 | 14, 7, 8, 34, 107, 15 | dchrelbas3 26589 |
. . 3
β’ ((π β β β§ Β¬ 2
β₯ π) β (π β π· β (π:π΅βΆβ β§ (βπ₯ β (Unitβπ)βπ¦ β (Unitβπ)(πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(1rβπ)) = 1 β§ βπ₯ β π΅ ((πβπ₯) β 0 β π₯ β (Unitβπ)))))) |
109 | 33, 106, 108 | mpbir2and 712 |
. 2
β’ ((π β β β§ Β¬ 2
β₯ π) β π β π·) |
110 | 109, 30 | jca 513 |
1
β’ ((π β β β§ Β¬ 2
β₯ π) β (π β π· β§ π:π΅βΆβ)) |