coeaddlem

	Ref	Expression
Hypotheses	coefv0.1	$⊢ A = coeff (F)$
	coeadd.2	$⊢ B = coeff (G)$
	coeadd.3	$⊢ M = \deg (F)$
	coeadd.4	$⊢ N = \deg (G)$
Assertion	coeaddlem	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (coeff (F +_{f} G) = A +_{f} B \land \deg (F +_{f} G) \leq if (M \leq N, N, M))$

Proof

Step	Hyp	Ref	Expression
1		coefv0.1	$⊢ A = coeff (F)$
2		coeadd.2	$⊢ B = coeff (G)$
3		coeadd.3	$⊢ M = \deg (F)$
4		coeadd.4	$⊢ N = \deg (G)$
5		plyaddcl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F +_{f} G \in Poly (ℂ)$
6		dgrcl	$⊢ G \in Poly (S) \to \deg (G) \in ℕ_{0}$
7	4 6	eqeltrid	$⊢ G \in Poly (S) \to N \in ℕ_{0}$
8	7	adantl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to N \in ℕ_{0}$
9		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
10	3 9	eqeltrid	$⊢ F \in Poly (S) \to M \in ℕ_{0}$
11	10	adantr	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to M \in ℕ_{0}$
12	8 11	ifcld	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to if (M \leq N, N, M) \in ℕ_{0}$
13		addcl	$⊢ (x \in ℂ \land y \in ℂ) \to x + y \in ℂ$
14	13	adantl	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (x \in ℂ \land y \in ℂ)) \to x + y \in ℂ$
15	1	coef3	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ ℂ$
16	15	adantr	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to A : ℕ_{0} ⟶ ℂ$
17	2	coef3	$⊢ G \in Poly (S) \to B : ℕ_{0} ⟶ ℂ$
18	17	adantl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to B : ℕ_{0} ⟶ ℂ$
19		nn0ex	$⊢ ℕ_{0} \in V$
20	19	a1i	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to ℕ_{0} \in V$
21		inidm	$⊢ ℕ_{0} \cap ℕ_{0} = ℕ_{0}$
22	14 16 18 20 20 21	off	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (A +_{f} B) : ℕ_{0} ⟶ ℂ$
23		oveq12	$⊢ (A (k) = 0 \land B (k) = 0) \to A (k) + B (k) = 0 + 0$
24		00id	$⊢ 0 + 0 = 0$
25	23 24	eqtrdi	$⊢ (A (k) = 0 \land B (k) = 0) \to A (k) + B (k) = 0$
26	16	ffnd	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to A Fn ℕ_{0}$
27	18	ffnd	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to B Fn ℕ_{0}$
28		eqidd	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to A (k) = A (k)$
29		eqidd	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to B (k) = B (k)$
30	26 27 20 20 21 28 29	ofval	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to (A +_{f} B) (k) = A (k) + B (k)$
31	30	eqeq1d	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to ((A +_{f} B) (k) = 0 \leftrightarrow A (k) + B (k) = 0)$
32	25 31	syl5ibr	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to ((A (k) = 0 \land B (k) = 0) \to (A +_{f} B) (k) = 0)$
33	32	necon3ad	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to ((A +_{f} B) (k) \neq 0 \to \neg (A (k) = 0 \land B (k) = 0))$
34		neorian	$⊢ (A (k) \neq 0 \lor B (k) \neq 0) \leftrightarrow \neg (A (k) = 0 \land B (k) = 0)$
35	33 34	syl6ibr	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to ((A +_{f} B) (k) \neq 0 \to (A (k) \neq 0 \lor B (k) \neq 0))$
36	1 3	dgrub2	$⊢ F \in Poly (S) \to A [ℤ_{\geq (M + 1)}] = \{0\}$
37	36	adantr	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to A [ℤ_{\geq (M + 1)}] = \{0\}$
38		plyco0	$⊢ (M \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to (A [ℤ_{\geq (M + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq M))$
39	11 16 38	syl2anc	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (A [ℤ_{\geq (M + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq M))$
40	37 39	mpbid	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq M)$
41	40	r19.21bi	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to (A (k) \neq 0 \to k \leq M)$
42	11	adantr	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to M \in ℕ_{0}$
43	42	nn0red	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to M \in ℝ$
44	8	adantr	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to N \in ℕ_{0}$
45	44	nn0red	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to N \in ℝ$
46		max1	$⊢ (M \in ℝ \land N \in ℝ) \to M \leq if (M \leq N, N, M)$
47	43 45 46	syl2anc	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to M \leq if (M \leq N, N, M)$
48		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
49	48	adantl	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to k \in ℝ$
50	12	adantr	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to if (M \leq N, N, M) \in ℕ_{0}$
51	50	nn0red	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to if (M \leq N, N, M) \in ℝ$
52		letr	$⊢ (k \in ℝ \land M \in ℝ \land if (M \leq N, N, M) \in ℝ) \to ((k \leq M \land M \leq if (M \leq N, N, M)) \to k \leq if (M \leq N, N, M))$
53	49 43 51 52	syl3anc	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to ((k \leq M \land M \leq if (M \leq N, N, M)) \to k \leq if (M \leq N, N, M))$
54	47 53	mpan2d	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to (k \leq M \to k \leq if (M \leq N, N, M))$
55	41 54	syld	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to (A (k) \neq 0 \to k \leq if (M \leq N, N, M))$
56	2 4	dgrub2	$⊢ G \in Poly (S) \to B [ℤ_{\geq (N + 1)}] = \{0\}$
57	56	adantl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to B [ℤ_{\geq (N + 1)}] = \{0\}$
58		plyco0	$⊢ (N \in ℕ_{0} \land B : ℕ_{0} ⟶ ℂ) \to (B [ℤ_{\geq (N + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (B (k) \neq 0 \to k \leq N))$
59	8 18 58	syl2anc	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (B [ℤ_{\geq (N + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (B (k) \neq 0 \to k \leq N))$
60	57 59	mpbid	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to \forall k \in ℕ_{0} (B (k) \neq 0 \to k \leq N)$
61	60	r19.21bi	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to (B (k) \neq 0 \to k \leq N)$
62		max2	$⊢ (M \in ℝ \land N \in ℝ) \to N \leq if (M \leq N, N, M)$
63	43 45 62	syl2anc	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to N \leq if (M \leq N, N, M)$
64		letr	$⊢ (k \in ℝ \land N \in ℝ \land if (M \leq N, N, M) \in ℝ) \to ((k \leq N \land N \leq if (M \leq N, N, M)) \to k \leq if (M \leq N, N, M))$
65	49 45 51 64	syl3anc	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to ((k \leq N \land N \leq if (M \leq N, N, M)) \to k \leq if (M \leq N, N, M))$
66	63 65	mpan2d	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to (k \leq N \to k \leq if (M \leq N, N, M))$
67	61 66	syld	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to (B (k) \neq 0 \to k \leq if (M \leq N, N, M))$
68	55 67	jaod	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to ((A (k) \neq 0 \lor B (k) \neq 0) \to k \leq if (M \leq N, N, M))$
69	35 68	syld	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in ℕ_{0}) \to ((A +_{f} B) (k) \neq 0 \to k \leq if (M \leq N, N, M))$
70	69	ralrimiva	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to \forall k \in ℕ_{0} ((A +_{f} B) (k) \neq 0 \to k \leq if (M \leq N, N, M))$
71		plyco0	$⊢ (if (M \leq N, N, M) \in ℕ_{0} \land (A +_{f} B) : ℕ_{0} ⟶ ℂ) \to ((A +_{f} B) [ℤ_{\geq (if (M \leq N, N, M) + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} ((A +_{f} B) (k) \neq 0 \to k \leq if (M \leq N, N, M)))$
72	12 22 71	syl2anc	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to ((A +_{f} B) [ℤ_{\geq (if (M \leq N, N, M) + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} ((A +_{f} B) (k) \neq 0 \to k \leq if (M \leq N, N, M)))$
73	70 72	mpbird	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (A +_{f} B) [ℤ_{\geq (if (M \leq N, N, M) + 1)}] = \{0\}$
74		simpl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F \in Poly (S)$
75		simpr	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to G \in Poly (S)$
76	1 3	coeid	$⊢ F \in Poly (S) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k})$
77	76	adantr	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k})$
78	2 4	coeid	$⊢ G \in Poly (S) \to G = (z \in ℂ ⟼ \sum_{k = 0}^{N} B (k) z^{k})$
79	78	adantl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to G = (z \in ℂ ⟼ \sum_{k = 0}^{N} B (k) z^{k})$
80	74 75 11 8 16 18 37 57 77 79	plyaddlem1	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F +_{f} G = (z \in ℂ ⟼ \sum_{k = 0}^{if (M \leq N, N, M)} (A +_{f} B) (k) z^{k})$
81	5 12 22 73 80	coeeq	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to coeff (F +_{f} G) = A +_{f} B$
82		elfznn0	$⊢ k \in (0 \dots if (M \leq N, N, M)) \to k \in ℕ_{0}$
83		ffvelrn	$⊢ ((A +_{f} B) : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to (A +_{f} B) (k) \in ℂ$
84	22 82 83	syl2an	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land k \in (0 \dots if (M \leq N, N, M))) \to (A +_{f} B) (k) \in ℂ$
85	5 12 84 80	dgrle	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to \deg (F +_{f} G) \leq if (M \leq N, N, M)$
86	81 85	jca	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (coeff (F +_{f} G) = A +_{f} B \land \deg (F +_{f} G) \leq if (M \leq N, N, M))$

Metamath Proof Explorer

Theorem coeaddlem

Proof