dgradd2

Description: The degree of a sum of polynomials of unequal degrees is the degree of the larger polynomial. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypotheses	dgradd.1	$⊢ M = \deg (F)$
	dgradd.2	$⊢ N = \deg (G)$
Assertion	dgradd2	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to \deg (F +_{f} G) = N$

Proof

Step	Hyp	Ref	Expression
1		dgradd.1	$⊢ M = \deg (F)$
2		dgradd.2	$⊢ N = \deg (G)$
3		plyaddcl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F +_{f} G \in Poly (ℂ)$
4	3	3adant3	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to F +_{f} G \in Poly (ℂ)$
5		dgrcl	$⊢ F +_{f} G \in Poly (ℂ) \to \deg (F +_{f} G) \in ℕ_{0}$
6	4 5	syl	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to \deg (F +_{f} G) \in ℕ_{0}$
7	6	nn0red	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to \deg (F +_{f} G) \in ℝ$
8		dgrcl	$⊢ G \in Poly (S) \to \deg (G) \in ℕ_{0}$
9	2 8	eqeltrid	$⊢ G \in Poly (S) \to N \in ℕ_{0}$
10	9	3ad2ant2	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to N \in ℕ_{0}$
11	10	nn0red	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to N \in ℝ$
12		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
13	1 12	eqeltrid	$⊢ F \in Poly (S) \to M \in ℕ_{0}$
14	13	3ad2ant1	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to M \in ℕ_{0}$
15	14	nn0red	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to M \in ℝ$
16	11 15	ifcld	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to if (M \leq N, N, M) \in ℝ$
17	1 2	dgradd	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to \deg (F +_{f} G) \leq if (M \leq N, N, M)$
18	17	3adant3	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to \deg (F +_{f} G) \leq if (M \leq N, N, M)$
19	11	leidd	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to N \leq N$
20		simp3	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to M < N$
21	15 11 20	ltled	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to M \leq N$
22		breq1	$⊢ N = if (M \leq N, N, M) \to (N \leq N \leftrightarrow if (M \leq N, N, M) \leq N)$
23		breq1	$⊢ M = if (M \leq N, N, M) \to (M \leq N \leftrightarrow if (M \leq N, N, M) \leq N)$
24	22 23	ifboth	$⊢ (N \leq N \land M \leq N) \to if (M \leq N, N, M) \leq N$
25	19 21 24	syl2anc	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to if (M \leq N, N, M) \leq N$
26	7 16 11 18 25	letrd	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to \deg (F +_{f} G) \leq N$
27		eqid	$⊢ coeff (F) = coeff (F)$
28		eqid	$⊢ coeff (G) = coeff (G)$
29	27 28	coeadd	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to coeff (F +_{f} G) = coeff (F) +_{f} coeff (G)$
30	29	3adant3	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to coeff (F +_{f} G) = coeff (F) +_{f} coeff (G)$
31	30	fveq1d	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to coeff (F +_{f} G) (N) = (coeff (F) +_{f} coeff (G)) (N)$
32	27	coef3	$⊢ F \in Poly (S) \to coeff (F) : ℕ_{0} ⟶ ℂ$
33	32	3ad2ant1	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to coeff (F) : ℕ_{0} ⟶ ℂ$
34	33	ffnd	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to coeff (F) Fn ℕ_{0}$
35	28	coef3	$⊢ G \in Poly (S) \to coeff (G) : ℕ_{0} ⟶ ℂ$
36	35	3ad2ant2	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to coeff (G) : ℕ_{0} ⟶ ℂ$
37	36	ffnd	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to coeff (G) Fn ℕ_{0}$
38		nn0ex	$⊢ ℕ_{0} \in V$
39	38	a1i	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to ℕ_{0} \in V$
40		inidm	$⊢ ℕ_{0} \cap ℕ_{0} = ℕ_{0}$
41	15 11	ltnled	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to (M < N \leftrightarrow \neg N \leq M)$
42	20 41	mpbid	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to \neg N \leq M$
43		simp1	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to F \in Poly (S)$
44	27 1	dgrub	$⊢ (F \in Poly (S) \land N \in ℕ_{0} \land coeff (F) (N) \neq 0) \to N \leq M$
45	44	3expia	$⊢ (F \in Poly (S) \land N \in ℕ_{0}) \to (coeff (F) (N) \neq 0 \to N \leq M)$
46	43 10 45	syl2anc	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to (coeff (F) (N) \neq 0 \to N \leq M)$
47	46	necon1bd	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to (\neg N \leq M \to coeff (F) (N) = 0)$
48	42 47	mpd	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to coeff (F) (N) = 0$
49	48	adantr	$⊢ ((F \in Poly (S) \land G \in Poly (S) \land M < N) \land N \in ℕ_{0}) \to coeff (F) (N) = 0$
50		eqidd	$⊢ ((F \in Poly (S) \land G \in Poly (S) \land M < N) \land N \in ℕ_{0}) \to coeff (G) (N) = coeff (G) (N)$
51	34 37 39 39 40 49 50	ofval	$⊢ ((F \in Poly (S) \land G \in Poly (S) \land M < N) \land N \in ℕ_{0}) \to (coeff (F) +_{f} coeff (G)) (N) = 0 + coeff (G) (N)$
52	10 51	mpdan	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to (coeff (F) +_{f} coeff (G)) (N) = 0 + coeff (G) (N)$
53	36 10	ffvelcdmd	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to coeff (G) (N) \in ℂ$
54	53	addlidd	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to 0 + coeff (G) (N) = coeff (G) (N)$
55	31 52 54	3eqtrd	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to coeff (F +_{f} G) (N) = coeff (G) (N)$
56		simp2	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to G \in Poly (S)$
57		0red	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to 0 \in ℝ$
58	14	nn0ge0d	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to 0 \leq M$
59	57 15 11 58 20	lelttrd	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to 0 < N$
60	59	gt0ne0d	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to N \neq 0$
61	2 28	dgreq0	$⊢ G \in Poly (S) \to (G = 0_{𝑝} \leftrightarrow coeff (G) (N) = 0)$
62		fveq2	$⊢ G = 0_{𝑝} \to \deg (G) = \deg (0_{𝑝})$
63		dgr0	$⊢ \deg (0_{𝑝}) = 0$
64	63	eqcomi	$⊢ 0 = \deg (0_{𝑝})$
65	62 2 64	3eqtr4g	$⊢ G = 0_{𝑝} \to N = 0$
66	61 65	biimtrrdi	$⊢ G \in Poly (S) \to (coeff (G) (N) = 0 \to N = 0)$
67	66	necon3d	$⊢ G \in Poly (S) \to (N \neq 0 \to coeff (G) (N) \neq 0)$
68	56 60 67	sylc	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to coeff (G) (N) \neq 0$
69	55 68	eqnetrd	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to coeff (F +_{f} G) (N) \neq 0$
70		eqid	$⊢ coeff (F +_{f} G) = coeff (F +_{f} G)$
71		eqid	$⊢ \deg (F +_{f} G) = \deg (F +_{f} G)$
72	70 71	dgrub	$⊢ (F +_{f} G \in Poly (ℂ) \land N \in ℕ_{0} \land coeff (F +_{f} G) (N) \neq 0) \to N \leq \deg (F +_{f} G)$
73	4 10 69 72	syl3anc	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to N \leq \deg (F +_{f} G)$
74	7 11	letri3d	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to (\deg (F +_{f} G) = N \leftrightarrow (\deg (F +_{f} G) \leq N \land N \leq \deg (F +_{f} G)))$
75	26 73 74	mpbir2and	$⊢ (F \in Poly (S) \land G \in Poly (S) \land M < N) \to \deg (F +_{f} G) = N$

Metamath Proof Explorer

Theorem dgradd2

Proof