fprodntriv

Description: A non-triviality lemma for finite sequences. (Contributed by Scott Fenton, 16-Dec-2017)

	Ref	Expression
Hypotheses	fprodntriv.1	$⊢ Z = ℤ_{\geq M}$
	fprodntriv.2	$⊢ φ \to N \in Z$
	fprodntriv.3	$⊢ φ \to A \subseteq (M \dots N)$
Assertion	fprodntriv	$⊢ φ \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ y)$

Proof

Step	Hyp	Ref	Expression
1		fprodntriv.1	$⊢ Z = ℤ_{\geq M}$
2		fprodntriv.2	$⊢ φ \to N \in Z$
3		fprodntriv.3	$⊢ φ \to A \subseteq (M \dots N)$
4	2 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
5		peano2uz	$⊢ N \in ℤ_{\geq M} \to N + 1 \in ℤ_{\geq M}$
6	4 5	syl	$⊢ φ \to N + 1 \in ℤ_{\geq M}$
7	6 1	eleqtrrdi	$⊢ φ \to N + 1 \in Z$
8		ax-1ne0	$⊢ 1 \neq 0$
9		eqid	$⊢ ℤ_{\geq (N + 1)} = ℤ_{\geq (N + 1)}$
10		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
11	10 1	eleq2s	$⊢ N \in Z \to N \in ℤ$
12	2 11	syl	$⊢ φ \to N \in ℤ$
13	12	peano2zd	$⊢ φ \to N + 1 \in ℤ$
14		seqex	$⊢ seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) \in V$
15	14	a1i	$⊢ φ \to seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) \in V$
16		1cnd	$⊢ φ \to 1 \in ℂ$
17		simpr	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to n \in ℤ_{\geq (N + 1)}$
18	3	ad2antrr	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to A \subseteq (M \dots N)$
19	12	ad2antrr	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to N \in ℤ$
20	19	zred	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to N \in ℝ$
21	19	peano2zd	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to N + 1 \in ℤ$
22	21	zred	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to N + 1 \in ℝ$
23		elfzelz	$⊢ m \in (N + 1 \dots n) \to m \in ℤ$
24	23	adantl	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to m \in ℤ$
25	24	zred	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to m \in ℝ$
26	20	ltp1d	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to N < N + 1$
27		elfzle1	$⊢ m \in (N + 1 \dots n) \to N + 1 \leq m$
28	27	adantl	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to N + 1 \leq m$
29	20 22 25 26 28	ltletrd	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to N < m$
30	20 25	ltnled	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to (N < m \leftrightarrow \neg m \leq N)$
31	29 30	mpbid	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to \neg m \leq N$
32	31	intnand	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to \neg (M \leq m \land m \leq N)$
33	32	intnand	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to \neg ((M \in ℤ \land N \in ℤ \land m \in ℤ) \land (M \leq m \land m \leq N))$
34		elfz2	$⊢ m \in (M \dots N) \leftrightarrow ((M \in ℤ \land N \in ℤ \land m \in ℤ) \land (M \leq m \land m \leq N))$
35	33 34	sylnibr	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to \neg m \in (M \dots N)$
36	18 35	ssneldd	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to \neg m \in A$
37	36	iffalsed	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to if (m \in A, ⦋ m / k ⦌ B, 1) = 1$
38		fzssuz	$⊢ (N + 1 \dots n) \subseteq ℤ_{\geq (N + 1)}$
39	6	adantr	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to N + 1 \in ℤ_{\geq M}$
40		uzss	$⊢ N + 1 \in ℤ_{\geq M} \to ℤ_{\geq (N + 1)} \subseteq ℤ_{\geq M}$
41	39 40	syl	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to ℤ_{\geq (N + 1)} \subseteq ℤ_{\geq M}$
42	41 1	sseqtrrdi	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to ℤ_{\geq (N + 1)} \subseteq Z$
43	38 42	sstrid	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to (N + 1 \dots n) \subseteq Z$
44	43	sselda	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to m \in Z$
45		ax-1cn	$⊢ 1 \in ℂ$
46	37 45	eqeltrdi	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to if (m \in A, ⦋ m / k ⦌ B, 1) \in ℂ$
47		nfcv	$⊢ \underline{Ⅎ} k m$
48		nfv	$⊢ Ⅎ k m \in A$
49		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ m / k ⦌ B$
50		nfcv	$⊢ \underline{Ⅎ} k 1$
51	48 49 50	nfif	$⊢ \underline{Ⅎ} k if (m \in A, ⦋ m / k ⦌ B, 1)$
52		eleq1w	$⊢ k = m \to (k \in A \leftrightarrow m \in A)$
53		csbeq1a	$⊢ k = m \to B = ⦋ m / k ⦌ B$
54	52 53	ifbieq1d	$⊢ k = m \to if (k \in A, B, 1) = if (m \in A, ⦋ m / k ⦌ B, 1)$
55		eqid	$⊢ (k \in Z ⟼ if (k \in A, B, 1)) = (k \in Z ⟼ if (k \in A, B, 1))$
56	47 51 54 55	fvmptf	$⊢ (m \in Z \land if (m \in A, ⦋ m / k ⦌ B, 1) \in ℂ) \to (k \in Z ⟼ if (k \in A, B, 1)) (m) = if (m \in A, ⦋ m / k ⦌ B, 1)$
57	44 46 56	syl2anc	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to (k \in Z ⟼ if (k \in A, B, 1)) (m) = if (m \in A, ⦋ m / k ⦌ B, 1)$
58		elfzuz	$⊢ m \in (N + 1 \dots n) \to m \in ℤ_{\geq (N + 1)}$
59	58	adantl	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to m \in ℤ_{\geq (N + 1)}$
60		1ex	$⊢ 1 \in V$
61	60	fvconst2	$⊢ m \in ℤ_{\geq (N + 1)} \to (ℤ_{\geq (N + 1)} \times \{1\}) (m) = 1$
62	59 61	syl	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to (ℤ_{\geq (N + 1)} \times \{1\}) (m) = 1$
63	37 57 62	3eqtr4d	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land m \in (N + 1 \dots n)) \to (k \in Z ⟼ if (k \in A, B, 1)) (m) = (ℤ_{\geq (N + 1)} \times \{1\}) (m)$
64	17 63	seqfveq	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) (n) = seq (N + 1) (\times (ℤ_{\geq (N + 1)} \times \{1\})) (n)$
65	9	prodf1	$⊢ n \in ℤ_{\geq (N + 1)} \to seq (N + 1) (\times (ℤ_{\geq (N + 1)} \times \{1\})) (n) = 1$
66	65	adantl	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to seq (N + 1) (\times (ℤ_{\geq (N + 1)} \times \{1\})) (n) = 1$
67	64 66	eqtrd	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) (n) = 1$
68	9 13 15 16 67	climconst	$⊢ φ \to seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ 1$
69		neeq1	$⊢ y = 1 \to (y \neq 0 \leftrightarrow 1 \neq 0)$
70		breq2	$⊢ y = 1 \to (seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ y \leftrightarrow seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ 1)$
71	69 70	anbi12d	$⊢ y = 1 \to ((y \neq 0 \land seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ y) \leftrightarrow (1 \neq 0 \land seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ 1))$
72	60 71	spcev	$⊢ (1 \neq 0 \land seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ 1) \to \exists y (y \neq 0 \land seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ y)$
73	8 68 72	sylancr	$⊢ φ \to \exists y (y \neq 0 \land seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ y)$
74		seqeq1	$⊢ n = N + 1 \to seq n (\times (k \in Z ⟼ if (k \in A, B, 1))) = seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1)))$
75	74	breq1d	$⊢ n = N + 1 \to (seq n (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ y \leftrightarrow seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ y)$
76	75	anbi2d	$⊢ n = N + 1 \to ((y \neq 0 \land seq n (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ y) \leftrightarrow (y \neq 0 \land seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ y))$
77	76	exbidv	$⊢ n = N + 1 \to (\exists y (y \neq 0 \land seq n (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ y) \leftrightarrow \exists y (y \neq 0 \land seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ y))$
78	77	rspcev	$⊢ (N + 1 \in Z \land \exists y (y \neq 0 \land seq (N + 1) (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ y)) \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ y)$
79	7 73 78	syl2anc	$⊢ φ \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times (k \in Z ⟼ if (k \in A, B, 1))) ⇝ y)$

Metamath Proof Explorer

Theorem fprodntriv

Proof