# Metamath Proof Explorer

## Theorem nfcprod

Description: Bound-variable hypothesis builder for product: if x is (effectively) not free in A and B , it is not free in prod_ k e. A B . (Contributed by Scott Fenton, 1-Dec-2017)

Ref Expression
Hypotheses nfcprod.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
nfcprod.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
Assertion nfcprod ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\prod _{{k}\in {A}}{B}$

### Proof

Step Hyp Ref Expression
1 nfcprod.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 nfcprod.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
3 df-prod
4 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}ℤ$
5 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{ℤ}_{\ge {m}}$
6 1 5 nfss ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}\subseteq {ℤ}_{\ge {m}}$
7 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\ne 0$
8 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{n}$
9 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}×$
10 1 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{k}\in {A}$
11 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}1$
12 10 2 11 nfif ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}if\left({k}\in {A},{B},1\right)$
13 4 12 nfmpt ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)$
14 8 9 13 nfseq ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)$
15 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}⇝$
16 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{z}$
17 14 15 16 nfbr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{z}$
18 7 17 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({z}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{z}\right)$
19 18 nfex ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{z}\right)$
20 5 19 nfrex ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{z}\right)$
21 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{m}$
22 21 9 13 nfseq ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)$
23 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
24 22 15 23 nfbr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{y}$
25 6 20 24 nf3an ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{z}\right)\wedge seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{y}\right)$
26 4 25 nfrex ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{z}\right)\wedge seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{y}\right)$
27 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}ℕ$
28 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{f}$
29 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left(1\dots {m}\right)$
30 28 29 1 nff1o ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}$
31 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)$
32 31 2 nfcsbw
33 27 32 nfmpt
34 11 9 33 nfseq
35 34 21 nffv
36 35 nfeq2
37 30 36 nfan
38 37 nfex
39 27 38 nfrex
40 26 39 nfor
41 40 nfiotaw
42 3 41 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\prod _{{k}\in {A}}{B}$