Step | Hyp | Ref
| Expression |
1 | | nnnn0 12421 |
. . . . . 6
β’ (π β β β π β
β0) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π β β β§ Β¬ 2
β₯ π) β π β
β0) |
3 | | lgsdchr.z |
. . . . . 6
β’ π =
(β€/nβ€βπ) |
4 | | lgsdchr.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
5 | | lgsdchr.l |
. . . . . 6
β’ πΏ = (β€RHomβπ) |
6 | 3, 4, 5 | znzrhfo 20957 |
. . . . 5
β’ (π β β0
β πΏ:β€βontoβπ΅) |
7 | | fof 6757 |
. . . . 5
β’ (πΏ:β€βontoβπ΅ β πΏ:β€βΆπ΅) |
8 | 2, 6, 7 | 3syl 18 |
. . . 4
β’ ((π β β β§ Β¬ 2
β₯ π) β πΏ:β€βΆπ΅) |
9 | 8 | ffvelcdmda 7036 |
. . 3
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β (πΏβπ΄) β π΅) |
10 | | eqeq1 2741 |
. . . . . . 7
β’ (π¦ = (πΏβπ΄) β (π¦ = (πΏβπ) β (πΏβπ΄) = (πΏβπ))) |
11 | 10 | anbi1d 631 |
. . . . . 6
β’ (π¦ = (πΏβπ΄) β ((π¦ = (πΏβπ) β§ β = (π /L π)) β ((πΏβπ΄) = (πΏβπ) β§ β = (π /L π)))) |
12 | 11 | rexbidv 3176 |
. . . . 5
β’ (π¦ = (πΏβπ΄) β (βπ β β€ (π¦ = (πΏβπ) β§ β = (π /L π)) β βπ β β€ ((πΏβπ΄) = (πΏβπ) β§ β = (π /L π)))) |
13 | 12 | iotabidv 6481 |
. . . 4
β’ (π¦ = (πΏβπ΄) β (β©ββπ β β€ (π¦ = (πΏβπ) β§ β = (π /L π))) = (β©ββπ β β€ ((πΏβπ΄) = (πΏβπ) β§ β = (π /L π)))) |
14 | | lgsdchr.x |
. . . 4
β’ π = (π¦ β π΅ β¦ (β©ββπ β β€ (π¦ = (πΏβπ) β§ β = (π /L π)))) |
15 | | iotaex 6470 |
. . . 4
β’
(β©ββπ β β€ (π¦ = (πΏβπ) β§ β = (π /L π))) β V |
16 | 13, 14, 15 | fvmpt3i 6954 |
. . 3
β’ ((πΏβπ΄) β π΅ β (πβ(πΏβπ΄)) = (β©ββπ β β€ ((πΏβπ΄) = (πΏβπ) β§ β = (π /L π)))) |
17 | 9, 16 | syl 17 |
. 2
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β (πβ(πΏβπ΄)) = (β©ββπ β β€ ((πΏβπ΄) = (πΏβπ) β§ β = (π /L π)))) |
18 | | ovex 7391 |
. . 3
β’ (π΄ /L π) β V |
19 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β (πΏβπ΄) = (πΏβπ)) |
20 | | simplll 774 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β π β β) |
21 | 20, 1 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β π β
β0) |
22 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β π΄ β β€) |
23 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β π β β€) |
24 | 3, 5 | zndvds 20959 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π΄ β β€
β§ π β β€)
β ((πΏβπ΄) = (πΏβπ) β π β₯ (π΄ β π))) |
25 | 21, 22, 23, 24 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β ((πΏβπ΄) = (πΏβπ) β π β₯ (π΄ β π))) |
26 | 19, 25 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β π β₯ (π΄ β π)) |
27 | | moddvds 16148 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π΄ β β€ β§ π β β€) β ((π΄ mod π) = (π mod π) β π β₯ (π΄ β π))) |
28 | 20, 22, 23, 27 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β ((π΄ mod π) = (π mod π) β π β₯ (π΄ β π))) |
29 | 26, 28 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β (π΄ mod π) = (π mod π)) |
30 | 29 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β ((π΄ mod π) /L π) = ((π mod π) /L π)) |
31 | | simpllr 775 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β Β¬ 2 β₯ π) |
32 | | lgsmod 26674 |
. . . . . . . . . . . . 13
β’ ((π΄ β β€ β§ π β β β§ Β¬ 2
β₯ π) β ((π΄ mod π) /L π) = (π΄ /L π)) |
33 | 22, 20, 31, 32 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β ((π΄ mod π) /L π) = (π΄ /L π)) |
34 | | lgsmod 26674 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β β§ Β¬ 2
β₯ π) β ((π mod π) /L π) = (π /L π)) |
35 | 23, 20, 31, 34 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β ((π mod π) /L π) = (π /L π)) |
36 | 30, 33, 35 | 3eqtr3d 2785 |
. . . . . . . . . . 11
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β (π΄ /L π) = (π /L π)) |
37 | 36 | eqeq2d 2748 |
. . . . . . . . . 10
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β (β = (π΄ /L π) β β = (π /L π))) |
38 | 37 | biimprd 248 |
. . . . . . . . 9
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π β β€ β§ (πΏβπ΄) = (πΏβπ))) β (β = (π /L π) β β = (π΄ /L π))) |
39 | 38 | anassrs 469 |
. . . . . . . 8
β’
(((((π β
β β§ Β¬ 2 β₯ π) β§ π΄ β β€) β§ π β β€) β§ (πΏβπ΄) = (πΏβπ)) β (β = (π /L π) β β = (π΄ /L π))) |
40 | 39 | expimpd 455 |
. . . . . . 7
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ π β β€) β (((πΏβπ΄) = (πΏβπ) β§ β = (π /L π)) β β = (π΄ /L π))) |
41 | 40 | rexlimdva 3153 |
. . . . . 6
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β
(βπ β β€
((πΏβπ΄) = (πΏβπ) β§ β = (π /L π)) β β = (π΄ /L π))) |
42 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = π΄ β (πΏβπ) = (πΏβπ΄)) |
43 | 42 | eqcomd 2743 |
. . . . . . . . . . 11
β’ (π = π΄ β (πΏβπ΄) = (πΏβπ)) |
44 | 43 | biantrurd 534 |
. . . . . . . . . 10
β’ (π = π΄ β (β = (π /L π) β ((πΏβπ΄) = (πΏβπ) β§ β = (π /L π)))) |
45 | | oveq1 7365 |
. . . . . . . . . . 11
β’ (π = π΄ β (π /L π) = (π΄ /L π)) |
46 | 45 | eqeq2d 2748 |
. . . . . . . . . 10
β’ (π = π΄ β (β = (π /L π) β β = (π΄ /L π))) |
47 | 44, 46 | bitr3d 281 |
. . . . . . . . 9
β’ (π = π΄ β (((πΏβπ΄) = (πΏβπ) β§ β = (π /L π)) β β = (π΄ /L π))) |
48 | 47 | rspcev 3582 |
. . . . . . . 8
β’ ((π΄ β β€ β§ β = (π΄ /L π)) β βπ β β€ ((πΏβπ΄) = (πΏβπ) β§ β = (π /L π))) |
49 | 48 | ex 414 |
. . . . . . 7
β’ (π΄ β β€ β (β = (π΄ /L π) β βπ β β€ ((πΏβπ΄) = (πΏβπ) β§ β = (π /L π)))) |
50 | 49 | adantl 483 |
. . . . . 6
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β (β = (π΄ /L π) β βπ β β€ ((πΏβπ΄) = (πΏβπ) β§ β = (π /L π)))) |
51 | 41, 50 | impbid 211 |
. . . . 5
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β
(βπ β β€
((πΏβπ΄) = (πΏβπ) β§ β = (π /L π)) β β = (π΄ /L π))) |
52 | 51 | adantr 482 |
. . . 4
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π΄ /L π) β V) β (βπ β β€ ((πΏβπ΄) = (πΏβπ) β§ β = (π /L π)) β β = (π΄ /L π))) |
53 | 52 | iota5 6480 |
. . 3
β’ ((((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β§ (π΄ /L π) β V) β (β©ββπ β β€ ((πΏβπ΄) = (πΏβπ) β§ β = (π /L π))) = (π΄ /L π)) |
54 | 18, 53 | mpan2 690 |
. 2
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β
(β©ββπ β β€ ((πΏβπ΄) = (πΏβπ) β§ β = (π /L π))) = (π΄ /L π)) |
55 | 17, 54 | eqtrd 2777 |
1
β’ (((π β β β§ Β¬ 2
β₯ π) β§ π΄ β β€) β (πβ(πΏβπ΄)) = (π΄ /L π)) |