Step | Hyp | Ref
| Expression |
1 | | zcn 11382 |
. . . . . . . . . 10
|
2 | 1 | mul01d 10235 |
. . . . . . . . 9
|
3 | 2 | 3ad2ant1 1082 |
. . . . . . . 8
|
4 | | zcn 11382 |
. . . . . . . . . 10
|
5 | 4 | mul01d 10235 |
. . . . . . . . 9
|
6 | 5 | 3ad2ant2 1083 |
. . . . . . . 8
|
7 | 3, 6 | eqtr4d 2659 |
. . . . . . 7
|
8 | 7 | adantr 481 |
. . . . . 6
|
9 | 8 | oveq1d 6665 |
. . . . 5
|
10 | 9 | adantr 481 |
. . . 4
|
11 | | oveq2 6658 |
. . . . . 6
|
12 | 11 | oveq1d 6665 |
. . . . 5
|
13 | | oveq2 6658 |
. . . . . 6
|
14 | 13 | oveq1d 6665 |
. . . . 5
|
15 | 12, 14 | eqeq12d 2637 |
. . . 4
|
16 | 10, 15 | syl5ibr 236 |
. . 3
|
17 | | oveq2 6658 |
. . . . . . . . . 10
|
18 | | oveq2 6658 |
. . . . . . . . . 10
|
19 | 17, 18 | eqeq12d 2637 |
. . . . . . . . 9
|
20 | 19 | adantl 482 |
. . . . . . . 8
|
21 | 20 | adantl 482 |
. . . . . . 7
|
22 | | simpl 473 |
. . . . . . . . 9
|
23 | | simp3 1063 |
. . . . . . . . 9
|
24 | | divgcdnnr 15237 |
. . . . . . . . 9
|
25 | 22, 23, 24 | syl2anr 495 |
. . . . . . . 8
|
26 | | simpl1 1064 |
. . . . . . . 8
|
27 | | simpl2 1065 |
. . . . . . . 8
|
28 | | moddvds 14991 |
. . . . . . . 8
|
29 | 25, 26, 27, 28 | syl3anc 1326 |
. . . . . . 7
|
30 | 25 | nnzd 11481 |
. . . . . . . . 9
|
31 | | zsubcl 11419 |
. . . . . . . . . . 11
|
32 | 31 | 3adant3 1081 |
. . . . . . . . . 10
|
33 | 32 | adantr 481 |
. . . . . . . . 9
|
34 | 30, 33 | jca 554 |
. . . . . . . 8
|
35 | | divides 14985 |
. . . . . . . 8
|
36 | 34, 35 | syl 17 |
. . . . . . 7
|
37 | 21, 29, 36 | 3bitrd 294 |
. . . . . 6
|
38 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
39 | 30 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
40 | 39 | adantr 481 |
. . . . . . . . . . . . . . 15
|
41 | 38, 40 | zmulcld 11488 |
. . . . . . . . . . . . . 14
|
42 | 41 | zcnd 11483 |
. . . . . . . . . . . . 13
|
43 | 31 | zcnd 11483 |
. . . . . . . . . . . . . . 15
|
44 | 43 | 3adant3 1081 |
. . . . . . . . . . . . . 14
|
45 | 44 | ad3antrrr 766 |
. . . . . . . . . . . . 13
|
46 | 23 | zcnd 11483 |
. . . . . . . . . . . . . 14
|
47 | 46 | ad3antrrr 766 |
. . . . . . . . . . . . 13
|
48 | | simpr 477 |
. . . . . . . . . . . . . 14
|
49 | 48 | adantr 481 |
. . . . . . . . . . . . 13
|
50 | 42, 45, 47, 49 | mulcan2d 10661 |
. . . . . . . . . . . 12
|
51 | | zcn 11382 |
. . . . . . . . . . . . . . 15
|
52 | | subdir 10464 |
. . . . . . . . . . . . . . 15
|
53 | 1, 4, 51, 52 | syl3an 1368 |
. . . . . . . . . . . . . 14
|
54 | 53 | ad3antrrr 766 |
. . . . . . . . . . . . 13
|
55 | 54 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
56 | 50, 55 | bitr3d 270 |
. . . . . . . . . . 11
|
57 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . 20
|
58 | 57 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
59 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
60 | 59 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . 22
|
61 | 60 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
62 | 46 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
63 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
64 | 63 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
65 | 23, 64 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
66 | | gcdcl 15228 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
68 | 67 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . 21
|
69 | | nnne0 11053 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
70 | 69 | neneqd 2799 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
72 | 71 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
73 | 72 | intnand 962 |
. . . . . . . . . . . . . . . . . . . . . 22
|
74 | | gcdeq0 15238 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
75 | 65, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
76 | 75 | necon3abid 2830 |
. . . . . . . . . . . . . . . . . . . . . 22
|
77 | 73, 76 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . 21
|
78 | 61, 62, 68, 77 | divassd 10836 |
. . . . . . . . . . . . . . . . . . . 20
|
79 | 59 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
80 | 57, 69 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
81 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
82 | 23, 81 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
83 | | 3anass 1042 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
84 | 82, 83 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . 22
|
85 | | divgcdz 15233 |
. . . . . . . . . . . . . . . . . . . . . 22
|
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
87 | 79, 86 | zmulcld 11488 |
. . . . . . . . . . . . . . . . . . . 20
|
88 | 78, 87 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . 19
|
89 | | dvdsmul1 15003 |
. . . . . . . . . . . . . . . . . . 19
|
90 | 58, 88, 89 | syl2an2 875 |
. . . . . . . . . . . . . . . . . 18
|
91 | 63 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
|
92 | 91 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
93 | | divmulasscom 10709 |
. . . . . . . . . . . . . . . . . . 19
|
94 | 61, 92, 62, 68, 77, 93 | syl32anc 1334 |
. . . . . . . . . . . . . . . . . 18
|
95 | 90, 94 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . 17
|
96 | 95 | exp32 631 |
. . . . . . . . . . . . . . . 16
|
97 | 96 | adantrd 484 |
. . . . . . . . . . . . . . 15
|
98 | 97 | imp 445 |
. . . . . . . . . . . . . 14
|
99 | 98 | adantr 481 |
. . . . . . . . . . . . 13
|
100 | 99 | imp 445 |
. . . . . . . . . . . 12
|
101 | | breq2 4657 |
. . . . . . . . . . . 12
|
102 | 100, 101 | syl5ibcom 235 |
. . . . . . . . . . 11
|
103 | 56, 102 | sylbid 230 |
. . . . . . . . . 10
|
104 | 103 | rexlimdva 3031 |
. . . . . . . . 9
|
105 | 22 | adantl 482 |
. . . . . . . . . . 11
|
106 | | zmulcl 11426 |
. . . . . . . . . . . . 13
|
107 | 106 | 3adant2 1080 |
. . . . . . . . . . . 12
|
108 | 107 | adantr 481 |
. . . . . . . . . . 11
|
109 | | zmulcl 11426 |
. . . . . . . . . . . . 13
|
110 | 109 | 3adant1 1079 |
. . . . . . . . . . . 12
|
111 | 110 | adantr 481 |
. . . . . . . . . . 11
|
112 | | moddvds 14991 |
. . . . . . . . . . 11
|
113 | 105, 108,
111, 112 | syl3anc 1326 |
. . . . . . . . . 10
|
114 | 113 | adantr 481 |
. . . . . . . . 9
|
115 | 104, 114 | sylibrd 249 |
. . . . . . . 8
|
116 | 115 | ex 450 |
. . . . . . 7
|
117 | 116 | com23 86 |
. . . . . 6
|
118 | 37, 117 | sylbid 230 |
. . . . 5
|
119 | 118 | imp 445 |
. . . 4
|
120 | 119 | com12 32 |
. . 3
|
121 | 16, 120 | pm2.61ine 2877 |
. 2
|
122 | 121 | ex 450 |
1
|