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

Theorem fprodconst 13934
 Description: The product of constant terms ( is not free in .) (Contributed by Scott Fenton, 12-Jan-2018.)
Assertion
Ref Expression
fprodconst
Distinct variable groups:   ,   ,

Proof of Theorem fprodconst
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 exp0 12214 . . . . 5
21eqcomd 2410 . . . 4
3 prodeq1 13868 . . . . . 6
4 prod0 13902 . . . . . 6
53, 4syl6eq 2459 . . . . 5
6 fveq2 5849 . . . . . . 7
7 hash0 12485 . . . . . . 7
86, 7syl6eq 2459 . . . . . 6
98oveq2d 6294 . . . . 5
105, 9eqeq12d 2424 . . . 4
112, 10syl5ibrcom 222 . . 3
13 eqidd 2403 . . . . . . 7
14 simprl 756 . . . . . . 7
15 simprr 758 . . . . . . 7
16 simpllr 761 . . . . . . 7
17 simpllr 761 . . . . . . . 8
18 elfznn 11768 . . . . . . . . 9
1918adantl 464 . . . . . . . 8
20 fvconst2g 6105 . . . . . . . 8
2117, 19, 20syl2anc 659 . . . . . . 7
2213, 14, 15, 16, 21fprod 13900 . . . . . 6
23 expnnval 12213 . . . . . . 7
2423ad2ant2lr 746 . . . . . 6
2522, 24eqtr4d 2446 . . . . 5
2625expr 613 . . . 4
2726exlimdv 1745 . . 3
2827expimpd 601 . 2
29 fz1f1o 13681 . . 3