Step | Hyp | Ref
| Expression |
1 | | fzfid 12772 |
. . . . 5
|
2 | | odf1.1 |
. . . . . . . . . . . . 13
|
3 | | odf1.3 |
. . . . . . . . . . . . 13
.g |
4 | 2, 3 | mulgcl 17559 |
. . . . . . . . . . . 12
|
5 | 4 | 3expa 1265 |
. . . . . . . . . . 11
|
6 | 5 | an32s 846 |
. . . . . . . . . 10
|
7 | 6 | adantlr 751 |
. . . . . . . . 9
|
8 | | odf1.4 |
. . . . . . . . 9
|
9 | 7, 8 | fmptd 6385 |
. . . . . . . 8
|
10 | | frn 6053 |
. . . . . . . 8
|
11 | | fvex 6201 |
. . . . . . . . . 10
|
12 | 2, 11 | eqeltri 2697 |
. . . . . . . . 9
|
13 | 12 | ssex 4802 |
. . . . . . . 8
|
14 | 9, 10, 13 | 3syl 18 |
. . . . . . 7
|
15 | | elfzelz 12342 |
. . . . . . . . . . 11
|
16 | 15 | adantl 482 |
. . . . . . . . . 10
|
17 | | ovex 6678 |
. . . . . . . . . 10
|
18 | | oveq1 6657 |
. . . . . . . . . . 11
|
19 | 8, 18 | elrnmpt1s 5373 |
. . . . . . . . . 10
|
20 | 16, 17, 19 | sylancl 694 |
. . . . . . . . 9
|
21 | 20 | ralrimiva 2966 |
. . . . . . . 8
|
22 | | zmodfz 12692 |
. . . . . . . . . . . . 13
|
23 | 22 | ancoms 469 |
. . . . . . . . . . . 12
|
24 | 23 | adantll 750 |
. . . . . . . . . . 11
|
25 | | simpllr 799 |
. . . . . . . . . . . . . 14
|
26 | | simplr 792 |
. . . . . . . . . . . . . 14
|
27 | 15 | adantl 482 |
. . . . . . . . . . . . . 14
|
28 | | moddvds 14991 |
. . . . . . . . . . . . . 14
|
29 | 25, 26, 27, 28 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
30 | 27 | zred 11482 |
. . . . . . . . . . . . . . . 16
|
31 | 25 | nnrpd 11870 |
. . . . . . . . . . . . . . . 16
|
32 | | 0z 11388 |
. . . . . . . . . . . . . . . . . . 19
|
33 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | 33 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
35 | 34 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
36 | | elfzm11 12411 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 32, 35, 36 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
|
38 | 37 | biimpa 501 |
. . . . . . . . . . . . . . . . 17
|
39 | 38 | simp2d 1074 |
. . . . . . . . . . . . . . . 16
|
40 | 38 | simp3d 1075 |
. . . . . . . . . . . . . . . 16
|
41 | | modid 12695 |
. . . . . . . . . . . . . . . 16
|
42 | 30, 31, 39, 40, 41 | syl22anc 1327 |
. . . . . . . . . . . . . . 15
|
43 | 42 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
|
44 | | eqcom 2629 |
. . . . . . . . . . . . . 14
|
45 | 43, 44 | syl6bb 276 |
. . . . . . . . . . . . 13
|
46 | | simp-4l 806 |
. . . . . . . . . . . . . 14
|
47 | | simp-4r 807 |
. . . . . . . . . . . . . 14
|
48 | | odf1.2 |
. . . . . . . . . . . . . . 15
|
49 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
50 | 2, 48, 3, 49 | odcong 17968 |
. . . . . . . . . . . . . 14
|
51 | 46, 47, 26, 27, 50 | syl112anc 1330 |
. . . . . . . . . . . . 13
|
52 | 29, 45, 51 | 3bitr3rd 299 |
. . . . . . . . . . . 12
|
53 | 52 | ralrimiva 2966 |
. . . . . . . . . . 11
|
54 | | reu6i 3397 |
. . . . . . . . . . 11
|
55 | 24, 53, 54 | syl2anc 693 |
. . . . . . . . . 10
|
56 | 55 | ralrimiva 2966 |
. . . . . . . . 9
|
57 | | ovex 6678 |
. . . . . . . . . . 11
|
58 | 57 | rgenw 2924 |
. . . . . . . . . 10
|
59 | | eqeq1 2626 |
. . . . . . . . . . . 12
|
60 | 59 | reubidv 3126 |
. . . . . . . . . . 11
|
61 | 8, 60 | ralrnmpt 6368 |
. . . . . . . . . 10
|
62 | 58, 61 | ax-mp 5 |
. . . . . . . . 9
|
63 | 56, 62 | sylibr 224 |
. . . . . . . 8
|
64 | | eqid 2622 |
. . . . . . . . 9
|
65 | 64 | f1ompt 6382 |
. . . . . . . 8
|
66 | 21, 63, 65 | sylanbrc 698 |
. . . . . . 7
|
67 | | f1oen2g 7972 |
. . . . . . 7
|
68 | 1, 14, 66, 67 | syl3anc 1326 |
. . . . . 6
|
69 | | enfi 8176 |
. . . . . 6
|
70 | 68, 69 | syl 17 |
. . . . 5
|
71 | 1, 70 | mpbid 222 |
. . . 4
|
72 | 71 | iftrued 4094 |
. . 3
|
73 | | fz01en 12369 |
. . . . . 6
|
74 | | ensym 8005 |
. . . . . 6
|
75 | 34, 73, 74 | 3syl 18 |
. . . . 5
|
76 | | entr 8008 |
. . . . 5
|
77 | 75, 68, 76 | syl2anc 693 |
. . . 4
|
78 | | fzfid 12772 |
. . . . 5
|
79 | | hashen 13135 |
. . . . 5
|
80 | 78, 71, 79 | syl2anc 693 |
. . . 4
|
81 | 77, 80 | mpbird 247 |
. . 3
|
82 | | nnnn0 11299 |
. . . . 5
|
83 | 82 | adantl 482 |
. . . 4
|
84 | | hashfz1 13134 |
. . . 4
|
85 | 83, 84 | syl 17 |
. . 3
|
86 | 72, 81, 85 | 3eqtr2rd 2663 |
. 2
|
87 | | simp3 1063 |
. . . 4
|
88 | 2, 48, 3, 8 | odinf 17980 |
. . . . 5
|
89 | 88 | iffalsed 4097 |
. . . 4
|
90 | 87, 89 | eqtr4d 2659 |
. . 3
|
91 | 90 | 3expa 1265 |
. 2
|
92 | 2, 48 | odcl 17955 |
. . . 4
|
93 | 92 | adantl 482 |
. . 3
|
94 | | elnn0 11294 |
. . 3
|
95 | 93, 94 | sylib 208 |
. 2
|
96 | 86, 91, 95 | mpjaodan 827 |
1
|