Step | Hyp | Ref
| Expression |
1 | | 0exp 12895 |
. . . . . 6
|
2 | 1 | oveq1d 6665 |
. . . . 5
|
3 | 2 | eqeq1d 2624 |
. . . 4
|
4 | | oveq1 6657 |
. . . . . . 7
|
5 | | oveq12 6659 |
. . . . . . 7
|
6 | 4, 5 | sylan 488 |
. . . . . 6
|
7 | 6 | eqeq1d 2624 |
. . . . 5
|
8 | | oveq12 6659 |
. . . . . 6
|
9 | 8 | eqeq1d 2624 |
. . . . 5
|
10 | 7, 9 | bibi12d 335 |
. . . 4
|
11 | 3, 10 | syl5ibrcom 237 |
. . 3
|
12 | 11 | 3ad2ant3 1084 |
. 2
|
13 | | exprmfct 15416 |
. . . . . . 7
|
14 | | simpl1 1064 |
. . . . . . . . . . . . . . . . 17
|
15 | | simpl3 1066 |
. . . . . . . . . . . . . . . . . 18
|
16 | 15 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . 17
|
17 | | zexpcl 12875 |
. . . . . . . . . . . . . . . . 17
|
18 | 14, 16, 17 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
19 | 18 | adantr 481 |
. . . . . . . . . . . . . . 15
|
20 | | simpl2 1065 |
. . . . . . . . . . . . . . . 16
|
21 | 20 | adantr 481 |
. . . . . . . . . . . . . . 15
|
22 | | gcddvds 15225 |
. . . . . . . . . . . . . . 15
|
23 | 19, 21, 22 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
24 | 23 | simpld 475 |
. . . . . . . . . . . . 13
|
25 | | prmz 15389 |
. . . . . . . . . . . . . . 15
|
26 | 25 | adantl 482 |
. . . . . . . . . . . . . 14
|
27 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
28 | 14 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | | expeq0 12890 |
. . . . . . . . . . . . . . . . . . . 20
|
30 | 28, 15, 29 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
31 | 30 | anbi1d 741 |
. . . . . . . . . . . . . . . . . 18
|
32 | 27, 31 | mtbird 315 |
. . . . . . . . . . . . . . . . 17
|
33 | | gcdn0cl 15224 |
. . . . . . . . . . . . . . . . 17
|
34 | 18, 20, 32, 33 | syl21anc 1325 |
. . . . . . . . . . . . . . . 16
|
35 | 34 | nnzd 11481 |
. . . . . . . . . . . . . . 15
|
36 | 35 | adantr 481 |
. . . . . . . . . . . . . 14
|
37 | | dvdstr 15018 |
. . . . . . . . . . . . . 14
|
38 | 26, 36, 19, 37 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
39 | 24, 38 | mpan2d 710 |
. . . . . . . . . . . 12
|
40 | | simpr 477 |
. . . . . . . . . . . . 13
|
41 | | simpll1 1100 |
. . . . . . . . . . . . 13
|
42 | 15 | adantr 481 |
. . . . . . . . . . . . 13
|
43 | | prmdvdsexp 15427 |
. . . . . . . . . . . . 13
|
44 | 40, 41, 42, 43 | syl3anc 1326 |
. . . . . . . . . . . 12
|
45 | 39, 44 | sylibd 229 |
. . . . . . . . . . 11
|
46 | 23 | simprd 479 |
. . . . . . . . . . . 12
|
47 | | dvdstr 15018 |
. . . . . . . . . . . . 13
|
48 | 26, 36, 21, 47 | syl3anc 1326 |
. . . . . . . . . . . 12
|
49 | 46, 48 | mpan2d 710 |
. . . . . . . . . . 11
|
50 | 45, 49 | jcad 555 |
. . . . . . . . . 10
|
51 | | dvdsgcd 15261 |
. . . . . . . . . . 11
|
52 | 26, 41, 21, 51 | syl3anc 1326 |
. . . . . . . . . 10
|
53 | | nprmdvds1 15418 |
. . . . . . . . . . . . 13
|
54 | | breq2 4657 |
. . . . . . . . . . . . . 14
|
55 | 54 | notbid 308 |
. . . . . . . . . . . . 13
|
56 | 53, 55 | syl5ibrcom 237 |
. . . . . . . . . . . 12
|
57 | 56 | necon2ad 2809 |
. . . . . . . . . . 11
|
58 | 57 | adantl 482 |
. . . . . . . . . 10
|
59 | 50, 52, 58 | 3syld 60 |
. . . . . . . . 9
|
60 | 59 | rexlimdva 3031 |
. . . . . . . 8
|
61 | | gcdn0cl 15224 |
. . . . . . . . . 10
|
62 | 61 | 3adantl3 1219 |
. . . . . . . . 9
|
63 | | eluz2b3 11762 |
. . . . . . . . . 10
|
64 | 63 | baib 944 |
. . . . . . . . 9
|
65 | 62, 64 | syl 17 |
. . . . . . . 8
|
66 | 60, 65 | sylibrd 249 |
. . . . . . 7
|
67 | 13, 66 | syl5 34 |
. . . . . 6
|
68 | | exprmfct 15416 |
. . . . . . 7
|
69 | | gcddvds 15225 |
. . . . . . . . . . . . . . 15
|
70 | 41, 21, 69 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
71 | 70 | simpld 475 |
. . . . . . . . . . . . 13
|
72 | | iddvdsexp 15005 |
. . . . . . . . . . . . . 14
|
73 | 41, 42, 72 | syl2anc 693 |
. . . . . . . . . . . . 13
|
74 | 62 | nnzd 11481 |
. . . . . . . . . . . . . . 15
|
75 | 74 | adantr 481 |
. . . . . . . . . . . . . 14
|
76 | | dvdstr 15018 |
. . . . . . . . . . . . . 14
|
77 | 75, 41, 19, 76 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
78 | 71, 73, 77 | mp2and 715 |
. . . . . . . . . . . 12
|
79 | | dvdstr 15018 |
. . . . . . . . . . . . 13
|
80 | 26, 75, 19, 79 | syl3anc 1326 |
. . . . . . . . . . . 12
|
81 | 78, 80 | mpan2d 710 |
. . . . . . . . . . 11
|
82 | 70 | simprd 479 |
. . . . . . . . . . . 12
|
83 | | dvdstr 15018 |
. . . . . . . . . . . . 13
|
84 | 26, 75, 21, 83 | syl3anc 1326 |
. . . . . . . . . . . 12
|
85 | 82, 84 | mpan2d 710 |
. . . . . . . . . . 11
|
86 | 81, 85 | jcad 555 |
. . . . . . . . . 10
|
87 | | dvdsgcd 15261 |
. . . . . . . . . . 11
|
88 | 26, 19, 21, 87 | syl3anc 1326 |
. . . . . . . . . 10
|
89 | | breq2 4657 |
. . . . . . . . . . . . . 14
|
90 | 89 | notbid 308 |
. . . . . . . . . . . . 13
|
91 | 53, 90 | syl5ibrcom 237 |
. . . . . . . . . . . 12
|
92 | 91 | necon2ad 2809 |
. . . . . . . . . . 11
|
93 | 92 | adantl 482 |
. . . . . . . . . 10
|
94 | 86, 88, 93 | 3syld 60 |
. . . . . . . . 9
|
95 | 94 | rexlimdva 3031 |
. . . . . . . 8
|
96 | | eluz2b3 11762 |
. . . . . . . . . 10
|
97 | 96 | baib 944 |
. . . . . . . . 9
|
98 | 34, 97 | syl 17 |
. . . . . . . 8
|
99 | 95, 98 | sylibrd 249 |
. . . . . . 7
|
100 | 68, 99 | syl5 34 |
. . . . . 6
|
101 | 67, 100 | impbid 202 |
. . . . 5
|
102 | 101, 98, 65 | 3bitr3d 298 |
. . . 4
|
103 | 102 | necon4bid 2839 |
. . 3
|
104 | 103 | ex 450 |
. 2
|
105 | 12, 104 | pm2.61d 170 |
1
|