Step | Hyp | Ref
| Expression |
1 | | 0z 11388 |
. . . . . . 7
|
2 | | eltpg 4227 |
. . . . . . 7
|
3 | 1, 2 | ax-mp 5 |
. . . . . 6
|
4 | 3 | biimpri 218 |
. . . . 5
|
5 | | tpssi 4369 |
. . . . 5
|
6 | 4, 5 | anim12ci 591 |
. . . 4
|
7 | | lcmf0val 15335 |
. . . 4
lcm
|
8 | 6, 7 | syl 17 |
. . 3
lcm
|
9 | | 0zd 11389 |
. . . . . . . . . 10
|
10 | | lcmcom 15306 |
. . . . . . . . . 10
lcm lcm |
11 | 9, 10 | mpancom 703 |
. . . . . . . . 9
lcm lcm |
12 | | lcm0val 15307 |
. . . . . . . . 9
lcm |
13 | 11, 12 | eqtrd 2656 |
. . . . . . . 8
lcm |
14 | 13 | eqcomd 2628 |
. . . . . . 7
lcm |
15 | 14 | 3ad2ant3 1084 |
. . . . . 6
lcm |
16 | 15 | adantl 482 |
. . . . 5
lcm
|
17 | | 0zd 11389 |
. . . . . . . . . . 11
|
18 | | lcmcom 15306 |
. . . . . . . . . . 11
lcm lcm |
19 | 17, 18 | mpancom 703 |
. . . . . . . . . 10
lcm lcm |
20 | | lcm0val 15307 |
. . . . . . . . . 10
lcm |
21 | 19, 20 | eqtrd 2656 |
. . . . . . . . 9
lcm |
22 | 21 | eqcomd 2628 |
. . . . . . . 8
lcm |
23 | 22 | 3ad2ant2 1083 |
. . . . . . 7
lcm |
24 | 23 | adantl 482 |
. . . . . 6
lcm
|
25 | 24 | oveq1d 6665 |
. . . . 5
lcm lcm lcm |
26 | | oveq1 6657 |
. . . . . . 7
lcm lcm |
27 | 26 | oveq1d 6665 |
. . . . . 6
lcm lcm lcm lcm |
28 | 27 | adantr 481 |
. . . . 5
lcm lcm lcm lcm |
29 | 16, 25, 28 | 3eqtrd 2660 |
. . . 4
lcm lcm |
30 | | lcm0val 15307 |
. . . . . . . . 9
lcm |
31 | 30 | eqcomd 2628 |
. . . . . . . 8
lcm |
32 | 31 | 3ad2ant1 1082 |
. . . . . . 7
lcm |
33 | 32 | adantl 482 |
. . . . . 6
lcm |
34 | 33 | oveq1d 6665 |
. . . . 5
lcm lcm lcm |
35 | 13 | 3ad2ant3 1084 |
. . . . . 6
lcm |
36 | 35 | adantl 482 |
. . . . 5
lcm |
37 | | oveq2 6658 |
. . . . . . 7
lcm lcm |
38 | 37 | adantr 481 |
. . . . . 6
lcm lcm |
39 | 38 | oveq1d 6665 |
. . . . 5
lcm lcm lcm lcm |
40 | 34, 36, 39 | 3eqtr3d 2664 |
. . . 4
lcm lcm |
41 | | lcmcl 15314 |
. . . . . . . 8
lcm |
42 | 41 | nn0zd 11480 |
. . . . . . 7
lcm |
43 | | lcm0val 15307 |
. . . . . . . 8
lcm
lcm lcm |
44 | 43 | eqcomd 2628 |
. . . . . . 7
lcm
lcm lcm |
45 | 42, 44 | syl 17 |
. . . . . 6
lcm lcm |
46 | 45 | 3adant3 1081 |
. . . . 5
lcm lcm |
47 | | oveq2 6658 |
. . . . 5
lcm lcm lcm lcm |
48 | 46, 47 | sylan9eqr 2678 |
. . . 4
lcm lcm |
49 | 29, 40, 48 | 3jaoian 1393 |
. . 3
lcm lcm |
50 | 8, 49 | eqtrd 2656 |
. 2
lcm
lcm lcm |
51 | 42 | 3adant3 1081 |
. . . . . . . . . 10
lcm |
52 | | simp3 1063 |
. . . . . . . . . 10
|
53 | 51, 52 | jca 554 |
. . . . . . . . 9
lcm |
54 | 53 | adantl 482 |
. . . . . . . 8
lcm
|
55 | | dvdslcm 15311 |
. . . . . . . 8
lcm lcm lcm lcm lcm lcm |
56 | 54, 55 | syl 17 |
. . . . . . 7
lcm
lcm lcm lcm lcm |
57 | | dvdslcm 15311 |
. . . . . . . . . . . . . 14
lcm lcm |
58 | 57 | 3adant3 1081 |
. . . . . . . . . . . . 13
lcm
lcm |
59 | | simp1 1061 |
. . . . . . . . . . . . . . . . . 18
|
60 | | lcmcl 15314 |
. . . . . . . . . . . . . . . . . . . 20
lcm lcm lcm |
61 | 53, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
lcm lcm |
62 | 61 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . 18
lcm lcm |
63 | 59, 51, 62 | 3jca 1242 |
. . . . . . . . . . . . . . . . 17
lcm lcm lcm |
64 | | dvdstr 15018 |
. . . . . . . . . . . . . . . . 17
lcm lcm lcm lcm
lcm lcm lcm lcm lcm |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
lcm lcm lcm lcm lcm lcm |
66 | 65 | expd 452 |
. . . . . . . . . . . . . . 15
lcm
lcm lcm lcm lcm lcm |
67 | 66 | com12 32 |
. . . . . . . . . . . . . 14
lcm
lcm lcm lcm lcm lcm |
68 | 67 | adantr 481 |
. . . . . . . . . . . . 13
lcm lcm
lcm lcm lcm lcm lcm |
69 | 58, 68 | mpcom 38 |
. . . . . . . . . . . 12
lcm lcm lcm lcm lcm |
70 | 69 | adantl 482 |
. . . . . . . . . . 11
lcm
lcm lcm lcm lcm |
71 | 70 | com12 32 |
. . . . . . . . . 10
lcm lcm lcm
lcm lcm |
72 | 71 | adantr 481 |
. . . . . . . . 9
lcm lcm lcm lcm lcm
lcm lcm |
73 | 72 | impcom 446 |
. . . . . . . 8
lcm lcm lcm lcm lcm
lcm lcm |
74 | | simpr 477 |
. . . . . . . . . . . . . . 15
lcm lcm
lcm |
75 | 57, 74 | syl 17 |
. . . . . . . . . . . . . 14
lcm |
76 | 75 | 3adant3 1081 |
. . . . . . . . . . . . 13
lcm |
77 | 76 | adantl 482 |
. . . . . . . . . . . 12
lcm |
78 | | simp2 1062 |
. . . . . . . . . . . . . . 15
|
79 | 78, 51, 62 | 3jca 1242 |
. . . . . . . . . . . . . 14
lcm lcm lcm |
80 | 79 | adantl 482 |
. . . . . . . . . . . . 13
lcm lcm lcm |
81 | | dvdstr 15018 |
. . . . . . . . . . . . 13
lcm lcm lcm lcm
lcm lcm lcm lcm lcm |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . 12
lcm lcm lcm lcm
lcm lcm |
83 | 77, 82 | mpand 711 |
. . . . . . . . . . 11
lcm
lcm lcm lcm lcm |
84 | 83 | com12 32 |
. . . . . . . . . 10
lcm lcm lcm
lcm lcm |
85 | 84 | adantr 481 |
. . . . . . . . 9
lcm lcm lcm lcm lcm
lcm lcm |
86 | 85 | impcom 446 |
. . . . . . . 8
lcm lcm lcm lcm lcm
lcm lcm |
87 | | simpr 477 |
. . . . . . . . 9
lcm lcm lcm lcm lcm lcm lcm |
88 | 87 | adantl 482 |
. . . . . . . 8
lcm lcm lcm lcm lcm
lcm lcm |
89 | 73, 86, 88 | 3jca 1242 |
. . . . . . 7
lcm lcm lcm lcm lcm
lcm lcm lcm lcm lcm lcm |
90 | 56, 89 | mpdan 702 |
. . . . . 6
lcm lcm lcm lcm lcm lcm |
91 | | breq1 4656 |
. . . . . . . 8
lcm lcm
lcm lcm |
92 | | breq1 4656 |
. . . . . . . 8
lcm lcm
lcm lcm |
93 | | breq1 4656 |
. . . . . . . 8
lcm lcm
lcm lcm |
94 | 91, 92, 93 | raltpg 4236 |
. . . . . . 7
lcm lcm lcm lcm lcm lcm lcm lcm |
95 | 94 | adantl 482 |
. . . . . 6
lcm lcm
lcm lcm lcm lcm lcm lcm |
96 | 90, 95 | mpbird 247 |
. . . . 5
lcm lcm |
97 | | breq1 4656 |
. . . . . . . . 9
|
98 | | breq1 4656 |
. . . . . . . . 9
|
99 | | breq1 4656 |
. . . . . . . . 9
|
100 | 97, 98, 99 | raltpg 4236 |
. . . . . . . 8
|
101 | 100 | ad2antlr 763 |
. . . . . . 7
|
102 | | simpr 477 |
. . . . . . . . . . 11
|
103 | 51 | ad2antlr 763 |
. . . . . . . . . . 11
lcm |
104 | 52 | ad2antlr 763 |
. . . . . . . . . . 11
|
105 | 102, 103,
104 | 3jca 1242 |
. . . . . . . . . 10
lcm |
106 | 105 | adantr 481 |
. . . . . . . . 9
lcm |
107 | | 3ioran 1056 |
. . . . . . . . . . . . . . . . 17
|
108 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . 22
|
109 | 108 | notbii 310 |
. . . . . . . . . . . . . . . . . . . . 21
|
110 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . 22
|
111 | 110 | notbii 310 |
. . . . . . . . . . . . . . . . . . . . 21
|
112 | 109, 111 | anbi12i 733 |
. . . . . . . . . . . . . . . . . . . 20
|
113 | 112 | biimpi 206 |
. . . . . . . . . . . . . . . . . . 19
|
114 | | ioran 511 |
. . . . . . . . . . . . . . . . . . 19
|
115 | 113, 114 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
|
116 | 115 | 3adant3 1081 |
. . . . . . . . . . . . . . . . 17
|
117 | 107, 116 | sylbi 207 |
. . . . . . . . . . . . . . . 16
|
118 | | id 22 |
. . . . . . . . . . . . . . . . 17
|
119 | 118 | 3adant3 1081 |
. . . . . . . . . . . . . . . 16
|
120 | 117, 119 | anim12ci 591 |
. . . . . . . . . . . . . . 15
|
121 | | lcmn0cl 15310 |
. . . . . . . . . . . . . . 15
lcm |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . 14
lcm |
123 | | nnne0 11053 |
. . . . . . . . . . . . . . 15
lcm
lcm |
124 | 123 | neneqd 2799 |
. . . . . . . . . . . . . 14
lcm
lcm |
125 | 122, 124 | syl 17 |
. . . . . . . . . . . . 13
lcm |
126 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . 18
|
127 | 126 | notbii 310 |
. . . . . . . . . . . . . . . . 17
|
128 | 127 | biimpi 206 |
. . . . . . . . . . . . . . . 16
|
129 | 128 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . 15
|
130 | 107, 129 | sylbi 207 |
. . . . . . . . . . . . . 14
|
131 | 130 | adantr 481 |
. . . . . . . . . . . . 13
|
132 | 125, 131 | jca 554 |
. . . . . . . . . . . 12
lcm |
133 | 132 | adantr 481 |
. . . . . . . . . . 11
lcm
|
134 | 133 | adantr 481 |
. . . . . . . . . 10
lcm |
135 | | ioran 511 |
. . . . . . . . . 10
lcm lcm |
136 | 134, 135 | sylibr 224 |
. . . . . . . . 9
lcm |
137 | 119 | adantl 482 |
. . . . . . . . . . . . . . 15
|
138 | | nnz 11399 |
. . . . . . . . . . . . . . 15
|
139 | 137, 138 | anim12ci 591 |
. . . . . . . . . . . . . 14
|
140 | | 3anass 1042 |
. . . . . . . . . . . . . 14
|
141 | 139, 140 | sylibr 224 |
. . . . . . . . . . . . 13
|
142 | | lcmdvds 15321 |
. . . . . . . . . . . . 13
lcm
|
143 | 141, 142 | syl 17 |
. . . . . . . . . . . 12
lcm |
144 | 143 | com12 32 |
. . . . . . . . . . 11
lcm |
145 | 144 | 3adant3 1081 |
. . . . . . . . . 10
lcm |
146 | 145 | impcom 446 |
. . . . . . . . 9
lcm |
147 | | simp3 1063 |
. . . . . . . . . 10
|
148 | 147 | adantl 482 |
. . . . . . . . 9
|
149 | | lcmledvds 15312 |
. . . . . . . . . 10
lcm lcm
lcm lcm lcm |
150 | 149 | imp 445 |
. . . . . . . . 9
lcm lcm lcm
lcm lcm |
151 | 106, 136,
146, 148, 150 | syl22anc 1327 |
. . . . . . . 8
lcm lcm |
152 | 151 | ex 450 |
. . . . . . 7
lcm lcm |
153 | 101, 152 | sylbid 230 |
. . . . . 6
lcm lcm |
154 | 153 | ralrimiva 2966 |
. . . . 5
lcm lcm |
155 | 96, 154 | jca 554 |
. . . 4
lcm lcm
lcm lcm |
156 | 109 | biimpi 206 |
. . . . . . . . . . . . . . . 16
|
157 | 111 | biimpi 206 |
. . . . . . . . . . . . . . . 16
|
158 | 156, 157 | anim12i 590 |
. . . . . . . . . . . . . . 15
|
159 | 158, 114 | sylibr 224 |
. . . . . . . . . . . . . 14
|
160 | 159 | 3adant3 1081 |
. . . . . . . . . . . . 13
|
161 | 107, 160 | sylbi 207 |
. . . . . . . . . . . 12
|
162 | 161, 119 | anim12ci 591 |
. . . . . . . . . . 11
|
163 | 162, 121 | syl 17 |
. . . . . . . . . 10
lcm |
164 | 163, 124 | syl 17 |
. . . . . . . . 9
lcm |
165 | 164, 131 | jca 554 |
. . . . . . . 8
lcm |
166 | 165, 135 | sylibr 224 |
. . . . . . 7
lcm |
167 | 54, 166 | jca 554 |
. . . . . 6
lcm lcm |
168 | | lcmn0cl 15310 |
. . . . . 6
lcm
lcm lcm lcm |
169 | 167, 168 | syl 17 |
. . . . 5
lcm lcm |
170 | 5 | adantl 482 |
. . . . 5
|
171 | | tpfi 8236 |
. . . . . 6
|
172 | 171 | a1i 11 |
. . . . 5
|
173 | 3 | a1i 11 |
. . . . . . . . 9
|
174 | 173 | biimpd 219 |
. . . . . . . 8
|
175 | 174 | con3d 148 |
. . . . . . 7
|
176 | 175 | impcom 446 |
. . . . . 6
|
177 | | df-nel 2898 |
. . . . . 6
|
178 | 176, 177 | sylibr 224 |
. . . . 5
|
179 | | lcmf 15346 |
. . . . 5
lcm lcm
lcm lcm lcm
lcm lcm
lcm lcm |
180 | 169, 170,
172, 178, 179 | syl13anc 1328 |
. . . 4
lcm lcm lcm
lcm lcm
lcm lcm |
181 | 155, 180 | mpbird 247 |
. . 3
lcm lcm lcm
|
182 | 181 | eqcomd 2628 |
. 2
lcm
lcm lcm |
183 | 50, 182 | pm2.61ian 831 |
1
lcm lcm lcm |