Step | Hyp | Ref
| Expression |
1 | | algcvga.5 |
. . 3
     |
2 | | algcvga.3 |
. . . 4
     |
3 | 2 | ffvelrni 5952 |
. . 3
       |
4 | 1, 3 | syl5eqel 2546 |
. 2
   |
5 | | nn0z 10781 |
. . . 4

  |
6 | | eluz1 10977 |
. . . . 5
 
   
     |
7 | | fveq2 5800 |
. . . . . . . . . 10
           |
8 | 7 | fveq2d 5804 |
. . . . . . . . 9
                   |
9 | 8 | eqeq1d 2456 |
. . . . . . . 8
                     |
10 | 9 | imbi2d 316 |
. . . . . . 7
                         |
11 | | fveq2 5800 |
. . . . . . . . . 10
           |
12 | 11 | fveq2d 5804 |
. . . . . . . . 9
                   |
13 | 12 | eqeq1d 2456 |
. . . . . . . 8
                     |
14 | 13 | imbi2d 316 |
. . . . . . 7
                         |
15 | | fveq2 5800 |
. . . . . . . . . 10
               |
16 | 15 | fveq2d 5804 |
. . . . . . . . 9
                       |
17 | 16 | eqeq1d 2456 |
. . . . . . . 8
                         |
18 | 17 | imbi2d 316 |
. . . . . . 7
                             |
19 | | fveq2 5800 |
. . . . . . . . . 10
           |
20 | 19 | fveq2d 5804 |
. . . . . . . . 9
                   |
21 | 20 | eqeq1d 2456 |
. . . . . . . 8
                     |
22 | 21 | imbi2d 316 |
. . . . . . 7
                         |
23 | | algcvga.1 |
. . . . . . . . 9
     |
24 | | algcvga.2 |
. . . . . . . . 9
            |
25 | | algcvga.4 |
. . . . . . . . 9
                 
       |
26 | 23, 24, 2, 25, 1 | algcvg 13870 |
. . . . . . . 8
           |
27 | 26 | a1i 11 |
. . . . . . 7
 
           |
28 | | nn0ge0 10717 |
. . . . . . . . . . . . . . . . 17

  |
29 | 28 | adantr 465 |
. . . . . . . . . . . . . . . 16
 

  |
30 | | nn0re 10700 |
. . . . . . . . . . . . . . . . 17

  |
31 | | zre 10762 |
. . . . . . . . . . . . . . . . 17
   |
32 | | 0re 9498 |
. . . . . . . . . . . . . . . . . 18
 |
33 | | letr 9580 |
. . . . . . . . . . . . . . . . . 18
 
  
    |
34 | 32, 33 | mp3an1 1302 |
. . . . . . . . . . . . . . . . 17
 
   
   |
35 | 30, 31, 34 | syl2an 477 |
. . . . . . . . . . . . . . . 16
 
   
   |
36 | 29, 35 | mpand 675 |
. . . . . . . . . . . . . . 15
 
 
   |
37 | | elnn0z 10771 |
. . . . . . . . . . . . . . . . 17

    |
38 | 37 | simplbi2 625 |
. . . . . . . . . . . . . . . 16
 
   |
39 | 38 | adantl 466 |
. . . . . . . . . . . . . . 15
 
     |
40 | 36, 39 | syld 44 |
. . . . . . . . . . . . . 14
 
     |
41 | 4, 40 | sylan 471 |
. . . . . . . . . . . . 13
 
     |
42 | 41 | impr 619 |
. . . . . . . . . . . 12
  
 
  |
43 | 42 | expcom 435 |
. . . . . . . . . . 11
       |
44 | 43 | 3adant1 1006 |
. . . . . . . . . 10
 
 
   |
45 | 44 | ancld 553 |
. . . . . . . . 9
 
 

    |
46 | | nn0uz 11007 |
. . . . . . . . . . . . 13
     |
47 | | 0zd 10770 |
. . . . . . . . . . . . 13
   |
48 | | id 22 |
. . . . . . . . . . . . 13
   |
49 | 23 | a1i 11 |
. . . . . . . . . . . . 13
       |
50 | 46, 24, 47, 48, 49 | algrf 13867 |
. . . . . . . . . . . 12
       |
51 | 50 | ffvelrnda 5953 |
. . . . . . . . . . 11
 
       |
52 | | fveq2 5800 |
. . . . . . . . . . . . . . . 16
                   |
53 | 52 | fveq2d 5804 |
. . . . . . . . . . . . . . 15
                           |
54 | 53 | neeq1d 2729 |
. . . . . . . . . . . . . 14
                             |
55 | | fveq2 5800 |
. . . . . . . . . . . . . . 15
                   |
56 | 53, 55 | breq12d 4414 |
. . . . . . . . . . . . . 14
             
   
                       |
57 | 54, 56 | imbi12d 320 |
. . . . . . . . . . . . 13
                      
    
            
                        |
58 | 57, 25 | vtoclga 3142 |
. . . . . . . . . . . 12
                                         |
59 | 23, 2 | algcvgb 13872 |
. . . . . . . . . . . . 13
                                       
                                                         |
60 | | simpr 461 |
. . . . . . . . . . . . 13
                                                               
               |
61 | 59, 60 | syl6bi 228 |
. . . . . . . . . . . 12
                                                                 |
62 | 58, 61 | mpd 15 |
. . . . . . . . . . 11
                             |
63 | 51, 62 | syl 16 |
. . . . . . . . . 10
 
                         |
64 | 46, 24, 47, 48, 49 | algrp1 13868 |
. . . . . . . . . . . 12
 
                 |
65 | 64 | fveq2d 5804 |
. . . . . . . . . . 11
 
                         |
66 | 65 | eqeq1d 2456 |
. . . . . . . . . 10
 
                           |
67 | 63, 66 | sylibrd 234 |
. . . . . . . . 9
 
                       |
68 | 45, 67 | syl6 33 |
. . . . . . . 8
 
 
                       |
69 | 68 | a2d 26 |
. . . . . . 7
 
            
              |
70 | 10, 14, 18, 22, 27, 69 | uzind 10845 |
. . . . . 6
 
 
           |
71 | 70 | 3expib 1191 |
. . . . 5
  
              |
72 | 6, 71 | sylbid 215 |
. . . 4
 
    
            |
73 | 5, 72 | syl 16 |
. . 3

    

            |
74 | 73 | com3r 79 |
. 2
 

                |
75 | 4, 74 | mpd 15 |
1
 
               |