Theorem elaa2lem 46277

Description: Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 46278. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by AV, 1-Oct-2020.)

Hypotheses

Ref	Expression
elaa2lem.a	⊢ (𝜑 → 𝐴 ∈ 𝔸)
elaa2lem.an0	⊢ (𝜑 → 𝐴 ≠ 0)
elaa2lem.g	⊢ (𝜑 → 𝐺 ∈ (Poly‘ℤ))
elaa2lem.gn0	⊢ (𝜑 → 𝐺 ≠ 0𝑝)
elaa2lem.ga	⊢ (𝜑 → (𝐺‘𝐴) = 0)
elaa2lem.m	⊢ 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )
elaa2lem.i	⊢ 𝐼 = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀)))
elaa2lem.f	⊢ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)))

Assertion

Ref	Expression
elaa2lem	⊢ (𝜑 → ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0))

Distinct variable groups:   𝐴,𝑓   𝐴,𝑘,𝑧   𝑓,𝐹   𝑘,𝐺   𝑛,𝐺   𝑧,𝐺   𝑘,𝐼,𝑧   𝑘,𝑀   𝑛,𝑀   𝑧,𝑀   𝜑,𝑘,𝑧

Allowed substitution hints:   𝜑(𝑓,𝑛)   𝐴(𝑛)   𝐹(𝑧,𝑘,𝑛)   𝐺(𝑓)   𝐼(𝑓,𝑛)   𝑀(𝑓)

Proof of Theorem elaa2lem

Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elaa2lem.f	. . . 4 ⊢ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)))
2	1	a1i 11	. . 3 ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))))
3		zsscn 12476	. . . . 5 ⊢ ℤ ⊆ ℂ
4	3	a1i 11	. . . 4 ⊢ (𝜑 → ℤ ⊆ ℂ)
5		elaa2lem.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ (Poly‘ℤ))
6		dgrcl 26166	. . . . . . . . 9 ⊢ (𝐺 ∈ (Poly‘ℤ) → (deg‘𝐺) ∈ ℕ0)
7	5, 6	syl 17	. . . . . . . 8 ⊢ (𝜑 → (deg‘𝐺) ∈ ℕ0)
8	7	nn0zd 12494	. . . . . . 7 ⊢ (𝜑 → (deg‘𝐺) ∈ ℤ)
9		elaa2lem.m	. . . . . . . . 9 ⊢ 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )
10		ssrab2 4030	. . . . . . . . . 10 ⊢ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ ℕ0
11		nn0uz 12774	. . . . . . . . . . . . 13 ⊢ ℕ0 = (ℤ≥‘0)
12	10, 11	sseqtri 3983	. . . . . . . . . . . 12 ⊢ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ≥‘0)
13	12	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ≥‘0))
14		elaa2lem.gn0	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺 ≠ 0𝑝)
15	14	neneqd 2933	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝐺 = 0𝑝)
16		eqid 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (deg‘𝐺) = (deg‘𝐺)
17		eqid 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (coeff‘𝐺) = (coeff‘𝐺)
18	16, 17	dgreq0 26199	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 ∈ (Poly‘ℤ) → (𝐺 = 0𝑝 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) = 0))
19	5, 18	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐺 = 0𝑝 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) = 0))
20	15, 19	mtbid 324	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ ((coeff‘𝐺)‘(deg‘𝐺)) = 0)
21	20	neqned 2935	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0)
22	7, 21	jca 511	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((deg‘𝐺) ∈ ℕ0 ∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
23		fveq2 6822	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (deg‘𝐺) → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘(deg‘𝐺)))
24	23	neeq1d 2987	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (deg‘𝐺) → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
25	24	elrab 3647	. . . . . . . . . . . . 13 ⊢ ((deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ ((deg‘𝐺) ∈ ℕ0 ∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
26	22, 25	sylibr 234	. . . . . . . . . . . 12 ⊢ (𝜑 → (deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
27	26	ne0d 4292	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅)
28		infssuzcl 12830	. . . . . . . . . . 11 ⊢ (({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ≥‘0) ∧ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
29	13, 27, 28	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
30	10, 29	sselid 3932	. . . . . . . . 9 ⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ ℕ0)
31	9, 30	eqeltrid 2835	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
32	31	nn0zd 12494	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℤ)
33	8, 32	zsubcld 12582	. . . . . 6 ⊢ (𝜑 → ((deg‘𝐺) − 𝑀) ∈ ℤ)
34	9	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ))
35		infssuzle 12829	. . . . . . . . 9 ⊢ (({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ≥‘0) ∧ (deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ (deg‘𝐺))
36	13, 26, 35	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ (deg‘𝐺))
37	34, 36	eqbrtrd 5113	. . . . . . 7 ⊢ (𝜑 → 𝑀 ≤ (deg‘𝐺))
38	7	nn0red 12443	. . . . . . . 8 ⊢ (𝜑 → (deg‘𝐺) ∈ ℝ)
39	31	nn0red 12443	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℝ)
40	38, 39	subge0d 11707	. . . . . . 7 ⊢ (𝜑 → (0 ≤ ((deg‘𝐺) − 𝑀) ↔ 𝑀 ≤ (deg‘𝐺)))
41	37, 40	mpbird 257	. . . . . 6 ⊢ (𝜑 → 0 ≤ ((deg‘𝐺) − 𝑀))
42	33, 41	jca 511	. . . . 5 ⊢ (𝜑 → (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤ ((deg‘𝐺) − 𝑀)))
43		elnn0z 12481	. . . . 5 ⊢ (((deg‘𝐺) − 𝑀) ∈ ℕ0 ↔ (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤ ((deg‘𝐺) − 𝑀)))
44	42, 43	sylibr 234	. . . 4 ⊢ (𝜑 → ((deg‘𝐺) − 𝑀) ∈ ℕ0)
45		0zd 12480	. . . . . . . 8 ⊢ (𝐺 ∈ (Poly‘ℤ) → 0 ∈ ℤ)
46	17	coef2 26164	. . . . . . . 8 ⊢ ((𝐺 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → (coeff‘𝐺):ℕ0⟶ℤ)
47	5, 45, 46	syl2anc2 585	. . . . . . 7 ⊢ (𝜑 → (coeff‘𝐺):ℕ0⟶ℤ)
48	47	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (coeff‘𝐺):ℕ0⟶ℤ)
49		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
50	31	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈ ℕ0)
51	49, 50	nn0addcld 12446	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 𝑀) ∈ ℕ0)
52	48, 51	ffvelcdmd 7018	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ)
53		elaa2lem.i	. . . . 5 ⊢ 𝐼 = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀)))
54	52, 53	fmptd 7047	. . . 4 ⊢ (𝜑 → 𝐼:ℕ0⟶ℤ)
55		elplyr 26134	. . . 4 ⊢ ((ℤ ⊆ ℂ ∧ ((deg‘𝐺) − 𝑀) ∈ ℕ0 ∧ 𝐼:ℕ0⟶ℤ) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘ℤ))
56	4, 44, 54, 55	syl3anc 1373	. . 3 ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘ℤ))
57	2, 56	eqeltrd 2831	. 2 ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))
58		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ≤ ((deg‘𝐺) − 𝑀))
59	58	iftrued 4483	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
60		iffalse 4484	. . . . . . . . . . 11 ⊢ (¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = 0)
61	60	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = 0)
62		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀))
63	38	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) ∈ ℝ)
64	39	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑀 ∈ ℝ)
65	63, 64	resubcld 11545	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) ∈ ℝ)
66		nn0re 12390	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ)
67	66	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℝ)
68	65, 67	ltnled 11260	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)))
69	62, 68	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) < 𝑘)
70	63, 64, 67	ltsubaddd 11713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ (deg‘𝐺) < (𝑘 + 𝑀)))
71	69, 70	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) < (𝑘 + 𝑀))
72		olc 868	. . . . . . . . . . . . 13 ⊢ ((deg‘𝐺) < (𝑘 + 𝑀) → (𝐺 = 0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)))
73	71, 72	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝐺 = 0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)))
74	5	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝐺 ∈ (Poly‘ℤ))
75	51	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝑘 + 𝑀) ∈ ℕ0)
76	16, 17	dgrlt 26200	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ (Poly‘ℤ) ∧ (𝑘 + 𝑀) ∈ ℕ0) → ((𝐺 = 0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)) ↔ ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)))
77	74, 75, 76	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((𝐺 = 0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)) ↔ ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)))
78	73, 77	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0))
79	78	simprd 495	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)
80	61, 79	eqtr4d 2769	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
81	59, 80	pm2.61dan 812	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
82	81	mpteq2dva 5184	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0)) = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀))))
83	47, 4	fssd 6668	. . . . . . . . . 10 ⊢ (𝜑 → (coeff‘𝐺):ℕ0⟶ℂ)
84	83	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (coeff‘𝐺):ℕ0⟶ℂ)
85		elfznn0 13520	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℕ0)
86	85	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑘 ∈ ℕ0)
87	31	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑀 ∈ ℕ0)
88	86, 87	nn0addcld 12446	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑘 + 𝑀) ∈ ℕ0)
89	84, 88	ffvelcdmd 7018	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℂ)
90		eqidd 2732	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...((deg‘𝐺) − 𝑀)) = (0...((deg‘𝐺) − 𝑀)))
91		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝜑)
92	53	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀))))
93	92, 52	fvmpt2d 6942	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
94	91, 86, 93	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
95	94	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
96	95	oveq1d 7361	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘)))
97	90, 96	sumeq12rdv 15614	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘)))
98	97	mpteq2dva 5184	. . . . . . . . 9 ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘))))
99	2, 98	eqtrd 2766	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘))))
100	57, 44, 89, 99	coeeq2 26175	. . . . . . 7 ⊢ (𝜑 → (coeff‘𝐹) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0)))
101	82, 100, 92	3eqtr4d 2776	. . . . . 6 ⊢ (𝜑 → (coeff‘𝐹) = 𝐼)
102	101	fveq1d 6824	. . . . 5 ⊢ (𝜑 → ((coeff‘𝐹)‘0) = (𝐼‘0))
103		oveq1 7353	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑘 + 𝑀) = (0 + 𝑀))
104	103	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑘 + 𝑀) = (0 + 𝑀))
105	3, 32	sselid 3932	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℂ)
106	105	addlidd 11314	. . . . . . . . 9 ⊢ (𝜑 → (0 + 𝑀) = 𝑀)
107	106	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 = 0) → (0 + 𝑀) = 𝑀)
108	104, 107	eqtrd 2766	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑘 + 𝑀) = 𝑀)
109	108	fveq2d 6826	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 = 0) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘𝑀))
110		0nn0 12396	. . . . . . 7 ⊢ 0 ∈ ℕ0
111	110	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℕ0)
112	47, 31	ffvelcdmd 7018	. . . . . 6 ⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) ∈ ℤ)
113	92, 109, 111, 112	fvmptd 6936	. . . . 5 ⊢ (𝜑 → (𝐼‘0) = ((coeff‘𝐺)‘𝑀))
114		eqidd 2732	. . . . 5 ⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) = ((coeff‘𝐺)‘𝑀))
115	102, 113, 114	3eqtrd 2770	. . . 4 ⊢ (𝜑 → ((coeff‘𝐹)‘0) = ((coeff‘𝐺)‘𝑀))
116	34, 29	eqeltrd 2831	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
117		fveq2 6822	. . . . . . . 8 ⊢ (𝑛 = 𝑀 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑀))
118	117	neeq1d 2987	. . . . . . 7 ⊢ (𝑛 = 𝑀 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑀) ≠ 0))
119	118	elrab 3647	. . . . . 6 ⊢ (𝑀 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ (𝑀 ∈ ℕ0 ∧ ((coeff‘𝐺)‘𝑀) ≠ 0))
120	116, 119	sylib 218	. . . . 5 ⊢ (𝜑 → (𝑀 ∈ ℕ0 ∧ ((coeff‘𝐺)‘𝑀) ≠ 0))
121	120	simprd 495	. . . 4 ⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) ≠ 0)
122	115, 121	eqnetrd 2995	. . 3 ⊢ (𝜑 → ((coeff‘𝐹)‘0) ≠ 0)
123	5, 45	syl 17	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
124		aasscn 26254	. . . . . . . . . . 11 ⊢ 𝔸 ⊆ ℂ
125		elaa2lem.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ 𝔸)
126	124, 125	sselid 3932	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
127	91, 126	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝐴 ∈ ℂ)
128	127, 86	expcld 14053	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐴↑𝑘) ∈ ℂ)
129	89, 128	mulcld 11132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) ∈ ℂ)
130		fvoveq1 7369	. . . . . . . 8 ⊢ (𝑘 = (𝑗 − 𝑀) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)))
131		oveq2 7354	. . . . . . . 8 ⊢ (𝑘 = (𝑗 − 𝑀) → (𝐴↑𝑘) = (𝐴↑(𝑗 − 𝑀)))
132	130, 131	oveq12d 7364	. . . . . . 7 ⊢ (𝑘 = (𝑗 − 𝑀) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))))
133	32, 123, 33, 129, 132	fsumshft 15687	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))))
134	3, 8	sselid 3932	. . . . . . . . . 10 ⊢ (𝜑 → (deg‘𝐺) ∈ ℂ)
135	134, 105	npcand 11476	. . . . . . . . 9 ⊢ (𝜑 → (((deg‘𝐺) − 𝑀) + 𝑀) = (deg‘𝐺))
136	106, 135	oveq12d 7364	. . . . . . . 8 ⊢ (𝜑 → ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀)) = (𝑀...(deg‘𝐺)))
137	136	sumeq1d 15607	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))))
138		elfzelz 13424	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑗 ∈ ℤ)
139	138	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ)
140	3, 139	sselid 3932	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℂ)
141	105	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℂ)
142	140, 141	npcand 11476	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((𝑗 − 𝑀) + 𝑀) = 𝑗)
143	142	fveq2d 6826	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) = ((coeff‘𝐺)‘𝑗))
144	143	oveq1d 7361	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀))))
145	126	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝐴 ∈ ℂ)
146		elaa2lem.an0	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ≠ 0)
147	146	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝐴 ≠ 0)
148	32	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℤ)
149	145, 147, 148, 139	expsubd 14064	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑(𝑗 − 𝑀)) = ((𝐴↑𝑗) / (𝐴↑𝑀)))
150	149	oveq2d 7362	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀))) = (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀))))
151	83	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (coeff‘𝐺):ℕ0⟶ℂ)
152		0red 11115	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ∈ ℝ)
153	39	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℝ)
154	139	zred 12577	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ)
155	31	nn0ge0d 12445	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ≤ 𝑀)
156	155	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑀)
157		elfzle1 13427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑀 ≤ 𝑗)
158	157	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ≤ 𝑗)
159	152, 153, 154, 156, 158	letrd 11270	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑗)
160	139, 159	jca 511	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
161		elnn0z 12481	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ0 ↔ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
162	160, 161	sylibr 234	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ0)
163	151, 162	ffvelcdmd 7018	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ)
164	145, 162	expcld 14053	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑗) ∈ ℂ)
165	126, 31	expcld 14053	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴↑𝑀) ∈ ℂ)
166	165	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑀) ∈ ℂ)
167	145, 147, 148	expne0d 14059	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑀) ≠ 0)
168	163, 164, 166, 167	divassd 11932	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀))))
169	168	eqcomd 2737	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
170	150, 169	eqtr2d 2767	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀))))
171	144, 170	eqtr4d 2769	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
172	171	sumeq2dv 15609	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
173	137, 172	eqtrd 2766	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
174	31, 11	eleqtrdi 2841	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘0))
175		fzss1 13463	. . . . . . . 8 ⊢ (𝑀 ∈ (ℤ≥‘0) → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺)))
176	174, 175	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺)))
177	163, 164	mulcld 11132	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) ∈ ℂ)
178	177, 166, 167	divcld 11897	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) ∈ ℂ)
179	32	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℤ)
180	8	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (deg‘𝐺) ∈ ℤ)
181		eldifi 4081	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ (0...(deg‘𝐺)))
182	181	elfzelzd 13425	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ)
183	182	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℤ)
184		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ¬ 𝑗 < 𝑀)
185	39	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℝ)
186	183	zred 12577	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℝ)
187	185, 186	lenltd 11259	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (𝑀 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑀))
188	184, 187	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ≤ 𝑗)
189		elfzle2 13428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ≤ (deg‘𝐺))
190	181, 189	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ≤ (deg‘𝐺))
191	190	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ≤ (deg‘𝐺))
192	179, 180, 183, 188, 191	elfzd 13415	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ (𝑀...(deg‘𝐺)))
193		eldifn 4082	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → ¬ 𝑗 ∈ (𝑀...(deg‘𝐺)))
194	193	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ¬ 𝑗 ∈ (𝑀...(deg‘𝐺)))
195	192, 194	condan 817	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝑗 < 𝑀)
196	195	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 < 𝑀)
197	9	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ))
198	12	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ≥‘0))
199		elfznn0 13520	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ∈ ℕ0)
200	181, 199	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ0)
201	200	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℕ0)
202		neqne 2936	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((coeff‘𝐺)‘𝑗) = 0 → ((coeff‘𝐺)‘𝑗) ≠ 0)
203	202	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → ((coeff‘𝐺)‘𝑗) ≠ 0)
204	201, 203	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → (𝑗 ∈ ℕ0 ∧ ((coeff‘𝐺)‘𝑗) ≠ 0))
205		fveq2 6822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑗))
206	205	neeq1d 2987	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑗) ≠ 0))
207	206	elrab 3647	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ (𝑗 ∈ ℕ0 ∧ ((coeff‘𝐺)‘𝑗) ≠ 0))
208	204, 207	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
209	208	adantll 714	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
210		infssuzle 12829	. . . . . . . . . . . . . . 15 ⊢ (({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ≥‘0) ∧ 𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗)
211	198, 209, 210	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗)
212	197, 211	eqbrtrd 5113	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ≤ 𝑗)
213	39	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ∈ ℝ)
214	182	zred 12577	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ)
215	214	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℝ)
216	213, 215	lenltd 11259	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → (𝑀 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑀))
217	212, 216	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → ¬ 𝑗 < 𝑀)
218	196, 217	condan 817	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((coeff‘𝐺)‘𝑗) = 0)
219	218	oveq1d 7361	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) = (0 · (𝐴↑𝑗)))
220	126	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝐴 ∈ ℂ)
221	200	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝑗 ∈ ℕ0)
222	220, 221	expcld 14053	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (𝐴↑𝑗) ∈ ℂ)
223	222	mul02d 11311	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 · (𝐴↑𝑗)) = 0)
224	219, 223	eqtrd 2766	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) = 0)
225	224	oveq1d 7361	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (0 / (𝐴↑𝑀)))
226	126, 146, 32	expne0d 14059	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴↑𝑀) ≠ 0)
227	165, 226	div0d 11896	. . . . . . . . 9 ⊢ (𝜑 → (0 / (𝐴↑𝑀)) = 0)
228	227	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 / (𝐴↑𝑀)) = 0)
229	225, 228	eqtrd 2766	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = 0)
230		fzfid 13880	. . . . . . 7 ⊢ (𝜑 → (0...(deg‘𝐺)) ∈ Fin)
231	176, 178, 229, 230	fsumss 15632	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
232	133, 173, 231	3eqtrd 2770	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
233	86, 52	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ)
234	53	fvmpt2 6940	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ0 ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
235	86, 233, 234	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
236	235	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
237		oveq1 7353	. . . . . . . . 9 ⊢ (𝑧 = 𝐴 → (𝑧↑𝑘) = (𝐴↑𝑘))
238	237	ad2antlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑧↑𝑘) = (𝐴↑𝑘))
239	236, 238	oveq12d 7364	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)))
240	239	sumeq2dv 15609	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 = 𝐴) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)))
241		fzfid 13880	. . . . . . 7 ⊢ (𝜑 → (0...((deg‘𝐺) − 𝑀)) ∈ Fin)
242	241, 129	fsumcl 15640	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) ∈ ℂ)
243	2, 240, 126, 242	fvmptd 6936	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐴) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)))
244	17, 16	coeid2 26172	. . . . . . . 8 ⊢ ((𝐺 ∈ (Poly‘ℤ) ∧ 𝐴 ∈ ℂ) → (𝐺‘𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)))
245	5, 126, 244	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)))
246	245	oveq1d 7361	. . . . . 6 ⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
247	83	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (coeff‘𝐺):ℕ0⟶ℂ)
248	199	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → 𝑗 ∈ ℕ0)
249	247, 248	ffvelcdmd 7018	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ)
250	126	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → 𝐴 ∈ ℂ)
251	250, 248	expcld 14053	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (𝐴↑𝑗) ∈ ℂ)
252	249, 251	mulcld 11132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) ∈ ℂ)
253	230, 165, 252, 226	fsumdivc 15693	. . . . . 6 ⊢ (𝜑 → (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
254	246, 253	eqtrd 2766	. . . . 5 ⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
255	232, 243, 254	3eqtr4d 2776	. . . 4 ⊢ (𝜑 → (𝐹‘𝐴) = ((𝐺‘𝐴) / (𝐴↑𝑀)))
256		elaa2lem.ga	. . . . 5 ⊢ (𝜑 → (𝐺‘𝐴) = 0)
257	256	oveq1d 7361	. . . 4 ⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = (0 / (𝐴↑𝑀)))
258	255, 257, 227	3eqtrd 2770	. . 3 ⊢ (𝜑 → (𝐹‘𝐴) = 0)
259	122, 258	jca 511	. 2 ⊢ (𝜑 → (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0))
260		fveq2 6822	. . . . . 6 ⊢ (𝑓 = 𝐹 → (coeff‘𝑓) = (coeff‘𝐹))
261	260	fveq1d 6824	. . . . 5 ⊢ (𝑓 = 𝐹 → ((coeff‘𝑓)‘0) = ((coeff‘𝐹)‘0))
262	261	neeq1d 2987	. . . 4 ⊢ (𝑓 = 𝐹 → (((coeff‘𝑓)‘0) ≠ 0 ↔ ((coeff‘𝐹)‘0) ≠ 0))
263		fveq1 6821	. . . . 5 ⊢ (𝑓 = 𝐹 → (𝑓‘𝐴) = (𝐹‘𝐴))
264	263	eqeq1d 2733	. . . 4 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝐴) = 0 ↔ (𝐹‘𝐴) = 0))
265	262, 264	anbi12d 632	. . 3 ⊢ (𝑓 = 𝐹 → ((((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0) ↔ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0)))
266	265	rspcev 3577	. 2 ⊢ ((𝐹 ∈ (Poly‘ℤ) ∧ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0)) → ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0))
267	57, 259, 266	syl2anc 584	1 ⊢ (𝜑 → ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2111   ≠ wne 2928  ∃wrex 3056  {crab 3395   ∖ cdif 3899   ⊆ wss 3902  ∅c0 4283  ifcif 4475   class class class wbr 5091   ↦ cmpt 5172  ⟶wf 6477  ‘cfv 6481  (class class class)co 7346  infcinf 9325  ℂcc 11004  ℝcr 11005  0cc0 11006   + caddc 11009   · cmul 11011   < clt 11146   ≤ cle 11147   − cmin 11344   / cdiv 11774  ℕ₀cn0 12381  ℤcz 12468  ℤ_≥cuz 12732  ...cfz 13407  ↑cexp 13968  Σcsu 15593  0_𝑝c0p 25598  Polycply 26117  coeffccoe 26119  degcdgr 26120  𝔸caa 26250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5217  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-inf2 9531  ax-cnex 11062  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082  ax-pre-mulgt0 11083  ax-pre-sup 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-int 4898  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-se 5570  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-isom 6490  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-of 7610  df-om 7797  df-1st 7921  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-1o 8385  df-er 8622  df-map 8752  df-pm 8753  df-en 8870  df-dom 8871  df-sdom 8872  df-fin 8873  df-sup 9326  df-inf 9327  df-oi 9396  df-card 9832  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-sub 11346  df-neg 11347  df-div 11775  df-nn 12126  df-2 12188  df-3 12189  df-n0 12382  df-z 12469  df-uz 12733  df-rp 12891  df-fz 13408  df-fzo 13555  df-fl 13696  df-seq 13909  df-exp 13969  df-hash 14238  df-cj 15006  df-re 15007  df-im 15008  df-sqrt 15142  df-abs 15143  df-clim 15395  df-rlim 15396  df-sum 15594  df-0p 25599  df-ply 26121  df-coe 26123  df-dgr 26124  df-aa 26251

This theorem is referenced by:  elaa2  46278