Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fprodsub Unicode version

Theorem fprodsub 25379
 Description: The "difference" (or "quotient") of two finite composites. (Contributed by FL, 14-Sep-2010.) (Revised by Mario Carneiro, 30-May-2014.)
Hypotheses
Ref Expression
fprodsub.1
fprodsub.2
Assertion
Ref Expression
fprodsub
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem fprodsub
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp3 957 . . . . . 6
2 ablogrpo 20951 . . . . . 6
31, 2syl 15 . . . . 5
4 fprodsub.1 . . . . . . 7
54grpocl 20867 . . . . . 6
653expb 1152 . . . . 5
73, 6sylan 457 . . . 4
8 fprodsub.2 . . . . . . 7
94, 8grpodivcl 20914 . . . . . 6
1093expb 1152 . . . . 5
113, 10sylan 457 . . . 4
12 simpl 443 . . . . . . . 8
13 simprll 738 . . . . . . . 8
14 simprlr 739 . . . . . . . 8
15 simprrl 740 . . . . . . . 8
164, 8ablomuldiv 20956 . . . . . . . 8
1712, 13, 14, 15, 16syl13anc 1184 . . . . . . 7
1817oveq1d 5873 . . . . . 6
192adantr 451 . . . . . . . 8
2019, 13, 14, 5syl3anc 1182 . . . . . . 7
21 simprrr 741 . . . . . . 7
224, 8ablodivdiv4 20958 . . . . . . 7
2312, 20, 15, 21, 22syl13anc 1184 . . . . . 6
244, 8grpodivcl 20914 . . . . . . . 8
2519, 13, 15, 24syl3anc 1182 . . . . . . 7
264, 8grpomuldivass 20916 . . . . . . 7
2719, 25, 14, 21, 26syl13anc 1184 . . . . . 6
2818, 23, 273eqtr3rd 2324 . . . . 5
291, 28sylan 457 . . . 4
30 simp1 955 . . . 4
31 simpl 443 . . . . . . . 8
3231ralimi 2618 . . . . . . 7
33323ad2ant2 977 . . . . . 6
34 eqid 2283 . . . . . . 7
3534fmpt 5681 . . . . . 6
3633, 35sylib 188 . . . . 5
37 ffvelrn 5663 . . . . 5
3836, 37sylan 457 . . . 4
39 simpr 447 . . . . . . . 8
4039ralimi 2618 . . . . . . 7
41403ad2ant2 977 . . . . . 6
42 eqid 2283 . . . . . . 7
4342fmpt 5681 . . . . . 6
4441, 43sylib 188 . . . . 5
45 ffvelrn 5663 . . . . 5
4644, 45sylan 457 . . . 4
47 ovex 5883 . . . . . . . . . 10
48 eqid 2283 . . . . . . . . . . 11
4948fvmpt2 5608 . . . . . . . . . 10
5047, 49mpan2 652 . . . . . . . . 9
5150adantr 451 . . . . . . . 8
5234fvmpt2 5608 . . . . . . . . . 10
5342fvmpt2 5608 . . . . . . . . . 10
5452, 53anim12dan 810 . . . . . . . . 9
55 oveq12 5867 . . . . . . . . 9
5654, 55syl 15 . . . . . . . 8
5751, 56eqtr4d 2318 . . . . . . 7
5857ralimiaa 2617 . . . . . 6
59583ad2ant2 977 . . . . 5
60 nfmpt1 4109 . . . . . . . 8
61 nfcv 2419 . . . . . . . 8
6260, 61nffv 5532 . . . . . . 7
63 nfmpt1 4109 . . . . . . . . 9
6463, 61nffv 5532 . . . . . . . 8
65 nfcv 2419 . . . . . . . 8
66 nfmpt1 4109 . . . . . . . . 9
6766, 61nffv 5532 . . . . . . . 8
6864, 65, 67nfov 5881 . . . . . . 7
6962, 68nfeq 2426 . . . . . 6
70 fveq2 5525 . . . . . . 7
71 fveq2 5525 . . . . . . . 8
72 fveq2 5525 . . . . . . . 8
7371, 72oveq12d 5876 . . . . . . 7
7470, 73eqeq12d 2297 . . . . . 6
7569, 74rspc 2878 . . . . 5
7659, 75mpan9 455 . . . 4
777, 11, 29, 30, 38, 46, 76seqcaopr2 11082 . . 3
78 fprodser 25320 . . . 4
80 fprodser 25320 . . . . 5
81 fprodser 25320 . . . . 5
8280, 81oveq12d 5876 . . . 4