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

Theorem fta1lem 22681
 Description: Lemma for fta1 22682. (Contributed by Mario Carneiro, 26-Jul-2014.)
Hypotheses
Ref Expression
fta1.1
fta1.2
fta1.3 Poly
fta1.4 deg
fta1.5
fta1.6 Poly deg deg
Assertion
Ref Expression
fta1lem deg
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem fta1lem
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 fta1.3 . . . . . . . . . 10 Poly
2 eldifsn 4140 . . . . . . . . . 10 Poly Poly
31, 2sylib 196 . . . . . . . . 9 Poly
43simpld 459 . . . . . . . 8 Poly
5 fta1.5 . . . . . . . . . 10
6 plyf 22573 . . . . . . . . . . 11 Poly
7 ffn 5721 . . . . . . . . . . 11
8 fniniseg 5993 . . . . . . . . . . 11
94, 6, 7, 84syl 21 . . . . . . . . . 10
105, 9mpbid 210 . . . . . . . . 9
1110simpld 459 . . . . . . . 8
1210simprd 463 . . . . . . . 8
13 eqid 2443 . . . . . . . . 9
1413facth 22680 . . . . . . . 8 Poly quot
154, 11, 12, 14syl3anc 1229 . . . . . . 7 quot
1615cnveqd 5168 . . . . . 6 quot
1716imaeq1d 5326 . . . . 5 quot
18 cnex 9576 . . . . . . 7
1918a1i 11 . . . . . 6
20 ssid 3508 . . . . . . . . 9
21 ax-1cn 9553 . . . . . . . . 9
22 plyid 22584 . . . . . . . . 9 Poly
2320, 21, 22mp2an 672 . . . . . . . 8 Poly
24 plyconst 22581 . . . . . . . . 9 Poly
2520, 11, 24sylancr 663 . . . . . . . 8 Poly
26 plysubcl 22597 . . . . . . . 8 Poly Poly Poly
2723, 25, 26sylancr 663 . . . . . . 7 Poly
28 plyf 22573 . . . . . . 7 Poly
2927, 28syl 16 . . . . . 6
3013plyremlem 22678 . . . . . . . . . . . 12 Poly deg
3111, 30syl 16 . . . . . . . . . . 11 Poly deg
3231simp2d 1010 . . . . . . . . . 10 deg
33 ax-1ne0 9564 . . . . . . . . . . 11
3433a1i 11 . . . . . . . . . 10
3532, 34eqnetrd 2736 . . . . . . . . 9 deg
36 fveq2 5856 . . . . . . . . . . 11 deg deg
37 dgr0 22637 . . . . . . . . . . 11 deg
3836, 37syl6eq 2500 . . . . . . . . . 10 deg
3938necon3i 2683 . . . . . . . . 9 deg
4035, 39syl 16 . . . . . . . 8
41 quotcl2 22676 . . . . . . . 8 Poly Poly quot Poly
424, 27, 40, 41syl3anc 1229 . . . . . . 7 quot Poly
43 plyf 22573 . . . . . . 7 quot Poly quot
4442, 43syl 16 . . . . . 6 quot
45 ofmulrt 22656 . . . . . 6 quot quot quot
4619, 29, 44, 45syl3anc 1229 . . . . 5 quot quot
4731simp3d 1011 . . . . . 6
4847uneq1d 3642 . . . . 5 quot quot
4917, 46, 483eqtrd 2488 . . . 4 quot
50 fta1.1 . . . 4
51 uncom 3633 . . . 4 quot quot
5249, 50, 513eqtr4g 2509 . . 3 quot
533simprd 463 . . . . . . . . 9
5415eqcomd 2451 . . . . . . . . 9 quot
55 0cnd 9592 . . . . . . . . . . 11
56 mul01 9762 . . . . . . . . . . . 12
5756adantl 466 . . . . . . . . . . 11
5819, 29, 55, 55, 57caofid1 6555 . . . . . . . . . 10
59 df-0p 22055 . . . . . . . . . . 11
6059oveq2i 6292 . . . . . . . . . 10
6158, 60, 593eqtr4g 2509 . . . . . . . . 9
6253, 54, 613netr4d 2748 . . . . . . . 8 quot
63 oveq2 6289 . . . . . . . . 9 quot quot
6463necon3i 2683 . . . . . . . 8 quot quot
6562, 64syl 16 . . . . . . 7 quot
66 eldifsn 4140 . . . . . . 7 quot Poly quot Poly quot
6742, 65, 66sylanbrc 664 . . . . . 6 quot Poly
68 fta1.6 . . . . . 6 Poly deg deg
6921a1i 11 . . . . . . 7
70 dgrcl 22608 . . . . . . . . 9 quot Poly deg quot
7142, 70syl 16 . . . . . . . 8 deg quot
7271nn0cnd 10861 . . . . . . 7 deg quot
73 fta1.2 . . . . . . . 8
7473nn0cnd 10861 . . . . . . 7
75 addcom 9769 . . . . . . . . 9
7621, 74, 75sylancr 663 . . . . . . . 8
7715fveq2d 5860 . . . . . . . . 9 deg deg quot
78 fta1.4 . . . . . . . . 9 deg
79 eqid 2443 . . . . . . . . . . 11 deg deg
80 eqid 2443 . . . . . . . . . . 11 deg quot deg quot
8179, 80dgrmul 22645 . . . . . . . . . 10 Poly quot Poly quot deg quot deg deg quot
8227, 40, 42, 65, 81syl22anc 1230 . . . . . . . . 9 deg quot deg deg quot
8377, 78, 823eqtr3d 2492 . . . . . . . 8 deg deg quot
8432oveq1d 6296 . . . . . . . 8 deg deg quot deg quot
8576, 83, 843eqtrrd 2489 . . . . . . 7 deg quot
8669, 72, 74, 85addcanad 9788 . . . . . 6 deg quot
87 fveq2 5856 . . . . . . . . 9 quot deg deg quot
8887eqeq1d 2445 . . . . . . . 8 quot deg deg quot
89 cnveq 5166 . . . . . . . . . . 11 quot quot
9089imaeq1d 5326 . . . . . . . . . 10 quot quot
9190eleq1d 2512 . . . . . . . . 9 quot quot
9290fveq2d 5860 . . . . . . . . . 10 quot quot
9392, 87breq12d 4450 . . . . . . . . 9 quot deg quot deg quot
9491, 93anbi12d 710 . . . . . . . 8 quot deg quot quot deg quot
9588, 94imbi12d 320 . . . . . . 7 quot deg deg deg quot quot quot deg quot
9695rspcv 3192 . . . . . 6 quot Poly Poly deg deg deg quot quot quot deg quot
9767, 68, 86, 96syl3c 61 . . . . 5 quot quot deg quot
9897simpld 459 . . . 4 quot
99 snfi 7598 . . . 4
100 unfi 7789 . . . 4 quot quot
10198, 99, 100sylancl 662 . . 3 quot
10252, 101eqeltrd 2531 . 2
10352fveq2d 5860 . . 3 quot
104 hashcl 12410 . . . . . 6 quot quot
105101, 104syl 16 . . . . 5 quot
106105nn0red 10860 . . . 4 quot
107 hashcl 12410 . . . . . . 7 quot quot
10898, 107syl 16 . . . . . 6 quot
109108nn0red 10860 . . . . 5 quot
110 peano2re 9756 . . . . 5 quot quot
111109, 110syl 16 . . . 4 quot
112 dgrcl 22608 . . . . . 6 Poly deg
1134, 112syl 16 . . . . 5 deg
114113nn0red 10860 . . . 4 deg
115 hashun2 12433 . . . . . 6 quot quot quot
11698, 99, 115sylancl 662 . . . . 5 quot quot
117 hashsng 12420 . . . . . . 7
11811, 117syl 16 . . . . . 6
119118oveq2d 6297 . . . . 5 quot quot
120116, 119breqtrd 4461 . . . 4 quot quot
12173nn0red 10860 . . . . . 6
122 1red 9614 . . . . . 6
12397simprd 463 . . . . . . 7 quot deg quot
124123, 86breqtrd 4461 . . . . . 6 quot
125109, 121, 122, 124leadd1dd 10173 . . . . 5 quot
126125, 78breqtrrd 4463 . . . 4 quot deg
127106, 111, 114, 120, 126letrd 9742 . . 3 quot deg
128103, 127eqbrtrd 4457 . 2 deg
129102, 128jca 532 1 deg
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3a 974   wceq 1383   wcel 1804   wne 2638  wral 2793  cvv 3095   cdif 3458   cun 3459   wss 3461  csn 4014   class class class wbr 4437   cxp 4987  ccnv 4988  cima 4992   wfn 5573  wf 5574  cfv 5578  (class class class)co 6281   cof 6523  cfn 7518  cc 9493  cr 9494  cc0 9495  c1 9496   caddc 9498   cmul 9500   cle 9632   cmin 9810  cn0 10802  chash 12387  c0p 22054  Polycply 22559  cidp 22560  degcdgr 22562   quot cquot 22664 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-inf2 8061  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572  ax-pre-sup 9573  ax-addf 9574 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-fal 1389  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-se 4829  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-isom 5587  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-of 6525  df-om 6686  df-1st 6785  df-2nd 6786  df-recs 7044  df-rdg 7078  df-1o 7132  df-oadd 7136  df-er 7313  df-map 7424  df-pm 7425  df-en 7519  df-dom 7520  df-sdom 7521  df-fin 7522  df-sup 7903  df-oi 7938  df-card 8323  df-cda 8551  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-div 10214  df-nn 10544  df-2 10601  df-3 10602  df-n0 10803  df-z 10872  df-uz 11093  df-rp 11232  df-fz 11684  df-fzo 11807  df-fl 11911  df-seq 12090  df-exp 12149  df-hash 12388  df-cj 12914  df-re 12915  df-im 12916  df-sqrt 13050  df-abs 13051  df-clim 13293  df-rlim 13294  df-sum 13491  df-0p 22055  df-ply 22563  df-idp 22564  df-coe 22565  df-dgr 22566  df-quot 22665 This theorem is referenced by:  fta1  22682
 Copyright terms: Public domain W3C validator