Step | Hyp | Ref
| Expression |
1 | | drngring 20314 |
. . . . 5
β’ (π
β DivRing β π
β Ring) |
2 | | qqhval2.2 |
. . . . . 6
β’ πΏ = (β€RHomβπ
) |
3 | 2 | zrhrhm 21052 |
. . . . 5
β’ (π
β Ring β πΏ β (β€ring
RingHom π
)) |
4 | 1, 3 | syl 17 |
. . . 4
β’ (π
β DivRing β πΏ β (β€ring
RingHom π
)) |
5 | 4 | ad2antrr 724 |
. . 3
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β πΏ β (β€ring
RingHom π
)) |
6 | | simpr1 1194 |
. . . . . 6
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β π β
β€) |
7 | | simpr2 1195 |
. . . . . 6
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β π β
β€) |
8 | 6, 7 | gcdcld 16445 |
. . . . 5
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (π gcd π) β
β0) |
9 | 8 | nn0zd 12580 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (π gcd π) β β€) |
10 | | simpr3 1196 |
. . . . 5
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β π β 0) |
11 | | gcdeq0 16454 |
. . . . . . . . 9
β’ ((π β β€ β§ π β β€) β ((π gcd π) = 0 β (π = 0 β§ π = 0))) |
12 | 11 | simplbda 500 |
. . . . . . . 8
β’ (((π β β€ β§ π β β€) β§ (π gcd π) = 0) β π = 0) |
13 | 12 | ex 413 |
. . . . . . 7
β’ ((π β β€ β§ π β β€) β ((π gcd π) = 0 β π = 0)) |
14 | 13 | necon3d 2961 |
. . . . . 6
β’ ((π β β€ β§ π β β€) β (π β 0 β (π gcd π) β 0)) |
15 | 14 | imp 407 |
. . . . 5
β’ (((π β β€ β§ π β β€) β§ π β 0) β (π gcd π) β 0) |
16 | 6, 7, 10, 15 | syl21anc 836 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (π gcd π) β 0) |
17 | | gcddvds 16440 |
. . . . . 6
β’ ((π β β€ β§ π β β€) β ((π gcd π) β₯ π β§ (π gcd π) β₯ π)) |
18 | 6, 7, 17 | syl2anc 584 |
. . . . 5
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β ((π gcd π) β₯ π β§ (π gcd π) β₯ π)) |
19 | 18 | simpld 495 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (π gcd π) β₯ π) |
20 | | dvdsval2 16196 |
. . . . 5
β’ (((π gcd π) β β€ β§ (π gcd π) β 0 β§ π β β€) β ((π gcd π) β₯ π β (π / (π gcd π)) β β€)) |
21 | 20 | biimpa 477 |
. . . 4
β’ ((((π gcd π) β β€ β§ (π gcd π) β 0 β§ π β β€) β§ (π gcd π) β₯ π) β (π / (π gcd π)) β β€) |
22 | 9, 16, 6, 19, 21 | syl31anc 1373 |
. . 3
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (π / (π gcd π)) β β€) |
23 | 18 | simprd 496 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (π gcd π) β₯ π) |
24 | | dvdsval2 16196 |
. . . . 5
β’ (((π gcd π) β β€ β§ (π gcd π) β 0 β§ π β β€) β ((π gcd π) β₯ π β (π / (π gcd π)) β β€)) |
25 | 24 | biimpa 477 |
. . . 4
β’ ((((π gcd π) β β€ β§ (π gcd π) β 0 β§ π β β€) β§ (π gcd π) β₯ π) β (π / (π gcd π)) β β€) |
26 | 9, 16, 7, 23, 25 | syl31anc 1373 |
. . 3
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (π / (π gcd π)) β β€) |
27 | | zringbas 21015 |
. . . . . . 7
β’ β€ =
(Baseββ€ring) |
28 | | qqhval2.0 |
. . . . . . 7
β’ π΅ = (Baseβπ
) |
29 | 27, 28 | rhmf 20255 |
. . . . . 6
β’ (πΏ β (β€ring
RingHom π
) β πΏ:β€βΆπ΅) |
30 | 5, 29 | syl 17 |
. . . . 5
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β πΏ:β€βΆπ΅) |
31 | 30, 26 | ffvelcdmd 7084 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (πΏβ(π / (π gcd π))) β π΅) |
32 | 30 | ffnd 6715 |
. . . . 5
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β πΏ Fn β€) |
33 | 7 | zcnd 12663 |
. . . . . . . 8
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β π β
β) |
34 | 9 | zcnd 12663 |
. . . . . . . 8
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (π gcd π) β β) |
35 | 33, 34, 10, 16 | divne0d 12002 |
. . . . . . 7
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (π / (π gcd π)) β 0) |
36 | | ovex 7438 |
. . . . . . . . 9
β’ (π / (π gcd π)) β V |
37 | 36 | elsn 4642 |
. . . . . . . 8
β’ ((π / (π gcd π)) β {0} β (π / (π gcd π)) = 0) |
38 | 37 | necon3bbii 2988 |
. . . . . . 7
β’ (Β¬
(π / (π gcd π)) β {0} β (π / (π gcd π)) β 0) |
39 | 35, 38 | sylibr 233 |
. . . . . 6
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β Β¬
(π / (π gcd π)) β {0}) |
40 | 1 | ad2antrr 724 |
. . . . . . 7
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β π
β Ring) |
41 | | simplr 767 |
. . . . . . 7
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β
(chrβπ
) =
0) |
42 | | eqid 2732 |
. . . . . . . . 9
β’
(0gβπ
) = (0gβπ
) |
43 | 28, 2, 42 | zrhker 32945 |
. . . . . . . 8
β’ (π
β Ring β
((chrβπ
) = 0 β
(β‘πΏ β {(0gβπ
)}) = {0})) |
44 | 43 | biimpa 477 |
. . . . . . 7
β’ ((π
β Ring β§
(chrβπ
) = 0) β
(β‘πΏ β {(0gβπ
)}) = {0}) |
45 | 40, 41, 44 | syl2anc 584 |
. . . . . 6
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (β‘πΏ β {(0gβπ
)}) = {0}) |
46 | 39, 45 | neleqtrrd 2856 |
. . . . 5
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β Β¬
(π / (π gcd π)) β (β‘πΏ β {(0gβπ
)})) |
47 | | elpreima 7056 |
. . . . . . . . 9
β’ (πΏ Fn β€ β ((π / (π gcd π)) β (β‘πΏ β {(0gβπ
)}) β ((π / (π gcd π)) β β€ β§ (πΏβ(π / (π gcd π))) β {(0gβπ
)}))) |
48 | 47 | baibd 540 |
. . . . . . . 8
β’ ((πΏ Fn β€ β§ (π / (π gcd π)) β β€) β ((π / (π gcd π)) β (β‘πΏ β {(0gβπ
)}) β (πΏβ(π / (π gcd π))) β {(0gβπ
)})) |
49 | 48 | biimprd 247 |
. . . . . . 7
β’ ((πΏ Fn β€ β§ (π / (π gcd π)) β β€) β ((πΏβ(π / (π gcd π))) β {(0gβπ
)} β (π / (π gcd π)) β (β‘πΏ β {(0gβπ
)}))) |
50 | 49 | con3dimp 409 |
. . . . . 6
β’ (((πΏ Fn β€ β§ (π / (π gcd π)) β β€) β§ Β¬ (π / (π gcd π)) β (β‘πΏ β {(0gβπ
)})) β Β¬ (πΏβ(π / (π gcd π))) β {(0gβπ
)}) |
51 | | fvex 6901 |
. . . . . . . 8
β’ (πΏβ(π / (π gcd π))) β V |
52 | 51 | elsn 4642 |
. . . . . . 7
β’ ((πΏβ(π / (π gcd π))) β {(0gβπ
)} β (πΏβ(π / (π gcd π))) = (0gβπ
)) |
53 | 52 | necon3bbii 2988 |
. . . . . 6
β’ (Β¬
(πΏβ(π / (π gcd π))) β {(0gβπ
)} β (πΏβ(π / (π gcd π))) β (0gβπ
)) |
54 | 50, 53 | sylib 217 |
. . . . 5
β’ (((πΏ Fn β€ β§ (π / (π gcd π)) β β€) β§ Β¬ (π / (π gcd π)) β (β‘πΏ β {(0gβπ
)})) β (πΏβ(π / (π gcd π))) β (0gβπ
)) |
55 | 32, 26, 46, 54 | syl21anc 836 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (πΏβ(π / (π gcd π))) β (0gβπ
)) |
56 | | eqid 2732 |
. . . . . 6
β’
(Unitβπ
) =
(Unitβπ
) |
57 | 28, 56, 42 | drngunit 20312 |
. . . . 5
β’ (π
β DivRing β ((πΏβ(π / (π gcd π))) β (Unitβπ
) β ((πΏβ(π / (π gcd π))) β π΅ β§ (πΏβ(π / (π gcd π))) β (0gβπ
)))) |
58 | 57 | ad2antrr 724 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β ((πΏβ(π / (π gcd π))) β (Unitβπ
) β ((πΏβ(π / (π gcd π))) β π΅ β§ (πΏβ(π / (π gcd π))) β (0gβπ
)))) |
59 | 31, 55, 58 | mpbir2and 711 |
. . 3
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (πΏβ(π / (π gcd π))) β (Unitβπ
)) |
60 | 30, 9 | ffvelcdmd 7084 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (πΏβ(π gcd π)) β π΅) |
61 | | ovex 7438 |
. . . . . . . . 9
β’ (π gcd π) β V |
62 | 61 | elsn 4642 |
. . . . . . . 8
β’ ((π gcd π) β {0} β (π gcd π) = 0) |
63 | 62 | necon3bbii 2988 |
. . . . . . 7
β’ (Β¬
(π gcd π) β {0} β (π gcd π) β 0) |
64 | 16, 63 | sylibr 233 |
. . . . . 6
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β Β¬
(π gcd π) β {0}) |
65 | 64, 45 | neleqtrrd 2856 |
. . . . 5
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β Β¬
(π gcd π) β (β‘πΏ β {(0gβπ
)})) |
66 | | elpreima 7056 |
. . . . . . . . 9
β’ (πΏ Fn β€ β ((π gcd π) β (β‘πΏ β {(0gβπ
)}) β ((π gcd π) β β€ β§ (πΏβ(π gcd π)) β {(0gβπ
)}))) |
67 | 66 | baibd 540 |
. . . . . . . 8
β’ ((πΏ Fn β€ β§ (π gcd π) β β€) β ((π gcd π) β (β‘πΏ β {(0gβπ
)}) β (πΏβ(π gcd π)) β {(0gβπ
)})) |
68 | 67 | biimprd 247 |
. . . . . . 7
β’ ((πΏ Fn β€ β§ (π gcd π) β β€) β ((πΏβ(π gcd π)) β {(0gβπ
)} β (π gcd π) β (β‘πΏ β {(0gβπ
)}))) |
69 | 68 | con3dimp 409 |
. . . . . 6
β’ (((πΏ Fn β€ β§ (π gcd π) β β€) β§ Β¬ (π gcd π) β (β‘πΏ β {(0gβπ
)})) β Β¬ (πΏβ(π gcd π)) β {(0gβπ
)}) |
70 | | fvex 6901 |
. . . . . . . 8
β’ (πΏβ(π gcd π)) β V |
71 | 70 | elsn 4642 |
. . . . . . 7
β’ ((πΏβ(π gcd π)) β {(0gβπ
)} β (πΏβ(π gcd π)) = (0gβπ
)) |
72 | 71 | necon3bbii 2988 |
. . . . . 6
β’ (Β¬
(πΏβ(π gcd π)) β {(0gβπ
)} β (πΏβ(π gcd π)) β (0gβπ
)) |
73 | 69, 72 | sylib 217 |
. . . . 5
β’ (((πΏ Fn β€ β§ (π gcd π) β β€) β§ Β¬ (π gcd π) β (β‘πΏ β {(0gβπ
)})) β (πΏβ(π gcd π)) β (0gβπ
)) |
74 | 32, 9, 65, 73 | syl21anc 836 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (πΏβ(π gcd π)) β (0gβπ
)) |
75 | 28, 56, 42 | drngunit 20312 |
. . . . 5
β’ (π
β DivRing β ((πΏβ(π gcd π)) β (Unitβπ
) β ((πΏβ(π gcd π)) β π΅ β§ (πΏβ(π gcd π)) β (0gβπ
)))) |
76 | 75 | ad2antrr 724 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β ((πΏβ(π gcd π)) β (Unitβπ
) β ((πΏβ(π gcd π)) β π΅ β§ (πΏβ(π gcd π)) β (0gβπ
)))) |
77 | 60, 74, 76 | mpbir2and 711 |
. . 3
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (πΏβ(π gcd π)) β (Unitβπ
)) |
78 | | qqhval2.1 |
. . . 4
β’ / =
(/rβπ
) |
79 | | zringmulr 21018 |
. . . 4
β’ Β·
= (.rββ€ring) |
80 | 56, 27, 78, 79 | rhmdvd 32424 |
. . 3
β’ ((πΏ β (β€ring
RingHom π
) β§ ((π / (π gcd π)) β β€ β§ (π / (π gcd π)) β β€ β§ (π gcd π) β β€) β§ ((πΏβ(π / (π gcd π))) β (Unitβπ
) β§ (πΏβ(π gcd π)) β (Unitβπ
))) β ((πΏβ(π / (π gcd π))) / (πΏβ(π / (π gcd π)))) = ((πΏβ((π / (π gcd π)) Β· (π gcd π))) / (πΏβ((π / (π gcd π)) Β· (π gcd π))))) |
81 | 5, 22, 26, 9, 59, 77, 80 | syl132anc 1388 |
. 2
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β ((πΏβ(π / (π gcd π))) / (πΏβ(π / (π gcd π)))) = ((πΏβ((π / (π gcd π)) Β· (π gcd π))) / (πΏβ((π / (π gcd π)) Β· (π gcd π))))) |
82 | | divnumden 16680 |
. . . . . . . 8
β’ ((π β β€ β§ π β β) β
((numerβ(π / π)) = (π / (π gcd π)) β§ (denomβ(π / π)) = (π / (π gcd π)))) |
83 | 6, 82 | sylan 580 |
. . . . . . 7
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ π β β) β
((numerβ(π / π)) = (π / (π gcd π)) β§ (denomβ(π / π)) = (π / (π gcd π)))) |
84 | 83 | simpld 495 |
. . . . . 6
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ π β β) β
(numerβ(π / π)) = (π / (π gcd π))) |
85 | 84 | eqcomd 2738 |
. . . . 5
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ π β β) β (π / (π gcd π)) = (numerβ(π / π))) |
86 | 85 | fveq2d 6892 |
. . . 4
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ π β β) β (πΏβ(π / (π gcd π))) = (πΏβ(numerβ(π / π)))) |
87 | 83 | simprd 496 |
. . . . . 6
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ π β β) β
(denomβ(π / π)) = (π / (π gcd π))) |
88 | 87 | eqcomd 2738 |
. . . . 5
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ π β β) β (π / (π gcd π)) = (denomβ(π / π))) |
89 | 88 | fveq2d 6892 |
. . . 4
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ π β β) β (πΏβ(π / (π gcd π))) = (πΏβ(denomβ(π / π)))) |
90 | 86, 89 | oveq12d 7423 |
. . 3
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ π β β) β ((πΏβ(π / (π gcd π))) / (πΏβ(π / (π gcd π)))) = ((πΏβ(numerβ(π / π))) / (πΏβ(denomβ(π / π))))) |
91 | 22 | adantr 481 |
. . . . . . . . 9
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β (π / (π gcd π)) β β€) |
92 | 91 | zcnd 12663 |
. . . . . . . 8
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β (π / (π gcd π)) β β) |
93 | 92 | mulm1d 11662 |
. . . . . . 7
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β (-1
Β· (π / (π gcd π))) = -(π / (π gcd π))) |
94 | | neg1cn 12322 |
. . . . . . . . 9
β’ -1 β
β |
95 | 94 | a1i 11 |
. . . . . . . 8
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β -1
β β) |
96 | 95, 92 | mulcomd 11231 |
. . . . . . 7
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β (-1
Β· (π / (π gcd π))) = ((π / (π gcd π)) Β· -1)) |
97 | 93, 96 | eqtr3d 2774 |
. . . . . 6
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β -(π / (π gcd π)) = ((π / (π gcd π)) Β· -1)) |
98 | 97 | fveq2d 6892 |
. . . . 5
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β (πΏβ-(π / (π gcd π))) = (πΏβ((π / (π gcd π)) Β· -1))) |
99 | 26 | adantr 481 |
. . . . . . . . 9
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β (π / (π gcd π)) β β€) |
100 | 99 | zcnd 12663 |
. . . . . . . 8
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β (π / (π gcd π)) β β) |
101 | 100 | mulm1d 11662 |
. . . . . . 7
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β (-1
Β· (π / (π gcd π))) = -(π / (π gcd π))) |
102 | 95, 100 | mulcomd 11231 |
. . . . . . 7
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β (-1
Β· (π / (π gcd π))) = ((π / (π gcd π)) Β· -1)) |
103 | 101, 102 | eqtr3d 2774 |
. . . . . 6
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β -(π / (π gcd π)) = ((π / (π gcd π)) Β· -1)) |
104 | 103 | fveq2d 6892 |
. . . . 5
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β (πΏβ-(π / (π gcd π))) = (πΏβ((π / (π gcd π)) Β· -1))) |
105 | 98, 104 | oveq12d 7423 |
. . . 4
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β ((πΏβ-(π / (π gcd π))) / (πΏβ-(π / (π gcd π)))) = ((πΏβ((π / (π gcd π)) Β· -1)) / (πΏβ((π / (π gcd π)) Β· -1)))) |
106 | 6 | adantr 481 |
. . . . . . . 8
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β π β
β€) |
107 | 7 | adantr 481 |
. . . . . . . 8
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β π β
β€) |
108 | | simpr 485 |
. . . . . . . 8
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β -π β
β) |
109 | | divnumden2 32011 |
. . . . . . . 8
β’ ((π β β€ β§ π β β€ β§ -π β β) β
((numerβ(π / π)) = -(π / (π gcd π)) β§ (denomβ(π / π)) = -(π / (π gcd π)))) |
110 | 106, 107,
108, 109 | syl3anc 1371 |
. . . . . . 7
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β
((numerβ(π / π)) = -(π / (π gcd π)) β§ (denomβ(π / π)) = -(π / (π gcd π)))) |
111 | 110 | simpld 495 |
. . . . . 6
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β
(numerβ(π / π)) = -(π / (π gcd π))) |
112 | 111 | fveq2d 6892 |
. . . . 5
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β (πΏβ(numerβ(π / π))) = (πΏβ-(π / (π gcd π)))) |
113 | 110 | simprd 496 |
. . . . . 6
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β
(denomβ(π / π)) = -(π / (π gcd π))) |
114 | 113 | fveq2d 6892 |
. . . . 5
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β (πΏβ(denomβ(π / π))) = (πΏβ-(π / (π gcd π)))) |
115 | 112, 114 | oveq12d 7423 |
. . . 4
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β ((πΏβ(numerβ(π / π))) / (πΏβ(denomβ(π / π)))) = ((πΏβ-(π / (π gcd π))) / (πΏβ-(π / (π gcd π))))) |
116 | 5 | adantr 481 |
. . . . 5
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β πΏ β (β€ring
RingHom π
)) |
117 | | 1zzd 12589 |
. . . . . 6
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β 1 β
β€) |
118 | 117 | znegcld 12664 |
. . . . 5
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β -1
β β€) |
119 | 59 | adantr 481 |
. . . . 5
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β (πΏβ(π / (π gcd π))) β (Unitβπ
)) |
120 | | neg1z 12594 |
. . . . . . . 8
β’ -1 β
β€ |
121 | | ax-1cn 11164 |
. . . . . . . . . 10
β’ 1 β
β |
122 | 121 | absnegi 15343 |
. . . . . . . . 9
β’
(absβ-1) = (absβ1) |
123 | | abs1 15240 |
. . . . . . . . 9
β’
(absβ1) = 1 |
124 | 122, 123 | eqtri 2760 |
. . . . . . . 8
β’
(absβ-1) = 1 |
125 | | zringunit 21027 |
. . . . . . . 8
β’ (-1
β (Unitββ€ring) β (-1 β β€ β§
(absβ-1) = 1)) |
126 | 120, 124,
125 | mpbir2an 709 |
. . . . . . 7
β’ -1 β
(Unitββ€ring) |
127 | 126 | a1i 11 |
. . . . . 6
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β -1
β (Unitββ€ring)) |
128 | | elrhmunit 20281 |
. . . . . 6
β’ ((πΏ β (β€ring
RingHom π
) β§ -1 β
(Unitββ€ring)) β (πΏβ-1) β (Unitβπ
)) |
129 | 116, 127,
128 | syl2anc 584 |
. . . . 5
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β (πΏβ-1) β
(Unitβπ
)) |
130 | 56, 27, 78, 79 | rhmdvd 32424 |
. . . . 5
β’ ((πΏ β (β€ring
RingHom π
) β§ ((π / (π gcd π)) β β€ β§ (π / (π gcd π)) β β€ β§ -1 β β€)
β§ ((πΏβ(π / (π gcd π))) β (Unitβπ
) β§ (πΏβ-1) β (Unitβπ
))) β ((πΏβ(π / (π gcd π))) / (πΏβ(π / (π gcd π)))) = ((πΏβ((π / (π gcd π)) Β· -1)) / (πΏβ((π / (π gcd π)) Β· -1)))) |
131 | 116, 91, 99, 118, 119, 129, 130 | syl132anc 1388 |
. . . 4
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β ((πΏβ(π / (π gcd π))) / (πΏβ(π / (π gcd π)))) = ((πΏβ((π / (π gcd π)) Β· -1)) / (πΏβ((π / (π gcd π)) Β· -1)))) |
132 | 105, 115,
131 | 3eqtr4rd 2783 |
. . 3
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β§ -π β β) β ((πΏβ(π / (π gcd π))) / (πΏβ(π / (π gcd π)))) = ((πΏβ(numerβ(π / π))) / (πΏβ(denomβ(π / π))))) |
133 | | simp3 1138 |
. . . . . 6
β’ ((π β β€ β§ π β β€ β§ π β 0) β π β 0) |
134 | 133 | neneqd 2945 |
. . . . 5
β’ ((π β β€ β§ π β β€ β§ π β 0) β Β¬ π = 0) |
135 | | simp2 1137 |
. . . . . . . 8
β’ ((π β β€ β§ π β β€ β§ π β 0) β π β
β€) |
136 | | elz 12556 |
. . . . . . . 8
β’ (π β β€ β (π β β β§ (π = 0 β¨ π β β β¨ -π β β))) |
137 | 135, 136 | sylib 217 |
. . . . . . 7
β’ ((π β β€ β§ π β β€ β§ π β 0) β (π β β β§ (π = 0 β¨ π β β β¨ -π β β))) |
138 | 137 | simprd 496 |
. . . . . 6
β’ ((π β β€ β§ π β β€ β§ π β 0) β (π = 0 β¨ π β β β¨ -π β β)) |
139 | | 3orass 1090 |
. . . . . 6
β’ ((π = 0 β¨ π β β β¨ -π β β) β (π = 0 β¨ (π β β β¨ -π β β))) |
140 | 138, 139 | sylib 217 |
. . . . 5
β’ ((π β β€ β§ π β β€ β§ π β 0) β (π = 0 β¨ (π β β β¨ -π β β))) |
141 | | orel1 887 |
. . . . 5
β’ (Β¬
π = 0 β ((π = 0 β¨ (π β β β¨ -π β β)) β (π β β β¨ -π β β))) |
142 | 134, 140,
141 | sylc 65 |
. . . 4
β’ ((π β β€ β§ π β β€ β§ π β 0) β (π β β β¨ -π β
β)) |
143 | 142 | adantl 482 |
. . 3
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (π β β β¨ -π β
β)) |
144 | 90, 132, 143 | mpjaodan 957 |
. 2
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β ((πΏβ(π / (π gcd π))) / (πΏβ(π / (π gcd π)))) = ((πΏβ(numerβ(π / π))) / (πΏβ(denomβ(π / π))))) |
145 | 6 | zcnd 12663 |
. . . . 5
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β π β
β) |
146 | 145, 34, 16 | divcan1d 11987 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β ((π / (π gcd π)) Β· (π gcd π)) = π) |
147 | 146 | fveq2d 6892 |
. . 3
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (πΏβ((π / (π gcd π)) Β· (π gcd π))) = (πΏβπ)) |
148 | 33, 34, 16 | divcan1d 11987 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β ((π / (π gcd π)) Β· (π gcd π)) = π) |
149 | 148 | fveq2d 6892 |
. . 3
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β (πΏβ((π / (π gcd π)) Β· (π gcd π))) = (πΏβπ)) |
150 | 147, 149 | oveq12d 7423 |
. 2
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β ((πΏβ((π / (π gcd π)) Β· (π gcd π))) / (πΏβ((π / (π gcd π)) Β· (π gcd π)))) = ((πΏβπ) / (πΏβπ))) |
151 | 81, 144, 150 | 3eqtr3d 2780 |
1
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π β β€ β§
π β β€ β§
π β 0)) β ((πΏβ(numerβ(π / π))) / (πΏβ(denomβ(π / π)))) = ((πΏβπ) / (πΏβπ))) |