Step | Hyp | Ref
| Expression |
1 | | algcvga.5 |
. . 3
|
2 | | algcvga.3 |
. . . 4
|
3 | 2 | ffvelrni 5322 |
. . 3
|
4 | 1, 3 | syl5eqel 2165 |
. 2
|
5 | | nn0z 8371 |
. . . 4
|
6 | | eluz1 8623 |
. . . . 5
|
7 | | fveq2 5198 |
. . . . . . . . . 10
|
8 | 7 | fveq2d 5202 |
. . . . . . . . 9
|
9 | 8 | eqeq1d 2089 |
. . . . . . . 8
|
10 | 9 | imbi2d 228 |
. . . . . . 7
|
11 | | fveq2 5198 |
. . . . . . . . . 10
|
12 | 11 | fveq2d 5202 |
. . . . . . . . 9
|
13 | 12 | eqeq1d 2089 |
. . . . . . . 8
|
14 | 13 | imbi2d 228 |
. . . . . . 7
|
15 | | fveq2 5198 |
. . . . . . . . . 10
|
16 | 15 | fveq2d 5202 |
. . . . . . . . 9
|
17 | 16 | eqeq1d 2089 |
. . . . . . . 8
|
18 | 17 | imbi2d 228 |
. . . . . . 7
|
19 | | fveq2 5198 |
. . . . . . . . . 10
|
20 | 19 | fveq2d 5202 |
. . . . . . . . 9
|
21 | 20 | eqeq1d 2089 |
. . . . . . . 8
|
22 | 21 | imbi2d 228 |
. . . . . . 7
|
23 | | algcvga.1 |
. . . . . . . . 9
|
24 | | algcvga.2 |
. . . . . . . . 9
|
25 | | algcvga.4 |
. . . . . . . . 9
|
26 | | ialgcvga.s |
. . . . . . . . 9
|
27 | 23, 24, 2, 25, 1, 26 | ialgcvg 10430 |
. . . . . . . 8
|
28 | 27 | a1i 9 |
. . . . . . 7
|
29 | | nn0ge0 8313 |
. . . . . . . . . . . . . . . . 17
|
30 | 29 | adantr 270 |
. . . . . . . . . . . . . . . 16
|
31 | | nn0re 8297 |
. . . . . . . . . . . . . . . . 17
|
32 | | zre 8355 |
. . . . . . . . . . . . . . . . 17
|
33 | | 0re 7119 |
. . . . . . . . . . . . . . . . . 18
|
34 | | letr 7194 |
. . . . . . . . . . . . . . . . . 18
|
35 | 33, 34 | mp3an1 1255 |
. . . . . . . . . . . . . . . . 17
|
36 | 31, 32, 35 | syl2an 283 |
. . . . . . . . . . . . . . . 16
|
37 | 30, 36 | mpand 419 |
. . . . . . . . . . . . . . 15
|
38 | | elnn0z 8364 |
. . . . . . . . . . . . . . . . 17
|
39 | 38 | simplbi2 377 |
. . . . . . . . . . . . . . . 16
|
40 | 39 | adantl 271 |
. . . . . . . . . . . . . . 15
|
41 | 37, 40 | syld 44 |
. . . . . . . . . . . . . 14
|
42 | 4, 41 | sylan 277 |
. . . . . . . . . . . . 13
|
43 | 42 | impr 371 |
. . . . . . . . . . . 12
|
44 | 43 | expcom 114 |
. . . . . . . . . . 11
|
45 | 44 | 3adant1 956 |
. . . . . . . . . 10
|
46 | 45 | ancld 318 |
. . . . . . . . 9
|
47 | | nn0uz 8653 |
. . . . . . . . . . . . 13
|
48 | | 0zd 8363 |
. . . . . . . . . . . . 13
|
49 | | id 19 |
. . . . . . . . . . . . 13
|
50 | 23 | a1i 9 |
. . . . . . . . . . . . 13
|
51 | 26 | a1i 9 |
. . . . . . . . . . . . 13
|
52 | 47, 24, 48, 49, 50, 51 | ialgrf 10427 |
. . . . . . . . . . . 12
|
53 | 52 | ffvelrnda 5323 |
. . . . . . . . . . 11
|
54 | | fveq2 5198 |
. . . . . . . . . . . . . . . 16
|
55 | 54 | fveq2d 5202 |
. . . . . . . . . . . . . . 15
|
56 | 55 | neeq1d 2263 |
. . . . . . . . . . . . . 14
|
57 | | fveq2 5198 |
. . . . . . . . . . . . . . 15
|
58 | 55, 57 | breq12d 3798 |
. . . . . . . . . . . . . 14
|
59 | 56, 58 | imbi12d 232 |
. . . . . . . . . . . . 13
|
60 | 59, 25 | vtoclga 2664 |
. . . . . . . . . . . 12
|
61 | 23, 2 | algcvgb 10432 |
. . . . . . . . . . . . 13
|
62 | | simpr 108 |
. . . . . . . . . . . . 13
|
63 | 61, 62 | syl6bi 161 |
. . . . . . . . . . . 12
|
64 | 60, 63 | mpd 13 |
. . . . . . . . . . 11
|
65 | 53, 64 | syl 14 |
. . . . . . . . . 10
|
66 | 47, 24, 48, 49, 50, 51 | ialgrp1 10428 |
. . . . . . . . . . . 12
|
67 | 66 | fveq2d 5202 |
. . . . . . . . . . 11
|
68 | 67 | eqeq1d 2089 |
. . . . . . . . . 10
|
69 | 65, 68 | sylibrd 167 |
. . . . . . . . 9
|
70 | 46, 69 | syl6 33 |
. . . . . . . 8
|
71 | 70 | a2d 26 |
. . . . . . 7
|
72 | 10, 14, 18, 22, 28, 71 | uzind 8458 |
. . . . . 6
|
73 | 72 | 3expib 1141 |
. . . . 5
|
74 | 6, 73 | sylbid 148 |
. . . 4
|
75 | 5, 74 | syl 14 |
. . 3
|
76 | 75 | com3r 78 |
. 2
|
77 | 4, 76 | mpd 13 |
1
|