Proof of Theorem mulgcddvds
Step | Hyp | Ref
| Expression |
1 | | simp1 938 |
. . . . . . 7
|
2 | | simp2 939 |
. . . . . . . 8
|
3 | | simp3 940 |
. . . . . . . 8
|
4 | 2, 3 | zmulcld 8475 |
. . . . . . 7
|
5 | 1, 4 | gcdcld 10360 |
. . . . . 6
|
6 | 5 | nn0zd 8467 |
. . . . 5
|
7 | | dvds0 10210 |
. . . . 5
|
8 | 6, 7 | syl 14 |
. . . 4
|
9 | 8 | adantr 270 |
. . 3
|
10 | | oveq2 5540 |
. . . 4
|
11 | 1, 2 | gcdcld 10360 |
. . . . . 6
|
12 | 11 | nn0cnd 8343 |
. . . . 5
|
13 | 12 | mul01d 7497 |
. . . 4
|
14 | 10, 13 | sylan9eqr 2135 |
. . 3
|
15 | 9, 14 | breqtrrd 3811 |
. 2
|
16 | 6 | adantr 270 |
. . . . 5
|
17 | 16 | zcnd 8470 |
. . . 4
|
18 | 1, 3 | gcdcld 10360 |
. . . . . . 7
|
19 | 18 | nn0zd 8467 |
. . . . . 6
|
20 | 19 | adantr 270 |
. . . . 5
|
21 | 20 | zcnd 8470 |
. . . 4
|
22 | | 0zd 8363 |
. . . . . 6
|
23 | | zapne 8422 |
. . . . . 6
#
|
24 | 19, 22, 23 | syl2anc 403 |
. . . . 5
#
|
25 | 24 | biimpar 291 |
. . . 4
# |
26 | 17, 21, 25 | divcanap1d 7878 |
. . 3
|
27 | | gcddvds 10355 |
. . . . . . . . . . 11
|
28 | 1, 4, 27 | syl2anc 403 |
. . . . . . . . . 10
|
29 | 28 | simpld 110 |
. . . . . . . . 9
|
30 | 6, 1, 19, 29 | dvdsmultr1d 10234 |
. . . . . . . 8
|
31 | 30 | adantr 270 |
. . . . . . 7
|
32 | 26, 31 | eqbrtrd 3805 |
. . . . . 6
|
33 | | gcddvds 10355 |
. . . . . . . . . . . 12
|
34 | 1, 3, 33 | syl2anc 403 |
. . . . . . . . . . 11
|
35 | 34 | simpld 110 |
. . . . . . . . . 10
|
36 | 34 | simprd 112 |
. . . . . . . . . . 11
|
37 | | dvdsmultr2 10235 |
. . . . . . . . . . . 12
|
38 | 19, 2, 3, 37 | syl3anc 1169 |
. . . . . . . . . . 11
|
39 | 36, 38 | mpd 13 |
. . . . . . . . . 10
|
40 | | dvdsgcd 10401 |
. . . . . . . . . . 11
|
41 | 19, 1, 4, 40 | syl3anc 1169 |
. . . . . . . . . 10
|
42 | 35, 39, 41 | mp2and 423 |
. . . . . . . . 9
|
43 | 42 | adantr 270 |
. . . . . . . 8
|
44 | | simpr 108 |
. . . . . . . . 9
|
45 | | dvdsval2 10198 |
. . . . . . . . 9
|
46 | 20, 44, 16, 45 | syl3anc 1169 |
. . . . . . . 8
|
47 | 43, 46 | mpbid 145 |
. . . . . . 7
|
48 | 1 | adantr 270 |
. . . . . . 7
|
49 | | dvdsmulcr 10225 |
. . . . . . 7
|
50 | 47, 48, 20, 44, 49 | syl112anc 1173 |
. . . . . 6
|
51 | 32, 50 | mpbid 145 |
. . . . 5
|
52 | | nn0abscl 9971 |
. . . . . . . . . . . . . . 15
|
53 | 2, 52 | syl 14 |
. . . . . . . . . . . . . 14
|
54 | 53 | nn0zd 8467 |
. . . . . . . . . . . . 13
|
55 | | dvdsmultr2 10235 |
. . . . . . . . . . . . 13
|
56 | 6, 54, 1, 55 | syl3anc 1169 |
. . . . . . . . . . . 12
|
57 | 29, 56 | mpd 13 |
. . . . . . . . . . 11
|
58 | 28 | simprd 112 |
. . . . . . . . . . . 12
|
59 | | iddvds 10208 |
. . . . . . . . . . . . . . 15
|
60 | 2, 59 | syl 14 |
. . . . . . . . . . . . . 14
|
61 | | dvdsabsb 10214 |
. . . . . . . . . . . . . . 15
|
62 | 2, 2, 61 | syl2anc 403 |
. . . . . . . . . . . . . 14
|
63 | 60, 62 | mpbid 145 |
. . . . . . . . . . . . 13
|
64 | | dvdsmulc 10223 |
. . . . . . . . . . . . . 14
|
65 | 2, 54, 3, 64 | syl3anc 1169 |
. . . . . . . . . . . . 13
|
66 | 63, 65 | mpd 13 |
. . . . . . . . . . . 12
|
67 | 54, 3 | zmulcld 8475 |
. . . . . . . . . . . . 13
|
68 | | dvdstr 10232 |
. . . . . . . . . . . . 13
|
69 | 6, 4, 67, 68 | syl3anc 1169 |
. . . . . . . . . . . 12
|
70 | 58, 66, 69 | mp2and 423 |
. . . . . . . . . . 11
|
71 | 54, 1 | zmulcld 8475 |
. . . . . . . . . . . 12
|
72 | | dvdsgcd 10401 |
. . . . . . . . . . . 12
|
73 | 6, 71, 67, 72 | syl3anc 1169 |
. . . . . . . . . . 11
|
74 | 57, 70, 73 | mp2and 423 |
. . . . . . . . . 10
|
75 | 18 | nn0red 8342 |
. . . . . . . . . . . . 13
|
76 | 18 | nn0ge0d 8344 |
. . . . . . . . . . . . 13
|
77 | 75, 76 | absidd 10053 |
. . . . . . . . . . . 12
|
78 | 77 | oveq2d 5548 |
. . . . . . . . . . 11
|
79 | 2 | zcnd 8470 |
. . . . . . . . . . . 12
|
80 | 18 | nn0cnd 8343 |
. . . . . . . . . . . 12
|
81 | 79, 80 | absmuld 10080 |
. . . . . . . . . . 11
|
82 | | mulgcd 10405 |
. . . . . . . . . . . 12
|
83 | 53, 1, 3, 82 | syl3anc 1169 |
. . . . . . . . . . 11
|
84 | 78, 81, 83 | 3eqtr4d 2123 |
. . . . . . . . . 10
|
85 | 74, 84 | breqtrrd 3811 |
. . . . . . . . 9
|
86 | 2, 19 | zmulcld 8475 |
. . . . . . . . . 10
|
87 | | dvdsabsb 10214 |
. . . . . . . . . 10
|
88 | 6, 86, 87 | syl2anc 403 |
. . . . . . . . 9
|
89 | 85, 88 | mpbird 165 |
. . . . . . . 8
|
90 | 89 | adantr 270 |
. . . . . . 7
|
91 | 26, 90 | eqbrtrd 3805 |
. . . . . 6
|
92 | 2 | adantr 270 |
. . . . . . 7
|
93 | | dvdsmulcr 10225 |
. . . . . . 7
|
94 | 47, 92, 20, 44, 93 | syl112anc 1173 |
. . . . . 6
|
95 | 91, 94 | mpbid 145 |
. . . . 5
|
96 | | dvdsgcd 10401 |
. . . . . 6
|
97 | 47, 48, 92, 96 | syl3anc 1169 |
. . . . 5
|
98 | 51, 95, 97 | mp2and 423 |
. . . 4
|
99 | 11 | nn0zd 8467 |
. . . . . 6
|
100 | 99 | adantr 270 |
. . . . 5
|
101 | | dvdsmulc 10223 |
. . . . 5
|
102 | 47, 100, 20, 101 | syl3anc 1169 |
. . . 4
|
103 | 98, 102 | mpd 13 |
. . 3
|
104 | 26, 103 | eqbrtrrd 3807 |
. 2
|
105 | | zdceq 8423 |
. . . 4
DECID |
106 | 19, 22, 105 | syl2anc 403 |
. . 3
DECID |
107 | | exmiddc 777 |
. . . 4
DECID
|
108 | | df-ne 2246 |
. . . . 5
|
109 | 108 | orbi2i 711 |
. . . 4
|
110 | 107, 109 | sylibr 132 |
. . 3
DECID
|
111 | 106, 110 | syl 14 |
. 2
|
112 | 15, 104, 111 | mpjaodan 744 |
1
|