Proof of Theorem coprmproddvdslem
Step | Hyp | Ref
| Expression |
1 | | nfv 1843 |
. . . . 5
|
2 | | nfcv 2764 |
. . . . 5
|
3 | | simpll 790 |
. . . . 5
|
4 | | unss 3787 |
. . . . . . . 8
|
5 | | vex 3203 |
. . . . . . . . . . 11
|
6 | 5 | snss 4316 |
. . . . . . . . . 10
|
7 | 6 | biimpri 218 |
. . . . . . . . 9
|
8 | 7 | adantl 482 |
. . . . . . . 8
|
9 | 4, 8 | sylbir 225 |
. . . . . . 7
|
10 | 9 | adantr 481 |
. . . . . 6
|
11 | 10 | adantl 482 |
. . . . 5
|
12 | | simplr 792 |
. . . . 5
|
13 | | simprrr 805 |
. . . . . . . 8
|
14 | 13 | adantr 481 |
. . . . . . 7
|
15 | | simpl 473 |
. . . . . . . . . . 11
|
16 | 4, 15 | sylbir 225 |
. . . . . . . . . 10
|
17 | 16 | adantr 481 |
. . . . . . . . 9
|
18 | 17 | adantl 482 |
. . . . . . . 8
|
19 | 18 | sselda 3603 |
. . . . . . 7
|
20 | 14, 19 | ffvelrnd 6360 |
. . . . . 6
|
21 | 20 | nncnd 11036 |
. . . . 5
|
22 | | fveq2 6191 |
. . . . 5
|
23 | 13, 11 | ffvelrnd 6360 |
. . . . . 6
|
24 | 23 | nncnd 11036 |
. . . . 5
|
25 | 1, 2, 3, 11, 12, 21, 22, 24 | fprodsplitsn 14720 |
. . . 4
|
26 | 25 | ad2ant2r 783 |
. . 3
|
27 | | simprl 794 |
. . . . . . . . . . . 12
|
28 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
29 | 28 | adantr 481 |
. . . . . . . . . . . . . 14
|
30 | 29 | adantr 481 |
. . . . . . . . . . . . 13
|
31 | 17 | adantr 481 |
. . . . . . . . . . . . . 14
|
32 | 31 | sselda 3603 |
. . . . . . . . . . . . 13
|
33 | 30, 32 | ffvelrnd 6360 |
. . . . . . . . . . . 12
|
34 | 27, 33 | fprodnncl 14685 |
. . . . . . . . . . 11
|
35 | 34 | ex 450 |
. . . . . . . . . 10
|
36 | 35 | adantr 481 |
. . . . . . . . 9
|
37 | 36 | com12 32 |
. . . . . . . 8
|
38 | 37 | adantr 481 |
. . . . . . 7
|
39 | 38 | imp 445 |
. . . . . 6
|
40 | 39 | nnzd 11481 |
. . . . 5
|
41 | 28, 10 | ffvelrnd 6360 |
. . . . . . . 8
|
42 | 41 | nnzd 11481 |
. . . . . . 7
|
43 | 42 | adantr 481 |
. . . . . 6
|
44 | 43 | adantl 482 |
. . . . 5
|
45 | | nnz 11399 |
. . . . . . . . 9
|
46 | 45 | adantr 481 |
. . . . . . . 8
|
47 | 46 | adantl 482 |
. . . . . . 7
|
48 | 47 | adantr 481 |
. . . . . 6
|
49 | 48 | adantl 482 |
. . . . 5
|
50 | 40, 44, 49 | 3jca 1242 |
. . . 4
|
51 | | simpl 473 |
. . . . . . . . . . . . . . . . 17
|
52 | 9 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
53 | 51, 52 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
|
54 | 53 | ex 450 |
. . . . . . . . . . . . . . 15
|
55 | 54 | adantl 482 |
. . . . . . . . . . . . . 14
|
56 | 55 | impcom 446 |
. . . . . . . . . . . . 13
|
57 | 56 | adantl 482 |
. . . . . . . . . . . 12
|
58 | 3, 18, 57 | 3jca 1242 |
. . . . . . . . . . 11
|
59 | 58 | adantr 481 |
. . . . . . . . . 10
|
60 | 13 | adantr 481 |
. . . . . . . . . 10
|
61 | | ralunb 3794 |
. . . . . . . . . . . . 13
|
62 | 61 | simplbi 476 |
. . . . . . . . . . . 12
|
63 | | vsnid 4209 |
. . . . . . . . . . . . . . . . . 18
|
64 | 63 | olci 406 |
. . . . . . . . . . . . . . . . 17
|
65 | | elun 3753 |
. . . . . . . . . . . . . . . . 17
|
66 | 64, 65 | mpbir 221 |
. . . . . . . . . . . . . . . 16
|
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . 15
|
68 | | snssi 4339 |
. . . . . . . . . . . . . . . . . . . 20
|
69 | 68 | ssneld 3605 |
. . . . . . . . . . . . . . . . . . 19
|
70 | 69 | com12 32 |
. . . . . . . . . . . . . . . . . 18
|
71 | 70 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
72 | 71 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
73 | 72 | imp 445 |
. . . . . . . . . . . . . . 15
|
74 | 67, 73 | eldifd 3585 |
. . . . . . . . . . . . . 14
|
75 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
76 | 75 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
77 | 76 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
|
78 | 77 | rspcv 3305 |
. . . . . . . . . . . . . 14
|
79 | 74, 78 | syl 17 |
. . . . . . . . . . . . 13
|
80 | 79 | ralimdva 2962 |
. . . . . . . . . . . 12
|
81 | 62, 80 | syl5 34 |
. . . . . . . . . . 11
|
82 | 81 | imp 445 |
. . . . . . . . . 10
|
83 | | raldifb 3750 |
. . . . . . . . . . . . . . 15
|
84 | | ralunb 3794 |
. . . . . . . . . . . . . . . 16
|
85 | | raldifb 3750 |
. . . . . . . . . . . . . . . . . 18
|
86 | 85 | biimpi 206 |
. . . . . . . . . . . . . . . . 17
|
87 | 86 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
88 | 84, 87 | sylbi 207 |
. . . . . . . . . . . . . . 15
|
89 | 83, 88 | sylbir 225 |
. . . . . . . . . . . . . 14
|
90 | 89 | ralimi 2952 |
. . . . . . . . . . . . 13
|
91 | 90 | adantr 481 |
. . . . . . . . . . . 12
|
92 | 61, 91 | sylbi 207 |
. . . . . . . . . . 11
|
93 | 92 | adantl 482 |
. . . . . . . . . 10
|
94 | | coprmprod 15375 |
. . . . . . . . . . 11
|
95 | 94 | imp 445 |
. . . . . . . . . 10
|
96 | 59, 60, 82, 93, 95 | syl31anc 1329 |
. . . . . . . . 9
|
97 | 96 | ex 450 |
. . . . . . . 8
|
98 | 97 | adantrd 484 |
. . . . . . 7
|
99 | 98 | expimpd 629 |
. . . . . 6
|
100 | 99 | adantr 481 |
. . . . 5
|
101 | 100 | imp 445 |
. . . 4
|
102 | 84 | simplbi 476 |
. . . . . . . . . 10
|
103 | 83, 102 | sylbir 225 |
. . . . . . . . 9
|
104 | 103 | ralimi 2952 |
. . . . . . . 8
|
105 | 104 | adantr 481 |
. . . . . . 7
|
106 | 61, 105 | sylbi 207 |
. . . . . 6
|
107 | | ralunb 3794 |
. . . . . . 7
|
108 | 107 | simplbi 476 |
. . . . . 6
|
109 | 85 | ralbii 2980 |
. . . . . . . 8
|
110 | 109 | anbi1i 731 |
. . . . . . 7
|
111 | 17 | adantl 482 |
. . . . . . . . . . . . 13
|
112 | | simprrl 804 |
. . . . . . . . . . . . 13
|
113 | | simprrr 805 |
. . . . . . . . . . . . 13
|
114 | 111, 112,
113 | jca32 558 |
. . . . . . . . . . . 12
|
115 | | simplr 792 |
. . . . . . . . . . . 12
|
116 | | pm2.27 42 |
. . . . . . . . . . . 12
|
117 | 114, 115,
116 | syl2anc 693 |
. . . . . . . . . . 11
|
118 | 117 | exp31 630 |
. . . . . . . . . 10
|
119 | 118 | com24 95 |
. . . . . . . . 9
|
120 | 119 | imp 445 |
. . . . . . . 8
|
121 | 120 | imp 445 |
. . . . . . 7
|
122 | 110, 121 | syl5bi 232 |
. . . . . 6
|
123 | 106, 108,
122 | syl2ani 688 |
. . . . 5
|
124 | 123 | impr 649 |
. . . 4
|
125 | 22 | breq1d 4663 |
. . . . . . . . 9
|
126 | 125 | rspcv 3305 |
. . . . . . . 8
|
127 | 66, 126 | ax-mp 5 |
. . . . . . 7
|
128 | 127 | adantl 482 |
. . . . . 6
|
129 | 128 | adantl 482 |
. . . . 5
|
130 | 129 | adantl 482 |
. . . 4
|
131 | | coprmdvds2 15368 |
. . . . 5
|
132 | 131 | imp 445 |
. . . 4
|
133 | 50, 101, 124, 130, 132 | syl22anc 1327 |
. . 3
|
134 | 26, 133 | eqbrtrd 4675 |
. 2
|
135 | 134 | exp31 630 |
1
|