ntrivcvgmul

Description: The product of two non-trivially converging products converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017)

	Ref	Expression
Hypotheses	ntrivcvgmul.1	$⊢ Z = ℤ_{\geq M}$
	ntrivcvgmul.3	$⊢ φ \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y)$
	ntrivcvgmul.4	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
	ntrivcvgmul.5	$⊢ φ \to \exists m \in Z \exists z (z \neq 0 \land seq m (\times G) ⇝ z)$
	ntrivcvgmul.6	$⊢ (φ \land k \in Z) \to G (k) \in ℂ$
	ntrivcvgmul.7	$⊢ (φ \land k \in Z) \to H (k) = F (k) G (k)$
Assertion	ntrivcvgmul	$⊢ φ \to \exists p \in Z \exists w (w \neq 0 \land seq p (\times H) ⇝ w)$

Proof

Step	Hyp	Ref	Expression
1		ntrivcvgmul.1	$⊢ Z = ℤ_{\geq M}$
2		ntrivcvgmul.3	$⊢ φ \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y)$
3		ntrivcvgmul.4	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
4		ntrivcvgmul.5	$⊢ φ \to \exists m \in Z \exists z (z \neq 0 \land seq m (\times G) ⇝ z)$
5		ntrivcvgmul.6	$⊢ (φ \land k \in Z) \to G (k) \in ℂ$
6		ntrivcvgmul.7	$⊢ (φ \land k \in Z) \to H (k) = F (k) G (k)$
7		exdistrv	$⊢ \exists y \exists z ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z)) \leftrightarrow (\exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land \exists z (z \neq 0 \land seq m (\times G) ⇝ z))$
8	7	2rexbii	$⊢ \exists n \in Z \exists m \in Z \exists y \exists z ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z)) \leftrightarrow \exists n \in Z \exists m \in Z (\exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land \exists z (z \neq 0 \land seq m (\times G) ⇝ z))$
9		reeanv	$⊢ \exists n \in Z \exists m \in Z (\exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land \exists z (z \neq 0 \land seq m (\times G) ⇝ z)) \leftrightarrow (\exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land \exists m \in Z \exists z (z \neq 0 \land seq m (\times G) ⇝ z))$
10	8 9	bitri	$⊢ \exists n \in Z \exists m \in Z \exists y \exists z ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z)) \leftrightarrow (\exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \land \exists m \in Z \exists z (z \neq 0 \land seq m (\times G) ⇝ z))$
11	2 4 10	sylanbrc	$⊢ φ \to \exists n \in Z \exists m \in Z \exists y \exists z ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))$
12		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
13	1 12	eqsstri	$⊢ Z \subseteq ℤ$
14		simp2l	$⊢ (φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \to n \in Z$
15	13 14	sselid	$⊢ (φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \to n \in ℤ$
16	15	zred	$⊢ (φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \to n \in ℝ$
17		simp2r	$⊢ (φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \to m \in Z$
18	13 17	sselid	$⊢ (φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \to m \in ℤ$
19	18	zred	$⊢ (φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \to m \in ℝ$
20		simpl2l	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land n \leq m) \to n \in Z$
21		simpl2r	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land n \leq m) \to m \in Z$
22		simp3ll	$⊢ (φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \to y \neq 0$
23	22	adantr	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land n \leq m) \to y \neq 0$
24		simp3rl	$⊢ (φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \to z \neq 0$
25	24	adantr	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land n \leq m) \to z \neq 0$
26		simp3lr	$⊢ (φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \to seq n (\times F) ⇝ y$
27	26	adantr	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land n \leq m) \to seq n (\times F) ⇝ y$
28		simp3rr	$⊢ (φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \to seq m (\times G) ⇝ z$
29	28	adantr	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land n \leq m) \to seq m (\times G) ⇝ z$
30		simpl1	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land n \leq m) \to φ$
31	30 3	sylan	$⊢ (((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land n \leq m) \land k \in Z) \to F (k) \in ℂ$
32	30 5	sylan	$⊢ (((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land n \leq m) \land k \in Z) \to G (k) \in ℂ$
33		simpr	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land n \leq m) \to n \leq m$
34	30 6	sylan	$⊢ (((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land n \leq m) \land k \in Z) \to H (k) = F (k) G (k)$
35	1 20 21 23 25 27 29 31 32 33 34	ntrivcvgmullem	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land n \leq m) \to \exists p \in Z \exists w (w \neq 0 \land seq p (\times H) ⇝ w)$
36		simpl2r	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land m \leq n) \to m \in Z$
37		simpl2l	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land m \leq n) \to n \in Z$
38	24	adantr	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land m \leq n) \to z \neq 0$
39	22	adantr	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land m \leq n) \to y \neq 0$
40	28	adantr	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land m \leq n) \to seq m (\times G) ⇝ z$
41	26	adantr	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land m \leq n) \to seq n (\times F) ⇝ y$
42		simpl1	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land m \leq n) \to φ$
43	42 5	sylan	$⊢ (((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land m \leq n) \land k \in Z) \to G (k) \in ℂ$
44	42 3	sylan	$⊢ (((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land m \leq n) \land k \in Z) \to F (k) \in ℂ$
45		simpr	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land m \leq n) \to m \leq n$
46	3 5	mulcomd	$⊢ (φ \land k \in Z) \to F (k) G (k) = G (k) F (k)$
47	6 46	eqtrd	$⊢ (φ \land k \in Z) \to H (k) = G (k) F (k)$
48	42 47	sylan	$⊢ (((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land m \leq n) \land k \in Z) \to H (k) = G (k) F (k)$
49	1 36 37 38 39 40 41 43 44 45 48	ntrivcvgmullem	$⊢ ((φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \land m \leq n) \to \exists p \in Z \exists w (w \neq 0 \land seq p (\times H) ⇝ w)$
50	16 19 35 49	lecasei	$⊢ (φ \land (n \in Z \land m \in Z) \land ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z))) \to \exists p \in Z \exists w (w \neq 0 \land seq p (\times H) ⇝ w)$
51	50	3expia	$⊢ (φ \land (n \in Z \land m \in Z)) \to (((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z)) \to \exists p \in Z \exists w (w \neq 0 \land seq p (\times H) ⇝ w))$
52	51	exlimdvv	$⊢ (φ \land (n \in Z \land m \in Z)) \to (\exists y \exists z ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z)) \to \exists p \in Z \exists w (w \neq 0 \land seq p (\times H) ⇝ w))$
53	52	rexlimdvva	$⊢ φ \to (\exists n \in Z \exists m \in Z \exists y \exists z ((y \neq 0 \land seq n (\times F) ⇝ y) \land (z \neq 0 \land seq m (\times G) ⇝ z)) \to \exists p \in Z \exists w (w \neq 0 \land seq p (\times H) ⇝ w))$
54	11 53	mpd	$⊢ φ \to \exists p \in Z \exists w (w \neq 0 \land seq p (\times H) ⇝ w)$

Metamath Proof Explorer

Theorem ntrivcvgmul

Proof