Proof of Theorem mulgcddvds
Step | Hyp | Ref
| Expression |
1 | | simp1 992 |
. . . . . . 7
|
2 | | simp2 993 |
. . . . . . . 8
|
3 | | simp3 994 |
. . . . . . . 8
|
4 | 2, 3 | zmulcld 9327 |
. . . . . . 7
|
5 | 1, 4 | gcdcld 11910 |
. . . . . 6
|
6 | 5 | nn0zd 9319 |
. . . . 5
|
7 | | dvds0 11755 |
. . . . 5
|
8 | 6, 7 | syl 14 |
. . . 4
|
9 | 8 | adantr 274 |
. . 3
|
10 | | oveq2 5858 |
. . . 4
|
11 | 1, 2 | gcdcld 11910 |
. . . . . 6
|
12 | 11 | nn0cnd 9177 |
. . . . 5
|
13 | 12 | mul01d 8299 |
. . . 4
|
14 | 10, 13 | sylan9eqr 2225 |
. . 3
|
15 | 9, 14 | breqtrrd 4015 |
. 2
|
16 | 6 | adantr 274 |
. . . . 5
|
17 | 16 | zcnd 9322 |
. . . 4
|
18 | 1, 3 | gcdcld 11910 |
. . . . . . 7
|
19 | 18 | nn0zd 9319 |
. . . . . 6
|
20 | 19 | adantr 274 |
. . . . 5
|
21 | 20 | zcnd 9322 |
. . . 4
|
22 | | 0zd 9211 |
. . . . . 6
|
23 | | zapne 9273 |
. . . . . 6
#
|
24 | 19, 22, 23 | syl2anc 409 |
. . . . 5
#
|
25 | 24 | biimpar 295 |
. . . 4
# |
26 | 17, 21, 25 | divcanap1d 8695 |
. . 3
|
27 | | gcddvds 11905 |
. . . . . . . . . . 11
|
28 | 1, 4, 27 | syl2anc 409 |
. . . . . . . . . 10
|
29 | 28 | simpld 111 |
. . . . . . . . 9
|
30 | 6, 1, 19, 29 | dvdsmultr1d 11781 |
. . . . . . . 8
|
31 | 30 | adantr 274 |
. . . . . . 7
|
32 | 26, 31 | eqbrtrd 4009 |
. . . . . 6
|
33 | | gcddvds 11905 |
. . . . . . . . . . . 12
|
34 | 1, 3, 33 | syl2anc 409 |
. . . . . . . . . . 11
|
35 | 34 | simpld 111 |
. . . . . . . . . 10
|
36 | 34 | simprd 113 |
. . . . . . . . . . 11
|
37 | | dvdsmultr2 11782 |
. . . . . . . . . . . 12
|
38 | 19, 2, 3, 37 | syl3anc 1233 |
. . . . . . . . . . 11
|
39 | 36, 38 | mpd 13 |
. . . . . . . . . 10
|
40 | | dvdsgcd 11954 |
. . . . . . . . . . 11
|
41 | 19, 1, 4, 40 | syl3anc 1233 |
. . . . . . . . . 10
|
42 | 35, 39, 41 | mp2and 431 |
. . . . . . . . 9
|
43 | 42 | adantr 274 |
. . . . . . . 8
|
44 | | simpr 109 |
. . . . . . . . 9
|
45 | | dvdsval2 11739 |
. . . . . . . . 9
|
46 | 20, 44, 16, 45 | syl3anc 1233 |
. . . . . . . 8
|
47 | 43, 46 | mpbid 146 |
. . . . . . 7
|
48 | 1 | adantr 274 |
. . . . . . 7
|
49 | | dvdsmulcr 11770 |
. . . . . . 7
|
50 | 47, 48, 20, 44, 49 | syl112anc 1237 |
. . . . . 6
|
51 | 32, 50 | mpbid 146 |
. . . . 5
|
52 | | nn0abscl 11036 |
. . . . . . . . . . . . . . 15
|
53 | 2, 52 | syl 14 |
. . . . . . . . . . . . . 14
|
54 | 53 | nn0zd 9319 |
. . . . . . . . . . . . 13
|
55 | | dvdsmultr2 11782 |
. . . . . . . . . . . . 13
|
56 | 6, 54, 1, 55 | syl3anc 1233 |
. . . . . . . . . . . 12
|
57 | 29, 56 | mpd 13 |
. . . . . . . . . . 11
|
58 | 28 | simprd 113 |
. . . . . . . . . . . 12
|
59 | | iddvds 11753 |
. . . . . . . . . . . . . . 15
|
60 | 2, 59 | syl 14 |
. . . . . . . . . . . . . 14
|
61 | | dvdsabsb 11759 |
. . . . . . . . . . . . . . 15
|
62 | 2, 2, 61 | syl2anc 409 |
. . . . . . . . . . . . . 14
|
63 | 60, 62 | mpbid 146 |
. . . . . . . . . . . . 13
|
64 | | dvdsmulc 11768 |
. . . . . . . . . . . . . 14
|
65 | 2, 54, 3, 64 | syl3anc 1233 |
. . . . . . . . . . . . 13
|
66 | 63, 65 | mpd 13 |
. . . . . . . . . . . 12
|
67 | 54, 3 | zmulcld 9327 |
. . . . . . . . . . . . 13
|
68 | | dvdstr 11777 |
. . . . . . . . . . . . 13
|
69 | 6, 4, 67, 68 | syl3anc 1233 |
. . . . . . . . . . . 12
|
70 | 58, 66, 69 | mp2and 431 |
. . . . . . . . . . 11
|
71 | 54, 1 | zmulcld 9327 |
. . . . . . . . . . . 12
|
72 | | dvdsgcd 11954 |
. . . . . . . . . . . 12
|
73 | 6, 71, 67, 72 | syl3anc 1233 |
. . . . . . . . . . 11
|
74 | 57, 70, 73 | mp2and 431 |
. . . . . . . . . 10
|
75 | 18 | nn0red 9176 |
. . . . . . . . . . . . 13
|
76 | 18 | nn0ge0d 9178 |
. . . . . . . . . . . . 13
|
77 | 75, 76 | absidd 11118 |
. . . . . . . . . . . 12
|
78 | 77 | oveq2d 5866 |
. . . . . . . . . . 11
|
79 | 2 | zcnd 9322 |
. . . . . . . . . . . 12
|
80 | 18 | nn0cnd 9177 |
. . . . . . . . . . . 12
|
81 | 79, 80 | absmuld 11145 |
. . . . . . . . . . 11
|
82 | | mulgcd 11958 |
. . . . . . . . . . . 12
|
83 | 53, 1, 3, 82 | syl3anc 1233 |
. . . . . . . . . . 11
|
84 | 78, 81, 83 | 3eqtr4d 2213 |
. . . . . . . . . 10
|
85 | 74, 84 | breqtrrd 4015 |
. . . . . . . . 9
|
86 | 2, 19 | zmulcld 9327 |
. . . . . . . . . 10
|
87 | | dvdsabsb 11759 |
. . . . . . . . . 10
|
88 | 6, 86, 87 | syl2anc 409 |
. . . . . . . . 9
|
89 | 85, 88 | mpbird 166 |
. . . . . . . 8
|
90 | 89 | adantr 274 |
. . . . . . 7
|
91 | 26, 90 | eqbrtrd 4009 |
. . . . . 6
|
92 | 2 | adantr 274 |
. . . . . . 7
|
93 | | dvdsmulcr 11770 |
. . . . . . 7
|
94 | 47, 92, 20, 44, 93 | syl112anc 1237 |
. . . . . 6
|
95 | 91, 94 | mpbid 146 |
. . . . 5
|
96 | | dvdsgcd 11954 |
. . . . . 6
|
97 | 47, 48, 92, 96 | syl3anc 1233 |
. . . . 5
|
98 | 51, 95, 97 | mp2and 431 |
. . . 4
|
99 | 11 | nn0zd 9319 |
. . . . . 6
|
100 | 99 | adantr 274 |
. . . . 5
|
101 | | dvdsmulc 11768 |
. . . . 5
|
102 | 47, 100, 20, 101 | syl3anc 1233 |
. . . 4
|
103 | 98, 102 | mpd 13 |
. . 3
|
104 | 26, 103 | eqbrtrrd 4011 |
. 2
|
105 | | zdceq 9274 |
. . . 4
DECID |
106 | 19, 22, 105 | syl2anc 409 |
. . 3
DECID |
107 | | exmiddc 831 |
. . . 4
DECID
|
108 | | df-ne 2341 |
. . . . 5
|
109 | 108 | orbi2i 757 |
. . . 4
|
110 | 107, 109 | sylibr 133 |
. . 3
DECID
|
111 | 106, 110 | syl 14 |
. 2
|
112 | 15, 104, 111 | mpjaodan 793 |
1
|