ntrivcvgmullem

	Ref	Expression
Hypotheses	ntrivcvgmullem.1	$⊢ Z = ℤ_{\geq M}$
	ntrivcvgmullem.2	$⊢ φ \to N \in Z$
	ntrivcvgmullem.3	$⊢ φ \to P \in Z$
	ntrivcvgmullem.4	$⊢ φ \to X \neq 0$
	ntrivcvgmullem.5	$⊢ φ \to Y \neq 0$
	ntrivcvgmullem.6	$⊢ φ \to seq N (\times F) ⇝ X$
	ntrivcvgmullem.7	$⊢ φ \to seq P (\times G) ⇝ Y$
	ntrivcvgmullem.8	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
	ntrivcvgmullem.9	$⊢ (φ \land k \in Z) \to G (k) \in ℂ$
	ntrivcvgmullem.a	$⊢ φ \to N \leq P$
	ntrivcvgmullem.b	$⊢ (φ \land k \in Z) \to H (k) = F (k) G (k)$
Assertion	ntrivcvgmullem	$⊢ φ \to \exists q \in Z \exists w (w \neq 0 \land seq q (\times H) ⇝ w)$

Proof

Step	Hyp	Ref	Expression
1		ntrivcvgmullem.1	$⊢ Z = ℤ_{\geq M}$
2		ntrivcvgmullem.2	$⊢ φ \to N \in Z$
3		ntrivcvgmullem.3	$⊢ φ \to P \in Z$
4		ntrivcvgmullem.4	$⊢ φ \to X \neq 0$
5		ntrivcvgmullem.5	$⊢ φ \to Y \neq 0$
6		ntrivcvgmullem.6	$⊢ φ \to seq N (\times F) ⇝ X$
7		ntrivcvgmullem.7	$⊢ φ \to seq P (\times G) ⇝ Y$
8		ntrivcvgmullem.8	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
9		ntrivcvgmullem.9	$⊢ (φ \land k \in Z) \to G (k) \in ℂ$
10		ntrivcvgmullem.a	$⊢ φ \to N \leq P$
11		ntrivcvgmullem.b	$⊢ (φ \land k \in Z) \to H (k) = F (k) G (k)$
12		eqid	$⊢ ℤ_{\geq N} = ℤ_{\geq N}$
13		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
14	1 13	eqsstri	$⊢ Z \subseteq ℤ$
15	14 2	sseldi	$⊢ φ \to N \in ℤ$
16	14 3	sseldi	$⊢ φ \to P \in ℤ$
17		eluz	$⊢ (N \in ℤ \land P \in ℤ) \to (P \in ℤ_{\geq N} \leftrightarrow N \leq P)$
18	15 16 17	syl2anc	$⊢ φ \to (P \in ℤ_{\geq N} \leftrightarrow N \leq P)$
19	10 18	mpbird	$⊢ φ \to P \in ℤ_{\geq N}$
20	1	uztrn2	$⊢ (N \in Z \land k \in ℤ_{\geq N}) \to k \in Z$
21	2 20	sylan	$⊢ (φ \land k \in ℤ_{\geq N}) \to k \in Z$
22	21 8	syldan	$⊢ (φ \land k \in ℤ_{\geq N}) \to F (k) \in ℂ$
23	12 19 6 4 22	ntrivcvgtail	$⊢ φ \to (⇝ (seq P (\times F)) \neq 0 \land seq P (\times F) ⇝ ⇝ (seq P (\times F)))$
24	23	simprd	$⊢ φ \to seq P (\times F) ⇝ ⇝ (seq P (\times F))$
25		climcl	$⊢ seq P (\times F) ⇝ ⇝ (seq P (\times F)) \to ⇝ (seq P (\times F)) \in ℂ$
26	24 25	syl	$⊢ φ \to ⇝ (seq P (\times F)) \in ℂ$
27		climcl	$⊢ seq P (\times G) ⇝ Y \to Y \in ℂ$
28	7 27	syl	$⊢ φ \to Y \in ℂ$
29	23	simpld	$⊢ φ \to ⇝ (seq P (\times F)) \neq 0$
30	26 28 29 5	mulne0d	$⊢ φ \to ⇝ (seq P (\times F)) Y \neq 0$
31		eqid	$⊢ ℤ_{\geq P} = ℤ_{\geq P}$
32		seqex	$⊢ seq P (\times H) \in V$
33	32	a1i	$⊢ φ \to seq P (\times H) \in V$
34	1	uztrn2	$⊢ (P \in Z \land k \in ℤ_{\geq P}) \to k \in Z$
35	3 34	sylan	$⊢ (φ \land k \in ℤ_{\geq P}) \to k \in Z$
36	35 8	syldan	$⊢ (φ \land k \in ℤ_{\geq P}) \to F (k) \in ℂ$
37	31 16 36	prodf	$⊢ φ \to seq P (\times F) : ℤ_{\geq P} ⟶ ℂ$
38	37	ffvelrnda	$⊢ (φ \land j \in ℤ_{\geq P}) \to seq P (\times F) (j) \in ℂ$
39	35 9	syldan	$⊢ (φ \land k \in ℤ_{\geq P}) \to G (k) \in ℂ$
40	31 16 39	prodf	$⊢ φ \to seq P (\times G) : ℤ_{\geq P} ⟶ ℂ$
41	40	ffvelrnda	$⊢ (φ \land j \in ℤ_{\geq P}) \to seq P (\times G) (j) \in ℂ$
42		simpr	$⊢ (φ \land j \in ℤ_{\geq P}) \to j \in ℤ_{\geq P}$
43		simpll	$⊢ ((φ \land j \in ℤ_{\geq P}) \land k \in (P \dots j)) \to φ$
44	3	adantr	$⊢ (φ \land j \in ℤ_{\geq P}) \to P \in Z$
45		elfzuz	$⊢ k \in (P \dots j) \to k \in ℤ_{\geq P}$
46	44 45 34	syl2an	$⊢ ((φ \land j \in ℤ_{\geq P}) \land k \in (P \dots j)) \to k \in Z$
47	43 46 8	syl2anc	$⊢ ((φ \land j \in ℤ_{\geq P}) \land k \in (P \dots j)) \to F (k) \in ℂ$
48	43 46 9	syl2anc	$⊢ ((φ \land j \in ℤ_{\geq P}) \land k \in (P \dots j)) \to G (k) \in ℂ$
49	43 46 11	syl2anc	$⊢ ((φ \land j \in ℤ_{\geq P}) \land k \in (P \dots j)) \to H (k) = F (k) G (k)$
50	42 47 48 49	prodfmul	$⊢ (φ \land j \in ℤ_{\geq P}) \to seq P (\times H) (j) = seq P (\times F) (j) seq P (\times G) (j)$
51	31 16 24 33 7 38 41 50	climmul	$⊢ φ \to seq P (\times H) ⇝ ⇝ (seq P (\times F)) Y$
52		ovex	$⊢ ⇝ (seq P (\times F)) Y \in V$
53		neeq1	$⊢ w = ⇝ (seq P (\times F)) Y \to (w \neq 0 \leftrightarrow ⇝ (seq P (\times F)) Y \neq 0)$
54		breq2	$⊢ w = ⇝ (seq P (\times F)) Y \to (seq P (\times H) ⇝ w \leftrightarrow seq P (\times H) ⇝ ⇝ (seq P (\times F)) Y)$
55	53 54	anbi12d	$⊢ w = ⇝ (seq P (\times F)) Y \to ((w \neq 0 \land seq P (\times H) ⇝ w) \leftrightarrow (⇝ (seq P (\times F)) Y \neq 0 \land seq P (\times H) ⇝ ⇝ (seq P (\times F)) Y))$
56	52 55	spcev	$⊢ (⇝ (seq P (\times F)) Y \neq 0 \land seq P (\times H) ⇝ ⇝ (seq P (\times F)) Y) \to \exists w (w \neq 0 \land seq P (\times H) ⇝ w)$
57	30 51 56	syl2anc	$⊢ φ \to \exists w (w \neq 0 \land seq P (\times H) ⇝ w)$
58		seqeq1	$⊢ q = P \to seq q (\times H) = seq P (\times H)$
59	58	breq1d	$⊢ q = P \to (seq q (\times H) ⇝ w \leftrightarrow seq P (\times H) ⇝ w)$
60	59	anbi2d	$⊢ q = P \to ((w \neq 0 \land seq q (\times H) ⇝ w) \leftrightarrow (w \neq 0 \land seq P (\times H) ⇝ w))$
61	60	exbidv	$⊢ q = P \to (\exists w (w \neq 0 \land seq q (\times H) ⇝ w) \leftrightarrow \exists w (w \neq 0 \land seq P (\times H) ⇝ w))$
62	61	rspcev	$⊢ (P \in Z \land \exists w (w \neq 0 \land seq P (\times H) ⇝ w)) \to \exists q \in Z \exists w (w \neq 0 \land seq q (\times H) ⇝ w)$
63	3 57 62	syl2anc	$⊢ φ \to \exists q \in Z \exists w (w \neq 0 \land seq q (\times H) ⇝ w)$

Metamath Proof Explorer

Theorem ntrivcvgmullem

Proof