Step | Hyp | Ref
| Expression |
1 | | simplr1 1213 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))
โง (๐ฆ โ โ
โง ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) โ (๐ฅโ2) = ๐ด) |
2 | | simprr1 1219 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))
โง (๐ฆ โ โ
โง ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) โ (๐ฆโ2) = ๐ด) |
3 | 1, 2 | eqtr4d 2773 |
. . . . . . . . . . 11
โข (((๐ฅ โ โ โง ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))
โง (๐ฆ โ โ
โง ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) โ (๐ฅโ2) = (๐ฆโ2)) |
4 | | sqeqor 14186 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ฅโ2) = (๐ฆโ2) โ (๐ฅ = ๐ฆ โจ ๐ฅ = -๐ฆ))) |
5 | 4 | ad2ant2r 743 |
. . . . . . . . . . 11
โข (((๐ฅ โ โ โง ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))
โง (๐ฆ โ โ
โง ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) โ ((๐ฅโ2) = (๐ฆโ2) โ (๐ฅ = ๐ฆ โจ ๐ฅ = -๐ฆ))) |
6 | 3, 5 | mpbid 231 |
. . . . . . . . . 10
โข (((๐ฅ โ โ โง ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))
โง (๐ฆ โ โ
โง ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) โ (๐ฅ = ๐ฆ โจ ๐ฅ = -๐ฆ)) |
7 | 6 | ord 860 |
. . . . . . . . 9
โข (((๐ฅ โ โ โง ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))
โง (๐ฆ โ โ
โง ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) โ (ยฌ ๐ฅ = ๐ฆ โ ๐ฅ = -๐ฆ)) |
8 | | 3simpc 1148 |
. . . . . . . . . . 11
โข (((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+)
โ (0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ
โ+)) |
9 | | fveq2 6892 |
. . . . . . . . . . . . 13
โข (๐ฅ = -๐ฆ โ (โโ๐ฅ) = (โโ-๐ฆ)) |
10 | 9 | breq2d 5161 |
. . . . . . . . . . . 12
โข (๐ฅ = -๐ฆ โ (0 โค (โโ๐ฅ) โ 0 โค
(โโ-๐ฆ))) |
11 | | oveq2 7421 |
. . . . . . . . . . . . 13
โข (๐ฅ = -๐ฆ โ (i ยท ๐ฅ) = (i ยท -๐ฆ)) |
12 | | neleq1 3050 |
. . . . . . . . . . . . 13
โข ((i
ยท ๐ฅ) = (i ยท
-๐ฆ) โ ((i ยท
๐ฅ) โ
โ+ โ (i ยท -๐ฆ) โ
โ+)) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . 12
โข (๐ฅ = -๐ฆ โ ((i ยท ๐ฅ) โ โ+ โ (i
ยท -๐ฆ) โ
โ+)) |
14 | 10, 13 | anbi12d 629 |
. . . . . . . . . . 11
โข (๐ฅ = -๐ฆ โ ((0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+)
โ (0 โค (โโ-๐ฆ) โง (i ยท -๐ฆ) โ
โ+))) |
15 | 8, 14 | syl5ibcom 244 |
. . . . . . . . . 10
โข (((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+)
โ (๐ฅ = -๐ฆ โ (0 โค
(โโ-๐ฆ) โง (i
ยท -๐ฆ) โ
โ+))) |
16 | 15 | ad2antlr 723 |
. . . . . . . . 9
โข (((๐ฅ โ โ โง ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))
โง (๐ฆ โ โ
โง ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) โ (๐ฅ = -๐ฆ โ (0 โค (โโ-๐ฆ) โง (i ยท -๐ฆ) โ
โ+))) |
17 | 7, 16 | syld 47 |
. . . . . . . 8
โข (((๐ฅ โ โ โง ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))
โง (๐ฆ โ โ
โง ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) โ (ยฌ ๐ฅ = ๐ฆ โ (0 โค (โโ-๐ฆ) โง (i ยท -๐ฆ) โ
โ+))) |
18 | | negeq 11458 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = 0 โ -๐ฆ = -0) |
19 | | neg0 11512 |
. . . . . . . . . . . . . . 15
โข -0 =
0 |
20 | 18, 19 | eqtrdi 2786 |
. . . . . . . . . . . . . 14
โข (๐ฆ = 0 โ -๐ฆ = 0) |
21 | 20 | eqeq2d 2741 |
. . . . . . . . . . . . 13
โข (๐ฆ = 0 โ (๐ฅ = -๐ฆ โ ๐ฅ = 0)) |
22 | | eqeq2 2742 |
. . . . . . . . . . . . 13
โข (๐ฆ = 0 โ (๐ฅ = ๐ฆ โ ๐ฅ = 0)) |
23 | 21, 22 | bitr4d 281 |
. . . . . . . . . . . 12
โข (๐ฆ = 0 โ (๐ฅ = -๐ฆ โ ๐ฅ = ๐ฆ)) |
24 | 23 | biimpcd 248 |
. . . . . . . . . . 11
โข (๐ฅ = -๐ฆ โ (๐ฆ = 0 โ ๐ฅ = ๐ฆ)) |
25 | 24 | necon3bd 2952 |
. . . . . . . . . 10
โข (๐ฅ = -๐ฆ โ (ยฌ ๐ฅ = ๐ฆ โ ๐ฆ โ 0)) |
26 | 7, 25 | syli 39 |
. . . . . . . . 9
โข (((๐ฅ โ โ โง ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))
โง (๐ฆ โ โ
โง ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) โ (ยฌ ๐ฅ = ๐ฆ โ ๐ฆ โ 0)) |
27 | | 3simpc 1148 |
. . . . . . . . . . . 12
โข (((๐ฆโ2) = ๐ด โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+)
โ (0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ
โ+)) |
28 | | cnpart 15193 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ โง ๐ฆ โ 0) โ ((0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+) โ ยฌ (0 โค (โโ-๐ฆ) โง (i ยท -๐ฆ) โ
โ+))) |
29 | 27, 28 | imbitrid 243 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง ๐ฆ โ 0) โ (((๐ฆโ2) = ๐ด โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+)
โ ยฌ (0 โค (โโ-๐ฆ) โง (i ยท -๐ฆ) โ
โ+))) |
30 | 29 | impancom 450 |
. . . . . . . . . 10
โข ((๐ฆ โ โ โง ((๐ฆโ2) = ๐ด โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+))
โ (๐ฆ โ 0 โ
ยฌ (0 โค (โโ-๐ฆ) โง (i ยท -๐ฆ) โ
โ+))) |
31 | 30 | adantl 480 |
. . . . . . . . 9
โข (((๐ฅ โ โ โง ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))
โง (๐ฆ โ โ
โง ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) โ (๐ฆ โ 0 โ ยฌ (0 โค
(โโ-๐ฆ) โง (i
ยท -๐ฆ) โ
โ+))) |
32 | 26, 31 | syld 47 |
. . . . . . . 8
โข (((๐ฅ โ โ โง ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))
โง (๐ฆ โ โ
โง ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) โ (ยฌ ๐ฅ = ๐ฆ โ ยฌ (0 โค (โโ-๐ฆ) โง (i ยท -๐ฆ) โ
โ+))) |
33 | 17, 32 | pm2.65d 195 |
. . . . . . 7
โข (((๐ฅ โ โ โง ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))
โง (๐ฆ โ โ
โง ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) โ ยฌ ยฌ ๐ฅ = ๐ฆ) |
34 | 33 | notnotrd 133 |
. . . . . 6
โข (((๐ฅ โ โ โง ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))
โง (๐ฆ โ โ
โง ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) โ ๐ฅ = ๐ฆ) |
35 | 34 | an4s 656 |
. . . . 5
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+)
โง ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) โ ๐ฅ = ๐ฆ) |
36 | 35 | ex 411 |
. . . 4
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
((((๐ฅโ2) = ๐ด โง 0 โค
(โโ๐ฅ) โง (i
ยท ๐ฅ) โ
โ+) โง ((๐ฆโ2) = ๐ด โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+))
โ ๐ฅ = ๐ฆ)) |
37 | 36 | a1i 11 |
. . 3
โข (๐ด โ โ โ ((๐ฅ โ โ โง ๐ฆ โ โ) โ
((((๐ฅโ2) = ๐ด โง 0 โค
(โโ๐ฅ) โง (i
ยท ๐ฅ) โ
โ+) โง ((๐ฆโ2) = ๐ด โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+))
โ ๐ฅ = ๐ฆ))) |
38 | 37 | ralrimivv 3196 |
. 2
โข (๐ด โ โ โ
โ๐ฅ โ โ
โ๐ฆ โ โ
((((๐ฅโ2) = ๐ด โง 0 โค
(โโ๐ฅ) โง (i
ยท ๐ฅ) โ
โ+) โง ((๐ฆโ2) = ๐ด โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+))
โ ๐ฅ = ๐ฆ)) |
39 | | oveq1 7420 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ฅโ2) = (๐ฆโ2)) |
40 | 39 | eqeq1d 2732 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((๐ฅโ2) = ๐ด โ (๐ฆโ2) = ๐ด)) |
41 | | fveq2 6892 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (โโ๐ฅ) = (โโ๐ฆ)) |
42 | 41 | breq2d 5161 |
. . . 4
โข (๐ฅ = ๐ฆ โ (0 โค (โโ๐ฅ) โ 0 โค
(โโ๐ฆ))) |
43 | | oveq2 7421 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (i ยท ๐ฅ) = (i ยท ๐ฆ)) |
44 | | neleq1 3050 |
. . . . 5
โข ((i
ยท ๐ฅ) = (i ยท
๐ฆ) โ ((i ยท
๐ฅ) โ
โ+ โ (i ยท ๐ฆ) โ
โ+)) |
45 | 43, 44 | syl 17 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((i ยท ๐ฅ) โ โ+ โ (i
ยท ๐ฆ) โ
โ+)) |
46 | 40, 42, 45 | 3anbi123d 1434 |
. . 3
โข (๐ฅ = ๐ฆ โ (((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+)
โ ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) |
47 | 46 | rmo4 3727 |
. 2
โข
(โ*๐ฅ โ
โ ((๐ฅโ2) = ๐ด โง 0 โค
(โโ๐ฅ) โง (i
ยท ๐ฅ) โ
โ+) โ โ๐ฅ โ โ โ๐ฆ โ โ ((((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+)
โง ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+)) โ ๐ฅ = ๐ฆ)) |
48 | 38, 47 | sylibr 233 |
1
โข (๐ด โ โ โ
โ*๐ฅ โ โ
((๐ฅโ2) = ๐ด โง 0 โค
(โโ๐ฅ) โง (i
ยท ๐ฅ) โ
โ+)) |