Step | Hyp | Ref
| Expression |
1 | | elun 3753 |
. . . . . . . . . . . 12
|
2 | | elun 3753 |
. . . . . . . . . . . . . 14
|
3 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . 19
|
4 | 3 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
5 | 4 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
6 | | sneq 4187 |
. . . . . . . . . . . . . . . . . . . . 21
|
7 | 6 | uneq2d 3767 |
. . . . . . . . . . . . . . . . . . . 20
|
8 | 7 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
lcm lcm |
9 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
lcm lcm lcm lcm |
10 | 8, 9 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . 18
lcm lcm lcm lcm lcm lcm |
11 | 10 | rspcv 3305 |
. . . . . . . . . . . . . . . . 17
lcm lcm lcm lcm lcm lcm |
12 | 5, 11 | syl 17 |
. . . . . . . . . . . . . . . 16
lcm lcm lcm lcm lcm lcm |
13 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
lcm lcm |
14 | 13 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . 23
lcm
lcm |
15 | | dvdslcmf 15344 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
lcm |
16 | 15 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . 24
lcm |
17 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
lcm |
18 | 14, 17 | impel 485 |
. . . . . . . . . . . . . . . . . . . . . 22
lcm |
19 | | lcmfcl 15341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
lcm |
20 | 19 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
lcm |
21 | 20 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
lcm |
22 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
lcm |
23 | | lcmcl 15314 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
lcm |
24 | 3, 23 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
lcm |
25 | 24 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
lcm |
26 | 22, 25 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . 24
lcm lcm |
27 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
lcm lcm |
28 | | dvdslcm 15311 |
. . . . . . . . . . . . . . . . . . . . . . . 24
lcm lcm lcm
lcm lcm lcm lcm
lcm lcm lcm |
29 | 28 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . . 23
lcm lcm lcm lcm lcm lcm |
30 | 27, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
lcm lcm lcm lcm |
31 | | ssel 3597 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
32 | 31 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
33 | 32 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
34 | 33 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
35 | 22 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
lcm |
36 | 25 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
lcm |
37 | | lcmcl 15314 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
lcm lcm lcm lcm lcm |
38 | 35, 36, 37 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
lcm lcm lcm |
39 | 38 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . 23
lcm lcm lcm |
40 | | dvdstr 15018 |
. . . . . . . . . . . . . . . . . . . . . . 23
lcm lcm lcm lcm lcm lcm lcm lcm lcm
lcm lcm lcm |
41 | 34, 35, 39, 40 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
lcm lcm lcm lcm lcm
lcm lcm lcm |
42 | 18, 30, 41 | mp2and 715 |
. . . . . . . . . . . . . . . . . . . . 21
lcm lcm lcm |
43 | 4 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
44 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
45 | 44 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
46 | | lcmass 15327 |
. . . . . . . . . . . . . . . . . . . . . 22
lcm lcm lcm lcm lcm lcm lcm |
47 | 35, 43, 45, 46 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
lcm lcm lcm lcm lcm lcm |
48 | 42, 47 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . . . 20
lcm lcm lcm |
49 | 48 | ex 450 |
. . . . . . . . . . . . . . . . . . 19
lcm lcm lcm |
50 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . 20
|
51 | 21, 3 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . 24
lcm |
52 | 51 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
lcm |
53 | | dvdslcm 15311 |
. . . . . . . . . . . . . . . . . . . . . . . 24
lcm lcm lcm lcm
lcm lcm |
54 | 53 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . 23
lcm lcm lcm |
55 | 52, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
lcm lcm |
56 | 19 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
lcm |
57 | 56 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
lcm |
58 | | lcmcl 15314 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
lcm lcm lcm |
59 | 57, 3, 58 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
lcm lcm |
60 | 59 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . 23
lcm lcm |
61 | | dvdslcm 15311 |
. . . . . . . . . . . . . . . . . . . . . . . 24
lcm lcm lcm lcm
lcm lcm lcm lcm lcm lcm |
62 | 61 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . . 23
lcm lcm lcm lcm
lcm lcm lcm |
63 | 60, 62 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . 22
lcm lcm
lcm lcm lcm |
64 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
lcm lcm |
65 | | lcmcl 15314 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
lcm lcm lcm lcm lcm |
66 | 60, 65 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
lcm lcm lcm |
67 | 66 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . 23
lcm lcm lcm |
68 | | dvdstr 15018 |
. . . . . . . . . . . . . . . . . . . . . . 23
lcm lcm lcm lcm lcm lcm lcm lcm lcm
lcm lcm lcm lcm lcm lcm |
69 | 4, 64, 67, 68 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
lcm lcm
lcm lcm lcm lcm lcm
lcm lcm lcm |
70 | 55, 63, 69 | mp2and 715 |
. . . . . . . . . . . . . . . . . . . . 21
lcm lcm lcm |
71 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . 21
lcm lcm lcm
lcm lcm lcm |
72 | 70, 71 | syl5ibr 236 |
. . . . . . . . . . . . . . . . . . . 20
lcm lcm lcm |
73 | 50, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
lcm lcm lcm |
74 | 49, 73 | jaoi 394 |
. . . . . . . . . . . . . . . . . 18
lcm lcm lcm |
75 | 74 | imp 445 |
. . . . . . . . . . . . . . . . 17
lcm lcm lcm |
76 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
lcm lcm lcm lcm lcm lcm lcm lcm |
77 | 76 | breq2d 4665 |
. . . . . . . . . . . . . . . . 17
lcm lcm lcm lcm lcm
lcm lcm lcm |
78 | 75, 77 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . 16
lcm lcm lcm lcm lcm |
79 | 12, 78 | syld 47 |
. . . . . . . . . . . . . . 15
lcm lcm lcm lcm lcm |
80 | 79 | ex 450 |
. . . . . . . . . . . . . 14
lcm lcm lcm lcm lcm |
81 | 2, 80 | sylbi 207 |
. . . . . . . . . . . . 13
lcm lcm lcm lcm lcm |
82 | | elsni 4194 |
. . . . . . . . . . . . . 14
|
83 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
84 | | snssi 4339 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
85 | 84 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
86 | 83, 85 | unssd 3789 |
. . . . . . . . . . . . . . . . . . . . . 22
|
87 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
88 | | snfi 8038 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
89 | | unfi 8227 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
90 | 87, 88, 89 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
|
91 | | lcmfcl 15341 |
. . . . . . . . . . . . . . . . . . . . . 22
lcm |
92 | 86, 90, 91 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
lcm |
93 | 92 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . 20
lcm |
94 | 93 | anim1i 592 |
. . . . . . . . . . . . . . . . . . 19
lcm
|
95 | 94 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
lcm lcm lcm
lcm |
96 | | dvdslcm 15311 |
. . . . . . . . . . . . . . . . . 18
lcm
lcm lcm lcm lcm lcm |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . . . 17
lcm lcm lcm
lcm lcm lcm
lcm lcm |
98 | 97 | simprd 479 |
. . . . . . . . . . . . . . . 16
lcm lcm lcm
lcm lcm |
99 | | breq1 4656 |
. . . . . . . . . . . . . . . 16
lcm lcm
lcm lcm |
100 | 98, 99 | syl5ibr 236 |
. . . . . . . . . . . . . . 15
lcm lcm lcm lcm lcm |
101 | 100 | expd 452 |
. . . . . . . . . . . . . 14
lcm lcm lcm lcm lcm |
102 | 82, 101 | syl 17 |
. . . . . . . . . . . . 13
lcm lcm lcm lcm lcm |
103 | 81, 102 | jaoi 394 |
. . . . . . . . . . . 12
lcm lcm lcm lcm lcm |
104 | 1, 103 | sylbi 207 |
. . . . . . . . . . 11
lcm lcm lcm lcm lcm |
105 | 104 | com13 88 |
. . . . . . . . . 10
lcm lcm lcm
lcm lcm |
106 | 105 | expd 452 |
. . . . . . . . 9
lcm lcm lcm
lcm lcm |
107 | 106 | adantl 482 |
. . . . . . . 8
lcm
lcm lcm lcm
lcm lcm |
108 | 107 | impcom 446 |
. . . . . . 7
lcm
lcm lcm lcm
lcm lcm |
109 | 108 | impcom 446 |
. . . . . 6
lcm
lcm lcm lcm
lcm lcm |
110 | 109 | adantl 482 |
. . . . 5
lcm
lcm lcm lcm lcm lcm |
111 | 110 | ralrimiv 2965 |
. . . 4
lcm
lcm lcm lcm
lcm lcm |
112 | | lcmfunsnlem2lem1 15351 |
. . . 4
lcm
lcm lcm lcm
lcm lcm |
113 | 111, 112 | jca 554 |
. . 3
lcm
lcm lcm lcm lcm lcm
lcm lcm |
114 | 94 | adantr 481 |
. . . . . . . . . . 11
lcm
|
115 | 86 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
116 | 115 | adantr 481 |
. . . . . . . . . . . . . . 15
|
117 | 90 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
118 | 117 | adantr 481 |
. . . . . . . . . . . . . . 15
|
119 | | df-nel 2898 |
. . . . . . . . . . . . . . . . . . . . 21
|
120 | 119 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . 20
|
121 | 120 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . 19
|
122 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . . . 22
|
123 | 122 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . 21
|
124 | 123 | necon3ai 2819 |
. . . . . . . . . . . . . . . . . . . 20
|
125 | 124 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . 19
|
126 | | ioran 511 |
. . . . . . . . . . . . . . . . . . 19
|
127 | 121, 125,
126 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . 18
|
128 | | elun 3753 |
. . . . . . . . . . . . . . . . . 18
|
129 | 127, 128 | sylnibr 319 |
. . . . . . . . . . . . . . . . 17
|
130 | | df-nel 2898 |
. . . . . . . . . . . . . . . . 17
|
131 | 129, 130 | sylibr 224 |
. . . . . . . . . . . . . . . 16
|
132 | 131 | adantl 482 |
. . . . . . . . . . . . . . 15
|
133 | | lcmfn0cl 15339 |
. . . . . . . . . . . . . . 15
lcm |
134 | 116, 118,
132, 133 | syl3anc 1326 |
. . . . . . . . . . . . . 14
lcm |
135 | 134 | nnne0d 11065 |
. . . . . . . . . . . . 13
lcm |
136 | 135 | neneqd 2799 |
. . . . . . . . . . . 12
lcm |
137 | | df-ne 2795 |
. . . . . . . . . . . . . . 15
|
138 | 137 | biimpi 206 |
. . . . . . . . . . . . . 14
|
139 | 138 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
|
140 | 139 | adantl 482 |
. . . . . . . . . . . 12
|
141 | | ioran 511 |
. . . . . . . . . . . 12
lcm
lcm |
142 | 136, 140,
141 | sylanbrc 698 |
. . . . . . . . . . 11
lcm |
143 | | lcmn0cl 15310 |
. . . . . . . . . . 11
lcm lcm
lcm lcm |
144 | 114, 142,
143 | syl2anc 693 |
. . . . . . . . . 10
lcm lcm |
145 | | snssi 4339 |
. . . . . . . . . . . . . 14
|
146 | 145 | adantl 482 |
. . . . . . . . . . . . 13
|
147 | 115, 146 | unssd 3789 |
. . . . . . . . . . . 12
|
148 | 147 | adantr 481 |
. . . . . . . . . . 11
|
149 | 88, 89 | mpan2 707 |
. . . . . . . . . . . . . . 15
|
150 | | snfi 8038 |
. . . . . . . . . . . . . . 15
|
151 | | unfi 8227 |
. . . . . . . . . . . . . . 15
|
152 | 149, 150,
151 | sylancl 694 |
. . . . . . . . . . . . . 14
|
153 | 152 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
|
154 | 153 | adantr 481 |
. . . . . . . . . . . 12
|
155 | 154 | adantr 481 |
. . . . . . . . . . 11
|
156 | | elun 3753 |
. . . . . . . . . . . . . . . 16
|
157 | | nnel 2906 |
. . . . . . . . . . . . . . . . . . . . 21
|
158 | 157 | biimpri 218 |
. . . . . . . . . . . . . . . . . . . 20
|
159 | 158 | 3mix1d 1236 |
. . . . . . . . . . . . . . . . . . 19
|
160 | | nne 2798 |
. . . . . . . . . . . . . . . . . . . . 21
|
161 | 123, 160 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . 20
|
162 | 161 | 3mix2d 1237 |
. . . . . . . . . . . . . . . . . . 19
|
163 | 159, 162 | jaoi 394 |
. . . . . . . . . . . . . . . . . 18
|
164 | 128, 163 | sylbi 207 |
. . . . . . . . . . . . . . . . 17
|
165 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . 20
|
166 | 165 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . 19
|
167 | | nne 2798 |
. . . . . . . . . . . . . . . . . . 19
|
168 | 166, 167 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
|
169 | 168 | 3mix3d 1238 |
. . . . . . . . . . . . . . . . 17
|
170 | 164, 169 | jaoi 394 |
. . . . . . . . . . . . . . . 16
|
171 | 156, 170 | sylbi 207 |
. . . . . . . . . . . . . . 15
|
172 | | 3ianor 1055 |
. . . . . . . . . . . . . . 15
|
173 | 171, 172 | sylibr 224 |
. . . . . . . . . . . . . 14
|
174 | 173 | con2i 134 |
. . . . . . . . . . . . 13
|
175 | | df-nel 2898 |
. . . . . . . . . . . . 13
|
176 | 174, 175 | sylibr 224 |
. . . . . . . . . . . 12
|
177 | 176 | adantl 482 |
. . . . . . . . . . 11
|
178 | 148, 155,
177 | 3jca 1242 |
. . . . . . . . . 10
|
179 | 144, 178 | jca 554 |
. . . . . . . . 9
lcm lcm |
180 | 179 | ex 450 |
. . . . . . . 8
lcm lcm
|
181 | 180 | ex 450 |
. . . . . . 7
lcm lcm
|
182 | 181 | adantr 481 |
. . . . . 6
lcm
lcm lcm lcm
lcm lcm
|
183 | 182 | impcom 446 |
. . . . 5
lcm
lcm lcm lcm
lcm lcm
|
184 | 183 | impcom 446 |
. . . 4
lcm
lcm lcm lcm lcm lcm |
185 | | lcmf 15346 |
. . . 4
lcm lcm lcm lcm lcm
lcm lcm
lcm lcm
|
186 | 184, 185 | syl 17 |
. . 3
lcm
lcm lcm lcm lcm lcm lcm lcm lcm
lcm lcm |
187 | 113, 186 | mpbird 247 |
. 2
lcm
lcm lcm lcm lcm lcm lcm |
188 | 187 | eqcomd 2628 |
1
lcm
lcm lcm lcm lcm lcm lcm |