MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eulerthlem2 Unicode version

Theorem eulerthlem2 14312
Description: Lemma for eulerth 14313. (Contributed by Mario Carneiro, 28-Feb-2014.)
Hypotheses
Ref Expression
eulerth.1
eulerth.2
eulerth.3
eulerth.4
eulerth.5
Assertion
Ref Expression
eulerthlem2
Distinct variable groups:   , ,   , ,   , ,   ,N,   ,S   , ,   , ,

Proof of Theorem eulerthlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eulerth.1 . . . . . . . . . . 11
21simp1d 1008 . . . . . . . . . 10
32phicld 14302 . . . . . . . . 9
43nnred 10576 . . . . . . . 8
54leidd 10144 . . . . . . 7
63adantr 465 . . . . . . . 8
7 breq1 4455 . . . . . . . . . . 11
87anbi2d 703 . . . . . . . . . 10
9 oveq2 6304 . . . . . . . . . . . . . 14
10 fveq2 5871 . . . . . . . . . . . . . 14
119, 10oveq12d 6314 . . . . . . . . . . . . 13
1211oveq1d 6311 . . . . . . . . . . . 12
13 fveq2 5871 . . . . . . . . . . . . 13
1413oveq1d 6311 . . . . . . . . . . . 12
1512, 14eqeq12d 2479 . . . . . . . . . . 11
1610oveq2d 6312 . . . . . . . . . . . 12
1716eqeq1d 2459 . . . . . . . . . . 11
1815, 17anbi12d 710 . . . . . . . . . 10
198, 18imbi12d 320 . . . . . . . . 9
20 breq1 4455 . . . . . . . . . . 11
2120anbi2d 703 . . . . . . . . . 10
22 oveq2 6304 . . . . . . . . . . . . . 14
23 fveq2 5871 . . . . . . . . . . . . . 14
2422, 23oveq12d 6314 . . . . . . . . . . . . 13
2524oveq1d 6311 . . . . . . . . . . . 12
26 fveq2 5871 . . . . . . . . . . . . 13
2726oveq1d 6311 . . . . . . . . . . . 12
2825, 27eqeq12d 2479 . . . . . . . . . . 11
2923oveq2d 6312 . . . . . . . . . . . 12
3029eqeq1d 2459 . . . . . . . . . . 11
3128, 30anbi12d 710 . . . . . . . . . 10
3221, 31imbi12d 320 . . . . . . . . 9
33 breq1 4455 . . . . . . . . . . 11
3433anbi2d 703 . . . . . . . . . 10
35 oveq2 6304 . . . . . . . . . . . . . 14
36 fveq2 5871 . . . . . . . . . . . . . 14
3735, 36oveq12d 6314 . . . . . . . . . . . . 13
3837oveq1d 6311 . . . . . . . . . . . 12
39 fveq2 5871 . . . . . . . . . . . . 13
4039oveq1d 6311 . . . . . . . . . . . 12
4138, 40eqeq12d 2479 . . . . . . . . . . 11
4236oveq2d 6312 . . . . . . . . . . . 12
4342eqeq1d 2459 . . . . . . . . . . 11
4441, 43anbi12d 710 . . . . . . . . . 10
4534, 44imbi12d 320 . . . . . . . . 9
46 breq1 4455 . . . . . . . . . . 11
4746anbi2d 703 . . . . . . . . . 10
48 oveq2 6304 . . . . . . . . . . . . . 14
49 fveq2 5871 . . . . . . . . . . . . . 14
5048, 49oveq12d 6314 . . . . . . . . . . . . 13
5150oveq1d 6311 . . . . . . . . . . . 12
52 fveq2 5871 . . . . . . . . . . . . 13
5352oveq1d 6311 . . . . . . . . . . . 12
5451, 53eqeq12d 2479 . . . . . . . . . . 11
5549oveq2d 6312 . . . . . . . . . . . 12
5655eqeq1d 2459 . . . . . . . . . . 11
5754, 56anbi12d 710 . . . . . . . . . 10
5847, 57imbi12d 320 . . . . . . . . 9
591simp2d 1009 . . . . . . . . . . . . . . 15
60 eulerth.4 . . . . . . . . . . . . . . . . . . . 20
61 f1of 5821 . . . . . . . . . . . . . . . . . . . 20
6260, 61syl 16 . . . . . . . . . . . . . . . . . . 19
63 nnuz 11145 . . . . . . . . . . . . . . . . . . . . . 22
643, 63syl6eleq 2555 . . . . . . . . . . . . . . . . . . . . 21
65 eluzfz1 11722 . . . . . . . . . . . . . . . . . . . . 21
6664, 65syl 16 . . . . . . . . . . . . . . . . . . . 20
67 eulerth.3 . . . . . . . . . . . . . . . . . . . 20
6866, 67syl6eleqr 2556 . . . . . . . . . . . . . . . . . . 19
6962, 68ffvelrnd 6032 . . . . . . . . . . . . . . . . . 18
70 oveq1 6303 . . . . . . . . . . . . . . . . . . . 20
7170eqeq1d 2459 . . . . . . . . . . . . . . . . . . 19
72 eulerth.2 . . . . . . . . . . . . . . . . . . 19
7371, 72elrab2 3259 . . . . . . . . . . . . . . . . . 18
7469, 73sylib 196 . . . . . . . . . . . . . . . . 17
7574simpld 459 . . . . . . . . . . . . . . . 16
76 elfzoelz 11829 . . . . . . . . . . . . . . . 16
7775, 76syl 16 . . . . . . . . . . . . . . 15
7859, 77zmulcld 11000 . . . . . . . . . . . . . 14
7978zred 10994 . . . . . . . . . . . . 13
802nnrpd 11284 . . . . . . . . . . . . 13
81 modabs2 12030 . . . . . . . . . . . . 13
8279, 80, 81syl2anc 661 . . . . . . . . . . . 12
83 1z 10919 . . . . . . . . . . . . . 14
84 fveq2 5871 . . . . . . . . . . . . . . . . . 18
8584oveq2d 6312 . . . . . . . . . . . . . . . . 17
8685oveq1d 6311 . . . . . . . . . . . . . . . 16
87 eulerth.5 . . . . . . . . . . . . . . . 16
88 ovex 6324 . . . . . . . . . . . . . . . 16
8986, 87, 88fvmpt 5956 . . . . . . . . . . . . . . 15
9068, 89syl 16 . . . . . . . . . . . . . 14
9183, 90seq1i 12121 . . . . . . . . . . . . 13
9291oveq1d 6311 . . . . . . . . . . . 12
9359zcnd 10995 . . . . . . . . . . . . . . 15
9493exp1d 12305 . . . . . . . . . . . . . 14
95 seq1 12120 . . . . . . . . . . . . . . . 16
9683, 95ax-mp 5 . . . . . . . . . . . . . . 15
9796a1i 11 . . . . . . . . . . . . . 14
9894, 97oveq12d 6314 . . . . . . . . . . . . 13
9998oveq1d 6311 . . . . . . . . . . . 12
10082, 92, 993eqtr4rd 2509 . . . . . . . . . . 11
10196oveq2i 6307 . . . . . . . . . . . 12
1022nnzd 10993 . . . . . . . . . . . . . 14
103 gcdcom 14158 . . . . . . . . . . . . . 14
104102, 77, 103syl2anc 661 . . . . . . . . . . . . 13
10574simprd 463 . . . . . . . . . . . . 13
106104, 105eqtrd 2498 . . . . . . . . . . . 12
107101, 106syl5eq 2510 . . . . . . . . . . 11
108100, 107jca 532 . . . . . . . . . 10
109108adantr 465 . . . . . . . . 9
110 nnre 10568 . . . . . . . . . . . . . . 15
111110adantr 465 . . . . . . . . . . . . . 14
112111lep1d 10502 . . . . . . . . . . . . 13
113 peano2re 9774 . . . . . . . . . . . . . . 15
114111, 113syl 16 . . . . . . . . . . . . . 14
1154adantl 466 . . . . . . . . . . . . . 14
116 letr 9699 . . . . . . . . . . . . . 14
117111, 114, 115, 116syl3anc 1228 . . . . . . . . . . . . 13
118112, 117mpand 675 . . . . . . . . . . . 12
119118imdistanda 693 . . . . . . . . . . 11
120119imim1d 75 . . . . . . . . . 10
12159adantr 465 . . . . . . . . . . . . . . . . . . 19
122 nnnn0 10827 . . . . . . . . . . . . . . . . . . . 20
123122ad2antrl 727 . . . . . . . . . . . . . . . . . . 19
124 zexpcl 12181 . . . . . . . . . . . . . . . . . . 19
125121, 123, 124syl2anc 661 . . . . . . . . . . . . . . . . . 18
126 simprl 756 . . . . . . . . . . . . . . . . . . . 20
127126, 63syl6eleq 2555 . . . . . . . . . . . . . . . . . . 19
128110ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . 25
129128, 113syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
1304adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
131128lep1d 10502 . . . . . . . . . . . . . . . . . . . . . . . . 25
132 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . 25
133128, 129, 130, 131, 132letrd 9760 . . . . . . . . . . . . . . . . . . . . . . . 24
134 nnz 10911 . . . . . . . . . . . . . . . . . . . . . . . . . 26
135134ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . 25
1363nnzd 10993 . . . . . . . . . . . . . . . . . . . . . . . . . 26
137136adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
138 eluz 11123 . . . . . . . . . . . . . . . . . . . . . . . . 25
139135, 137, 138syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24
140133, 139mpbird 232 . . . . . . . . . . . . . . . . . . . . . . 23
141 fzss2 11752 . . . . . . . . . . . . . . . . . . . . . . 23
142140, 141syl 16 . . . . . . . . . . . . . . . . . . . . . 22
143142, 67syl6sseqr 3550 . . . . . . . . . . . . . . . . . . . . 21
144143sselda 3503 . . . . . . . . . . . . . . . . . . . 20
14562ffvelrnda 6031 . . . . . . . . . . . . . . . . . . . . . . . 24
146 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . . . . 26
147146eqeq1d 2459 . . . . . . . . . . . . . . . . . . . . . . . . 25
148147, 72elrab2 3259 . . . . . . . . . . . . . . . . . . . . . . . 24
149145, 148sylib 196 . . . . . . . . . . . . . . . . . . . . . . 23
150149simpld 459 . . . . . . . . . . . . . . . . . . . . . 22
151 elfzoelz 11829 . . . . . . . . . . . . . . . . . . . . . 22
152150, 151syl 16 . . . . . . . . . . . . . . . . . . . . 21
153152adantlr 714 . . . . . . . . . . . . . . . . . . . 20
154144, 153syldan 470 . . . . . . . . . . . . . . . . . . 19
155 zmulcl 10937 . . . . . . . . . . . . . . . . . . . 20
156155adantl 466 . . . . . . . . . . . . . . . . . . 19
157127, 154, 156seqcl 12127 . . . . . . . . . . . . . . . . . 18
158125, 157zmulcld 11000 . . . . . . . . . . . . . . . . 17
159158zred 10994 . . . . . . . . . . . . . . . 16
160 ssrab2 3584 . . . . . . . . . . . . . . . . . . . . . . 23
16172, 160eqsstri 3533 . . . . . . . . . . . . . . . . . . . . . 22
1621, 72, 67, 60, 87eulerthlem1 14311 . . . . . . . . . . . . . . . . . . . . . . 23
163162ffvelrnda 6031 . . . . . . . . . . . . . . . . . . . . . 22
164161, 163sseldi 3501 . . . . . . . . . . . . . . . . . . . . 21
165 elfzoelz 11829 . . . . . . . . . . . . . . . . . . . . 21
166164, 165syl 16 . . . . . . . . . . . . . . . . . . . 20
167166adantlr 714 . . . . . . . . . . . . . . . . . . 19
168144, 167syldan 470 . . . . . . . . . . . . . . . . . 18
169127, 168, 156seqcl 12127 . . . . . . . . . . . . . . . . 17
170169zred 10994 . . . . . . . . . . . . . . . 16
17162adantr 465 . . . . . . . . . . . . . . . . . . . . 21
172 peano2nn 10573 . . . . . . . . . . . . . . . . . . . . . . . . 25
173172ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . 24
174173nnge1d 10603 . . . . . . . . . . . . . . . . . . . . . . 23
175173nnzd 10993 . . . . . . . . . . . . . . . . . . . . . . . 24
176 elfz 11707 . . . . . . . . . . . . . . . . . . . . . . . . 25
17783, 176mp3an2 1312 . . . . . . . . . . . . . . . . . . . . . . . 24
178175, 137, 177syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23
179174, 132, 178mpbir2and 922 . . . . . . . . . . . . . . . . . . . . . 22
180179, 67syl6eleqr 2556 . . . . . . . . . . . . . . . . . . . . 21
181171, 180ffvelrnd 6032 . . . . . . . . . . . . . . . . . . . 20
182 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . 22
183182eqeq1d 2459 . . . . . . . . . . . . . . . . . . . . 21
184183, 72elrab2 3259 . . . . . . . . . . . . . . . . . . . 20
185181, 184sylib 196 . . . . . . . . . . . . . . . . . . 19
186185simpld 459 . . . . . . . . . . . . . . . . . 18
187 elfzoelz 11829 . . . . . . . . . . . . . . . . . 18
188186, 187syl 16 . . . . . . . . . . . . . . . . 17
189121, 188zmulcld 11000 . . . . . . . . . . . . . . . 16
19080adantr 465 . . . . . . . . . . . . . . . 16
191 modmul1 12040 . . . . . . . . . . . . . . . . 17
1921913expia 1198 . . . . . . . . . . . . . . . 16
193159, 170, 189, 190, 192syl22anc 1229 . . . . . . . . . . . . . . 15
194125zcnd 10995 . . . . . . . . . . . . . . . . . . 19
195157zcnd 10995 . . . . . . . . . . . . . . . . . . 19
19693adantr 465 . . . . . . . . . . . . . . . . . . 19
197188zcnd 10995 . . . . . . . . . . . . . . . . . . 19
198194, 195, 196, 197mul4d 9813 . . . . . . . . . . . . . . . . . 18
199196, 123expp1d 12311 . . . . . . . . . . . . . . . . . . 19
200 seqp1 12122 . . . . . . . . . . . . . . . . . . . 20
201127, 200syl 16 . . . . . . . . . . . . . . . . . . 19
202199, 201oveq12d 6314 . . . . . . . . . . . . . . . . . 18
203198, 202eqtr4d 2501 . . . . . . . . . . . . . . . . 17
204203oveq1d 6311 . . . . . . . . . . . . . . . 16
205189zred 10994 . . . . . . . . . . . . . . . . . . 19
206205, 190modcld 12002 . . . . . . . . . . . . . . . . . 18
207 modabs2 12030 . . . . . . . . . . . . . . . . . . 19
208205, 190, 207syl2anc 661 . . . . . . . . . . . . . . . . . 18