Step | Hyp | Ref
| Expression |
1 | | cnre 7944 |
. 2
         |
2 | | cnegexlem2 8123 |
. . . . 5
    |
3 | | cnegexlem3 8124 |
. . . . . . . 8
 
      |
4 | 3 | ad2ant2lr 510 |
. . . . . . 7
         
    |
5 | | ax-icn 7897 |
. . . . . . . . . . . . . 14
 |
6 | | recn 7935 |
. . . . . . . . . . . . . 14
   |
7 | | mulcl 7929 |
. . . . . . . . . . . . . 14
 
     |
8 | 5, 6, 7 | sylancr 414 |
. . . . . . . . . . . . 13
 
   |
9 | | recn 7935 |
. . . . . . . . . . . . 13
   |
10 | | addcl 7927 |
. . . . . . . . . . . . 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 7935 |
. . . . . . . . . . . . . . . . 17
   |
16 | | recn 7935 |
. . . . . . . . . . . . . . . . 17
   |
17 | 15, 16 | anim12i 338 |
. . . . . . . . . . . . . . . 16
 
     |
18 | 17, 6 | anim12i 338 |
. . . . . . . . . . . . . . 15
           |
19 | | mulcl 7929 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
20 | 5, 19 | mpan 424 |
. . . . . . . . . . . . . . . . . . 19
 
   |
21 | | addcl 7927 |
. . . . . . . . . . . . . . . . . . 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 7970 |
. . . . . . . . . . . . . . . 16
                             |
28 | | simpll 527 |
. . . . . . . . . . . . . . . . . . . 20
       |
29 | 20 | ad2antlr 489 |
. . . . . . . . . . . . . . . . . . . 20
         |
30 | 24 | adantl 277 |
. . . . . . . . . . . . . . . . . . . 20
         |
31 | 28, 29, 30 | addassd 7970 |
. . . . . . . . . . . . . . . . . . 19
                       |
32 | | adddi 7934 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
           |
33 | 5, 32 | mp3an1 1324 |
. . . . . . . . . . . . . . . . . . . . 21
 
             |
34 | 33 | adantll 476 |
. . . . . . . . . . . . . . . . . . . 20
                 |
35 | 34 | oveq2d 5885 |
. . . . . . . . . . . . . . . . . . 19
                     |
36 | 31, 35 | eqtr4d 2213 |
. . . . . . . . . . . . . . . . . 18
                     |
37 | 36 | adantr 276 |
. . . . . . . . . . . . . . . . 17
                       |
38 | 37 | oveq1d 5884 |
. . . . . . . . . . . . . . . 16
                           |
39 | 27, 38 | eqtr3d 2212 |
. . . . . . . . . . . . . . 15
                           |
40 | 18, 9, 39 | syl2an 289 |
. . . . . . . . . . . . . 14
                           |
41 | 40 | adantlrr 483 |
. . . . . . . . . . . . 13
                               |
42 | | oveq2 5877 |
. . . . . . . . . . . . . . . . 17
   
       |
43 | 42 | oveq2d 5885 |
. . . . . . . . . . . . . . . 16
               |
44 | 43 | oveq1d 5884 |
. . . . . . . . . . . . . . 15
                   |
45 | 44 | adantl 277 |
. . . . . . . . . . . . . 14
                     |
46 | 45 | ad2antlr 489 |
. . . . . . . . . . . . 13
                           |
47 | 41, 46 | eqtr2d 2211 |
. . . . . . . . . . . 12
                             |
48 | 47 | adantllr 481 |
. . . . . . . . . . 11
       
                           |
49 | 48 | eqeq1d 2186 |
. . . . . . . . . 10
       
                             |
50 | 49 | biimpa 296 |
. . . . . . . . 9
     
                  
            |
51 | | oveq2 5877 |
. . . . . . . . . . 11
                       |
52 | 51 | eqeq1d 2186 |
. . . . . . . . . 10
                         |
53 | 52 | rspcev 2841 |
. . . . . . . . 9
                          |
54 | 14, 50, 53 | syl2anc 411 |
. . . . . . . 8
     
                  
         |
55 | | readdcl 7928 |
. . . . . . . . . . 11
  
        |
56 | | ax-rnegex 7911 |
. . . . . . . . . . 11
              |
57 | 55, 56 | syl 14 |
. . . . . . . . . 10
  
           |
58 | 57 | ad2ant2rl 511 |
. . . . . . . . 9
         
        |
59 | 58 | adantr 276 |
. . . . . . . 8
      
                 |
60 | 54, 59 | r19.29a 2620 |
. . . . . . 7
      
                 |
61 | 4, 60 | rexlimddv 2599 |
. . . . . 6
         
        |
62 | 61 | rexlimdvaa 2595 |
. . . . 5
 
               |
63 | 2, 62 | mpi 15 |
. . . 4
 
          |
64 | | oveq1 5876 |
. . . . . 6
     
         |
65 | 64 | eqeq1d 2186 |
. . . . 5
                 |
66 | 65 | rexbidv 2478 |
. . . 4
      

 
         |
67 | 63, 66 | syl5ibrcom 157 |
. . 3
 
       
    |
68 | 67 | rexlimivv 2600 |
. 2
  
         |
69 | 1, 68 | syl 14 |
1
      |