Step | Hyp | Ref
| Expression |
1 | | nn0z 9232 |
. . . . . . . . . 10
|
2 | | zq 9585 |
. . . . . . . . . 10
|
3 | 1, 2 | syl 14 |
. . . . . . . . 9
|
4 | 3 | adantl 275 |
. . . . . . . 8
|
5 | | odzcl 12197 |
. . . . . . . . . 10
|
6 | 5 | adantr 274 |
. . . . . . . . 9
|
7 | | nnq 9592 |
. . . . . . . . 9
|
8 | 6, 7 | syl 14 |
. . . . . . . 8
|
9 | 6 | nngt0d 8922 |
. . . . . . . 8
|
10 | | modqlt 10289 |
. . . . . . . 8
|
11 | 4, 8, 9, 10 | syl3anc 1233 |
. . . . . . 7
|
12 | 1 | adantl 275 |
. . . . . . . . . 10
|
13 | 12, 6 | zmodcld 10301 |
. . . . . . . . 9
|
14 | 13 | nn0zd 9332 |
. . . . . . . 8
|
15 | 6 | nnzd 9333 |
. . . . . . . 8
|
16 | | zltnle 9258 |
. . . . . . . 8
|
17 | 14, 15, 16 | syl2anc 409 |
. . . . . . 7
|
18 | 11, 17 | mpbid 146 |
. . . . . 6
|
19 | | 1zzd 9239 |
. . . . . . . . . 10
|
20 | | nnuz 9522 |
. . . . . . . . . . 11
|
21 | 20 | rabeqi 2723 |
. . . . . . . . . 10
|
22 | | oveq2 5861 |
. . . . . . . . . . . . . . 15
|
23 | 22 | oveq1d 5868 |
. . . . . . . . . . . . . 14
|
24 | 23 | breq2d 4001 |
. . . . . . . . . . . . 13
|
25 | 24 | elrab 2886 |
. . . . . . . . . . . 12
|
26 | 25 | biimpri 132 |
. . . . . . . . . . 11
|
27 | 26 | adantl 275 |
. . . . . . . . . 10
|
28 | | simp1 992 |
. . . . . . . . . . . 12
|
29 | 28 | ad3antrrr 489 |
. . . . . . . . . . 11
|
30 | | simp2 993 |
. . . . . . . . . . . . . 14
|
31 | 30 | ad3antrrr 489 |
. . . . . . . . . . . . 13
|
32 | | elfznn 10010 |
. . . . . . . . . . . . . . 15
|
33 | 32 | nnnn0d 9188 |
. . . . . . . . . . . . . 14
|
34 | 33 | adantl 275 |
. . . . . . . . . . . . 13
|
35 | | zexpcl 10491 |
. . . . . . . . . . . . 13
|
36 | 31, 34, 35 | syl2anc 409 |
. . . . . . . . . . . 12
|
37 | | peano2zm 9250 |
. . . . . . . . . . . 12
|
38 | 36, 37 | syl 14 |
. . . . . . . . . . 11
|
39 | | dvdsdc 11760 |
. . . . . . . . . . 11
DECID
|
40 | 29, 38, 39 | syl2anc 409 |
. . . . . . . . . 10
DECID
|
41 | 19, 21, 27, 40 | infssuzledc 11905 |
. . . . . . . . 9
inf
|
42 | 41 | ex 114 |
. . . . . . . 8
inf
|
43 | 42 | ancomsd 267 |
. . . . . . 7
inf
|
44 | | odzval 12195 |
. . . . . . . . 9
inf
|
45 | 44 | adantr 274 |
. . . . . . . 8
inf
|
46 | 45 | breq1d 3999 |
. . . . . . 7
inf
|
47 | 43, 46 | sylibrd 168 |
. . . . . 6
|
48 | 18, 47 | mtod 658 |
. . . . 5
|
49 | | imnan 685 |
. . . . 5
|
50 | 48, 49 | sylibr 133 |
. . . 4
|
51 | | elnn0 9137 |
. . . . . 6
|
52 | 13, 51 | sylib 121 |
. . . . 5
|
53 | 52 | ord 719 |
. . . 4
|
54 | 50, 53 | syld 45 |
. . 3
|
55 | | simpl1 995 |
. . . . . . 7
|
56 | 55 | nnzd 9333 |
. . . . . 6
|
57 | | dvds0 11768 |
. . . . . 6
|
58 | 56, 57 | syl 14 |
. . . . 5
|
59 | | simpl2 996 |
. . . . . . . . 9
|
60 | 59 | zcnd 9335 |
. . . . . . . 8
|
61 | 60 | exp0d 10603 |
. . . . . . 7
|
62 | 61 | oveq1d 5868 |
. . . . . 6
|
63 | | 1m1e0 8947 |
. . . . . 6
|
64 | 62, 63 | eqtrdi 2219 |
. . . . 5
|
65 | 58, 64 | breqtrrd 4017 |
. . . 4
|
66 | | oveq2 5861 |
. . . . . 6
|
67 | 66 | oveq1d 5868 |
. . . . 5
|
68 | 67 | breq2d 4001 |
. . . 4
|
69 | 65, 68 | syl5ibrcom 156 |
. . 3
|
70 | 54, 69 | impbid 128 |
. 2
|
71 | 6 | nnnn0d 9188 |
. . . . . . . . 9
|
72 | | znq 9583 |
. . . . . . . . . . 11
|
73 | 12, 6, 72 | syl2anc 409 |
. . . . . . . . . 10
|
74 | | nn0ge0 9160 |
. . . . . . . . . . . 12
|
75 | 74 | adantl 275 |
. . . . . . . . . . 11
|
76 | | nn0re 9144 |
. . . . . . . . . . . . 13
|
77 | 76 | adantl 275 |
. . . . . . . . . . . 12
|
78 | 6 | nnred 8891 |
. . . . . . . . . . . 12
|
79 | | ge0div 8787 |
. . . . . . . . . . . 12
|
80 | 77, 78, 9, 79 | syl3anc 1233 |
. . . . . . . . . . 11
|
81 | 75, 80 | mpbid 146 |
. . . . . . . . . 10
|
82 | | flqge0nn0 10249 |
. . . . . . . . . 10
|
83 | 73, 81, 82 | syl2anc 409 |
. . . . . . . . 9
|
84 | 71, 83 | nn0mulcld 9193 |
. . . . . . . 8
|
85 | | zexpcl 10491 |
. . . . . . . 8
|
86 | 59, 84, 85 | syl2anc 409 |
. . . . . . 7
|
87 | | zq 9585 |
. . . . . . 7
|
88 | 86, 87 | syl 14 |
. . . . . 6
|
89 | | 1z 9238 |
. . . . . . 7
|
90 | | zq 9585 |
. . . . . . 7
|
91 | 89, 90 | mp1i 10 |
. . . . . 6
|
92 | | zexpcl 10491 |
. . . . . . 7
|
93 | 59, 13, 92 | syl2anc 409 |
. . . . . 6
|
94 | | nnq 9592 |
. . . . . . 7
|
95 | 55, 94 | syl 14 |
. . . . . 6
|
96 | 55 | nngt0d 8922 |
. . . . . 6
|
97 | 60, 83, 71 | expmuld 10612 |
. . . . . . . 8
|
98 | 97 | oveq1d 5868 |
. . . . . . 7
|
99 | | zexpcl 10491 |
. . . . . . . . 9
|
100 | 59, 71, 99 | syl2anc 409 |
. . . . . . . 8
|
101 | | 1zzd 9239 |
. . . . . . . 8
|
102 | | odzid 12198 |
. . . . . . . . . 10
|
103 | 102 | adantr 274 |
. . . . . . . . 9
|
104 | | moddvds 11761 |
. . . . . . . . . 10
|
105 | 55, 100, 101, 104 | syl3anc 1233 |
. . . . . . . . 9
|
106 | 103, 105 | mpbird 166 |
. . . . . . . 8
|
107 | 100, 101,
83, 95, 96, 106 | modqexp 10602 |
. . . . . . 7
|
108 | 73 | flqcld 10233 |
. . . . . . . . 9
|
109 | | 1exp 10505 |
. . . . . . . . 9
|
110 | 108, 109 | syl 14 |
. . . . . . . 8
|
111 | 110 | oveq1d 5868 |
. . . . . . 7
|
112 | 98, 107, 111 | 3eqtrd 2207 |
. . . . . 6
|
113 | 88, 91, 93, 95, 96, 112 | modqmul1 10333 |
. . . . 5
|
114 | 60, 13, 84 | expaddd 10611 |
. . . . . . 7
|
115 | | modqval 10280 |
. . . . . . . . . . 11
|
116 | 4, 8, 9, 115 | syl3anc 1233 |
. . . . . . . . . 10
|
117 | 116 | oveq2d 5869 |
. . . . . . . . 9
|
118 | 84 | nn0cnd 9190 |
. . . . . . . . . 10
|
119 | 77 | recnd 7948 |
. . . . . . . . . 10
|
120 | 118, 119 | pncan3d 8233 |
. . . . . . . . 9
|
121 | 117, 120 | eqtrd 2203 |
. . . . . . . 8
|
122 | 121 | oveq2d 5869 |
. . . . . . 7
|
123 | 114, 122 | eqtr3d 2205 |
. . . . . 6
|
124 | 123 | oveq1d 5868 |
. . . . 5
|
125 | 93 | zcnd 9335 |
. . . . . . 7
|
126 | 125 | mulid2d 7938 |
. . . . . 6
|
127 | 126 | oveq1d 5868 |
. . . . 5
|
128 | 113, 124,
127 | 3eqtr3d 2211 |
. . . 4
|
129 | 128 | eqeq1d 2179 |
. . 3
|
130 | | zexpcl 10491 |
. . . . 5
|
131 | 59, 130 | sylancom 418 |
. . . 4
|
132 | | moddvds 11761 |
. . . 4
|
133 | 55, 131, 101, 132 | syl3anc 1233 |
. . 3
|
134 | | moddvds 11761 |
. . . 4
|
135 | 55, 93, 101, 134 | syl3anc 1233 |
. . 3
|
136 | 129, 133,
135 | 3bitr3d 217 |
. 2
|
137 | | dvdsval3 11753 |
. . 3
|
138 | 6, 12, 137 | syl2anc 409 |
. 2
|
139 | 70, 136, 138 | 3bitr4d 219 |
1
|