dvgrat

	Ref	Expression
Hypotheses	dvgrat.z	$⊢ Z = ℤ_{\geq M}$
	dvgrat.w	$⊢ W = ℤ_{\geq N}$
	dvgrat.n	$⊢ φ \to N \in Z$
	dvgrat.f	$⊢ φ \to F \in V$
	dvgrat.c	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
	dvgrat.n0	$⊢ (φ \land k \in W) \to F (k) \neq 0$
	dvgrat.le	$⊢ (φ \land k \in W) \to \|F (k)\| \leq \|F (k + 1)\|$
Assertion	dvgrat	$⊢ φ \to seq M (+ F) \notin dom ⇝$

Proof

Step	Hyp	Ref	Expression
1		dvgrat.z	$⊢ Z = ℤ_{\geq M}$
2		dvgrat.w	$⊢ W = ℤ_{\geq N}$
3		dvgrat.n	$⊢ φ \to N \in Z$
4		dvgrat.f	$⊢ φ \to F \in V$
5		dvgrat.c	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
6		dvgrat.n0	$⊢ (φ \land k \in W) \to F (k) \neq 0$
7		dvgrat.le	$⊢ (φ \land k \in W) \to \|F (k)\| \leq \|F (k + 1)\|$
8	3 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
9		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
10	8 9	syl	$⊢ φ \to N \in ℤ$
11		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
12	11 2	eleqtrrdi	$⊢ N \in ℤ \to N \in W$
13	10 12	syl	$⊢ φ \to N \in W$
14		simpr	$⊢ (φ \land k = N) \to k = N$
15	14	eleq1d	$⊢ (φ \land k = N) \to (k \in W \leftrightarrow N \in W)$
16	14	fveq2d	$⊢ (φ \land k = N) \to F (k) = F (N)$
17	16	fveq2d	$⊢ (φ \land k = N) \to \|F (k)\| = \|F (N)\|$
18	17	breq2d	$⊢ (φ \land k = N) \to (0 < \|F (k)\| \leftrightarrow 0 < \|F (N)\|)$
19	15 18	imbi12d	$⊢ (φ \land k = N) \to ((k \in W \to 0 < \|F (k)\|) \leftrightarrow (N \in W \to 0 < \|F (N)\|))$
20	2	eleq2i	$⊢ k \in W \leftrightarrow k \in ℤ_{\geq N}$
21	1	uztrn2	$⊢ (N \in Z \land k \in ℤ_{\geq N}) \to k \in Z$
22	20 21	sylan2b	$⊢ (N \in Z \land k \in W) \to k \in Z$
23	3 22	sylan	$⊢ (φ \land k \in W) \to k \in Z$
24	23 5	syldan	$⊢ (φ \land k \in W) \to F (k) \in ℂ$
25		absgt0	$⊢ F (k) \in ℂ \to (F (k) \neq 0 \leftrightarrow 0 < \|F (k)\|)$
26	24 25	syl	$⊢ (φ \land k \in W) \to (F (k) \neq 0 \leftrightarrow 0 < \|F (k)\|)$
27	6 26	mpbid	$⊢ (φ \land k \in W) \to 0 < \|F (k)\|$
28	27	ex	$⊢ φ \to (k \in W \to 0 < \|F (k)\|)$
29	3 19 28	vtocld	$⊢ φ \to (N \in W \to 0 < \|F (N)\|)$
30	13 29	mpd	$⊢ φ \to 0 < \|F (N)\|$
31		0red	$⊢ φ \to 0 \in ℝ$
32	14	eleq1d	$⊢ (φ \land k = N) \to (k \in Z \leftrightarrow N \in Z)$
33	16	eleq1d	$⊢ (φ \land k = N) \to (F (k) \in ℂ \leftrightarrow F (N) \in ℂ)$
34	32 33	imbi12d	$⊢ (φ \land k = N) \to ((k \in Z \to F (k) \in ℂ) \leftrightarrow (N \in Z \to F (N) \in ℂ))$
35	5	ex	$⊢ φ \to (k \in Z \to F (k) \in ℂ)$
36	3 34 35	vtocld	$⊢ φ \to (N \in Z \to F (N) \in ℂ)$
37	3 36	mpd	$⊢ φ \to F (N) \in ℂ$
38	37	abscld	$⊢ φ \to \|F (N)\| \in ℝ$
39	31 38	ltnled	$⊢ φ \to (0 < \|F (N)\| \leftrightarrow \neg \|F (N)\| \leq 0)$
40	30 39	mpbid	$⊢ φ \to \neg \|F (N)\| \leq 0$
41	10	adantr	$⊢ (φ \land F ⇝ 0) \to N \in ℤ$
42	38	adantr	$⊢ (φ \land F ⇝ 0) \to \|F (N)\| \in ℝ$
43		simpr	$⊢ (φ \land F ⇝ 0) \to F ⇝ 0$
44	2	fvexi	$⊢ W \in V$
45	44	mptex	$⊢ (i \in W ⟼ \|F (i)\|) \in V$
46	45	a1i	$⊢ (φ \land F ⇝ 0) \to (i \in W ⟼ \|F (i)\|) \in V$
47	24	adantlr	$⊢ ((φ \land F ⇝ 0) \land k \in W) \to F (k) \in ℂ$
48		eqidd	$⊢ ((φ \land F ⇝ 0) \land k \in W) \to (i \in W ⟼ \|F (i)\|) = (i \in W ⟼ \|F (i)\|)$
49		simpr	$⊢ (((φ \land F ⇝ 0) \land k \in W) \land i = k) \to i = k$
50	49	fveq2d	$⊢ (((φ \land F ⇝ 0) \land k \in W) \land i = k) \to F (i) = F (k)$
51	50	fveq2d	$⊢ (((φ \land F ⇝ 0) \land k \in W) \land i = k) \to \|F (i)\| = \|F (k)\|$
52		simpr	$⊢ ((φ \land F ⇝ 0) \land k \in W) \to k \in W$
53		fvex	$⊢ \|F (k)\| \in V$
54	53	a1i	$⊢ ((φ \land F ⇝ 0) \land k \in W) \to \|F (k)\| \in V$
55	48 51 52 54	fvmptd	$⊢ ((φ \land F ⇝ 0) \land k \in W) \to (i \in W ⟼ \|F (i)\|) (k) = \|F (k)\|$
56	2 43 46 41 47 55	climabs	$⊢ (φ \land F ⇝ 0) \to (i \in W ⟼ \|F (i)\|) ⇝ \|0\|$
57		abs0	$⊢ \|0\| = 0$
58	56 57	breqtrdi	$⊢ (φ \land F ⇝ 0) \to (i \in W ⟼ \|F (i)\|) ⇝ 0$
59	47	abscld	$⊢ ((φ \land F ⇝ 0) \land k \in W) \to \|F (k)\| \in ℝ$
60	55 59	eqeltrd	$⊢ ((φ \land F ⇝ 0) \land k \in W) \to (i \in W ⟼ \|F (i)\|) (k) \in ℝ$
61		2fveq3	$⊢ i = N \to \|F (i)\| = \|F (N)\|$
62	61	breq2d	$⊢ i = N \to (\|F (N)\| \leq \|F (i)\| \leftrightarrow \|F (N)\| \leq \|F (N)\|)$
63	62	imbi2d	$⊢ i = N \to ((φ \to \|F (N)\| \leq \|F (i)\|) \leftrightarrow (φ \to \|F (N)\| \leq \|F (N)\|))$
64		2fveq3	$⊢ i = k \to \|F (i)\| = \|F (k)\|$
65	64	breq2d	$⊢ i = k \to (\|F (N)\| \leq \|F (i)\| \leftrightarrow \|F (N)\| \leq \|F (k)\|)$
66	65	imbi2d	$⊢ i = k \to ((φ \to \|F (N)\| \leq \|F (i)\|) \leftrightarrow (φ \to \|F (N)\| \leq \|F (k)\|))$
67		2fveq3	$⊢ i = k + 1 \to \|F (i)\| = \|F (k + 1)\|$
68	67	breq2d	$⊢ i = k + 1 \to (\|F (N)\| \leq \|F (i)\| \leftrightarrow \|F (N)\| \leq \|F (k + 1)\|)$
69	68	imbi2d	$⊢ i = k + 1 \to ((φ \to \|F (N)\| \leq \|F (i)\|) \leftrightarrow (φ \to \|F (N)\| \leq \|F (k + 1)\|))$
70	38	adantr	$⊢ (φ \land N \in ℤ) \to \|F (N)\| \in ℝ$
71	70	leidd	$⊢ (φ \land N \in ℤ) \to \|F (N)\| \leq \|F (N)\|$
72	71	expcom	$⊢ N \in ℤ \to (φ \to \|F (N)\| \leq \|F (N)\|)$
73	38	ad2antrr	$⊢ ((φ \land k \in W) \land \|F (N)\| \leq \|F (k)\|) \to \|F (N)\| \in ℝ$
74	24	adantr	$⊢ ((φ \land k \in W) \land \|F (N)\| \leq \|F (k)\|) \to F (k) \in ℂ$
75	74	abscld	$⊢ ((φ \land k \in W) \land \|F (N)\| \leq \|F (k)\|) \to \|F (k)\| \in ℝ$
76	2	peano2uzs	$⊢ k \in W \to k + 1 \in W$
77		ovex	$⊢ k + 1 \in V$
78		eleq1	$⊢ i = k + 1 \to (i \in W \leftrightarrow k + 1 \in W)$
79	78	anbi2d	$⊢ i = k + 1 \to ((φ \land i \in W) \leftrightarrow (φ \land k + 1 \in W))$
80		fveq2	$⊢ i = k + 1 \to F (i) = F (k + 1)$
81	80	eleq1d	$⊢ i = k + 1 \to (F (i) \in ℂ \leftrightarrow F (k + 1) \in ℂ)$
82	79 81	imbi12d	$⊢ i = k + 1 \to (((φ \land i \in W) \to F (i) \in ℂ) \leftrightarrow ((φ \land k + 1 \in W) \to F (k + 1) \in ℂ))$
83		eleq1	$⊢ k = i \to (k \in W \leftrightarrow i \in W)$
84	83	anbi2d	$⊢ k = i \to ((φ \land k \in W) \leftrightarrow (φ \land i \in W))$
85		fveq2	$⊢ k = i \to F (k) = F (i)$
86	85	eleq1d	$⊢ k = i \to (F (k) \in ℂ \leftrightarrow F (i) \in ℂ)$
87	84 86	imbi12d	$⊢ k = i \to (((φ \land k \in W) \to F (k) \in ℂ) \leftrightarrow ((φ \land i \in W) \to F (i) \in ℂ))$
88	87 24	chvarvv	$⊢ (φ \land i \in W) \to F (i) \in ℂ$
89	77 82 88	vtocl	$⊢ (φ \land k + 1 \in W) \to F (k + 1) \in ℂ$
90	76 89	sylan2	$⊢ (φ \land k \in W) \to F (k + 1) \in ℂ$
91	90	adantr	$⊢ ((φ \land k \in W) \land \|F (N)\| \leq \|F (k)\|) \to F (k + 1) \in ℂ$
92	91	abscld	$⊢ ((φ \land k \in W) \land \|F (N)\| \leq \|F (k)\|) \to \|F (k + 1)\| \in ℝ$
93		simpr	$⊢ ((φ \land k \in W) \land \|F (N)\| \leq \|F (k)\|) \to \|F (N)\| \leq \|F (k)\|$
94	7	adantr	$⊢ ((φ \land k \in W) \land \|F (N)\| \leq \|F (k)\|) \to \|F (k)\| \leq \|F (k + 1)\|$
95	73 75 92 93 94	letrd	$⊢ ((φ \land k \in W) \land \|F (N)\| \leq \|F (k)\|) \to \|F (N)\| \leq \|F (k + 1)\|$
96	95	ex	$⊢ (φ \land k \in W) \to (\|F (N)\| \leq \|F (k)\| \to \|F (N)\| \leq \|F (k + 1)\|)$
97	20 96	sylan2br	$⊢ (φ \land k \in ℤ_{\geq N}) \to (\|F (N)\| \leq \|F (k)\| \to \|F (N)\| \leq \|F (k + 1)\|)$
98	97	expcom	$⊢ k \in ℤ_{\geq N} \to (φ \to (\|F (N)\| \leq \|F (k)\| \to \|F (N)\| \leq \|F (k + 1)\|))$
99	98	a2d	$⊢ k \in ℤ_{\geq N} \to ((φ \to \|F (N)\| \leq \|F (k)\|) \to (φ \to \|F (N)\| \leq \|F (k + 1)\|))$
100	63 66 69 66 72 99	uzind4	$⊢ k \in ℤ_{\geq N} \to (φ \to \|F (N)\| \leq \|F (k)\|)$
101	100	impcom	$⊢ (φ \land k \in ℤ_{\geq N}) \to \|F (N)\| \leq \|F (k)\|$
102	20 101	sylan2b	$⊢ (φ \land k \in W) \to \|F (N)\| \leq \|F (k)\|$
103	102	adantlr	$⊢ ((φ \land F ⇝ 0) \land k \in W) \to \|F (N)\| \leq \|F (k)\|$
104	103 55	breqtrrd	$⊢ ((φ \land F ⇝ 0) \land k \in W) \to \|F (N)\| \leq (i \in W ⟼ \|F (i)\|) (k)$
105	2 41 42 58 60 104	climlec2	$⊢ (φ \land F ⇝ 0) \to \|F (N)\| \leq 0$
106	40 105	mtand	$⊢ φ \to \neg F ⇝ 0$
107		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
108	8 107	syl	$⊢ φ \to M \in ℤ$
109	108	adantr	$⊢ (φ \land seq M (+ F) \in dom ⇝) \to M \in ℤ$
110	4	adantr	$⊢ (φ \land seq M (+ F) \in dom ⇝) \to F \in V$
111		simpr	$⊢ (φ \land seq M (+ F) \in dom ⇝) \to seq M (+ F) \in dom ⇝$
112	5	adantlr	$⊢ ((φ \land seq M (+ F) \in dom ⇝) \land k \in Z) \to F (k) \in ℂ$
113	1 109 110 111 112	serf0	$⊢ (φ \land seq M (+ F) \in dom ⇝) \to F ⇝ 0$
114	106 113	mtand	$⊢ φ \to \neg seq M (+ F) \in dom ⇝$
115		df-nel	$⊢ seq M (+ F) \notin dom ⇝ \leftrightarrow \neg seq M (+ F) \in dom ⇝$
116	114 115	sylibr	$⊢ φ \to seq M (+ F) \notin dom ⇝$

Metamath Proof Explorer

Theorem dvgrat

Proof