Description: If a positive integer is divisible by each element of a set of pairwise coprime positive integers, then it is divisible by their product. (Contributed by AV, 19-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | coprmproddvds | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cleq1lem | |
|
2 | difeq1 | |
|
3 | 2 | raleqdv | |
4 | 3 | raleqbi1dv | |
5 | raleq | |
|
6 | 4 5 | anbi12d | |
7 | 1 6 | anbi12d | |
8 | prodeq1 | |
|
9 | 8 | breq1d | |
10 | 7 9 | imbi12d | |
11 | cleq1lem | |
|
12 | difeq1 | |
|
13 | 12 | raleqdv | |
14 | 13 | raleqbi1dv | |
15 | raleq | |
|
16 | 14 15 | anbi12d | |
17 | 11 16 | anbi12d | |
18 | prodeq1 | |
|
19 | 18 | breq1d | |
20 | 17 19 | imbi12d | |
21 | cleq1lem | |
|
22 | difeq1 | |
|
23 | 22 | raleqdv | |
24 | 23 | raleqbi1dv | |
25 | raleq | |
|
26 | 24 25 | anbi12d | |
27 | 21 26 | anbi12d | |
28 | prodeq1 | |
|
29 | 28 | breq1d | |
30 | 27 29 | imbi12d | |
31 | cleq1lem | |
|
32 | difeq1 | |
|
33 | 32 | raleqdv | |
34 | 33 | raleqbi1dv | |
35 | raleq | |
|
36 | 34 35 | anbi12d | |
37 | 31 36 | anbi12d | |
38 | prodeq1 | |
|
39 | 38 | breq1d | |
40 | 37 39 | imbi12d | |
41 | prod0 | |
|
42 | nnz | |
|
43 | 1dvds | |
|
44 | 42 43 | syl | |
45 | 41 44 | eqbrtrid | |
46 | 45 | adantr | |
47 | 46 | ad2antlr | |
48 | coprmproddvdslem | |
|
49 | 10 20 30 40 47 48 | findcard2s | |
50 | 49 | exp4c | |
51 | 50 | impcom | |
52 | 51 | 3imp | |