Step | Hyp | Ref
| Expression |
1 | | nnz 11399 |
. . . . . . . . . 10
|
2 | | gcddvds 15225 |
. . . . . . . . . . 11
|
3 | 2 | simpld 475 |
. . . . . . . . . 10
|
4 | 1, 3 | sylan2 491 |
. . . . . . . . 9
|
5 | | gcdcl 15228 |
. . . . . . . . . . . 12
|
6 | 1, 5 | sylan2 491 |
. . . . . . . . . . 11
|
7 | 6 | nn0zd 11480 |
. . . . . . . . . 10
|
8 | | simpl 473 |
. . . . . . . . . . . 12
|
9 | 1 | adantl 482 |
. . . . . . . . . . . 12
|
10 | | nnne0 11053 |
. . . . . . . . . . . . . . 15
|
11 | 10 | neneqd 2799 |
. . . . . . . . . . . . . 14
|
12 | 11 | intnand 962 |
. . . . . . . . . . . . 13
|
13 | 12 | adantl 482 |
. . . . . . . . . . . 12
|
14 | | gcdn0cl 15224 |
. . . . . . . . . . . 12
|
15 | 8, 9, 13, 14 | syl21anc 1325 |
. . . . . . . . . . 11
|
16 | | nnne0 11053 |
. . . . . . . . . . 11
|
17 | 15, 16 | syl 17 |
. . . . . . . . . 10
|
18 | | dvdsval2 14986 |
. . . . . . . . . 10
|
19 | 7, 17, 8, 18 | syl3anc 1326 |
. . . . . . . . 9
|
20 | 4, 19 | mpbid 222 |
. . . . . . . 8
|
21 | 20 | 3adant3 1081 |
. . . . . . 7
|
22 | 2 | simprd 479 |
. . . . . . . . . . . 12
|
23 | 1, 22 | sylan2 491 |
. . . . . . . . . . 11
|
24 | | dvdsval2 14986 |
. . . . . . . . . . . 12
|
25 | 7, 17, 9, 24 | syl3anc 1326 |
. . . . . . . . . . 11
|
26 | 23, 25 | mpbid 222 |
. . . . . . . . . 10
|
27 | | nnre 11027 |
. . . . . . . . . . . 12
|
28 | 27 | adantl 482 |
. . . . . . . . . . 11
|
29 | 6 | nn0red 11352 |
. . . . . . . . . . 11
|
30 | | nngt0 11049 |
. . . . . . . . . . . 12
|
31 | 30 | adantl 482 |
. . . . . . . . . . 11
|
32 | | nngt0 11049 |
. . . . . . . . . . . 12
|
33 | 15, 32 | syl 17 |
. . . . . . . . . . 11
|
34 | 28, 29, 31, 33 | divgt0d 10959 |
. . . . . . . . . 10
|
35 | 26, 34 | jca 554 |
. . . . . . . . 9
|
36 | 35 | 3adant3 1081 |
. . . . . . . 8
|
37 | | elnnz 11387 |
. . . . . . . 8
|
38 | 36, 37 | sylibr 224 |
. . . . . . 7
|
39 | 21, 38 | opelxpd 5149 |
. . . . . 6
|
40 | 20, 26 | gcdcld 15230 |
. . . . . . . . 9
|
41 | 40 | nn0cnd 11353 |
. . . . . . . 8
|
42 | | 1cnd 10056 |
. . . . . . . 8
|
43 | 6 | nn0cnd 11353 |
. . . . . . . 8
|
44 | 43 | mulid1d 10057 |
. . . . . . . . 9
|
45 | | zcn 11382 |
. . . . . . . . . . . 12
|
46 | 45 | adantr 481 |
. . . . . . . . . . 11
|
47 | 46, 43, 17 | divcan2d 10803 |
. . . . . . . . . 10
|
48 | | nncn 11028 |
. . . . . . . . . . . 12
|
49 | 48 | adantl 482 |
. . . . . . . . . . 11
|
50 | 49, 43, 17 | divcan2d 10803 |
. . . . . . . . . 10
|
51 | 47, 50 | oveq12d 6668 |
. . . . . . . . 9
|
52 | | mulgcd 15265 |
. . . . . . . . . 10
|
53 | 6, 20, 26, 52 | syl3anc 1326 |
. . . . . . . . 9
|
54 | 44, 51, 53 | 3eqtr2rd 2663 |
. . . . . . . 8
|
55 | 41, 42, 43, 17, 54 | mulcanad 10662 |
. . . . . . 7
|
56 | 55 | 3adant3 1081 |
. . . . . 6
|
57 | 10 | adantl 482 |
. . . . . . . . 9
|
58 | 46, 49, 43, 57, 17 | divcan7d 10829 |
. . . . . . . 8
|
59 | 58 | eqeq2d 2632 |
. . . . . . 7
|
60 | 59 | biimp3ar 1433 |
. . . . . 6
|
61 | | ovex 6678 |
. . . . . . . . . . 11
|
62 | | ovex 6678 |
. . . . . . . . . . 11
|
63 | 61, 62 | op1std 7178 |
. . . . . . . . . 10
|
64 | 61, 62 | op2ndd 7179 |
. . . . . . . . . 10
|
65 | 63, 64 | oveq12d 6668 |
. . . . . . . . 9
|
66 | 65 | eqeq1d 2624 |
. . . . . . . 8
|
67 | 63, 64 | oveq12d 6668 |
. . . . . . . . 9
|
68 | 67 | eqeq2d 2632 |
. . . . . . . 8
|
69 | 66, 68 | anbi12d 747 |
. . . . . . 7
|
70 | 69 | rspcev 3309 |
. . . . . 6
|
71 | 39, 56, 60, 70 | syl12anc 1324 |
. . . . 5
|
72 | | elxp6 7200 |
. . . . . . 7
|
73 | | elxp6 7200 |
. . . . . . 7
|
74 | | simprl 794 |
. . . . . . . . . . . 12
|
75 | 74 | ad2antrr 762 |
. . . . . . . . . . 11
|
76 | | simprr 796 |
. . . . . . . . . . . 12
|
77 | 76 | ad2antrr 762 |
. . . . . . . . . . 11
|
78 | | simprll 802 |
. . . . . . . . . . 11
|
79 | | simprl 794 |
. . . . . . . . . . . 12
|
80 | 79 | ad2antlr 763 |
. . . . . . . . . . 11
|
81 | | simprr 796 |
. . . . . . . . . . . 12
|
82 | 81 | ad2antlr 763 |
. . . . . . . . . . 11
|
83 | | simprrl 804 |
. . . . . . . . . . 11
|
84 | | simprlr 803 |
. . . . . . . . . . . 12
|
85 | | simprrr 805 |
. . . . . . . . . . . 12
|
86 | 84, 85 | eqtr3d 2658 |
. . . . . . . . . . 11
|
87 | | qredeq 15371 |
. . . . . . . . . . 11
|
88 | 75, 77, 78, 80, 82, 83, 86, 87 | syl331anc 1351 |
. . . . . . . . . 10
|
89 | | fvex 6201 |
. . . . . . . . . . 11
|
90 | | fvex 6201 |
. . . . . . . . . . 11
|
91 | 89, 90 | opth 4945 |
. . . . . . . . . 10
|
92 | 88, 91 | sylibr 224 |
. . . . . . . . 9
|
93 | | simplll 798 |
. . . . . . . . 9
|
94 | | simplrl 800 |
. . . . . . . . 9
|
95 | 92, 93, 94 | 3eqtr4d 2666 |
. . . . . . . 8
|
96 | 95 | ex 450 |
. . . . . . 7
|
97 | 72, 73, 96 | syl2anb 496 |
. . . . . 6
|
98 | 97 | rgen2a 2977 |
. . . . 5
|
99 | 71, 98 | jctir 561 |
. . . 4
|
100 | 99 | 3expia 1267 |
. . 3
|
101 | 100 | rexlimivv 3036 |
. 2
|
102 | | elq 11790 |
. 2
|
103 | | fveq2 6191 |
. . . . . 6
|
104 | | fveq2 6191 |
. . . . . 6
|
105 | 103, 104 | oveq12d 6668 |
. . . . 5
|
106 | 105 | eqeq1d 2624 |
. . . 4
|
107 | 103, 104 | oveq12d 6668 |
. . . . 5
|
108 | 107 | eqeq2d 2632 |
. . . 4
|
109 | 106, 108 | anbi12d 747 |
. . 3
|
110 | 109 | reu4 3400 |
. 2
|
111 | 101, 102,
110 | 3imtr4i 281 |
1
|