Step | Hyp | Ref
| Expression |
1 | | gzsubrg 21200 |
. . . . 5
β’
β€[i] β (SubRingββfld) |
2 | | gzrng.1 |
. . . . . 6
β’ π = (βfld
βΎs β€[i]) |
3 | 2 | subrgbas 20472 |
. . . . 5
β’
(β€[i] β (SubRingββfld) β
β€[i] = (Baseβπ)) |
4 | 1, 3 | ax-mp 5 |
. . . 4
β’
β€[i] = (Baseβπ) |
5 | | eqid 2731 |
. . . 4
β’
(Unitβπ) =
(Unitβπ) |
6 | 4, 5 | unitcl 20267 |
. . 3
β’ (π΄ β (Unitβπ) β π΄ β β€[i]) |
7 | | eqid 2731 |
. . . . . . . . . . . 12
β’
(invrββfld) =
(invrββfld) |
8 | | eqid 2731 |
. . . . . . . . . . . 12
β’
(invrβπ) = (invrβπ) |
9 | 2, 7, 5, 8 | subrginv 20479 |
. . . . . . . . . . 11
β’
((β€[i] β (SubRingββfld) β§ π΄ β (Unitβπ)) β
((invrββfld)βπ΄) = ((invrβπ)βπ΄)) |
10 | 1, 9 | mpan 687 |
. . . . . . . . . 10
β’ (π΄ β (Unitβπ) β
((invrββfld)βπ΄) = ((invrβπ)βπ΄)) |
11 | | gzcn 16870 |
. . . . . . . . . . . 12
β’ (π΄ β β€[i] β π΄ β
β) |
12 | 6, 11 | syl 17 |
. . . . . . . . . . 11
β’ (π΄ β (Unitβπ) β π΄ β β) |
13 | | 0red 11222 |
. . . . . . . . . . . . . 14
β’ (π΄ β (Unitβπ) β 0 β
β) |
14 | | 1re 11219 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π΄ β (Unitβπ) β 1 β
β) |
16 | 12 | abscld 15388 |
. . . . . . . . . . . . . 14
β’ (π΄ β (Unitβπ) β (absβπ΄) β
β) |
17 | | 0lt1 11741 |
. . . . . . . . . . . . . . 15
β’ 0 <
1 |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π΄ β (Unitβπ) β 0 <
1) |
19 | 2 | gzrngunitlem 21211 |
. . . . . . . . . . . . . 14
β’ (π΄ β (Unitβπ) β 1 β€ (absβπ΄)) |
20 | 13, 15, 16, 18, 19 | ltletrd 11379 |
. . . . . . . . . . . . 13
β’ (π΄ β (Unitβπ) β 0 < (absβπ΄)) |
21 | 20 | gt0ne0d 11783 |
. . . . . . . . . . . 12
β’ (π΄ β (Unitβπ) β (absβπ΄) β 0) |
22 | 12 | abs00ad 15242 |
. . . . . . . . . . . . 13
β’ (π΄ β (Unitβπ) β ((absβπ΄) = 0 β π΄ = 0)) |
23 | 22 | necon3bid 2984 |
. . . . . . . . . . . 12
β’ (π΄ β (Unitβπ) β ((absβπ΄) β 0 β π΄ β 0)) |
24 | 21, 23 | mpbid 231 |
. . . . . . . . . . 11
β’ (π΄ β (Unitβπ) β π΄ β 0) |
25 | | cnfldinv 21177 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΄ β 0) β
((invrββfld)βπ΄) = (1 / π΄)) |
26 | 12, 24, 25 | syl2anc 583 |
. . . . . . . . . 10
β’ (π΄ β (Unitβπ) β
((invrββfld)βπ΄) = (1 / π΄)) |
27 | 10, 26 | eqtr3d 2773 |
. . . . . . . . 9
β’ (π΄ β (Unitβπ) β
((invrβπ)βπ΄) = (1 / π΄)) |
28 | 2 | subrgring 20465 |
. . . . . . . . . . 11
β’
(β€[i] β (SubRingββfld) β π β Ring) |
29 | 1, 28 | ax-mp 5 |
. . . . . . . . . 10
β’ π β Ring |
30 | 5, 8 | unitinvcl 20282 |
. . . . . . . . . 10
β’ ((π β Ring β§ π΄ β (Unitβπ)) β
((invrβπ)βπ΄) β (Unitβπ)) |
31 | 29, 30 | mpan 687 |
. . . . . . . . 9
β’ (π΄ β (Unitβπ) β
((invrβπ)βπ΄) β (Unitβπ)) |
32 | 27, 31 | eqeltrrd 2833 |
. . . . . . . 8
β’ (π΄ β (Unitβπ) β (1 / π΄) β (Unitβπ)) |
33 | 2 | gzrngunitlem 21211 |
. . . . . . . 8
β’ ((1 /
π΄) β (Unitβπ) β 1 β€ (absβ(1 /
π΄))) |
34 | 32, 33 | syl 17 |
. . . . . . 7
β’ (π΄ β (Unitβπ) β 1 β€ (absβ(1 /
π΄))) |
35 | | 1cnd 11214 |
. . . . . . . 8
β’ (π΄ β (Unitβπ) β 1 β
β) |
36 | 35, 12, 24 | absdivd 15407 |
. . . . . . 7
β’ (π΄ β (Unitβπ) β (absβ(1 / π΄)) = ((absβ1) /
(absβπ΄))) |
37 | 34, 36 | breqtrd 5174 |
. . . . . 6
β’ (π΄ β (Unitβπ) β 1 β€ ((absβ1) /
(absβπ΄))) |
38 | | 1div1e1 11909 |
. . . . . 6
β’ (1 / 1) =
1 |
39 | | abs1 15249 |
. . . . . . . 8
β’
(absβ1) = 1 |
40 | 39 | eqcomi 2740 |
. . . . . . 7
β’ 1 =
(absβ1) |
41 | 40 | oveq1i 7422 |
. . . . . 6
β’ (1 /
(absβπ΄)) =
((absβ1) / (absβπ΄)) |
42 | 37, 38, 41 | 3brtr4g 5182 |
. . . . 5
β’ (π΄ β (Unitβπ) β (1 / 1) β€ (1 /
(absβπ΄))) |
43 | | lerec 12102 |
. . . . . 6
β’
((((absβπ΄)
β β β§ 0 < (absβπ΄)) β§ (1 β β β§ 0 < 1))
β ((absβπ΄) β€
1 β (1 / 1) β€ (1 / (absβπ΄)))) |
44 | 16, 20, 15, 18, 43 | syl22anc 836 |
. . . . 5
β’ (π΄ β (Unitβπ) β ((absβπ΄) β€ 1 β (1 / 1) β€ (1
/ (absβπ΄)))) |
45 | 42, 44 | mpbird 257 |
. . . 4
β’ (π΄ β (Unitβπ) β (absβπ΄) β€ 1) |
46 | | letri3 11304 |
. . . . 5
β’
(((absβπ΄)
β β β§ 1 β β) β ((absβπ΄) = 1 β ((absβπ΄) β€ 1 β§ 1 β€ (absβπ΄)))) |
47 | 16, 14, 46 | sylancl 585 |
. . . 4
β’ (π΄ β (Unitβπ) β ((absβπ΄) = 1 β ((absβπ΄) β€ 1 β§ 1 β€
(absβπ΄)))) |
48 | 45, 19, 47 | mpbir2and 710 |
. . 3
β’ (π΄ β (Unitβπ) β (absβπ΄) = 1) |
49 | 6, 48 | jca 511 |
. 2
β’ (π΄ β (Unitβπ) β (π΄ β β€[i] β§ (absβπ΄) = 1)) |
50 | 11 | adantr 480 |
. . . 4
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
π΄ β
β) |
51 | | simpr 484 |
. . . . . 6
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
(absβπ΄) =
1) |
52 | | ax-1ne0 11183 |
. . . . . . 7
β’ 1 β
0 |
53 | 52 | a1i 11 |
. . . . . 6
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β 1
β 0) |
54 | 51, 53 | eqnetrd 3007 |
. . . . 5
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
(absβπ΄) β
0) |
55 | | fveq2 6891 |
. . . . . . 7
β’ (π΄ = 0 β (absβπ΄) =
(absβ0)) |
56 | | abs0 15237 |
. . . . . . 7
β’
(absβ0) = 0 |
57 | 55, 56 | eqtrdi 2787 |
. . . . . 6
β’ (π΄ = 0 β (absβπ΄) = 0) |
58 | 57 | necon3i 2972 |
. . . . 5
β’
((absβπ΄) β
0 β π΄ β
0) |
59 | 54, 58 | syl 17 |
. . . 4
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
π΄ β 0) |
60 | | eldifsn 4790 |
. . . 4
β’ (π΄ β (β β {0})
β (π΄ β β
β§ π΄ β
0)) |
61 | 50, 59, 60 | sylanbrc 582 |
. . 3
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
π΄ β (β β
{0})) |
62 | | simpl 482 |
. . 3
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
π΄ β
β€[i]) |
63 | 50, 59, 25 | syl2anc 583 |
. . . . 5
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
((invrββfld)βπ΄) = (1 / π΄)) |
64 | 50 | absvalsqd 15394 |
. . . . . . 7
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
((absβπ΄)β2) =
(π΄ Β·
(ββπ΄))) |
65 | 51 | oveq1d 7427 |
. . . . . . . 8
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
((absβπ΄)β2) =
(1β2)) |
66 | | sq1 14164 |
. . . . . . . 8
β’
(1β2) = 1 |
67 | 65, 66 | eqtrdi 2787 |
. . . . . . 7
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
((absβπ΄)β2) =
1) |
68 | 64, 67 | eqtr3d 2773 |
. . . . . 6
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
(π΄ Β·
(ββπ΄)) =
1) |
69 | 68 | oveq1d 7427 |
. . . . 5
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
((π΄ Β·
(ββπ΄)) / π΄) = (1 / π΄)) |
70 | 50 | cjcld 15148 |
. . . . . 6
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
(ββπ΄) β
β) |
71 | 70, 50, 59 | divcan3d 12000 |
. . . . 5
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
((π΄ Β·
(ββπ΄)) / π΄) = (ββπ΄)) |
72 | 63, 69, 71 | 3eqtr2d 2777 |
. . . 4
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
((invrββfld)βπ΄) = (ββπ΄)) |
73 | | gzcjcl 16874 |
. . . . 5
β’ (π΄ β β€[i] β
(ββπ΄) β
β€[i]) |
74 | 73 | adantr 480 |
. . . 4
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
(ββπ΄) β
β€[i]) |
75 | 72, 74 | eqeltrd 2832 |
. . 3
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
((invrββfld)βπ΄) β β€[i]) |
76 | | cnfldbas 21149 |
. . . . . 6
β’ β =
(Baseββfld) |
77 | | cnfld0 21170 |
. . . . . 6
β’ 0 =
(0gββfld) |
78 | | cndrng 21175 |
. . . . . 6
β’
βfld β DivRing |
79 | 76, 77, 78 | drngui 20507 |
. . . . 5
β’ (β
β {0}) = (Unitββfld) |
80 | 2, 79, 5, 7 | subrgunit 20481 |
. . . 4
β’
(β€[i] β (SubRingββfld) β (π΄ β (Unitβπ) β (π΄ β (β β {0}) β§ π΄ β β€[i] β§
((invrββfld)βπ΄) β β€[i]))) |
81 | 1, 80 | ax-mp 5 |
. . 3
β’ (π΄ β (Unitβπ) β (π΄ β (β β {0}) β§ π΄ β β€[i] β§
((invrββfld)βπ΄) β β€[i])) |
82 | 61, 62, 75, 81 | syl3anbrc 1342 |
. 2
β’ ((π΄ β β€[i] β§
(absβπ΄) = 1) β
π΄ β (Unitβπ)) |
83 | 49, 82 | impbii 208 |
1
β’ (π΄ β (Unitβπ) β (π΄ β β€[i] β§ (absβπ΄) = 1)) |