Step | Hyp | Ref
| Expression |
1 | | ax-rnegex 7085 |
. . . 4
|
2 | 1 | 3ad2ant1 959 |
. . 3
|
3 | | recn 7106 |
. . . 4
|
4 | | recn 7106 |
. . . . . . 7
|
5 | | oveq2 5540 |
. . . . . . . . . . 11
|
6 | | simpr 108 |
. . . . . . . . . . . . 13
|
7 | | simpll 495 |
. . . . . . . . . . . . 13
|
8 | | simplrl 501 |
. . . . . . . . . . . . 13
|
9 | 6, 7, 8 | addassd 7141 |
. . . . . . . . . . . 12
|
10 | | simplrr 502 |
. . . . . . . . . . . . 13
|
11 | 6, 7, 10 | addassd 7141 |
. . . . . . . . . . . 12
|
12 | 9, 11 | eqeq12d 2095 |
. . . . . . . . . . 11
|
13 | 5, 12 | syl5ibr 154 |
. . . . . . . . . 10
|
14 | 13 | adantr 270 |
. . . . . . . . 9
|
15 | | addcom 7245 |
. . . . . . . . . . . . 13
|
16 | 15 | eqeq1d 2089 |
. . . . . . . . . . . 12
|
17 | 16 | adantlr 460 |
. . . . . . . . . . 11
|
18 | | oveq1 5539 |
. . . . . . . . . . . . . . 15
|
19 | | oveq1 5539 |
. . . . . . . . . . . . . . 15
|
20 | 18, 19 | eqeq12d 2095 |
. . . . . . . . . . . . . 14
|
21 | 20 | adantl 271 |
. . . . . . . . . . . . 13
|
22 | | addid2 7247 |
. . . . . . . . . . . . . . . 16
|
23 | | addid2 7247 |
. . . . . . . . . . . . . . . 16
|
24 | 22, 23 | eqeqan12d 2096 |
. . . . . . . . . . . . . . 15
|
25 | 24 | adantl 271 |
. . . . . . . . . . . . . 14
|
26 | 25 | ad2antrr 471 |
. . . . . . . . . . . . 13
|
27 | 21, 26 | bitrd 186 |
. . . . . . . . . . . 12
|
28 | 27 | ex 113 |
. . . . . . . . . . 11
|
29 | 17, 28 | sylbid 148 |
. . . . . . . . . 10
|
30 | 29 | imp 122 |
. . . . . . . . 9
|
31 | 14, 30 | sylibd 147 |
. . . . . . . 8
|
32 | 31 | ex 113 |
. . . . . . 7
|
33 | 4, 32 | sylan2 280 |
. . . . . 6
|
34 | 33 | rexlimdva 2477 |
. . . . 5
|
35 | 34 | 3impb 1134 |
. . . 4
|
36 | 3, 35 | syl3an1 1202 |
. . 3
|
37 | 2, 36 | mpd 13 |
. 2
|
38 | | oveq2 5540 |
. 2
|
39 | 37, 38 | impbid1 140 |
1
|