Step | Hyp | Ref
| Expression |
1 | | sq1 14108 |
. . 3
β’
(1β2) = 1 |
2 | | ax-1ne0 11128 |
. . . . . 6
β’ 1 β
0 |
3 | | gzsubrg 20874 |
. . . . . . 7
β’
β€[i] β (SubRingββfld) |
4 | | gzrng.1 |
. . . . . . . 8
β’ π = (βfld
βΎs β€[i]) |
5 | 4 | subrgring 20267 |
. . . . . . 7
β’
(β€[i] β (SubRingββfld) β π β Ring) |
6 | | eqid 2733 |
. . . . . . . 8
β’
(Unitβπ) =
(Unitβπ) |
7 | | subrgsubg 20270 |
. . . . . . . . 9
β’
(β€[i] β (SubRingββfld) β
β€[i] β (SubGrpββfld)) |
8 | | cnfld0 20844 |
. . . . . . . . . 10
β’ 0 =
(0gββfld) |
9 | 4, 8 | subg0 18942 |
. . . . . . . . 9
β’
(β€[i] β (SubGrpββfld) β 0 =
(0gβπ)) |
10 | 3, 7, 9 | mp2b 10 |
. . . . . . . 8
β’ 0 =
(0gβπ) |
11 | | cnfld1 20845 |
. . . . . . . . . 10
β’ 1 =
(1rββfld) |
12 | 4, 11 | subrg1 20274 |
. . . . . . . . 9
β’
(β€[i] β (SubRingββfld) β 1 =
(1rβπ)) |
13 | 3, 12 | ax-mp 5 |
. . . . . . . 8
β’ 1 =
(1rβπ) |
14 | 6, 10, 13 | 0unit 20117 |
. . . . . . 7
β’ (π β Ring β (0 β
(Unitβπ) β 1 =
0)) |
15 | 3, 5, 14 | mp2b 10 |
. . . . . 6
β’ (0 β
(Unitβπ) β 1 =
0) |
16 | 2, 15 | nemtbir 3037 |
. . . . 5
β’ Β¬ 0
β (Unitβπ) |
17 | 4 | subrgbas 20273 |
. . . . . . . . . . 11
β’
(β€[i] β (SubRingββfld) β
β€[i] = (Baseβπ)) |
18 | 3, 17 | ax-mp 5 |
. . . . . . . . . 10
β’
β€[i] = (Baseβπ) |
19 | 18, 6 | unitcl 20096 |
. . . . . . . . 9
β’ (π΄ β (Unitβπ) β π΄ β β€[i]) |
20 | | gzabssqcl 16821 |
. . . . . . . . 9
β’ (π΄ β β€[i] β
((absβπ΄)β2)
β β0) |
21 | 19, 20 | syl 17 |
. . . . . . . 8
β’ (π΄ β (Unitβπ) β ((absβπ΄)β2) β
β0) |
22 | | elnn0 12423 |
. . . . . . . 8
β’
(((absβπ΄)β2) β β0 β
(((absβπ΄)β2)
β β β¨ ((absβπ΄)β2) = 0)) |
23 | 21, 22 | sylib 217 |
. . . . . . 7
β’ (π΄ β (Unitβπ) β (((absβπ΄)β2) β β β¨
((absβπ΄)β2) =
0)) |
24 | 23 | ord 863 |
. . . . . 6
β’ (π΄ β (Unitβπ) β (Β¬
((absβπ΄)β2)
β β β ((absβπ΄)β2) = 0)) |
25 | | gzcn 16812 |
. . . . . . . . . . 11
β’ (π΄ β β€[i] β π΄ β
β) |
26 | 19, 25 | syl 17 |
. . . . . . . . . 10
β’ (π΄ β (Unitβπ) β π΄ β β) |
27 | 26 | abscld 15330 |
. . . . . . . . 9
β’ (π΄ β (Unitβπ) β (absβπ΄) β
β) |
28 | 27 | recnd 11191 |
. . . . . . . 8
β’ (π΄ β (Unitβπ) β (absβπ΄) β
β) |
29 | | sqeq0 14034 |
. . . . . . . 8
β’
((absβπ΄)
β β β (((absβπ΄)β2) = 0 β (absβπ΄) = 0)) |
30 | 28, 29 | syl 17 |
. . . . . . 7
β’ (π΄ β (Unitβπ) β (((absβπ΄)β2) = 0 β
(absβπ΄) =
0)) |
31 | 26 | abs00ad 15184 |
. . . . . . . 8
β’ (π΄ β (Unitβπ) β ((absβπ΄) = 0 β π΄ = 0)) |
32 | | eleq1 2822 |
. . . . . . . . 9
β’ (π΄ = 0 β (π΄ β (Unitβπ) β 0 β (Unitβπ))) |
33 | 32 | biimpcd 249 |
. . . . . . . 8
β’ (π΄ β (Unitβπ) β (π΄ = 0 β 0 β (Unitβπ))) |
34 | 31, 33 | sylbid 239 |
. . . . . . 7
β’ (π΄ β (Unitβπ) β ((absβπ΄) = 0 β 0 β
(Unitβπ))) |
35 | 30, 34 | sylbid 239 |
. . . . . 6
β’ (π΄ β (Unitβπ) β (((absβπ΄)β2) = 0 β 0 β
(Unitβπ))) |
36 | 24, 35 | syld 47 |
. . . . 5
β’ (π΄ β (Unitβπ) β (Β¬
((absβπ΄)β2)
β β β 0 β (Unitβπ))) |
37 | 16, 36 | mt3i 149 |
. . . 4
β’ (π΄ β (Unitβπ) β ((absβπ΄)β2) β
β) |
38 | 37 | nnge1d 12209 |
. . 3
β’ (π΄ β (Unitβπ) β 1 β€
((absβπ΄)β2)) |
39 | 1, 38 | eqbrtrid 5144 |
. 2
β’ (π΄ β (Unitβπ) β (1β2) β€
((absβπ΄)β2)) |
40 | 26 | absge0d 15338 |
. . 3
β’ (π΄ β (Unitβπ) β 0 β€ (absβπ΄)) |
41 | | 1re 11163 |
. . . 4
β’ 1 β
β |
42 | | 0le1 11686 |
. . . 4
β’ 0 β€
1 |
43 | | le2sq 14048 |
. . . 4
β’ (((1
β β β§ 0 β€ 1) β§ ((absβπ΄) β β β§ 0 β€
(absβπ΄))) β (1
β€ (absβπ΄) β
(1β2) β€ ((absβπ΄)β2))) |
44 | 41, 42, 43 | mpanl12 701 |
. . 3
β’
(((absβπ΄)
β β β§ 0 β€ (absβπ΄)) β (1 β€ (absβπ΄) β (1β2) β€
((absβπ΄)β2))) |
45 | 27, 40, 44 | syl2anc 585 |
. 2
β’ (π΄ β (Unitβπ) β (1 β€
(absβπ΄) β
(1β2) β€ ((absβπ΄)β2))) |
46 | 39, 45 | mpbird 257 |
1
β’ (π΄ β (Unitβπ) β 1 β€ (absβπ΄)) |