Step | Hyp | Ref
| Expression |
1 | | cnre 7023 |
. 2
|
2 | | cnegexlem2 7187 |
. . . . 5
|
3 | | cnegexlem3 7188 |
. . . . . . . 8
|
4 | 3 | ad2ant2lr 479 |
. . . . . . 7
|
5 | | ax-icn 6979 |
. . . . . . . . . . . . . 14
|
6 | | recn 7014 |
. . . . . . . . . . . . . 14
|
7 | | mulcl 7008 |
. . . . . . . . . . . . . 14
|
8 | 5, 6, 7 | sylancr 393 |
. . . . . . . . . . . . 13
|
9 | | recn 7014 |
. . . . . . . . . . . . 13
|
10 | | addcl 7006 |
. . . . . . . . . . . . 13
|
11 | 8, 9, 10 | syl2an 273 |
. . . . . . . . . . . 12
|
12 | 11 | adantlr 446 |
. . . . . . . . . . 11
|
13 | 12 | adantll 445 |
. . . . . . . . . 10
|
14 | 13 | adantr 261 |
. . . . . . . . 9
|
15 | | recn 7014 |
. . . . . . . . . . . . . . . . 17
|
16 | | recn 7014 |
. . . . . . . . . . . . . . . . 17
|
17 | 15, 16 | anim12i 321 |
. . . . . . . . . . . . . . . 16
|
18 | 17, 6 | anim12i 321 |
. . . . . . . . . . . . . . 15
|
19 | | mulcl 7008 |
. . . . . . . . . . . . . . . . . . . 20
|
20 | 5, 19 | mpan 400 |
. . . . . . . . . . . . . . . . . . 19
|
21 | | addcl 7006 |
. . . . . . . . . . . . . . . . . . 19
|
22 | 20, 21 | sylan2 270 |
. . . . . . . . . . . . . . . . . 18
|
23 | 22 | ad2antrr 457 |
. . . . . . . . . . . . . . . . 17
|
24 | 5, 7 | mpan 400 |
. . . . . . . . . . . . . . . . . 18
|
25 | 24 | ad2antlr 458 |
. . . . . . . . . . . . . . . . 17
|
26 | | simpr 103 |
. . . . . . . . . . . . . . . . 17
|
27 | 23, 25, 26 | addassd 7049 |
. . . . . . . . . . . . . . . 16
|
28 | | simpll 481 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | 20 | ad2antlr 458 |
. . . . . . . . . . . . . . . . . . . 20
|
30 | 24 | adantl 262 |
. . . . . . . . . . . . . . . . . . . 20
|
31 | 28, 29, 30 | addassd 7049 |
. . . . . . . . . . . . . . . . . . 19
|
32 | | adddi 7013 |
. . . . . . . . . . . . . . . . . . . . . 22
|
33 | 5, 32 | mp3an1 1219 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | 33 | adantll 445 |
. . . . . . . . . . . . . . . . . . . 20
|
35 | 34 | oveq2d 5528 |
. . . . . . . . . . . . . . . . . . 19
|
36 | 31, 35 | eqtr4d 2075 |
. . . . . . . . . . . . . . . . . 18
|
37 | 36 | adantr 261 |
. . . . . . . . . . . . . . . . 17
|
38 | 37 | oveq1d 5527 |
. . . . . . . . . . . . . . . 16
|
39 | 27, 38 | eqtr3d 2074 |
. . . . . . . . . . . . . . 15
|
40 | 18, 9, 39 | syl2an 273 |
. . . . . . . . . . . . . 14
|
41 | 40 | adantlrr 452 |
. . . . . . . . . . . . 13
|
42 | | oveq2 5520 |
. . . . . . . . . . . . . . . . 17
|
43 | 42 | oveq2d 5528 |
. . . . . . . . . . . . . . . 16
|
44 | 43 | oveq1d 5527 |
. . . . . . . . . . . . . . 15
|
45 | 44 | adantl 262 |
. . . . . . . . . . . . . 14
|
46 | 45 | ad2antlr 458 |
. . . . . . . . . . . . 13
|
47 | 41, 46 | eqtr2d 2073 |
. . . . . . . . . . . 12
|
48 | 47 | adantllr 450 |
. . . . . . . . . . 11
|
49 | 48 | eqeq1d 2048 |
. . . . . . . . . 10
|
50 | 49 | biimpa 280 |
. . . . . . . . 9
|
51 | | oveq2 5520 |
. . . . . . . . . . 11
|
52 | 51 | eqeq1d 2048 |
. . . . . . . . . 10
|
53 | 52 | rspcev 2656 |
. . . . . . . . 9
|
54 | 14, 50, 53 | syl2anc 391 |
. . . . . . . 8
|
55 | | readdcl 7007 |
. . . . . . . . . . 11
|
56 | | ax-rnegex 6993 |
. . . . . . . . . . 11
|
57 | 55, 56 | syl 14 |
. . . . . . . . . 10
|
58 | 57 | ad2ant2rl 480 |
. . . . . . . . 9
|
59 | 58 | adantr 261 |
. . . . . . . 8
|
60 | 54, 59 | r19.29a 2454 |
. . . . . . 7
|
61 | 4, 60 | rexlimddv 2437 |
. . . . . 6
|
62 | 61 | rexlimdvaa 2434 |
. . . . 5
|
63 | 2, 62 | mpi 15 |
. . . 4
|
64 | | oveq1 5519 |
. . . . . 6
|
65 | 64 | eqeq1d 2048 |
. . . . 5
|
66 | 65 | rexbidv 2327 |
. . . 4
|
67 | 63, 66 | syl5ibrcom 146 |
. . 3
|
68 | 67 | rexlimivv 2438 |
. 2
|
69 | 1, 68 | syl 14 |
1
|