Step | Hyp | Ref
| Expression |
1 | | nnz 9201 |
. . . . . . . . . 10
|
2 | | gcddvds 11881 |
. . . . . . . . . . 11
|
3 | 2 | simpld 111 |
. . . . . . . . . 10
|
4 | 1, 3 | sylan2 284 |
. . . . . . . . 9
|
5 | | gcdcl 11884 |
. . . . . . . . . . . 12
|
6 | 1, 5 | sylan2 284 |
. . . . . . . . . . 11
|
7 | 6 | nn0zd 9302 |
. . . . . . . . . 10
|
8 | | simpl 108 |
. . . . . . . . . . . 12
|
9 | 1 | adantl 275 |
. . . . . . . . . . . 12
|
10 | | nnne0 8876 |
. . . . . . . . . . . . . . 15
|
11 | 10 | neneqd 2355 |
. . . . . . . . . . . . . 14
|
12 | 11 | intnand 921 |
. . . . . . . . . . . . 13
|
13 | 12 | adantl 275 |
. . . . . . . . . . . 12
|
14 | | gcdn0cl 11880 |
. . . . . . . . . . . 12
|
15 | 8, 9, 13, 14 | syl21anc 1226 |
. . . . . . . . . . 11
|
16 | 15 | nnne0d 8893 |
. . . . . . . . . 10
|
17 | | dvdsval2 11716 |
. . . . . . . . . 10
|
18 | 7, 16, 8, 17 | syl3anc 1227 |
. . . . . . . . 9
|
19 | 4, 18 | mpbid 146 |
. . . . . . . 8
|
20 | 19 | 3adant3 1006 |
. . . . . . 7
|
21 | 2 | simprd 113 |
. . . . . . . . . . . 12
|
22 | 1, 21 | sylan2 284 |
. . . . . . . . . . 11
|
23 | | dvdsval2 11716 |
. . . . . . . . . . . 12
|
24 | 7, 16, 9, 23 | syl3anc 1227 |
. . . . . . . . . . 11
|
25 | 22, 24 | mpbid 146 |
. . . . . . . . . 10
|
26 | | nnre 8855 |
. . . . . . . . . . . 12
|
27 | 26 | adantl 275 |
. . . . . . . . . . 11
|
28 | 6 | nn0red 9159 |
. . . . . . . . . . 11
|
29 | | nngt0 8873 |
. . . . . . . . . . . 12
|
30 | 29 | adantl 275 |
. . . . . . . . . . 11
|
31 | 15 | nngt0d 8892 |
. . . . . . . . . . 11
|
32 | 27, 28, 30, 31 | divgt0d 8821 |
. . . . . . . . . 10
|
33 | 25, 32 | jca 304 |
. . . . . . . . 9
|
34 | 33 | 3adant3 1006 |
. . . . . . . 8
|
35 | | elnnz 9192 |
. . . . . . . 8
|
36 | 34, 35 | sylibr 133 |
. . . . . . 7
|
37 | | opelxpi 4630 |
. . . . . . 7
|
38 | 20, 36, 37 | syl2anc 409 |
. . . . . 6
|
39 | | fveq2 5480 |
. . . . . . . . . 10
|
40 | | simp1 986 |
. . . . . . . . . . . 12
|
41 | 15 | 3adant3 1006 |
. . . . . . . . . . . 12
|
42 | | znq 9553 |
. . . . . . . . . . . 12
|
43 | 40, 41, 42 | syl2anc 409 |
. . . . . . . . . . 11
|
44 | 9 | 3adant3 1006 |
. . . . . . . . . . . 12
|
45 | | znq 9553 |
. . . . . . . . . . . 12
|
46 | 44, 41, 45 | syl2anc 409 |
. . . . . . . . . . 11
|
47 | | op1stg 6110 |
. . . . . . . . . . 11
|
48 | 43, 46, 47 | syl2anc 409 |
. . . . . . . . . 10
|
49 | 39, 48 | sylan9eqr 2219 |
. . . . . . . . 9
|
50 | | fveq2 5480 |
. . . . . . . . . 10
|
51 | | op2ndg 6111 |
. . . . . . . . . . 11
|
52 | 43, 46, 51 | syl2anc 409 |
. . . . . . . . . 10
|
53 | 50, 52 | sylan9eqr 2219 |
. . . . . . . . 9
|
54 | 49, 53 | oveq12d 5854 |
. . . . . . . 8
|
55 | 54 | eqeq1d 2173 |
. . . . . . 7
|
56 | 49, 53 | oveq12d 5854 |
. . . . . . . 8
|
57 | 56 | eqeq2d 2176 |
. . . . . . 7
|
58 | 55, 57 | anbi12d 465 |
. . . . . 6
|
59 | 19, 25 | gcdcld 11886 |
. . . . . . . . . 10
|
60 | 59 | nn0cnd 9160 |
. . . . . . . . 9
|
61 | | 1cnd 7906 |
. . . . . . . . 9
|
62 | 6 | nn0cnd 9160 |
. . . . . . . . 9
|
63 | 15 | nnap0d 8894 |
. . . . . . . . 9
# |
64 | 62 | mulid1d 7907 |
. . . . . . . . . 10
|
65 | | zcn 9187 |
. . . . . . . . . . . . 13
|
66 | 65 | adantr 274 |
. . . . . . . . . . . 12
|
67 | 66, 62, 63 | divcanap2d 8679 |
. . . . . . . . . . 11
|
68 | | nncn 8856 |
. . . . . . . . . . . . 13
|
69 | 68 | adantl 275 |
. . . . . . . . . . . 12
|
70 | 69, 62, 63 | divcanap2d 8679 |
. . . . . . . . . . 11
|
71 | 67, 70 | oveq12d 5854 |
. . . . . . . . . 10
|
72 | | mulgcd 11934 |
. . . . . . . . . . 11
|
73 | 6, 19, 25, 72 | syl3anc 1227 |
. . . . . . . . . 10
|
74 | 64, 71, 73 | 3eqtr2rd 2204 |
. . . . . . . . 9
|
75 | 60, 61, 62, 63, 74 | mulcanapad 8551 |
. . . . . . . 8
|
76 | 75 | 3adant3 1006 |
. . . . . . 7
|
77 | | nnap0 8877 |
. . . . . . . . . . 11
# |
78 | 77 | adantl 275 |
. . . . . . . . . 10
# |
79 | 66, 69, 62, 78, 63 | divcanap7d 8706 |
. . . . . . . . 9
|
80 | 79 | eqeq2d 2176 |
. . . . . . . 8
|
81 | 80 | biimp3ar 1335 |
. . . . . . 7
|
82 | 76, 81 | jca 304 |
. . . . . 6
|
83 | 38, 58, 82 | rspcedvd 2831 |
. . . . 5
|
84 | | elxp6 6129 |
. . . . . . 7
|
85 | | elxp6 6129 |
. . . . . . 7
|
86 | | simprl 521 |
. . . . . . . . . . . 12
|
87 | 86 | ad2antrr 480 |
. . . . . . . . . . 11
|
88 | | simprr 522 |
. . . . . . . . . . . 12
|
89 | 88 | ad2antrr 480 |
. . . . . . . . . . 11
|
90 | | simprll 527 |
. . . . . . . . . . 11
|
91 | | simprl 521 |
. . . . . . . . . . . 12
|
92 | 91 | ad2antlr 481 |
. . . . . . . . . . 11
|
93 | | simprr 522 |
. . . . . . . . . . . 12
|
94 | 93 | ad2antlr 481 |
. . . . . . . . . . 11
|
95 | | simprrl 529 |
. . . . . . . . . . 11
|
96 | | simprlr 528 |
. . . . . . . . . . . 12
|
97 | | simprrr 530 |
. . . . . . . . . . . 12
|
98 | 96, 97 | eqtr3d 2199 |
. . . . . . . . . . 11
|
99 | | qredeq 12007 |
. . . . . . . . . . 11
|
100 | 87, 89, 90, 92, 94, 95, 98, 99 | syl331anc 1252 |
. . . . . . . . . 10
|
101 | | vex 2724 |
. . . . . . . . . . . 12
|
102 | | 1stexg 6127 |
. . . . . . . . . . . 12
|
103 | 101, 102 | ax-mp 5 |
. . . . . . . . . . 11
|
104 | | 2ndexg 6128 |
. . . . . . . . . . . 12
|
105 | 101, 104 | ax-mp 5 |
. . . . . . . . . . 11
|
106 | 103, 105 | opth 4209 |
. . . . . . . . . 10
|
107 | 100, 106 | sylibr 133 |
. . . . . . . . 9
|
108 | | simplll 523 |
. . . . . . . . 9
|
109 | | simplrl 525 |
. . . . . . . . 9
|
110 | 107, 108,
109 | 3eqtr4d 2207 |
. . . . . . . 8
|
111 | 110 | ex 114 |
. . . . . . 7
|
112 | 84, 85, 111 | syl2anb 289 |
. . . . . 6
|
113 | 112 | rgen2a 2518 |
. . . . 5
|
114 | 83, 113 | jctir 311 |
. . . 4
|
115 | 114 | 3expia 1194 |
. . 3
|
116 | 115 | rexlimivv 2587 |
. 2
|
117 | | elq 9551 |
. 2
|
118 | | fveq2 5480 |
. . . . . 6
|
119 | | fveq2 5480 |
. . . . . 6
|
120 | 118, 119 | oveq12d 5854 |
. . . . 5
|
121 | 120 | eqeq1d 2173 |
. . . 4
|
122 | 118, 119 | oveq12d 5854 |
. . . . 5
|
123 | 122 | eqeq2d 2176 |
. . . 4
|
124 | 121, 123 | anbi12d 465 |
. . 3
|
125 | 124 | reu4 2915 |
. 2
|
126 | 116, 117,
125 | 3imtr4i 200 |
1
|