Step | Hyp | Ref
| Expression |
1 | | cnre 7928 |
. 2
|
2 | | cnegexlem2 8107 |
. . . . 5
|
3 | | cnegexlem3 8108 |
. . . . . . . 8
|
4 | 3 | ad2ant2lr 510 |
. . . . . . 7
|
5 | | ax-icn 7881 |
. . . . . . . . . . . . . 14
|
6 | | recn 7919 |
. . . . . . . . . . . . . 14
|
7 | | mulcl 7913 |
. . . . . . . . . . . . . 14
|
8 | 5, 6, 7 | sylancr 414 |
. . . . . . . . . . . . 13
|
9 | | recn 7919 |
. . . . . . . . . . . . 13
|
10 | | addcl 7911 |
. . . . . . . . . . . . 13
|
11 | 8, 9, 10 | syl2an 289 |
. . . . . . . . . . . 12
|
12 | 11 | adantlr 477 |
. . . . . . . . . . 11
|
13 | 12 | adantll 476 |
. . . . . . . . . 10
|
14 | 13 | adantr 276 |
. . . . . . . . 9
|
15 | | recn 7919 |
. . . . . . . . . . . . . . . . 17
|
16 | | recn 7919 |
. . . . . . . . . . . . . . . . 17
|
17 | 15, 16 | anim12i 338 |
. . . . . . . . . . . . . . . 16
|
18 | 17, 6 | anim12i 338 |
. . . . . . . . . . . . . . 15
|
19 | | mulcl 7913 |
. . . . . . . . . . . . . . . . . . . 20
|
20 | 5, 19 | mpan 424 |
. . . . . . . . . . . . . . . . . . 19
|
21 | | addcl 7911 |
. . . . . . . . . . . . . . . . . . 19
|
22 | 20, 21 | sylan2 286 |
. . . . . . . . . . . . . . . . . 18
|
23 | 22 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
|
24 | 5, 7 | mpan 424 |
. . . . . . . . . . . . . . . . . 18
|
25 | 24 | ad2antlr 489 |
. . . . . . . . . . . . . . . . 17
|
26 | | simpr 110 |
. . . . . . . . . . . . . . . . 17
|
27 | 23, 25, 26 | addassd 7954 |
. . . . . . . . . . . . . . . 16
|
28 | | simpll 527 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | 20 | ad2antlr 489 |
. . . . . . . . . . . . . . . . . . . 20
|
30 | 24 | adantl 277 |
. . . . . . . . . . . . . . . . . . . 20
|
31 | 28, 29, 30 | addassd 7954 |
. . . . . . . . . . . . . . . . . . 19
|
32 | | adddi 7918 |
. . . . . . . . . . . . . . . . . . . . . 22
|
33 | 5, 32 | mp3an1 1324 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | 33 | adantll 476 |
. . . . . . . . . . . . . . . . . . . 20
|
35 | 34 | oveq2d 5881 |
. . . . . . . . . . . . . . . . . . 19
|
36 | 31, 35 | eqtr4d 2211 |
. . . . . . . . . . . . . . . . . 18
|
37 | 36 | adantr 276 |
. . . . . . . . . . . . . . . . 17
|
38 | 37 | oveq1d 5880 |
. . . . . . . . . . . . . . . 16
|
39 | 27, 38 | eqtr3d 2210 |
. . . . . . . . . . . . . . 15
|
40 | 18, 9, 39 | syl2an 289 |
. . . . . . . . . . . . . 14
|
41 | 40 | adantlrr 483 |
. . . . . . . . . . . . 13
|
42 | | oveq2 5873 |
. . . . . . . . . . . . . . . . 17
|
43 | 42 | oveq2d 5881 |
. . . . . . . . . . . . . . . 16
|
44 | 43 | oveq1d 5880 |
. . . . . . . . . . . . . . 15
|
45 | 44 | adantl 277 |
. . . . . . . . . . . . . 14
|
46 | 45 | ad2antlr 489 |
. . . . . . . . . . . . 13
|
47 | 41, 46 | eqtr2d 2209 |
. . . . . . . . . . . 12
|
48 | 47 | adantllr 481 |
. . . . . . . . . . 11
|
49 | 48 | eqeq1d 2184 |
. . . . . . . . . 10
|
50 | 49 | biimpa 296 |
. . . . . . . . 9
|
51 | | oveq2 5873 |
. . . . . . . . . . 11
|
52 | 51 | eqeq1d 2184 |
. . . . . . . . . 10
|
53 | 52 | rspcev 2839 |
. . . . . . . . 9
|
54 | 14, 50, 53 | syl2anc 411 |
. . . . . . . 8
|
55 | | readdcl 7912 |
. . . . . . . . . . 11
|
56 | | ax-rnegex 7895 |
. . . . . . . . . . 11
|
57 | 55, 56 | syl 14 |
. . . . . . . . . 10
|
58 | 57 | ad2ant2rl 511 |
. . . . . . . . 9
|
59 | 58 | adantr 276 |
. . . . . . . 8
|
60 | 54, 59 | r19.29a 2618 |
. . . . . . 7
|
61 | 4, 60 | rexlimddv 2597 |
. . . . . 6
|
62 | 61 | rexlimdvaa 2593 |
. . . . 5
|
63 | 2, 62 | mpi 15 |
. . . 4
|
64 | | oveq1 5872 |
. . . . . 6
|
65 | 64 | eqeq1d 2184 |
. . . . 5
|
66 | 65 | rexbidv 2476 |
. . . 4
|
67 | 63, 66 | syl5ibrcom 157 |
. . 3
|
68 | 67 | rexlimivv 2598 |
. 2
|
69 | 1, 68 | syl 14 |
1
|