Step | Hyp | Ref
| Expression |
1 | | bezout.3 |
. . . . . . . 8
|
2 | | bezout.4 |
. . . . . . . 8
|
3 | | gcddvds 15225 |
. . . . . . . 8
|
4 | 1, 2, 3 | syl2anc 693 |
. . . . . . 7
|
5 | 4 | simpld 475 |
. . . . . 6
|
6 | 1, 2 | gcdcld 15230 |
. . . . . . . 8
|
7 | 6 | nn0zd 11480 |
. . . . . . 7
|
8 | | divides 14985 |
. . . . . . 7
|
9 | 7, 1, 8 | syl2anc 693 |
. . . . . 6
|
10 | 5, 9 | mpbid 222 |
. . . . 5
|
11 | 4 | simprd 479 |
. . . . . 6
|
12 | | divides 14985 |
. . . . . . 7
|
13 | 7, 2, 12 | syl2anc 693 |
. . . . . 6
|
14 | 11, 13 | mpbid 222 |
. . . . 5
|
15 | | reeanv 3107 |
. . . . . 6
|
16 | | bezout.1 |
. . . . . . . . . . 11
|
17 | | bezout.2 |
. . . . . . . . . . 11
inf |
18 | | bezout.5 |
. . . . . . . . . . 11
|
19 | 16, 1, 2, 17, 18 | bezoutlem2 15257 |
. . . . . . . . . 10
|
20 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
|
21 | 20 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
22 | 21 | eqeq2d 2632 |
. . . . . . . . . . . . 13
|
23 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
|
24 | 23 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
25 | 24 | eqeq2d 2632 |
. . . . . . . . . . . . 13
|
26 | 22, 25 | cbvrex2v 3180 |
. . . . . . . . . . . 12
|
27 | | eqeq1 2626 |
. . . . . . . . . . . . 13
|
28 | 27 | 2rexbidv 3057 |
. . . . . . . . . . . 12
|
29 | 26, 28 | syl5bb 272 |
. . . . . . . . . . 11
|
30 | 29, 16 | elrab2 3366 |
. . . . . . . . . 10
|
31 | 19, 30 | sylib 208 |
. . . . . . . . 9
|
32 | 31 | simprd 479 |
. . . . . . . 8
|
33 | | simprrl 804 |
. . . . . . . . . . . . . . . . 17
|
34 | | simprll 802 |
. . . . . . . . . . . . . . . . 17
|
35 | 33, 34 | zmulcld 11488 |
. . . . . . . . . . . . . . . 16
|
36 | | simprrr 805 |
. . . . . . . . . . . . . . . . 17
|
37 | | simprlr 803 |
. . . . . . . . . . . . . . . . 17
|
38 | 36, 37 | zmulcld 11488 |
. . . . . . . . . . . . . . . 16
|
39 | 35, 38 | zaddcld 11486 |
. . . . . . . . . . . . . . 15
|
40 | 7 | adantr 481 |
. . . . . . . . . . . . . . 15
|
41 | | dvdsmul2 15004 |
. . . . . . . . . . . . . . 15
|
42 | 39, 40, 41 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
43 | 35 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
|
44 | 38 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
|
45 | 40 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
|
46 | 43, 44, 45 | adddird 10065 |
. . . . . . . . . . . . . . 15
|
47 | 33 | zcnd 11483 |
. . . . . . . . . . . . . . . . 17
|
48 | 34 | zcnd 11483 |
. . . . . . . . . . . . . . . . 17
|
49 | 47, 48, 45 | mul32d 10246 |
. . . . . . . . . . . . . . . 16
|
50 | 36 | zcnd 11483 |
. . . . . . . . . . . . . . . . 17
|
51 | 37 | zcnd 11483 |
. . . . . . . . . . . . . . . . 17
|
52 | 50, 51, 45 | mul32d 10246 |
. . . . . . . . . . . . . . . 16
|
53 | 49, 52 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
|
54 | 46, 53 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
55 | 42, 54 | breqtrd 4679 |
. . . . . . . . . . . . 13
|
56 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
57 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
58 | 56, 57 | oveqan12d 6669 |
. . . . . . . . . . . . . 14
|
59 | 58 | breq2d 4665 |
. . . . . . . . . . . . 13
|
60 | 55, 59 | syl5ibcom 235 |
. . . . . . . . . . . 12
|
61 | | breq2 4657 |
. . . . . . . . . . . . 13
|
62 | 61 | imbi2d 330 |
. . . . . . . . . . . 12
|
63 | 60, 62 | syl5ibrcom 237 |
. . . . . . . . . . 11
|
64 | 63 | expr 643 |
. . . . . . . . . 10
|
65 | 64 | com23 86 |
. . . . . . . . 9
|
66 | 65 | rexlimdvva 3038 |
. . . . . . . 8
|
67 | 32, 66 | mpd 15 |
. . . . . . 7
|
68 | 67 | rexlimdvv 3037 |
. . . . . 6
|
69 | 15, 68 | syl5bir 233 |
. . . . 5
|
70 | 10, 14, 69 | mp2and 715 |
. . . 4
|
71 | 31 | simpld 475 |
. . . . 5
|
72 | | dvdsle 15032 |
. . . . 5
|
73 | 7, 71, 72 | syl2anc 693 |
. . . 4
|
74 | 70, 73 | mpd 15 |
. . 3
|
75 | | breq2 4657 |
. . . . 5
|
76 | 16, 1, 2 | bezoutlem1 15256 |
. . . . . . . 8
|
77 | 16, 1, 2, 17, 18 | bezoutlem3 15258 |
. . . . . . . 8
|
78 | 76, 77 | syld 47 |
. . . . . . 7
|
79 | 71 | nnzd 11481 |
. . . . . . . 8
|
80 | | dvdsabsb 15001 |
. . . . . . . 8
|
81 | 79, 1, 80 | syl2anc 693 |
. . . . . . 7
|
82 | 78, 81 | sylibrd 249 |
. . . . . 6
|
83 | 82 | imp 445 |
. . . . 5
|
84 | | dvds0 14997 |
. . . . . 6
|
85 | 79, 84 | syl 17 |
. . . . 5
|
86 | 75, 83, 85 | pm2.61ne 2879 |
. . . 4
|
87 | | breq2 4657 |
. . . . 5
|
88 | | eqid 2622 |
. . . . . . . . . 10
|
89 | 88, 2, 1 | bezoutlem1 15256 |
. . . . . . . . 9
|
90 | | rexcom 3099 |
. . . . . . . . . . . . 13
|
91 | 1 | zcnd 11483 |
. . . . . . . . . . . . . . . . . 18
|
92 | 91 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
93 | | zcn 11382 |
. . . . . . . . . . . . . . . . . 18
|
94 | 93 | ad2antll 765 |
. . . . . . . . . . . . . . . . 17
|
95 | 92, 94 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
96 | 2 | zcnd 11483 |
. . . . . . . . . . . . . . . . . 18
|
97 | 96 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
98 | | zcn 11382 |
. . . . . . . . . . . . . . . . . 18
|
99 | 98 | ad2antrl 764 |
. . . . . . . . . . . . . . . . 17
|
100 | 97, 99 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
101 | 95, 100 | addcomd 10238 |
. . . . . . . . . . . . . . 15
|
102 | 101 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
|
103 | 102 | 2rexbidva 3056 |
. . . . . . . . . . . . 13
|
104 | 90, 103 | syl5bb 272 |
. . . . . . . . . . . 12
|
105 | 104 | rabbidv 3189 |
. . . . . . . . . . 11
|
106 | 16, 105 | syl5eq 2668 |
. . . . . . . . . 10
|
107 | 106 | eleq2d 2687 |
. . . . . . . . 9
|
108 | 89, 107 | sylibrd 249 |
. . . . . . . 8
|
109 | 16, 1, 2, 17, 18 | bezoutlem3 15258 |
. . . . . . . 8
|
110 | 108, 109 | syld 47 |
. . . . . . 7
|
111 | | dvdsabsb 15001 |
. . . . . . . 8
|
112 | 79, 2, 111 | syl2anc 693 |
. . . . . . 7
|
113 | 110, 112 | sylibrd 249 |
. . . . . 6
|
114 | 113 | imp 445 |
. . . . 5
|
115 | 87, 114, 85 | pm2.61ne 2879 |
. . . 4
|
116 | | dvdslegcd 15226 |
. . . . 5
|
117 | 79, 1, 2, 18, 116 | syl31anc 1329 |
. . . 4
|
118 | 86, 115, 117 | mp2and 715 |
. . 3
|
119 | 6 | nn0red 11352 |
. . . 4
|
120 | 71 | nnred 11035 |
. . . 4
|
121 | 119, 120 | letri3d 10179 |
. . 3
|
122 | 74, 118, 121 | mpbir2and 957 |
. 2
|
123 | 122, 19 | eqeltrd 2701 |
1
|