plyeq0lem

Description: Lemma for plyeq0 . If A is the coefficient function for a nonzero polynomial such that P ( z ) = sum_ k e. NN0 A ( k ) x. z ^ k = 0 for every z e. CC and A ( M ) is the nonzero leading coefficient, then the function F ( z ) = P ( z ) / z ^ M is a sum of powers of 1 / z , and so the limit of this function as z ~> +oo is the constant term, A ( M ) . But F ( z ) = 0 everywhere, so this limit is also equal to zero so that A ( M ) = 0 , a contradiction. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Hypotheses	plyeq0.1	$⊢ φ \to S \subseteq ℂ$
	plyeq0.2	$⊢ φ \to N \in ℕ_{0}$
	plyeq0.3	$⊢ φ \to A \in ({(S \cup \{0\})}^{ℕ_{0}})$
	plyeq0.4	$⊢ φ \to A [ℤ_{\geq (N + 1)}] = \{0\}$
	plyeq0.5	$⊢ φ \to 0_{𝑝} = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k})$
	plyeq0.6	$⊢ M = sup (A^{-1} [S ∖ \{0\}] ℝ <)$
	plyeq0.7	$⊢ φ \to A^{-1} [S ∖ \{0\}] \neq \emptyset$
Assertion	plyeq0lem	$⊢ \neg φ$

Proof

Step	Hyp	Ref	Expression
1		plyeq0.1	$⊢ φ \to S \subseteq ℂ$
2		plyeq0.2	$⊢ φ \to N \in ℕ_{0}$
3		plyeq0.3	$⊢ φ \to A \in ({(S \cup \{0\})}^{ℕ_{0}})$
4		plyeq0.4	$⊢ φ \to A [ℤ_{\geq (N + 1)}] = \{0\}$
5		plyeq0.5	$⊢ φ \to 0_{𝑝} = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k})$
6		plyeq0.6	$⊢ M = sup (A^{-1} [S ∖ \{0\}] ℝ <)$
7		plyeq0.7	$⊢ φ \to A^{-1} [S ∖ \{0\}] \neq \emptyset$
8		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
9		1zzd	$⊢ φ \to 1 \in ℤ$
10		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
11		1zzd	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to 1 \in ℤ$
12		0cn	$⊢ 0 \in ℂ$
13	12	a1i	$⊢ φ \to 0 \in ℂ$
14	13	snssd	$⊢ φ \to \{0\} \subseteq ℂ$
15	1 14	unssd	$⊢ φ \to S \cup \{0\} \subseteq ℂ$
16		cnex	$⊢ ℂ \in V$
17		ssexg	$⊢ (S \cup \{0\} \subseteq ℂ \land ℂ \in V) \to S \cup \{0\} \in V$
18	15 16 17	sylancl	$⊢ φ \to S \cup \{0\} \in V$
19		nn0ex	$⊢ ℕ_{0} \in V$
20		elmapg	$⊢ (S \cup \{0\} \in V \land ℕ_{0} \in V) \to (A \in ({(S \cup \{0\})}^{ℕ_{0}}) \leftrightarrow A : ℕ_{0} ⟶ S \cup \{0\})$
21	18 19 20	sylancl	$⊢ φ \to (A \in ({(S \cup \{0\})}^{ℕ_{0}}) \leftrightarrow A : ℕ_{0} ⟶ S \cup \{0\})$
22	3 21	mpbid	$⊢ φ \to A : ℕ_{0} ⟶ S \cup \{0\}$
23	22 15	fssd	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
24		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
25		ffvelrn	$⊢ (A : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to A (k) \in ℂ$
26	23 24 25	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to A (k) \in ℂ$
27	26	adantr	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to A (k) \in ℂ$
28	27	abscld	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to \|A (k)\| \in ℝ$
29	28	recnd	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to \|A (k)\| \in ℂ$
30		divcnv	$⊢ \|A (k)\| \in ℂ \to (n \in ℕ ⟼ \frac{\|A (k)\|}{n}) ⇝ 0$
31	29 30	syl	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to (n \in ℕ ⟼ \frac{\|A (k)\|}{n}) ⇝ 0$
32		nnex	$⊢ ℕ \in V$
33	32	mptex	$⊢ (n \in ℕ ⟼ \|A (k)\| n^{k - M}) \in V$
34	33	a1i	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to (n \in ℕ ⟼ \|A (k)\| n^{k - M}) \in V$
35		oveq2	$⊢ n = m \to \frac{\|A (k)\|}{n} = \frac{\|A (k)\|}{m}$
36		eqid	$⊢ (n \in ℕ ⟼ \frac{\|A (k)\|}{n}) = (n \in ℕ ⟼ \frac{\|A (k)\|}{n})$
37		ovex	$⊢ \frac{\|A (k)\|}{m} \in V$
38	35 36 37	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ \frac{\|A (k)\|}{n}) (m) = \frac{\|A (k)\|}{m}$
39	38	adantl	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to (n \in ℕ ⟼ \frac{\|A (k)\|}{n}) (m) = \frac{\|A (k)\|}{m}$
40		nndivre	$⊢ (\|A (k)\| \in ℝ \land m \in ℕ) \to \frac{\|A (k)\|}{m} \in ℝ$
41	28 40	sylan	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to \frac{\|A (k)\|}{m} \in ℝ$
42	39 41	eqeltrd	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to (n \in ℕ ⟼ \frac{\|A (k)\|}{n}) (m) \in ℝ$
43		oveq1	$⊢ n = m \to n^{k - M} = m^{k - M}$
44	43	oveq2d	$⊢ n = m \to \|A (k)\| n^{k - M} = \|A (k)\| m^{k - M}$
45		eqid	$⊢ (n \in ℕ ⟼ \|A (k)\| n^{k - M}) = (n \in ℕ ⟼ \|A (k)\| n^{k - M})$
46		ovex	$⊢ \|A (k)\| m^{k - M} \in V$
47	44 45 46	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ \|A (k)\| n^{k - M}) (m) = \|A (k)\| m^{k - M}$
48	47	adantl	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to (n \in ℕ ⟼ \|A (k)\| n^{k - M}) (m) = \|A (k)\| m^{k - M}$
49	26	ad2antrr	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to A (k) \in ℂ$
50	49	abscld	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to \|A (k)\| \in ℝ$
51		nnrp	$⊢ m \in ℕ \to m \in ℝ^{+}$
52	51	adantl	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to m \in ℝ^{+}$
53		elfzelz	$⊢ k \in (0 \dots N) \to k \in ℤ$
54		cnvimass	$⊢ A^{-1} [S ∖ \{0\}] \subseteq dom A$
55	54 22	fssdm	$⊢ φ \to A^{-1} [S ∖ \{0\}] \subseteq ℕ_{0}$
56		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
57	55 56	sstrdi	$⊢ φ \to A^{-1} [S ∖ \{0\}] \subseteq ℤ$
58	2	nn0red	$⊢ φ \to N \in ℝ$
59	22	ffnd	$⊢ φ \to A Fn ℕ_{0}$
60		elpreima	$⊢ A Fn ℕ_{0} \to (z \in A^{-1} [S ∖ \{0\}] \leftrightarrow (z \in ℕ_{0} \land A (z) \in (S ∖ \{0\})))$
61	59 60	syl	$⊢ φ \to (z \in A^{-1} [S ∖ \{0\}] \leftrightarrow (z \in ℕ_{0} \land A (z) \in (S ∖ \{0\})))$
62	61	simplbda	$⊢ (φ \land z \in A^{-1} [S ∖ \{0\}]) \to A (z) \in (S ∖ \{0\})$
63		eldifsni	$⊢ A (z) \in (S ∖ \{0\}) \to A (z) \neq 0$
64	62 63	syl	$⊢ (φ \land z \in A^{-1} [S ∖ \{0\}]) \to A (z) \neq 0$
65		fveq2	$⊢ k = z \to A (k) = A (z)$
66	65	neeq1d	$⊢ k = z \to (A (k) \neq 0 \leftrightarrow A (z) \neq 0)$
67		breq1	$⊢ k = z \to (k \leq N \leftrightarrow z \leq N)$
68	66 67	imbi12d	$⊢ k = z \to ((A (k) \neq 0 \to k \leq N) \leftrightarrow (A (z) \neq 0 \to z \leq N))$
69		plyco0	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to (A [ℤ_{\geq (N + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N))$
70	2 23 69	syl2anc	$⊢ φ \to (A [ℤ_{\geq (N + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N))$
71	4 70	mpbid	$⊢ φ \to \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)$
72	71	adantr	$⊢ (φ \land z \in A^{-1} [S ∖ \{0\}]) \to \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)$
73	55	sselda	$⊢ (φ \land z \in A^{-1} [S ∖ \{0\}]) \to z \in ℕ_{0}$
74	68 72 73	rspcdva	$⊢ (φ \land z \in A^{-1} [S ∖ \{0\}]) \to (A (z) \neq 0 \to z \leq N)$
75	64 74	mpd	$⊢ (φ \land z \in A^{-1} [S ∖ \{0\}]) \to z \leq N$
76	75	ralrimiva	$⊢ φ \to \forall z \in A^{-1} [S ∖ \{0\}] z \leq N$
77		brralrspcev	$⊢ (N \in ℝ \land \forall z \in A^{-1} [S ∖ \{0\}] z \leq N) \to \exists x \in ℝ \forall z \in A^{-1} [S ∖ \{0\}] z \leq x$
78	58 76 77	syl2anc	$⊢ φ \to \exists x \in ℝ \forall z \in A^{-1} [S ∖ \{0\}] z \leq x$
79		suprzcl	$⊢ (A^{-1} [S ∖ \{0\}] \subseteq ℤ \land A^{-1} [S ∖ \{0\}] \neq \emptyset \land \exists x \in ℝ \forall z \in A^{-1} [S ∖ \{0\}] z \leq x) \to sup (A^{-1} [S ∖ \{0\}] ℝ <) \in A^{-1} [S ∖ \{0\}]$
80	57 7 78 79	syl3anc	$⊢ φ \to sup (A^{-1} [S ∖ \{0\}] ℝ <) \in A^{-1} [S ∖ \{0\}]$
81	6 80	eqeltrid	$⊢ φ \to M \in A^{-1} [S ∖ \{0\}]$
82	55 81	sseldd	$⊢ φ \to M \in ℕ_{0}$
83	82	nn0zd	$⊢ φ \to M \in ℤ$
84		zsubcl	$⊢ (k \in ℤ \land M \in ℤ) \to k - M \in ℤ$
85	53 83 84	syl2anr	$⊢ (φ \land k \in (0 \dots N)) \to k - M \in ℤ$
86	85	ad2antrr	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to k - M \in ℤ$
87	52 86	rpexpcld	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to m^{k - M} \in ℝ^{+}$
88	87	rpred	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to m^{k - M} \in ℝ$
89	50 88	remulcld	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to \|A (k)\| m^{k - M} \in ℝ$
90	48 89	eqeltrd	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to (n \in ℕ ⟼ \|A (k)\| n^{k - M}) (m) \in ℝ$
91		nnrecre	$⊢ m \in ℕ \to \frac{1}{m} \in ℝ$
92	91	adantl	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to \frac{1}{m} \in ℝ$
93	27	absge0d	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to 0 \leq \|A (k)\|$
94	93	adantr	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to 0 \leq \|A (k)\|$
95		nnre	$⊢ m \in ℕ \to m \in ℝ$
96	95	adantl	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to m \in ℝ$
97		nnge1	$⊢ m \in ℕ \to 1 \leq m$
98	97	adantl	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to 1 \leq m$
99		1red	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to 1 \in ℝ$
100	86	zred	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to k - M \in ℝ$
101		simplr	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to k < M$
102	53	adantl	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℤ$
103	102	ad2antrr	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to k \in ℤ$
104	83	ad3antrrr	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to M \in ℤ$
105		zltp1le	$⊢ (k \in ℤ \land M \in ℤ) \to (k < M \leftrightarrow k + 1 \leq M)$
106	103 104 105	syl2anc	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to (k < M \leftrightarrow k + 1 \leq M)$
107	101 106	mpbid	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to k + 1 \leq M$
108	24	adantl	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℕ_{0}$
109	108	nn0red	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℝ$
110	109	ad2antrr	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to k \in ℝ$
111	82	adantr	$⊢ (φ \land k \in (0 \dots N)) \to M \in ℕ_{0}$
112	111	nn0red	$⊢ (φ \land k \in (0 \dots N)) \to M \in ℝ$
113	112	ad2antrr	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to M \in ℝ$
114	110 99 113	leaddsub2d	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to (k + 1 \leq M \leftrightarrow 1 \leq M - k)$
115	107 114	mpbid	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to 1 \leq M - k$
116	109	recnd	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℂ$
117	116	ad2antrr	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to k \in ℂ$
118	112	recnd	$⊢ (φ \land k \in (0 \dots N)) \to M \in ℂ$
119	118	ad2antrr	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to M \in ℂ$
120	117 119	negsubdi2d	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to - (k - M) = M - k$
121	115 120	breqtrrd	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to 1 \leq - (k - M)$
122	99 100 121	lenegcon2d	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to k - M \leq - 1$
123		neg1z	$⊢ - 1 \in ℤ$
124		eluz	$⊢ (k - M \in ℤ \land - 1 \in ℤ) \to (- 1 \in ℤ_{\geq (k - M)} \leftrightarrow k - M \leq - 1)$
125	86 123 124	sylancl	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to (- 1 \in ℤ_{\geq (k - M)} \leftrightarrow k - M \leq - 1)$
126	122 125	mpbird	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to - 1 \in ℤ_{\geq (k - M)}$
127	96 98 126	leexp2ad	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to m^{k - M} \leq m^{- 1}$
128		nncn	$⊢ m \in ℕ \to m \in ℂ$
129	128	adantl	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to m \in ℂ$
130		expn1	$⊢ m \in ℂ \to m^{- 1} = \frac{1}{m}$
131	129 130	syl	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to m^{- 1} = \frac{1}{m}$
132	127 131	breqtrd	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to m^{k - M} \leq \frac{1}{m}$
133	88 92 50 94 132	lemul2ad	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to \|A (k)\| m^{k - M} \leq \|A (k)\| (\frac{1}{m})$
134	29	adantr	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to \|A (k)\| \in ℂ$
135		nnne0	$⊢ m \in ℕ \to m \neq 0$
136	135	adantl	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to m \neq 0$
137	134 129 136	divrecd	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to \frac{\|A (k)\|}{m} = \|A (k)\| (\frac{1}{m})$
138	39 137	eqtrd	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to (n \in ℕ ⟼ \frac{\|A (k)\|}{n}) (m) = \|A (k)\| (\frac{1}{m})$
139	133 48 138	3brtr4d	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to (n \in ℕ ⟼ \|A (k)\| n^{k - M}) (m) \leq (n \in ℕ ⟼ \frac{\|A (k)\|}{n}) (m)$
140	87	rpge0d	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to 0 \leq m^{k - M}$
141	50 88 94 140	mulge0d	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to 0 \leq \|A (k)\| m^{k - M}$
142	141 48	breqtrrd	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to 0 \leq (n \in ℕ ⟼ \|A (k)\| n^{k - M}) (m)$
143	8 11 31 34 42 90 139 142	climsqz2	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to (n \in ℕ ⟼ \|A (k)\| n^{k - M}) ⇝ 0$
144	32	mptex	$⊢ (n \in ℕ ⟼ A (k) n^{k - M}) \in V$
145	144	a1i	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to (n \in ℕ ⟼ A (k) n^{k - M}) \in V$
146	43	oveq2d	$⊢ n = m \to A (k) n^{k - M} = A (k) m^{k - M}$
147		eqid	$⊢ (n \in ℕ ⟼ A (k) n^{k - M}) = (n \in ℕ ⟼ A (k) n^{k - M})$
148		ovex	$⊢ A (k) m^{k - M} \in V$
149	146 147 148	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ A (k) n^{k - M}) (m) = A (k) m^{k - M}$
150	149	ad2antlr	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to (n \in ℕ ⟼ A (k) n^{k - M}) (m) = A (k) m^{k - M}$
151	23	adantr	$⊢ (φ \land m \in ℕ) \to A : ℕ_{0} ⟶ ℂ$
152	151 24 25	syl2an	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to A (k) \in ℂ$
153	128	ad2antlr	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to m \in ℂ$
154	135	ad2antlr	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to m \neq 0$
155	83	adantr	$⊢ (φ \land m \in ℕ) \to M \in ℤ$
156	53 155 84	syl2anr	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to k - M \in ℤ$
157	153 154 156	expclzd	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to m^{k - M} \in ℂ$
158	152 157	mulcld	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to A (k) m^{k - M} \in ℂ$
159	150 158	eqeltrd	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to (n \in ℕ ⟼ A (k) n^{k - M}) (m) \in ℂ$
160	159	an32s	$⊢ ((φ \land k \in (0 \dots N)) \land m \in ℕ) \to (n \in ℕ ⟼ A (k) n^{k - M}) (m) \in ℂ$
161	160	adantlr	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to (n \in ℕ ⟼ A (k) n^{k - M}) (m) \in ℂ$
162	88	recnd	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to m^{k - M} \in ℂ$
163	49 162	absmuld	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to \|A (k) m^{k - M}\| = \|A (k)\| \|m^{k - M}\|$
164	88 140	absidd	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to \|m^{k - M}\| = m^{k - M}$
165	164	oveq2d	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to \|A (k)\| \|m^{k - M}\| = \|A (k)\| m^{k - M}$
166	163 165	eqtrd	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to \|A (k) m^{k - M}\| = \|A (k)\| m^{k - M}$
167	149	adantl	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to (n \in ℕ ⟼ A (k) n^{k - M}) (m) = A (k) m^{k - M}$
168	167	fveq2d	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to \|(n \in ℕ ⟼ A (k) n^{k - M}) (m)\| = \|A (k) m^{k - M}\|$
169	166 168 48	3eqtr4rd	$⊢ (((φ \land k \in (0 \dots N)) \land k < M) \land m \in ℕ) \to (n \in ℕ ⟼ \|A (k)\| n^{k - M}) (m) = \|(n \in ℕ ⟼ A (k) n^{k - M}) (m)\|$
170	8 11 145 34 161 169	climabs0	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to ((n \in ℕ ⟼ A (k) n^{k - M}) ⇝ 0 \leftrightarrow (n \in ℕ ⟼ \|A (k)\| n^{k - M}) ⇝ 0)$
171	143 170	mpbird	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to (n \in ℕ ⟼ A (k) n^{k - M}) ⇝ 0$
172	109	adantr	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to k \in ℝ$
173		simpr	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to k < M$
174	172 173	ltned	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to k \neq M$
175		velsn	$⊢ k \in \{M\} \leftrightarrow k = M$
176	175	necon3bbii	$⊢ \neg k \in \{M\} \leftrightarrow k \neq M$
177	174 176	sylibr	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to \neg k \in \{M\}$
178	177	iffalsed	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to if (k \in \{M\}, A (k), 0) = 0$
179	171 178	breqtrrd	$⊢ ((φ \land k \in (0 \dots N)) \land k < M) \to (n \in ℕ ⟼ A (k) n^{k - M}) ⇝ if (k \in \{M\}, A (k), 0)$
180		nncn	$⊢ n \in ℕ \to n \in ℂ$
181	180	ad2antlr	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) = 0) \to n \in ℂ$
182		nnne0	$⊢ n \in ℕ \to n \neq 0$
183	182	ad2antlr	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) = 0) \to n \neq 0$
184	85	ad3antrrr	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) = 0) \to k - M \in ℤ$
185	181 183 184	expclzd	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) = 0) \to n^{k - M} \in ℂ$
186	185	mul02d	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) = 0) \to 0 \cdot n^{k - M} = 0$
187		simpr	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) = 0) \to A (k) = 0$
188	187	oveq1d	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) = 0) \to A (k) n^{k - M} = 0 \cdot n^{k - M}$
189	187	ifeq1d	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) = 0) \to if (k \in \{M\}, A (k), 0) = if (k \in \{M\}, 0, 0)$
190		ifid	$⊢ if (k \in \{M\}, 0, 0) = 0$
191	189 190	eqtrdi	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) = 0) \to if (k \in \{M\}, A (k), 0) = 0$
192	186 188 191	3eqtr4d	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) = 0) \to A (k) n^{k - M} = if (k \in \{M\}, A (k), 0)$
193	26	adantr	$⊢ ((φ \land k \in (0 \dots N)) \land M \leq k) \to A (k) \in ℂ$
194	193	ad2antrr	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to A (k) \in ℂ$
195	194	mulid1d	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to A (k) \cdot 1 = A (k)$
196		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
197	55 196	sstrdi	$⊢ φ \to A^{-1} [S ∖ \{0\}] \subseteq ℝ$
198	197	ad2antrr	$⊢ ((φ \land k \in (0 \dots N)) \land A (k) \neq 0) \to A^{-1} [S ∖ \{0\}] \subseteq ℝ$
199	7	ad2antrr	$⊢ ((φ \land k \in (0 \dots N)) \land A (k) \neq 0) \to A^{-1} [S ∖ \{0\}] \neq \emptyset$
200	78	ad2antrr	$⊢ ((φ \land k \in (0 \dots N)) \land A (k) \neq 0) \to \exists x \in ℝ \forall z \in A^{-1} [S ∖ \{0\}] z \leq x$
201	24	ad2antlr	$⊢ ((φ \land k \in (0 \dots N)) \land A (k) \neq 0) \to k \in ℕ_{0}$
202		ffvelrn	$⊢ (A : ℕ_{0} ⟶ S \cup \{0\} \land k \in ℕ_{0}) \to A (k) \in (S \cup \{0\})$
203	22 24 202	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to A (k) \in (S \cup \{0\})$
204	203	anim1i	$⊢ ((φ \land k \in (0 \dots N)) \land A (k) \neq 0) \to (A (k) \in (S \cup \{0\}) \land A (k) \neq 0)$
205		eldifsn	$⊢ A (k) \in ((S \cup \{0\}) ∖ \{0\}) \leftrightarrow (A (k) \in (S \cup \{0\}) \land A (k) \neq 0)$
206	204 205	sylibr	$⊢ ((φ \land k \in (0 \dots N)) \land A (k) \neq 0) \to A (k) \in ((S \cup \{0\}) ∖ \{0\})$
207		difun2	$⊢ (S \cup \{0\}) ∖ \{0\} = S ∖ \{0\}$
208	206 207	eleqtrdi	$⊢ ((φ \land k \in (0 \dots N)) \land A (k) \neq 0) \to A (k) \in (S ∖ \{0\})$
209		elpreima	$⊢ A Fn ℕ_{0} \to (k \in A^{-1} [S ∖ \{0\}] \leftrightarrow (k \in ℕ_{0} \land A (k) \in (S ∖ \{0\})))$
210	59 209	syl	$⊢ φ \to (k \in A^{-1} [S ∖ \{0\}] \leftrightarrow (k \in ℕ_{0} \land A (k) \in (S ∖ \{0\})))$
211	210	ad2antrr	$⊢ ((φ \land k \in (0 \dots N)) \land A (k) \neq 0) \to (k \in A^{-1} [S ∖ \{0\}] \leftrightarrow (k \in ℕ_{0} \land A (k) \in (S ∖ \{0\})))$
212	201 208 211	mpbir2and	$⊢ ((φ \land k \in (0 \dots N)) \land A (k) \neq 0) \to k \in A^{-1} [S ∖ \{0\}]$
213	198 199 200 212	suprubd	$⊢ ((φ \land k \in (0 \dots N)) \land A (k) \neq 0) \to k \leq sup (A^{-1} [S ∖ \{0\}] ℝ <)$
214	213 6	breqtrrdi	$⊢ ((φ \land k \in (0 \dots N)) \land A (k) \neq 0) \to k \leq M$
215	214	ad4ant14	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to k \leq M$
216		simpllr	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to M \leq k$
217	109	ad3antrrr	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to k \in ℝ$
218	112	ad3antrrr	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to M \in ℝ$
219	217 218	letri3d	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to (k = M \leftrightarrow (k \leq M \land M \leq k))$
220	215 216 219	mpbir2and	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to k = M$
221	220	oveq1d	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to k - M = M - M$
222	118	ad3antrrr	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to M \in ℂ$
223	222	subidd	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to M - M = 0$
224	221 223	eqtrd	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to k - M = 0$
225	224	oveq2d	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to n^{k - M} = n^{0}$
226	180	ad2antlr	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to n \in ℂ$
227	226	exp0d	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to n^{0} = 1$
228	225 227	eqtrd	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to n^{k - M} = 1$
229	228	oveq2d	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to A (k) n^{k - M} = A (k) \cdot 1$
230	220 175	sylibr	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to k \in \{M\}$
231	230	iftrued	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to if (k \in \{M\}, A (k), 0) = A (k)$
232	195 229 231	3eqtr4d	$⊢ ((((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \land A (k) \neq 0) \to A (k) n^{k - M} = if (k \in \{M\}, A (k), 0)$
233	192 232	pm2.61dane	$⊢ (((φ \land k \in (0 \dots N)) \land M \leq k) \land n \in ℕ) \to A (k) n^{k - M} = if (k \in \{M\}, A (k), 0)$
234	233	mpteq2dva	$⊢ ((φ \land k \in (0 \dots N)) \land M \leq k) \to (n \in ℕ ⟼ A (k) n^{k - M}) = (n \in ℕ ⟼ if (k \in \{M\}, A (k), 0))$
235		fconstmpt	$⊢ ℕ \times \{if (k \in \{M\}, A (k), 0)\} = (n \in ℕ ⟼ if (k \in \{M\}, A (k), 0))$
236	234 235	eqtr4di	$⊢ ((φ \land k \in (0 \dots N)) \land M \leq k) \to (n \in ℕ ⟼ A (k) n^{k - M}) = ℕ \times \{if (k \in \{M\}, A (k), 0)\}$
237		ifcl	$⊢ (A (k) \in ℂ \land 0 \in ℂ) \to if (k \in \{M\}, A (k), 0) \in ℂ$
238	193 12 237	sylancl	$⊢ ((φ \land k \in (0 \dots N)) \land M \leq k) \to if (k \in \{M\}, A (k), 0) \in ℂ$
239		1z	$⊢ 1 \in ℤ$
240	8	eqimss2i	$⊢ ℤ_{\geq 1} \subseteq ℕ$
241	240 32	climconst2	$⊢ (if (k \in \{M\}, A (k), 0) \in ℂ \land 1 \in ℤ) \to (ℕ \times \{if (k \in \{M\}, A (k), 0)\}) ⇝ if (k \in \{M\}, A (k), 0)$
242	238 239 241	sylancl	$⊢ ((φ \land k \in (0 \dots N)) \land M \leq k) \to (ℕ \times \{if (k \in \{M\}, A (k), 0)\}) ⇝ if (k \in \{M\}, A (k), 0)$
243	236 242	eqbrtrd	$⊢ ((φ \land k \in (0 \dots N)) \land M \leq k) \to (n \in ℕ ⟼ A (k) n^{k - M}) ⇝ if (k \in \{M\}, A (k), 0)$
244	179 243 109 112	ltlecasei	$⊢ (φ \land k \in (0 \dots N)) \to (n \in ℕ ⟼ A (k) n^{k - M}) ⇝ if (k \in \{M\}, A (k), 0)$
245		snex	$⊢ \{0\} \in V$
246	32 245	xpex	$⊢ ℕ \times \{0\} \in V$
247	246	a1i	$⊢ φ \to ℕ \times \{0\} \in V$
248	160	anasss	$⊢ (φ \land (k \in (0 \dots N) \land m \in ℕ)) \to (n \in ℕ ⟼ A (k) n^{k - M}) (m) \in ℂ$
249	5	fveq1d	$⊢ φ \to 0_{𝑝} (m) = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) (m)$
250	249	adantr	$⊢ (φ \land m \in ℕ) \to 0_{𝑝} (m) = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) (m)$
251	128	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℂ$
252		0pval	$⊢ m \in ℂ \to 0_{𝑝} (m) = 0$
253	251 252	syl	$⊢ (φ \land m \in ℕ) \to 0_{𝑝} (m) = 0$
254		oveq1	$⊢ z = m \to z^{k} = m^{k}$
255	254	oveq2d	$⊢ z = m \to A (k) z^{k} = A (k) m^{k}$
256	255	sumeq2sdv	$⊢ z = m \to \sum_{k = 0}^{N} A (k) z^{k} = \sum_{k = 0}^{N} A (k) m^{k}$
257		eqid	$⊢ (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k})$
258		sumex	$⊢ \sum_{k = 0}^{N} A (k) m^{k} \in V$
259	256 257 258	fvmpt	$⊢ m \in ℂ \to (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) (m) = \sum_{k = 0}^{N} A (k) m^{k}$
260	251 259	syl	$⊢ (φ \land m \in ℕ) \to (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) (m) = \sum_{k = 0}^{N} A (k) m^{k}$
261	250 253 260	3eqtr3d	$⊢ (φ \land m \in ℕ) \to 0 = \sum_{k = 0}^{N} A (k) m^{k}$
262	261	oveq1d	$⊢ (φ \land m \in ℕ) \to \frac{0}{m^{M}} = \frac{\sum_{k = 0}^{N} A (k) m^{k}}{m^{M}}$
263		expcl	$⊢ (m \in ℂ \land M \in ℕ_{0}) \to m^{M} \in ℂ$
264	128 82 263	syl2anr	$⊢ (φ \land m \in ℕ) \to m^{M} \in ℂ$
265	135	adantl	$⊢ (φ \land m \in ℕ) \to m \neq 0$
266	251 265 155	expne0d	$⊢ (φ \land m \in ℕ) \to m^{M} \neq 0$
267	264 266	div0d	$⊢ (φ \land m \in ℕ) \to \frac{0}{m^{M}} = 0$
268		fzfid	$⊢ (φ \land m \in ℕ) \to (0 \dots N) \in Fin$
269		expcl	$⊢ (m \in ℂ \land k \in ℕ_{0}) \to m^{k} \in ℂ$
270	251 24 269	syl2an	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to m^{k} \in ℂ$
271	152 270	mulcld	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to A (k) m^{k} \in ℂ$
272	268 264 271 266	fsumdivc	$⊢ (φ \land m \in ℕ) \to \frac{\sum_{k = 0}^{N} A (k) m^{k}}{m^{M}} = \sum_{k = 0}^{N} (\frac{A (k) m^{k}}{m^{M}})$
273	262 267 272	3eqtr3d	$⊢ (φ \land m \in ℕ) \to 0 = \sum_{k = 0}^{N} (\frac{A (k) m^{k}}{m^{M}})$
274		fvconst2g	$⊢ (0 \in ℂ \land m \in ℕ) \to (ℕ \times \{0\}) (m) = 0$
275	13 274	sylan	$⊢ (φ \land m \in ℕ) \to (ℕ \times \{0\}) (m) = 0$
276	155	adantr	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to M \in ℤ$
277	53	adantl	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to k \in ℤ$
278	153 154 276 277	expsubd	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to m^{k - M} = \frac{m^{k}}{m^{M}}$
279	278	oveq2d	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to A (k) m^{k - M} = A (k) (\frac{m^{k}}{m^{M}})$
280	264	adantr	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to m^{M} \in ℂ$
281	266	adantr	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to m^{M} \neq 0$
282	152 270 280 281	divassd	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to \frac{A (k) m^{k}}{m^{M}} = A (k) (\frac{m^{k}}{m^{M}})$
283	279 150 282	3eqtr4d	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots N)) \to (n \in ℕ ⟼ A (k) n^{k - M}) (m) = \frac{A (k) m^{k}}{m^{M}}$
284	283	sumeq2dv	$⊢ (φ \land m \in ℕ) \to \sum_{k = 0}^{N} (n \in ℕ ⟼ A (k) n^{k - M}) (m) = \sum_{k = 0}^{N} (\frac{A (k) m^{k}}{m^{M}})$
285	273 275 284	3eqtr4d	$⊢ (φ \land m \in ℕ) \to (ℕ \times \{0\}) (m) = \sum_{k = 0}^{N} (n \in ℕ ⟼ A (k) n^{k - M}) (m)$
286	8 9 10 244 247 248 285	climfsum	$⊢ φ \to (ℕ \times \{0\}) ⇝ \sum_{k = 0}^{N} if (k \in \{M\}, A (k), 0)$
287		suprleub	$⊢ ((A^{-1} [S ∖ \{0\}] \subseteq ℝ \land A^{-1} [S ∖ \{0\}] \neq \emptyset \land \exists x \in ℝ \forall z \in A^{-1} [S ∖ \{0\}] z \leq x) \land N \in ℝ) \to (sup (A^{-1} [S ∖ \{0\}] ℝ <) \leq N \leftrightarrow \forall z \in A^{-1} [S ∖ \{0\}] z \leq N)$
288	197 7 78 58 287	syl31anc	$⊢ φ \to (sup (A^{-1} [S ∖ \{0\}] ℝ <) \leq N \leftrightarrow \forall z \in A^{-1} [S ∖ \{0\}] z \leq N)$
289	76 288	mpbird	$⊢ φ \to sup (A^{-1} [S ∖ \{0\}] ℝ <) \leq N$
290	6 289	eqbrtrid	$⊢ φ \to M \leq N$
291		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
292	82 291	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
293	2	nn0zd	$⊢ φ \to N \in ℤ$
294		elfz5	$⊢ (M \in ℤ_{\geq 0} \land N \in ℤ) \to (M \in (0 \dots N) \leftrightarrow M \leq N)$
295	292 293 294	syl2anc	$⊢ φ \to (M \in (0 \dots N) \leftrightarrow M \leq N)$
296	290 295	mpbird	$⊢ φ \to M \in (0 \dots N)$
297	296	snssd	$⊢ φ \to \{M\} \subseteq (0 \dots N)$
298	23 82	ffvelrnd	$⊢ φ \to A (M) \in ℂ$
299		elsni	$⊢ k \in \{M\} \to k = M$
300	299	fveq2d	$⊢ k \in \{M\} \to A (k) = A (M)$
301	300	eleq1d	$⊢ k \in \{M\} \to (A (k) \in ℂ \leftrightarrow A (M) \in ℂ)$
302	298 301	syl5ibrcom	$⊢ φ \to (k \in \{M\} \to A (k) \in ℂ)$
303	302	ralrimiv	$⊢ φ \to \forall k \in \{M\} A (k) \in ℂ$
304	10	olcd	$⊢ φ \to ((0 \dots N) \subseteq ℤ_{\geq 0} \lor (0 \dots N) \in Fin)$
305		sumss2	$⊢ ((\{M\} \subseteq (0 \dots N) \land \forall k \in \{M\} A (k) \in ℂ) \land ((0 \dots N) \subseteq ℤ_{\geq 0} \lor (0 \dots N) \in Fin)) \to \sum_{k \in \{M\}} A (k) = \sum_{k = 0}^{N} if (k \in \{M\}, A (k), 0)$
306	297 303 304 305	syl21anc	$⊢ φ \to \sum_{k \in \{M\}} A (k) = \sum_{k = 0}^{N} if (k \in \{M\}, A (k), 0)$
307		ltso	$⊢ < Or ℝ$
308	307	supex	$⊢ sup (A^{-1} [S ∖ \{0\}] ℝ <) \in V$
309	6 308	eqeltri	$⊢ M \in V$
310		fveq2	$⊢ k = M \to A (k) = A (M)$
311	310	sumsn	$⊢ (M \in V \land A (M) \in ℂ) \to \sum_{k \in \{M\}} A (k) = A (M)$
312	309 298 311	sylancr	$⊢ φ \to \sum_{k \in \{M\}} A (k) = A (M)$
313	306 312	eqtr3d	$⊢ φ \to \sum_{k = 0}^{N} if (k \in \{M\}, A (k), 0) = A (M)$
314	286 313	breqtrd	$⊢ φ \to (ℕ \times \{0\}) ⇝ A (M)$
315	240 32	climconst2	$⊢ (0 \in ℂ \land 1 \in ℤ) \to (ℕ \times \{0\}) ⇝ 0$
316	12 239 315	mp2an	$⊢ (ℕ \times \{0\}) ⇝ 0$
317		climuni	$⊢ ((ℕ \times \{0\}) ⇝ A (M) \land (ℕ \times \{0\}) ⇝ 0) \to A (M) = 0$
318	314 316 317	sylancl	$⊢ φ \to A (M) = 0$
319		fvex	$⊢ A (M) \in V$
320	319	elsn	$⊢ A (M) \in \{0\} \leftrightarrow A (M) = 0$
321	318 320	sylibr	$⊢ φ \to A (M) \in \{0\}$
322		elpreima	$⊢ A Fn ℕ_{0} \to (M \in A^{-1} [S ∖ \{0\}] \leftrightarrow (M \in ℕ_{0} \land A (M) \in (S ∖ \{0\})))$
323	59 322	syl	$⊢ φ \to (M \in A^{-1} [S ∖ \{0\}] \leftrightarrow (M \in ℕ_{0} \land A (M) \in (S ∖ \{0\})))$
324	81 323	mpbid	$⊢ φ \to (M \in ℕ_{0} \land A (M) \in (S ∖ \{0\}))$
325	324	simprd	$⊢ φ \to A (M) \in (S ∖ \{0\})$
326	325	eldifbd	$⊢ φ \to \neg A (M) \in \{0\}$
327	321 326	pm2.65i	$⊢ \neg φ$

Metamath Proof Explorer

Theorem plyeq0lem

Proof