Step | Hyp | Ref
| Expression |
1 | | eulerth.4 |
. . . 4
|
2 | | f1ocnv 5445 |
. . . 4
|
3 | 1, 2 | syl 14 |
. . 3
|
4 | | eulerth.1 |
. . . . . . 7
|
5 | | eulerth.2 |
. . . . . . 7
..^ |
6 | | eqid 2165 |
. . . . . . 7
|
7 | | fveq2 5486 |
. . . . . . . . . 10
|
8 | 7 | oveq2d 5858 |
. . . . . . . . 9
|
9 | 8 | oveq1d 5857 |
. . . . . . . 8
|
10 | 9 | cbvmptv 4078 |
. . . . . . 7
|
11 | 4, 5, 6, 1, 10 | eulerthlem1 12159 |
. . . . . 6
|
12 | | fveq2 5486 |
. . . . . . . . . 10
|
13 | 12 | oveq2d 5858 |
. . . . . . . . 9
|
14 | 13 | oveq1d 5857 |
. . . . . . . 8
|
15 | 14 | cbvmptv 4078 |
. . . . . . 7
|
16 | 15 | feq1i 5330 |
. . . . . 6
|
17 | 11, 16 | sylib 121 |
. . . . 5
|
18 | 4 | simp1d 999 |
. . . . . . . . . 10
|
19 | 18 | adantr 274 |
. . . . . . . . 9
|
20 | 4 | simp2d 1000 |
. . . . . . . . . . 11
|
21 | 20 | adantr 274 |
. . . . . . . . . 10
|
22 | | ssrab2 3227 |
. . . . . . . . . . . . 13
..^ ..^ |
23 | 5, 22 | eqsstri 3174 |
. . . . . . . . . . . 12
..^ |
24 | | fzo0ssnn0 10150 |
. . . . . . . . . . . . 13
..^ |
25 | | nn0ssz 9209 |
. . . . . . . . . . . . 13
|
26 | 24, 25 | sstri 3151 |
. . . . . . . . . . . 12
..^ |
27 | 23, 26 | sstri 3151 |
. . . . . . . . . . 11
|
28 | | f1of 5432 |
. . . . . . . . . . . . . 14
|
29 | 1, 28 | syl 14 |
. . . . . . . . . . . . 13
|
30 | 29 | adantr 274 |
. . . . . . . . . . . 12
|
31 | | simprl 521 |
. . . . . . . . . . . 12
|
32 | 30, 31 | ffvelrnd 5621 |
. . . . . . . . . . 11
|
33 | 27, 32 | sselid 3140 |
. . . . . . . . . 10
|
34 | 21, 33 | zmulcld 9319 |
. . . . . . . . 9
|
35 | 29 | ffvelrnda 5620 |
. . . . . . . . . . . 12
|
36 | 35 | adantrl 470 |
. . . . . . . . . . 11
|
37 | 27, 36 | sselid 3140 |
. . . . . . . . . 10
|
38 | 21, 37 | zmulcld 9319 |
. . . . . . . . 9
|
39 | | moddvds 11739 |
. . . . . . . . 9
|
40 | 19, 34, 38, 39 | syl3anc 1228 |
. . . . . . . 8
|
41 | | eqid 2165 |
. . . . . . . . . 10
|
42 | | fveq2 5486 |
. . . . . . . . . . . 12
|
43 | 42 | oveq2d 5858 |
. . . . . . . . . . 11
|
44 | 43 | oveq1d 5857 |
. . . . . . . . . 10
|
45 | | zmodfzo 10282 |
. . . . . . . . . . 11
..^ |
46 | 34, 19, 45 | syl2anc 409 |
. . . . . . . . . 10
..^ |
47 | 41, 44, 31, 46 | fvmptd3 5579 |
. . . . . . . . 9
|
48 | | fveq2 5486 |
. . . . . . . . . . . 12
|
49 | 48 | oveq2d 5858 |
. . . . . . . . . . 11
|
50 | 49 | oveq1d 5857 |
. . . . . . . . . 10
|
51 | | simprr 522 |
. . . . . . . . . 10
|
52 | | zmodfzo 10282 |
. . . . . . . . . . 11
..^ |
53 | 38, 19, 52 | syl2anc 409 |
. . . . . . . . . 10
..^ |
54 | 41, 50, 51, 53 | fvmptd3 5579 |
. . . . . . . . 9
|
55 | 47, 54 | eqeq12d 2180 |
. . . . . . . 8
|
56 | 21 | zcnd 9314 |
. . . . . . . . . 10
|
57 | 33 | zcnd 9314 |
. . . . . . . . . 10
|
58 | 37 | zcnd 9314 |
. . . . . . . . . 10
|
59 | 56, 57, 58 | subdid 8312 |
. . . . . . . . 9
|
60 | 59 | breq2d 3994 |
. . . . . . . 8
|
61 | 40, 55, 60 | 3bitr4d 219 |
. . . . . . 7
|
62 | 18 | nnzd 9312 |
. . . . . . . . . . 11
|
63 | 62, 20 | gcdcomd 11907 |
. . . . . . . . . 10
|
64 | 4 | simp3d 1001 |
. . . . . . . . . 10
|
65 | 63, 64 | eqtrd 2198 |
. . . . . . . . 9
|
66 | 65 | adantr 274 |
. . . . . . . 8
|
67 | 62 | adantr 274 |
. . . . . . . . . 10
|
68 | 33, 37 | zsubcld 9318 |
. . . . . . . . . 10
|
69 | | coprmdvds 12024 |
. . . . . . . . . 10
|
70 | 67, 21, 68, 69 | syl3anc 1228 |
. . . . . . . . 9
|
71 | | zq 9564 |
. . . . . . . . . . . . 13
|
72 | 33, 71 | syl 14 |
. . . . . . . . . . . 12
|
73 | | zq 9564 |
. . . . . . . . . . . . . 14
|
74 | 62, 73 | syl 14 |
. . . . . . . . . . . . 13
|
75 | 74 | adantr 274 |
. . . . . . . . . . . 12
|
76 | 23, 32 | sselid 3140 |
. . . . . . . . . . . . 13
..^ |
77 | | elfzole1 10090 |
. . . . . . . . . . . . 13
..^
|
78 | 76, 77 | syl 14 |
. . . . . . . . . . . 12
|
79 | | elfzolt2 10091 |
. . . . . . . . . . . . 13
..^
|
80 | 76, 79 | syl 14 |
. . . . . . . . . . . 12
|
81 | | modqid 10284 |
. . . . . . . . . . . 12
|
82 | 72, 75, 78, 80, 81 | syl22anc 1229 |
. . . . . . . . . . 11
|
83 | 27, 35 | sselid 3140 |
. . . . . . . . . . . . . 14
|
84 | 83 | adantrl 470 |
. . . . . . . . . . . . 13
|
85 | | zq 9564 |
. . . . . . . . . . . . 13
|
86 | 84, 85 | syl 14 |
. . . . . . . . . . . 12
|
87 | 23, 35 | sselid 3140 |
. . . . . . . . . . . . . 14
..^ |
88 | | elfzole1 10090 |
. . . . . . . . . . . . . 14
..^
|
89 | 87, 88 | syl 14 |
. . . . . . . . . . . . 13
|
90 | 89 | adantrl 470 |
. . . . . . . . . . . 12
|
91 | 87 | adantrl 470 |
. . . . . . . . . . . . 13
..^ |
92 | | elfzolt2 10091 |
. . . . . . . . . . . . 13
..^
|
93 | 91, 92 | syl 14 |
. . . . . . . . . . . 12
|
94 | | modqid 10284 |
. . . . . . . . . . . 12
|
95 | 86, 75, 90, 93, 94 | syl22anc 1229 |
. . . . . . . . . . 11
|
96 | 82, 95 | eqeq12d 2180 |
. . . . . . . . . 10
|
97 | | moddvds 11739 |
. . . . . . . . . . 11
|
98 | 19, 33, 37, 97 | syl3anc 1228 |
. . . . . . . . . 10
|
99 | | f1of1 5431 |
. . . . . . . . . . . 12
|
100 | 1, 99 | syl 14 |
. . . . . . . . . . 11
|
101 | | f1fveq 5740 |
. . . . . . . . . . 11
|
102 | 100, 101 | sylan 281 |
. . . . . . . . . 10
|
103 | 96, 98, 102 | 3bitr3d 217 |
. . . . . . . . 9
|
104 | 70, 103 | sylibd 148 |
. . . . . . . 8
|
105 | 66, 104 | mpan2d 425 |
. . . . . . 7
|
106 | 61, 105 | sylbid 149 |
. . . . . 6
|
107 | 106 | ralrimivva 2548 |
. . . . 5
|
108 | | dff13 5736 |
. . . . 5
|
109 | 17, 107, 108 | sylanbrc 414 |
. . . 4
|
110 | | 1zzd 9218 |
. . . . . . 7
|
111 | 18 | phicld 12150 |
. . . . . . . 8
|
112 | 111 | nnzd 9312 |
. . . . . . 7
|
113 | 110, 112 | fzfigd 10366 |
. . . . . 6
|
114 | | f1oeng 6723 |
. . . . . 6
|
115 | 113, 1, 114 | syl2anc 409 |
. . . . 5
|
116 | 4, 5 | eulerthlemfi 12160 |
. . . . 5
|
117 | | f1finf1o 6912 |
. . . . 5
|
118 | 115, 116,
117 | syl2anc 409 |
. . . 4
|
119 | 109, 118 | mpbid 146 |
. . 3
|
120 | | f1oco 5455 |
. . 3
|
121 | 3, 119, 120 | syl2anc 409 |
. 2
|
122 | | eulerth.h |
. . 3
|
123 | | f1oeq1 5421 |
. . 3
|
124 | 122, 123 | ax-mp 5 |
. 2
|
125 | 121, 124 | sylibr 133 |
1
|