Step | Hyp | Ref
| Expression |
1 | | breq1 3969 |
. . . . . 6
|
2 | 1 | elrab 2868 |
. . . . 5
|
3 | | hashgcdeq 12118 |
. . . . . . 7
♯ ..^
|
4 | 3 | adantrr 471 |
. . . . . 6
♯ ..^ |
5 | | iftrue 3510 |
. . . . . . 7
|
6 | 5 | ad2antll 483 |
. . . . . 6
|
7 | 4, 6 | eqtrd 2190 |
. . . . 5
♯ ..^
|
8 | 2, 7 | sylan2b 285 |
. . . 4
♯ ..^ |
9 | 8 | sumeq2dv 11269 |
. . 3
♯ ..^
|
10 | | 1zzd 9195 |
. . . . . 6
|
11 | | nnz 9187 |
. . . . . 6
|
12 | 10, 11 | fzfigd 10334 |
. . . . 5
|
13 | | dvdsssfz1 11748 |
. . . . 5
|
14 | | elfznn 9957 |
. . . . . . . 8
|
15 | | dvdsdc 11698 |
. . . . . . . 8
DECID |
16 | 14, 11, 15 | syl2anr 288 |
. . . . . . 7
DECID
|
17 | | ibar 299 |
. . . . . . . . . . 11
|
18 | 14, 17 | syl 14 |
. . . . . . . . . 10
|
19 | | breq1 3969 |
. . . . . . . . . . 11
|
20 | 19 | elrab 2868 |
. . . . . . . . . 10
|
21 | 18, 20 | bitr4di 197 |
. . . . . . . . 9
|
22 | 21 | dcbid 824 |
. . . . . . . 8
DECID
DECID
|
23 | 22 | adantl 275 |
. . . . . . 7
DECID
DECID
|
24 | 16, 23 | mpbid 146 |
. . . . . 6
DECID |
25 | 24 | ralrimiva 2530 |
. . . . 5
DECID |
26 | | ssfidc 6880 |
. . . . 5
DECID
|
27 | 12, 13, 25, 26 | syl3anc 1220 |
. . . 4
|
28 | | 0z 9179 |
. . . . . . 7
|
29 | | fzofig 10335 |
. . . . . . 7
..^ |
30 | 28, 11, 29 | sylancr 411 |
. . . . . 6
..^ |
31 | 30 | adantr 274 |
. . . . 5
..^ |
32 | | ssrab2 3213 |
. . . . . 6
..^ ..^ |
33 | 32 | a1i 9 |
. . . . 5
..^ ..^ |
34 | | elfzoelz 10050 |
. . . . . . . . . . 11
..^
|
35 | 34 | adantl 275 |
. . . . . . . . . 10
..^
|
36 | 11 | ad2antrr 480 |
. . . . . . . . . 10
..^
|
37 | 35, 36 | gcdcld 11856 |
. . . . . . . . 9
..^
|
38 | 37 | nn0zd 9285 |
. . . . . . . 8
..^
|
39 | | elrabi 2865 |
. . . . . . . . . 10
|
40 | 39 | ad2antlr 481 |
. . . . . . . . 9
..^
|
41 | 40 | nnzd 9286 |
. . . . . . . 8
..^
|
42 | | zdceq 9240 |
. . . . . . . 8
DECID |
43 | 38, 41, 42 | syl2anc 409 |
. . . . . . 7
..^
DECID |
44 | | ibar 299 |
. . . . . . . . . 10
..^
..^ |
45 | | oveq1 5832 |
. . . . . . . . . . . 12
|
46 | 45 | eqeq1d 2166 |
. . . . . . . . . . 11
|
47 | 46 | elrab 2868 |
. . . . . . . . . 10
..^ ..^ |
48 | 44, 47 | bitr4di 197 |
. . . . . . . . 9
..^
..^ |
49 | 48 | dcbid 824 |
. . . . . . . 8
..^
DECID
DECID ..^ |
50 | 49 | adantl 275 |
. . . . . . 7
..^
DECID
DECID ..^ |
51 | 43, 50 | mpbid 146 |
. . . . . 6
..^
DECID
..^ |
52 | 51 | ralrimiva 2530 |
. . . . 5
..^DECID ..^ |
53 | | ssfidc 6880 |
. . . . 5
..^ ..^ ..^ ..^DECID ..^ ..^ |
54 | 31, 33, 52, 53 | syl3anc 1220 |
. . . 4
..^ |
55 | | oveq1 5832 |
. . . . . . . . . 10
|
56 | 55 | eqeq1d 2166 |
. . . . . . . . 9
|
57 | 56 | elrab 2868 |
. . . . . . . 8
..^ ..^ |
58 | 57 | simprbi 273 |
. . . . . . 7
..^
|
59 | 58 | rgen 2510 |
. . . . . 6
..^ |
60 | 59 | rgenw 2512 |
. . . . 5
..^ |
61 | | invdisj 3960 |
. . . . 5
..^ Disj
..^ |
62 | 60, 61 | mp1i 10 |
. . . 4
Disj
..^ |
63 | 27, 54, 62 | hashiun 11379 |
. . 3
♯ ..^ ♯ ..^ |
64 | | fveq2 5469 |
. . . 4
|
65 | | eqid 2157 |
. . . . 5
|
66 | | eqid 2157 |
. . . . 5
|
67 | 65, 66 | dvdsflip 11747 |
. . . 4
|
68 | | oveq2 5833 |
. . . . 5
|
69 | | simpr 109 |
. . . . 5
|
70 | 11 | adantr 274 |
. . . . . 6
|
71 | 39 | adantl 275 |
. . . . . 6
|
72 | | znq 9534 |
. . . . . 6
|
73 | 70, 71, 72 | syl2anc 409 |
. . . . 5
|
74 | 66, 68, 69, 73 | fvmptd3 5562 |
. . . 4
|
75 | | elrabi 2865 |
. . . . . . 7
|
76 | 75 | adantl 275 |
. . . . . 6
|
77 | 76 | phicld 12097 |
. . . . 5
|
78 | 77 | nncnd 8848 |
. . . 4
|
79 | 64, 27, 67, 74, 78 | fsumf1o 11291 |
. . 3
|
80 | 9, 63, 79 | 3eqtr4rd 2201 |
. 2
♯
..^ |
81 | | iunrab 3897 |
. . . . 5
..^ ..^
|
82 | | breq1 3969 |
. . . . . . . . 9
|
83 | | elfzoelz 10050 |
. . . . . . . . . . 11
..^
|
84 | 83 | adantl 275 |
. . . . . . . . . 10
..^ |
85 | 11 | adantr 274 |
. . . . . . . . . 10
..^
|
86 | | nnne0 8862 |
. . . . . . . . . . . . 13
|
87 | 86 | neneqd 2348 |
. . . . . . . . . . . 12
|
88 | 87 | intnand 917 |
. . . . . . . . . . 11
|
89 | 88 | adantr 274 |
. . . . . . . . . 10
..^ |
90 | | gcdn0cl 11850 |
. . . . . . . . . 10
|
91 | 84, 85, 89, 90 | syl21anc 1219 |
. . . . . . . . 9
..^ |
92 | | gcddvds 11851 |
. . . . . . . . . . 11
|
93 | 84, 85, 92 | syl2anc 409 |
. . . . . . . . . 10
..^
|
94 | 93 | simprd 113 |
. . . . . . . . 9
..^
|
95 | 82, 91, 94 | elrabd 2870 |
. . . . . . . 8
..^ |
96 | | clel5 2849 |
. . . . . . . 8
|
97 | 95, 96 | sylib 121 |
. . . . . . 7
..^
|
98 | 97 | ralrimiva 2530 |
. . . . . 6
..^
|
99 | | rabid2 2633 |
. . . . . 6
..^ ..^
..^
|
100 | 98, 99 | sylibr 133 |
. . . . 5
..^ ..^
|
101 | 81, 100 | eqtr4id 2209 |
. . . 4
..^ ..^ |
102 | 101 | fveq2d 5473 |
. . 3
♯ ..^ ♯..^ |
103 | | nnnn0 9098 |
. . . 4
|
104 | | hashfzo0 10701 |
. . . 4
♯..^ |
105 | 103, 104 | syl 14 |
. . 3
♯..^ |
106 | 102, 105 | eqtrd 2190 |
. 2
♯ ..^ |
107 | 80, 106 | eqtrd 2190 |
1
|