MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  phimullem Unicode version

Theorem phimullem 14309
Description: Lemma for phimul 14310. (Contributed by Mario Carneiro, 24-Feb-2014.)
Hypotheses
Ref Expression
crt.1
crt.2
crt.3
crt.4
phimul.4
phimul.5
phimul.6
Assertion
Ref Expression
phimullem
Distinct variable groups:   ,   , ,M   , ,   ,S,   ,   ,N,

Proof of Theorem phimullem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 phimul.4 . . . . 5
2 fzofi 12084 . . . . . 6
3 ssrab2 3584 . . . . . 6
4 ssfi 7760 . . . . . 6
52, 3, 4mp2an 672 . . . . 5
61, 5eqeltri 2541 . . . 4
7 phimul.5 . . . . 5
8 fzofi 12084 . . . . . 6
9 ssrab2 3584 . . . . . 6
10 ssfi 7760 . . . . . 6
118, 9, 10mp2an 672 . . . . 5
127, 11eqeltri 2541 . . . 4
13 hashxp 12492 . . . 4
146, 12, 13mp2an 672 . . 3
15 oveq1 6303 . . . . . . . . . . . . . 14
1615eqeq1d 2459 . . . . . . . . . . . . 13
17 phimul.6 . . . . . . . . . . . . 13
1816, 17elrab2 3259 . . . . . . . . . . . 12
1918simplbi 460 . . . . . . . . . . 11
20 oveq1 6303 . . . . . . . . . . . . 13
21 oveq1 6303 . . . . . . . . . . . . 13
2220, 21opeq12d 4225 . . . . . . . . . . . 12
23 crt.3 . . . . . . . . . . . 12
24 opex 4716 . . . . . . . . . . . 12
2522, 23, 24fvmpt 5956 . . . . . . . . . . 11
2619, 25syl 16 . . . . . . . . . 10
2726adantl 466 . . . . . . . . 9
28 crt.1 . . . . . . . . . . . . . . 15
2919, 28syl6eleq 2555 . . . . . . . . . . . . . 14
3029adantl 466 . . . . . . . . . . . . 13
31 elfzoelz 11829 . . . . . . . . . . . . 13
3230, 31syl 16 . . . . . . . . . . . 12
33 crt.4 . . . . . . . . . . . . . 14
3433simp1d 1008 . . . . . . . . . . . . 13
3534adantr 465 . . . . . . . . . . . 12
36 zmodfzo 12018 . . . . . . . . . . . 12
3732, 35, 36syl2anc 661 . . . . . . . . . . 11
38 modgcd 14174 . . . . . . . . . . . . 13
3932, 35, 38syl2anc 661 . . . . . . . . . . . 12
4035nnzd 10993 . . . . . . . . . . . . . . . . 17
41 gcddvds 14153 . . . . . . . . . . . . . . . . 17
4232, 40, 41syl2anc 661 . . . . . . . . . . . . . . . 16
4342simpld 459 . . . . . . . . . . . . . . 15
4442simprd 463 . . . . . . . . . . . . . . . 16
4533simp2d 1009 . . . . . . . . . . . . . . . . . . 19
4645adantr 465 . . . . . . . . . . . . . . . . . 18
4746nnzd 10993 . . . . . . . . . . . . . . . . 17
48 dvdsmul1 14005 . . . . . . . . . . . . . . . . 17
4940, 47, 48syl2anc 661 . . . . . . . . . . . . . . . 16
50 nnne0 10593 . . . . . . . . . . . . . . . . . . . 20
51 simpr 461 . . . . . . . . . . . . . . . . . . . . 21
5251necon3ai 2685 . . . . . . . . . . . . . . . . . . . 20
5335, 50, 523syl 20 . . . . . . . . . . . . . . . . . . 19
54 gcdn0cl 14152 . . . . . . . . . . . . . . . . . . 19
5532, 40, 53, 54syl21anc 1227 . . . . . . . . . . . . . . . . . 18
5655nnzd 10993 . . . . . . . . . . . . . . . . 17
5735, 46nnmulcld 10608 . . . . . . . . . . . . . . . . . 18
5857nnzd 10993 . . . . . . . . . . . . . . . . 17
59 dvdstr 14018 . . . . . . . . . . . . . . . . 17
6056, 40, 58, 59syl3anc 1228 . . . . . . . . . . . . . . . 16
6144, 49, 60mp2and 679 . . . . . . . . . . . . . . 15
62 nnne0 10593 . . . . . . . . . . . . . . . . 17
63 simpr 461 . . . . . . . . . . . . . . . . . 18
6463necon3ai 2685 . . . . . . . . . . . . . . . . 17
6557, 62, 643syl 20 . . . . . . . . . . . . . . . 16
66 dvdslegcd 14154 . . . . . . . . . . . . . . . 16
6756, 32, 58, 65, 66syl31anc 1231 . . . . . . . . . . . . . . 15
6843, 61, 67mp2and 679 . . . . . . . . . . . . . 14
6918simprbi 464 . . . . . . . . . . . . . . 15
7069adantl 466 . . . . . . . . . . . . . 14
7168, 70breqtrd 4476 . . . . . . . . . . . . 13
72 nnle1eq1 10589 . . . . . . . . . . . . . 14
7355, 72syl 16 . . . . . . . . . . . . 13
7471, 73mpbid 210 . . . . . . . . . . . 12
7539, 74eqtrd 2498 . . . . . . . . . . 11
76 oveq1 6303 . . . . . . . . . . . . 13
7776eqeq1d 2459 . . . . . . . . . . . 12
7877, 1elrab2 3259 . . . . . . . . . . 11
7937, 75, 78sylanbrc 664 . . . . . . . . . 10
80 zmodfzo 12018 . . . . . . . . . . . 12
8132, 46, 80syl2anc 661 . . . . . . . . . . 11
82 modgcd 14174 . . . . . . . . . . . . 13
8332, 46, 82syl2anc 661 . . . . . . . . . . . 12
84 gcddvds 14153 . . . . . . . . . . . . . . . . 17
8532, 47, 84syl2anc 661 . . . . . . . . . . . . . . . 16
8685simpld 459 . . . . . . . . . . . . . . 15
8785simprd 463 . . . . . . . . . . . . . . . 16
88 dvdsmul2 14006 . . . . . . . . . . . . . . . . 17
8940, 47, 88syl2anc 661 . . . . . . . . . . . . . . . 16
90 nnne0 10593 . . . . . . . . . . . . . . . . . . . 20
91 simpr 461 . . . . . . . . . . . . . . . . . . . . 21
9291necon3ai 2685 . . . . . . . . . . . . . . . . . . . 20
9346, 90, 923syl 20 . . . . . . . . . . . . . . . . . . 19
94 gcdn0cl 14152 . . . . . . . . . . . . . . . . . . 19
9532, 47, 93, 94syl21anc 1227 . . . . . . . . . . . . . . . . . 18
9695nnzd 10993 . . . . . . . . . . . . . . . . 17
97 dvdstr 14018 . . . . . . . . . . . . . . . . 17
9896, 47, 58, 97syl3anc 1228 . . . . . . . . . . . . . . . 16
9987, 89, 98mp2and 679 . . . . . . . . . . . . . . 15
100 dvdslegcd 14154 . . . . . . . . . . . . . . . 16
10196, 32, 58, 65, 100syl31anc 1231 . . . . . . . . . . . . . . 15
10286, 99, 101mp2and 679 . . . . . . . . . . . . . 14
103102, 70breqtrd 4476 . . . . . . . . . . . . 13
104 nnle1eq1 10589 . . . . . . . . . . . . . 14
10595, 104syl 16 . . . . . . . . . . . . 13
106103, 105mpbid 210 . . . . . . . . . . . 12
10783, 106eqtrd 2498 . . . . . . . . . . 11
108 oveq1 6303 . . . . . . . . . . . . 13
109108eqeq1d 2459 . . . . . . . . . . . 12
110109, 7elrab2 3259 . . . . . . . . . . 11
11181, 107, 110sylanbrc 664 . . . . . . . . . 10
112 opelxpi 5036 . . . . . . . . . 10
11379, 111, 112syl2anc 661 . . . . . . . . 9
11427, 113eqeltrd 2545 . . . . . . . 8
115114ralrimiva 2871 . . . . . . 7
116 crt.2 . . . . . . . . . 10
11728, 116, 23, 33crt 14308 . . . . . . . . 9
118 f1ofn 5822 . . . . . . . . 9
119 fnfun 5683 . . . . . . . . 9
120117, 118, 1193syl 20 . . . . . . . 8
121 ssrab2 3584 . . . . . . . . . 10
12217, 121eqsstri 3533 . . . . . . . . 9
123 fndm 5685 . . . . . . . . . 10
124117, 118, 1233syl 20 . . . . . . . . 9
125122, 124syl5sseqr 3552 . . . . . . . 8
126 funimass4 5924 . . . . . . . 8
127120, 125, 126syl2anc 661 . . . . . . 7
128115, 127mpbird 232 . . . . . 6
1291, 3eqsstri 3533 . . . . . . . . . . . . 13
1307, 9eqsstri 3533 . . . . . . . . . . . . 13
131 xpss12 5113 . . . . . . . . . . . . 13
132129, 130, 131mp2an 672 . . . . . . . . . . . 12
133132, 116sseqtr4i 3536 . . . . . . . . . . 11
134133sseli 3499 . . . . . . . . . 10
135 f1ocnvfv2 6183 . . . . . . . . . 10
136117, 134, 135syl2an 477 . . . . . . . . 9
137 f1ocnv 5833 . . . . . . . . . . . . 13
138 f1of 5821 . . . . . . . . . . . . 13
139117, 137, 1383syl 20 . . . . . . . . . . . 12
140 ffvelrn 6029 . . . . . . . . . . . 12
141139, 134, 140syl2an 477 . . . . . . . . . . 11
142141, 28syl6eleq 2555 . . . . . . . . . . . . . . 15
143 elfzoelz 11829 . . . . . . . . . . . . . . 15
144142, 143syl 16 . . . . . . . . . . . . . 14
14534adantr 465 . . . . . . . . . . . . . 14
146 modgcd 14174 . . . . . . . . . . . . . 14
147144, 145, 146syl2anc 661 . . . . . . . . . . . . 13
148 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . 22
149 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . 22
150148, 149opeq12d 4225 . . . . . . . . . . . . . . . . . . . . 21
15122cbvmptv 4543 . . . . . . . . . . . . . . . . . . . . . 22
15223, 151eqtri 2486 . . . . . . . . . . . . . . . . . . . . 21
153 opex 4716 . . . . . . . . . . . . . . . . . . . . 21
154150, 152, 153fvmpt 5956 . . . . . . . . . . . . . . . . . . . 20
155141, 154syl 16 . . . . . . . . . . . . . . . . . . 19
156136, 155eqtr3d 2500 . . . . . . . . . . . . . . . . . 18
157 simpr 461 . . . . . . . . . . . . . . . . . 18
158156, 157eqeltrrd 2546 . . . . . . . . . . . . . . . . 17
159 opelxp 5034 . . . . . . . . . . . . . . . . 17
160158, 159sylib 196 . . . . . . . . . . . . . . . 16
161160simpld 459 . . . . . . . . . . . . . . 15
162 oveq1 6303 . . . . . . . . . . . . . . . . 17
163162eqeq1d 2459 . . . . . . . . . . . . . . . 16
164163, 1elrab2 3259 . . . . . . . . . . . . . . 15
165161, 164sylib 196 . . . . . . . . . . . . . 14
166165simprd 463 . . . . . . . . . . . . 13
167147, 166eqtr3d 2500 . . . . . . . . . . . 12
16845adantr 465 . . . . . . . . . . . . . 14
169 modgcd 14174 . . . . . . . . . . . . . 14
170144, 168, 169syl2anc 661 . . . . . . . . . . . . 13
171160simprd 463 . . . . . . . . . . . . . . 15
172 oveq1 6303 . . . . . . . . . . . . . . . . 17
173172eqeq1d 2459 . . . . . . . . . . . . . . . 16
174173, 7elrab2 3259 . . . . . . . . . . . . . . 15
175171, 174sylib 196 . . . . . . . . . . . . . 14
176175simprd 463 . . . . . . . . . . . . 13
177170, 176eqtr3d 2500 . . . . . . . . . . . 12
17834nnzd 10993 . . . . . . . . . . . . . 14
179178adantr 465 . . . . . . . . . . . . 13
18045nnzd 10993 . . . . . . . . . . . . . 14
181180adantr 465 . . . . . . . . . . . . 13
182 rpmul 14264 . . . . . . . . . . . . 13
183144, 179, 181, 182syl3anc 1228 . . . . . . . . . . . 12
184167, 177, 183mp2and 679 . . . . . . . . . . 11
185 oveq1 6303 . . . . . . . . . . . . 13
186185eqeq1d 2459 . . . . . . . . . . . 12
187186, 17elrab2 3259 . . . . . . . . . . 11
188141, 184, 187sylanbrc 664 . . . . . . . . . 10
189 funfvima2 6148 . . . . . . . . . . . 12
190120, 125, 189syl2anc 661 . . . . . . . . . . 11
191190imp 429 . . . . . . . . . 10
192188, 191syldan 470 . . . . . . . . 9
193136, 192eqeltrrd 2546 . . . . . . . 8
194193ex 434 . . . . . . 7
195194ssrdv 3509 . . . . . 6
196128, 195eqssd 3520 . . . . 5
197 f1of1 5820 . . . . . . 7
198117, 197syl 16 . . . . . 6
199 fzofi 12084 . . . . . . . . . 10
20028, 199eqeltri 2541 . . . . . . . . 9
201 ssfi 7760 . . . . . . . . 9
202200, 122, 201mp2an 672 . . . . . . . 8
203202elexi 3119 . . . . . . 7
204203f1imaen 7597 . . . . . 6
205198, 122, 204sylancl 662 . . . . 5
206196, 205eqbrtrrd 4474 . . . 4
207 xpfi 7811 . . . . . 6
2086, 12, 207mp2an 672 . . . . 5
209 hashen 12420 . . . . 5
210208, 202, 209mp2an 672 . . . 4
211206, 210sylibr 212 . . 3
21214, 211syl5reqr 2513 . 2
21334, 45nnmulcld 10608 . . 3
214 dfphi2 14304 . . . 4
215 rabeq 3103 . . . . . . 7
21628, 215ax-mp 5 . . . . . 6
21717, 216eqtri 2486 . . . . 5
218217fveq2i 5874 . . . 4
219214, 218syl6eqr 2516 . . 3
220213, 219syl 16 . 2
221 dfphi2 14304 . . . . 5
2221fveq2i 5874 . . . . 5
223221, 222syl6eqr 2516 . . . 4
22434, 223syl 16 . . 3
225 dfphi2 14304 . . . . 5
2267fveq2i 5874 . . . . 5
227225, 226syl6eqr 2516 . . . 4
22845, 227syl 16 . . 3
229224, 228oveq12d 6314 . 2
230212, 220, 2293eqtr4d 2508 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  /\w3a 973  =wceq 1395  e.wcel 1818  =/=wne 2652  A.wral 2807  {crab 2811  C_wss 3475  <.cop 4035   class class class wbr 4452  e.cmpt 4510  X.cxp 5002  `'ccnv 5003  domcdm 5004  "cima 5007  Funwfun 5587  Fnwfn 5588  -->wf 5589  -1-1->wf1 5590  -1-1-onto->wf1o 5592  `cfv 5593  (class class class)co 6296   cen 7533   cfn 7536  0cc0 9513  1c1 9514   cmul 9518   cle 9650   cn 10561   cz 10889   cfzo 11824   cmo 11996   chash 12405   cdvds 13986   cgcd 14144   cphi 14294
This theorem is referenced by:  phimul  14310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-cnex 9569  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589  ax-pre-mulgt0 9590  ax-pre-sup 9591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-int 4287  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-1st 6800  df-2nd 6801  df-recs 7061  df-rdg 7095  df-1o 7149  df-oadd 7153  df-er 7330  df-map 7441  df-en 7537  df-dom 7538  df-sdom 7539  df-fin 7540  df-sup 7921  df-card 8341  df-cda 8569  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831  df-div 10232  df-nn 10562  df-2 10619  df-3 10620  df-n0 10821  df-z 10890  df-uz 11111  df-rp 11250  df-fz 11702  df-fzo 11825  df-fl 11929  df-mod 11997  df-seq 12108  df-exp 12167  df-hash 12406  df-cj 12932  df-re 12933  df-im 12934  df-sqrt 13068  df-abs 13069  df-dvds 13987  df-gcd 14145  df-phi 14296
  Copyright terms: Public domain W3C validator