elply2

Description: The coefficient function can be assumed to have zeroes outside 0 ... n . (Contributed by Mario Carneiro, 20-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

		Ref	Expression
	Assertion	elply2	$⊢ F \in Poly (S) \leftrightarrow (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})))$

Proof

Step	Hyp	Ref	Expression
1		elply	$⊢ F \in Poly (S) \leftrightarrow (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists f \in ({(S \cup \{0\})}^{ℕ_{0}}) F = (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}))$
2		simpr	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to f \in ({(S \cup \{0\})}^{ℕ_{0}})$
3		simpll	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to S \subseteq ℂ$
4		cnex	$⊢ ℂ \in V$
5		ssexg	$⊢ (S \subseteq ℂ \land ℂ \in V) \to S \in V$
6	3 4 5	sylancl	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to S \in V$
7		snex	$⊢ \{0\} \in V$
8		unexg	$⊢ (S \in V \land \{0\} \in V) \to S \cup \{0\} \in V$
9	6 7 8	sylancl	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to S \cup \{0\} \in V$
10		nn0ex	$⊢ ℕ_{0} \in V$
11		elmapg	$⊢ (S \cup \{0\} \in V \land ℕ_{0} \in V) \to (f \in ({(S \cup \{0\})}^{ℕ_{0}}) \leftrightarrow f : ℕ_{0} ⟶ S \cup \{0\})$
12	9 10 11	sylancl	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to (f \in ({(S \cup \{0\})}^{ℕ_{0}}) \leftrightarrow f : ℕ_{0} ⟶ S \cup \{0\})$
13	2 12	mpbid	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to f : ℕ_{0} ⟶ S \cup \{0\}$
14	13	ffvelrnda	$⊢ (((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \land x \in ℕ_{0}) \to f (x) \in (S \cup \{0\})$
15		ssun2	$⊢ \{0\} \subseteq S \cup \{0\}$
16		c0ex	$⊢ 0 \in V$
17	16	snss	$⊢ 0 \in (S \cup \{0\}) \leftrightarrow \{0\} \subseteq S \cup \{0\}$
18	15 17	mpbir	$⊢ 0 \in (S \cup \{0\})$
19		ifcl	$⊢ (f (x) \in (S \cup \{0\}) \land 0 \in (S \cup \{0\})) \to if (x \in (0 \dots n), f (x), 0) \in (S \cup \{0\})$
20	14 18 19	sylancl	$⊢ (((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \land x \in ℕ_{0}) \to if (x \in (0 \dots n), f (x), 0) \in (S \cup \{0\})$
21	20	fmpttd	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) : ℕ_{0} ⟶ S \cup \{0\}$
22		elmapg	$⊢ (S \cup \{0\} \in V \land ℕ_{0} \in V) \to ((x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) \in ({(S \cup \{0\})}^{ℕ_{0}}) \leftrightarrow (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) : ℕ_{0} ⟶ S \cup \{0\})$
23	9 10 22	sylancl	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to ((x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) \in ({(S \cup \{0\})}^{ℕ_{0}}) \leftrightarrow (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) : ℕ_{0} ⟶ S \cup \{0\})$
24	21 23	mpbird	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) \in ({(S \cup \{0\})}^{ℕ_{0}})$
25		eleq1w	$⊢ x = k \to (x \in (0 \dots n) \leftrightarrow k \in (0 \dots n))$
26		fveq2	$⊢ x = k \to f (x) = f (k)$
27	25 26	ifbieq1d	$⊢ x = k \to if (x \in (0 \dots n), f (x), 0) = if (k \in (0 \dots n), f (k), 0)$
28		eqid	$⊢ (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) = (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0))$
29		fvex	$⊢ f (k) \in V$
30	29 16	ifex	$⊢ if (k \in (0 \dots n), f (k), 0) \in V$
31	27 28 30	fvmpt	$⊢ k \in ℕ_{0} \to (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) (k) = if (k \in (0 \dots n), f (k), 0)$
32	31	ad2antll	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land (f \in ({(S \cup \{0\})}^{ℕ_{0}}) \land k \in ℕ_{0})) \to (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) (k) = if (k \in (0 \dots n), f (k), 0)$
33		iffalse	$⊢ \neg k \in (0 \dots n) \to if (k \in (0 \dots n), f (k), 0) = 0$
34	33	eqeq2d	$⊢ \neg k \in (0 \dots n) \to ((x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) (k) = if (k \in (0 \dots n), f (k), 0) \leftrightarrow (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) (k) = 0)$
35	32 34	syl5ibcom	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land (f \in ({(S \cup \{0\})}^{ℕ_{0}}) \land k \in ℕ_{0})) \to (\neg k \in (0 \dots n) \to (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) (k) = 0)$
36	35	necon1ad	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land (f \in ({(S \cup \{0\})}^{ℕ_{0}}) \land k \in ℕ_{0})) \to ((x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) (k) \neq 0 \to k \in (0 \dots n))$
37		elfzle2	$⊢ k \in (0 \dots n) \to k \leq n$
38	36 37	syl6	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land (f \in ({(S \cup \{0\})}^{ℕ_{0}}) \land k \in ℕ_{0})) \to ((x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) (k) \neq 0 \to k \leq n)$
39	38	anassrs	$⊢ (((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \land k \in ℕ_{0}) \to ((x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) (k) \neq 0 \to k \leq n)$
40	39	ralrimiva	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to \forall k \in ℕ_{0} ((x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) (k) \neq 0 \to k \leq n)$
41		simplr	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to n \in ℕ_{0}$
42		0cnd	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to 0 \in ℂ$
43	42	snssd	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to \{0\} \subseteq ℂ$
44	3 43	unssd	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to S \cup \{0\} \subseteq ℂ$
45	21 44	fssd	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) : ℕ_{0} ⟶ ℂ$
46		plyco0	$⊢ (n \in ℕ_{0} \land (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) : ℕ_{0} ⟶ ℂ) \to ((x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) [ℤ_{\geq (n + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} ((x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) (k) \neq 0 \to k \leq n))$
47	41 45 46	syl2anc	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to ((x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) [ℤ_{\geq (n + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} ((x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) (k) \neq 0 \to k \leq n))$
48	40 47	mpbird	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) [ℤ_{\geq (n + 1)}] = \{0\}$
49		eqidd	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k})$
50		imaeq1	$⊢ a = (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) \to a [ℤ_{\geq (n + 1)}] = (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) [ℤ_{\geq (n + 1)}]$
51	50	eqeq1d	$⊢ a = (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) \to (a [ℤ_{\geq (n + 1)}] = \{0\} \leftrightarrow (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) [ℤ_{\geq (n + 1)}] = \{0\})$
52		fveq1	$⊢ a = (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) \to a (k) = (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) (k)$
53		elfznn0	$⊢ k \in (0 \dots n) \to k \in ℕ_{0}$
54	53 31	syl	$⊢ k \in (0 \dots n) \to (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) (k) = if (k \in (0 \dots n), f (k), 0)$
55		iftrue	$⊢ k \in (0 \dots n) \to if (k \in (0 \dots n), f (k), 0) = f (k)$
56	54 55	eqtrd	$⊢ k \in (0 \dots n) \to (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) (k) = f (k)$
57	52 56	sylan9eq	$⊢ (a = (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) \land k \in (0 \dots n)) \to a (k) = f (k)$
58	57	oveq1d	$⊢ (a = (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) \land k \in (0 \dots n)) \to a (k) z^{k} = f (k) z^{k}$
59	58	sumeq2dv	$⊢ a = (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) \to \sum_{k = 0}^{n} a (k) z^{k} = \sum_{k = 0}^{n} f (k) z^{k}$
60	59	mpteq2dv	$⊢ a = (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) \to (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k})$
61	60	eqeq2d	$⊢ a = (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) \to ((z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) \leftrightarrow (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}))$
62	51 61	anbi12d	$⊢ a = (x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) \to ((a [ℤ_{\geq (n + 1)}] = \{0\} \land (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \leftrightarrow ((x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) [ℤ_{\geq (n + 1)}] = \{0\} \land (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k})))$
63	62	rspcev	$⊢ ((x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) \in ({(S \cup \{0\})}^{ℕ_{0}}) \land ((x \in ℕ_{0} ⟼ if (x \in (0 \dots n), f (x), 0)) [ℤ_{\geq (n + 1)}] = \{0\} \land (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}))) \to \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$
64	24 48 49 63	syl12anc	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$
65		eqeq1	$⊢ F = (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) \to (F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) \leftrightarrow (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$
66	65	anbi2d	$⊢ F = (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) \to ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \leftrightarrow (a [ℤ_{\geq (n + 1)}] = \{0\} \land (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})))$
67	66	rexbidv	$⊢ F = (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) \to (\exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \leftrightarrow \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})))$
68	64 67	syl5ibrcom	$⊢ ((S \subseteq ℂ \land n \in ℕ_{0}) \land f \in ({(S \cup \{0\})}^{ℕ_{0}})) \to (F = (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) \to \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})))$
69	68	rexlimdva	$⊢ (S \subseteq ℂ \land n \in ℕ_{0}) \to (\exists f \in ({(S \cup \{0\})}^{ℕ_{0}}) F = (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) \to \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})))$
70	69	reximdva	$⊢ S \subseteq ℂ \to (\exists n \in ℕ_{0} \exists f \in ({(S \cup \{0\})}^{ℕ_{0}}) F = (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k}) \to \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})))$
71	70	imdistani	$⊢ (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists f \in ({(S \cup \{0\})}^{ℕ_{0}}) F = (z \in ℂ ⟼ \sum_{k = 0}^{n} f (k) z^{k})) \to (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})))$
72	1 71	sylbi	$⊢ F \in Poly (S) \to (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})))$
73		simpr	$⊢ (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})$
74	73	reximi	$⊢ \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \to \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})$
75	74	reximi	$⊢ \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \to \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})$
76	75	anim2i	$⊢ (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$
77		elply	$⊢ F \in Poly (S) \leftrightarrow (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$
78	76 77	sylibr	$⊢ (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))) \to F \in Poly (S)$
79	72 78	impbii	$⊢ F \in Poly (S) \leftrightarrow (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})))$

Metamath Proof Explorer

Theorem elply2

Proof