Step | Hyp | Ref
| Expression |
1 | | negnegs 27875 |
. . . 4
âĒ (ðī â
No â ( -us â( -us âðī)) = ðī) |
2 | 1 | adantr 480 |
. . 3
âĒ ((ðī â
No â§ 0s âĪs ðī) â ( -us â(
-us âðī)) =
ðī) |
3 | | negscl 27867 |
. . . 4
âĒ (ðī â
No â ( -us âðī) â No
) |
4 | | 0sno 27678 |
. . . . . . . 8
âĒ
0s â No |
5 | 4 | a1i 11 |
. . . . . . 7
âĒ (ðī â
No â 0s â No
) |
6 | | id 22 |
. . . . . . 7
âĒ (ðī â
No â ðī â
No ) |
7 | 5, 6 | slenegd 27879 |
. . . . . 6
âĒ (ðī â
No â ( 0s âĪs ðī â ( -us âðī) âĪs ( -us â
0s ))) |
8 | | negs0s 27858 |
. . . . . . 7
âĒ (
-us â 0s ) = 0s |
9 | 8 | breq2i 5147 |
. . . . . 6
âĒ ((
-us âðī)
âĪs ( -us â 0s ) â ( -us
âðī) âĪs
0s ) |
10 | 7, 9 | bitrdi 287 |
. . . . 5
âĒ (ðī â
No â ( 0s âĪs ðī â ( -us âðī) âĪs 0s
)) |
11 | 10 | biimpa 476 |
. . . 4
âĒ ((ðī â
No â§ 0s âĪs ðī) â ( -us âðī) âĪs 0s
) |
12 | | abssnid 28056 |
. . . 4
âĒ (((
-us âðī)
â No â§ ( -us âðī) âĪs 0s ) â
(abssâ( -us âðī)) = ( -us â(
-us âðī))) |
13 | 3, 11, 12 | syl2an2r 682 |
. . 3
âĒ ((ðī â
No â§ 0s âĪs ðī) â (abssâ(
-us âðī)) =
( -us â( -us âðī))) |
14 | | abssid 28054 |
. . 3
âĒ ((ðī â
No â§ 0s âĪs ðī) â (abssâðī) = ðī) |
15 | 2, 13, 14 | 3eqtr4d 2774 |
. 2
âĒ ((ðī â
No â§ 0s âĪs ðī) â (abssâ(
-us âðī)) =
(abssâðī)) |
16 | 6, 5 | slenegd 27879 |
. . . . . 6
âĒ (ðī â
No â (ðī âĪs
0s â ( -us â 0s ) âĪs (
-us âðī))) |
17 | 8 | breq1i 5146 |
. . . . . 6
âĒ ((
-us â 0s ) âĪs ( -us âðī) â 0s âĪs (
-us âðī)) |
18 | 16, 17 | bitrdi 287 |
. . . . 5
âĒ (ðī â
No â (ðī âĪs
0s â 0s âĪs ( -us âðī))) |
19 | 18 | biimpa 476 |
. . . 4
âĒ ((ðī â
No â§ ðī âĪs
0s ) â 0s âĪs ( -us âðī)) |
20 | | abssid 28054 |
. . . 4
âĒ (((
-us âðī)
â No â§ 0s âĪs (
-us âðī))
â (abssâ( -us âðī)) = ( -us âðī)) |
21 | 3, 19, 20 | syl2an2r 682 |
. . 3
âĒ ((ðī â
No â§ ðī âĪs
0s ) â (abssâ( -us âðī)) = ( -us
âðī)) |
22 | | abssnid 28056 |
. . 3
âĒ ((ðī â
No â§ ðī âĪs
0s ) â (abssâðī) = ( -us âðī)) |
23 | 21, 22 | eqtr4d 2767 |
. 2
âĒ ((ðī â
No â§ ðī âĪs
0s ) â (abssâ( -us âðī)) =
(abssâðī)) |
24 | | sletric 27616 |
. . 3
âĒ ((
0s â No â§ ðī â No )
â ( 0s âĪs ðī âĻ ðī âĪs 0s )) |
25 | 4, 24 | mpan 687 |
. 2
âĒ (ðī â
No â ( 0s âĪs ðī âĻ ðī âĪs 0s )) |
26 | 15, 23, 25 | mpjaodan 955 |
1
âĒ (ðī â
No â (abssâ( -us âðī)) =
(abssâðī)) |