Step | Hyp | Ref
| Expression |
1 | | resqrex 15144 |
. 2
โข ((๐ด โ โ โง 0 โค
๐ด) โ โ๐ฆ โ โ (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) |
2 | | simp1l 1198 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ฆ โ โ โง (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) โ ๐ด โ โ) |
3 | | recn 11149 |
. . . . . 6
โข (๐ด โ โ โ ๐ด โ
โ) |
4 | | sqrtval 15131 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) =
(โฉ๐ฅ โ
โ ((๐ฅโ2) = ๐ด โง 0 โค
(โโ๐ฅ) โง (i
ยท ๐ฅ) โ
โ+))) |
5 | 2, 3, 4 | 3syl 18 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ฆ โ โ โง (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) โ (โโ๐ด) = (โฉ๐ฅ โ โ ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ
โ+))) |
6 | | simp3r 1203 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ฆ โ โ โง (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) โ (๐ฆโ2) = ๐ด) |
7 | | simp3l 1202 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ฆ โ โ โง (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) โ 0 โค ๐ฆ) |
8 | | rere 15016 |
. . . . . . . . 9
โข (๐ฆ โ โ โ
(โโ๐ฆ) = ๐ฆ) |
9 | 8 | 3ad2ant2 1135 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ฆ โ โ โง (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) โ (โโ๐ฆ) = ๐ฆ) |
10 | 7, 9 | breqtrrd 5137 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ฆ โ โ โง (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) โ 0 โค (โโ๐ฆ)) |
11 | | rennim 15133 |
. . . . . . . 8
โข (๐ฆ โ โ โ (i
ยท ๐ฆ) โ
โ+) |
12 | 11 | 3ad2ant2 1135 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ฆ โ โ โง (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) โ (i ยท ๐ฆ) โ
โ+) |
13 | 6, 10, 12 | 3jca 1129 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ฆ โ โ โง (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) โ ((๐ฆโ2) = ๐ด โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ
โ+)) |
14 | | recn 11149 |
. . . . . . . 8
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
15 | 14 | 3ad2ant2 1135 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ฆ โ โ โง (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) โ ๐ฆ โ โ) |
16 | | resqreu 15146 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 โค
๐ด) โ โ!๐ฅ โ โ ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ
โ+)) |
17 | 16 | 3ad2ant1 1134 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ฆ โ โ โง (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) โ โ!๐ฅ โ โ ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ
โ+)) |
18 | | oveq1 7368 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ (๐ฅโ2) = (๐ฆโ2)) |
19 | 18 | eqeq1d 2735 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ ((๐ฅโ2) = ๐ด โ (๐ฆโ2) = ๐ด)) |
20 | | fveq2 6846 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ (โโ๐ฅ) = (โโ๐ฆ)) |
21 | 20 | breq2d 5121 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ (0 โค (โโ๐ฅ) โ 0 โค
(โโ๐ฆ))) |
22 | | oveq2 7369 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ (i ยท ๐ฅ) = (i ยท ๐ฆ)) |
23 | | neleq1 3051 |
. . . . . . . . . 10
โข ((i
ยท ๐ฅ) = (i ยท
๐ฆ) โ ((i ยท
๐ฅ) โ
โ+ โ (i ยท ๐ฆ) โ
โ+)) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ ((i ยท ๐ฅ) โ โ+ โ (i
ยท ๐ฆ) โ
โ+)) |
25 | 19, 21, 24 | 3anbi123d 1437 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ (((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+)
โ ((๐ฆโ2) = ๐ด โง 0 โค
(โโ๐ฆ) โง (i
ยท ๐ฆ) โ
โ+))) |
26 | 25 | riota2 7343 |
. . . . . . 7
โข ((๐ฆ โ โ โง
โ!๐ฅ โ โ
((๐ฅโ2) = ๐ด โง 0 โค
(โโ๐ฅ) โง (i
ยท ๐ฅ) โ
โ+)) โ (((๐ฆโ2) = ๐ด โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+)
โ (โฉ๐ฅ
โ โ ((๐ฅโ2)
= ๐ด โง 0 โค
(โโ๐ฅ) โง (i
ยท ๐ฅ) โ
โ+)) = ๐ฆ)) |
27 | 15, 17, 26 | syl2anc 585 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ฆ โ โ โง (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) โ (((๐ฆโ2) = ๐ด โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+)
โ (โฉ๐ฅ
โ โ ((๐ฅโ2)
= ๐ด โง 0 โค
(โโ๐ฅ) โง (i
ยท ๐ฅ) โ
โ+)) = ๐ฆ)) |
28 | 13, 27 | mpbid 231 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ฆ โ โ โง (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) โ (โฉ๐ฅ โ โ ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))
= ๐ฆ) |
29 | 5, 28 | eqtrd 2773 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ฆ โ โ โง (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) โ (โโ๐ด) = ๐ฆ) |
30 | | simp2 1138 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ฆ โ โ โง (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) โ ๐ฆ โ โ) |
31 | 29, 30 | eqeltrd 2834 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ฆ โ โ โง (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด)) โ (โโ๐ด) โ โ) |
32 | 31 | rexlimdv3a 3153 |
. 2
โข ((๐ด โ โ โง 0 โค
๐ด) โ (โ๐ฆ โ โ (0 โค ๐ฆ โง (๐ฆโ2) = ๐ด) โ (โโ๐ด) โ โ)) |
33 | 1, 32 | mpd 15 |
1
โข ((๐ด โ โ โง 0 โค
๐ด) โ
(โโ๐ด) โ
โ) |