Theorem elaa2lem 46231

Description: Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 46232. (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 12537	. . . . 5 ⊢ ℤ ⊆ ℂ
4	3	a1i 11	. . . 4 ⊢ (𝜑 → ℤ ⊆ ℂ)
5		elaa2lem.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ (Poly‘ℤ))
6		dgrcl 26138	. . . . . . . . 9 ⊢ (𝐺 ∈ (Poly‘ℤ) → (deg‘𝐺) ∈ ℕ0)
7	5, 6	syl 17	. . . . . . . 8 ⊢ (𝜑 → (deg‘𝐺) ∈ ℕ0)
8	7	nn0zd 12555	. . . . . . 7 ⊢ (𝜑 → (deg‘𝐺) ∈ ℤ)
9		elaa2lem.m	. . . . . . . . 9 ⊢ 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )
10		ssrab2 4043	. . . . . . . . . 10 ⊢ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ ℕ0
11		nn0uz 12835	. . . . . . . . . . . . 13 ⊢ ℕ0 = (ℤ≥‘0)
12	10, 11	sseqtri 3995	. . . . . . . . . . . 12 ⊢ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ≥‘0)
13	12	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ≥‘0))
14		elaa2lem.gn0	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺 ≠ 0𝑝)
15	14	neneqd 2930	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝐺 = 0𝑝)
16		eqid 2729	. . . . . . . . . . . . . . . . . 18 ⊢ (deg‘𝐺) = (deg‘𝐺)
17		eqid 2729	. . . . . . . . . . . . . . . . . 18 ⊢ (coeff‘𝐺) = (coeff‘𝐺)
18	16, 17	dgreq0 26171	. . . . . . . . . . . . . . . . 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 2932	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0)
22	7, 21	jca 511	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((deg‘𝐺) ∈ ℕ0 ∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
23		fveq2 6858	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (deg‘𝐺) → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘(deg‘𝐺)))
24	23	neeq1d 2984	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (deg‘𝐺) → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
25	24	elrab 3659	. . . . . . . . . . . . 13 ⊢ ((deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ ((deg‘𝐺) ∈ ℕ0 ∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
26	22, 25	sylibr 234	. . . . . . . . . . . 12 ⊢ (𝜑 → (deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
27	26	ne0d 4305	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅)
28		infssuzcl 12891	. . . . . . . . . . 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 3944	. . . . . . . . 9 ⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ ℕ0)
31	9, 30	eqeltrid 2832	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
32	31	nn0zd 12555	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℤ)
33	8, 32	zsubcld 12643	. . . . . 6 ⊢ (𝜑 → ((deg‘𝐺) − 𝑀) ∈ ℤ)
34	9	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ))
35		infssuzle 12890	. . . . . . . . 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 5129	. . . . . . 7 ⊢ (𝜑 → 𝑀 ≤ (deg‘𝐺))
38	7	nn0red 12504	. . . . . . . 8 ⊢ (𝜑 → (deg‘𝐺) ∈ ℝ)
39	31	nn0red 12504	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℝ)
40	38, 39	subge0d 11768	. . . . . . 7 ⊢ (𝜑 → (0 ≤ ((deg‘𝐺) − 𝑀) ↔ 𝑀 ≤ (deg‘𝐺)))
41	37, 40	mpbird 257	. . . . . 6 ⊢ (𝜑 → 0 ≤ ((deg‘𝐺) − 𝑀))
42	33, 41	jca 511	. . . . 5 ⊢ (𝜑 → (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤ ((deg‘𝐺) − 𝑀)))
43		elnn0z 12542	. . . . 5 ⊢ (((deg‘𝐺) − 𝑀) ∈ ℕ0 ↔ (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤ ((deg‘𝐺) − 𝑀)))
44	42, 43	sylibr 234	. . . 4 ⊢ (𝜑 → ((deg‘𝐺) − 𝑀) ∈ ℕ0)
45		0zd 12541	. . . . . . . 8 ⊢ (𝐺 ∈ (Poly‘ℤ) → 0 ∈ ℤ)
46	17	coef2 26136	. . . . . . . 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 12507	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 𝑀) ∈ ℕ0)
52	48, 51	ffvelcdmd 7057	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ)
53		elaa2lem.i	. . . . 5 ⊢ 𝐼 = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀)))
54	52, 53	fmptd 7086	. . . 4 ⊢ (𝜑 → 𝐼:ℕ0⟶ℤ)
55		elplyr 26106	. . . 4 ⊢ ((ℤ ⊆ ℂ ∧ ((deg‘𝐺) − 𝑀) ∈ ℕ0 ∧ 𝐼:ℕ0⟶ℤ) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘ℤ))
56	4, 44, 54, 55	syl3anc 1373	. . 3 ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘ℤ))
57	2, 56	eqeltrd 2828	. 2 ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))
58		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ≤ ((deg‘𝐺) − 𝑀))
59	58	iftrued 4496	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
60		iffalse 4497	. . . . . . . . . . 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 11606	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) ∈ ℝ)
66		nn0re 12451	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ)
67	66	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℝ)
68	65, 67	ltnled 11321	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)))
69	62, 68	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) < 𝑘)
70	63, 64, 67	ltsubaddd 11774	. . . . . . . . . . . . . 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 26172	. . . . . . . . . . . . 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 2767	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
81	59, 80	pm2.61dan 812	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
82	81	mpteq2dva 5200	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0)) = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀))))
83	47, 4	fssd 6705	. . . . . . . . . 10 ⊢ (𝜑 → (coeff‘𝐺):ℕ0⟶ℂ)
84	83	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (coeff‘𝐺):ℕ0⟶ℂ)
85		elfznn0 13581	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℕ0)
86	85	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑘 ∈ ℕ0)
87	31	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑀 ∈ ℕ0)
88	86, 87	nn0addcld 12507	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑘 + 𝑀) ∈ ℕ0)
89	84, 88	ffvelcdmd 7057	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℂ)
90		eqidd 2730	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...((deg‘𝐺) − 𝑀)) = (0...((deg‘𝐺) − 𝑀)))
91		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝜑)
92	53	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀))))
93	92, 52	fvmpt2d 6981	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
94	91, 86, 93	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
95	94	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
96	95	oveq1d 7402	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘)))
97	90, 96	sumeq12rdv 15673	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘)))
98	97	mpteq2dva 5200	. . . . . . . . 9 ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘))))
99	2, 98	eqtrd 2764	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘))))
100	57, 44, 89, 99	coeeq2 26147	. . . . . . 7 ⊢ (𝜑 → (coeff‘𝐹) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0)))
101	82, 100, 92	3eqtr4d 2774	. . . . . 6 ⊢ (𝜑 → (coeff‘𝐹) = 𝐼)
102	101	fveq1d 6860	. . . . 5 ⊢ (𝜑 → ((coeff‘𝐹)‘0) = (𝐼‘0))
103		oveq1 7394	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑘 + 𝑀) = (0 + 𝑀))
104	103	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑘 + 𝑀) = (0 + 𝑀))
105	3, 32	sselid 3944	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℂ)
106	105	addlidd 11375	. . . . . . . . 9 ⊢ (𝜑 → (0 + 𝑀) = 𝑀)
107	106	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 = 0) → (0 + 𝑀) = 𝑀)
108	104, 107	eqtrd 2764	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑘 + 𝑀) = 𝑀)
109	108	fveq2d 6862	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 = 0) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘𝑀))
110		0nn0 12457	. . . . . . 7 ⊢ 0 ∈ ℕ0
111	110	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℕ0)
112	47, 31	ffvelcdmd 7057	. . . . . 6 ⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) ∈ ℤ)
113	92, 109, 111, 112	fvmptd 6975	. . . . 5 ⊢ (𝜑 → (𝐼‘0) = ((coeff‘𝐺)‘𝑀))
114		eqidd 2730	. . . . 5 ⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) = ((coeff‘𝐺)‘𝑀))
115	102, 113, 114	3eqtrd 2768	. . . 4 ⊢ (𝜑 → ((coeff‘𝐹)‘0) = ((coeff‘𝐺)‘𝑀))
116	34, 29	eqeltrd 2828	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
117		fveq2 6858	. . . . . . . 8 ⊢ (𝑛 = 𝑀 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑀))
118	117	neeq1d 2984	. . . . . . 7 ⊢ (𝑛 = 𝑀 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑀) ≠ 0))
119	118	elrab 3659	. . . . . 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 2992	. . 3 ⊢ (𝜑 → ((coeff‘𝐹)‘0) ≠ 0)
123	5, 45	syl 17	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
124		aasscn 26226	. . . . . . . . . . 11 ⊢ 𝔸 ⊆ ℂ
125		elaa2lem.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ 𝔸)
126	124, 125	sselid 3944	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
127	91, 126	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝐴 ∈ ℂ)
128	127, 86	expcld 14111	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐴↑𝑘) ∈ ℂ)
129	89, 128	mulcld 11194	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) ∈ ℂ)
130		fvoveq1 7410	. . . . . . . 8 ⊢ (𝑘 = (𝑗 − 𝑀) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)))
131		oveq2 7395	. . . . . . . 8 ⊢ (𝑘 = (𝑗 − 𝑀) → (𝐴↑𝑘) = (𝐴↑(𝑗 − 𝑀)))
132	130, 131	oveq12d 7405	. . . . . . 7 ⊢ (𝑘 = (𝑗 − 𝑀) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))))
133	32, 123, 33, 129, 132	fsumshft 15746	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))))
134	3, 8	sselid 3944	. . . . . . . . . 10 ⊢ (𝜑 → (deg‘𝐺) ∈ ℂ)
135	134, 105	npcand 11537	. . . . . . . . 9 ⊢ (𝜑 → (((deg‘𝐺) − 𝑀) + 𝑀) = (deg‘𝐺))
136	106, 135	oveq12d 7405	. . . . . . . 8 ⊢ (𝜑 → ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀)) = (𝑀...(deg‘𝐺)))
137	136	sumeq1d 15666	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))))
138		elfzelz 13485	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑗 ∈ ℤ)
139	138	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ)
140	3, 139	sselid 3944	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℂ)
141	105	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℂ)
142	140, 141	npcand 11537	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((𝑗 − 𝑀) + 𝑀) = 𝑗)
143	142	fveq2d 6862	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) = ((coeff‘𝐺)‘𝑗))
144	143	oveq1d 7402	. . . . . . . . 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 14122	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑(𝑗 − 𝑀)) = ((𝐴↑𝑗) / (𝐴↑𝑀)))
150	149	oveq2d 7403	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀))) = (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀))))
151	83	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (coeff‘𝐺):ℕ0⟶ℂ)
152		0red 11177	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ∈ ℝ)
153	39	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℝ)
154	139	zred 12638	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ)
155	31	nn0ge0d 12506	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ≤ 𝑀)
156	155	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑀)
157		elfzle1 13488	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑀 ≤ 𝑗)
158	157	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ≤ 𝑗)
159	152, 153, 154, 156, 158	letrd 11331	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑗)
160	139, 159	jca 511	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
161		elnn0z 12542	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ0 ↔ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
162	160, 161	sylibr 234	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ0)
163	151, 162	ffvelcdmd 7057	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ)
164	145, 162	expcld 14111	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑗) ∈ ℂ)
165	126, 31	expcld 14111	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴↑𝑀) ∈ ℂ)
166	165	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑀) ∈ ℂ)
167	145, 147, 148	expne0d 14117	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑀) ≠ 0)
168	163, 164, 166, 167	divassd 11993	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀))))
169	168	eqcomd 2735	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
170	150, 169	eqtr2d 2765	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀))))
171	144, 170	eqtr4d 2767	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
172	171	sumeq2dv 15668	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
173	137, 172	eqtrd 2764	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
174	31, 11	eleqtrdi 2838	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘0))
175		fzss1 13524	. . . . . . . 8 ⊢ (𝑀 ∈ (ℤ≥‘0) → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺)))
176	174, 175	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺)))
177	163, 164	mulcld 11194	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) ∈ ℂ)
178	177, 166, 167	divcld 11958	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) ∈ ℂ)
179	32	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℤ)
180	8	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (deg‘𝐺) ∈ ℤ)
181		eldifi 4094	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ (0...(deg‘𝐺)))
182	181	elfzelzd 13486	. . . . . . . . . . . . . . . 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 12638	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℝ)
187	185, 186	lenltd 11320	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (𝑀 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑀))
188	184, 187	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ≤ 𝑗)
189		elfzle2 13489	. . . . . . . . . . . . . . . . 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 13476	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ (𝑀...(deg‘𝐺)))
193		eldifn 4095	. . . . . . . . . . . . . . 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 13581	. . . . . . . . . . . . . . . . . . . 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 2933	. . . . . . . . . . . . . . . . . . 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 6858	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑗))
206	205	neeq1d 2984	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑗) ≠ 0))
207	206	elrab 3659	. . . . . . . . . . . . . . . . 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 12890	. . . . . . . . . . . . . . 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 5129	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ≤ 𝑗)
213	39	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ∈ ℝ)
214	182	zred 12638	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ)
215	214	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℝ)
216	213, 215	lenltd 11320	. . . . . . . . . . . . 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 7402	. . . . . . . . . 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 14111	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (𝐴↑𝑗) ∈ ℂ)
223	222	mul02d 11372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 · (𝐴↑𝑗)) = 0)
224	219, 223	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) = 0)
225	224	oveq1d 7402	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (0 / (𝐴↑𝑀)))
226	126, 146, 32	expne0d 14117	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴↑𝑀) ≠ 0)
227	165, 226	div0d 11957	. . . . . . . . 9 ⊢ (𝜑 → (0 / (𝐴↑𝑀)) = 0)
228	227	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 / (𝐴↑𝑀)) = 0)
229	225, 228	eqtrd 2764	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = 0)
230		fzfid 13938	. . . . . . 7 ⊢ (𝜑 → (0...(deg‘𝐺)) ∈ Fin)
231	176, 178, 229, 230	fsumss 15691	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
232	133, 173, 231	3eqtrd 2768	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
233	86, 52	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ)
234	53	fvmpt2 6979	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ0 ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
235	86, 233, 234	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
236	235	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
237		oveq1 7394	. . . . . . . . 9 ⊢ (𝑧 = 𝐴 → (𝑧↑𝑘) = (𝐴↑𝑘))
238	237	ad2antlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑧↑𝑘) = (𝐴↑𝑘))
239	236, 238	oveq12d 7405	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)))
240	239	sumeq2dv 15668	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 = 𝐴) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)))
241		fzfid 13938	. . . . . . 7 ⊢ (𝜑 → (0...((deg‘𝐺) − 𝑀)) ∈ Fin)
242	241, 129	fsumcl 15699	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) ∈ ℂ)
243	2, 240, 126, 242	fvmptd 6975	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐴) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)))
244	17, 16	coeid2 26144	. . . . . . . 8 ⊢ ((𝐺 ∈ (Poly‘ℤ) ∧ 𝐴 ∈ ℂ) → (𝐺‘𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)))
245	5, 126, 244	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)))
246	245	oveq1d 7402	. . . . . 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 7057	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ)
250	126	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → 𝐴 ∈ ℂ)
251	250, 248	expcld 14111	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (𝐴↑𝑗) ∈ ℂ)
252	249, 251	mulcld 11194	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) ∈ ℂ)
253	230, 165, 252, 226	fsumdivc 15752	. . . . . 6 ⊢ (𝜑 → (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
254	246, 253	eqtrd 2764	. . . . 5 ⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
255	232, 243, 254	3eqtr4d 2774	. . . 4 ⊢ (𝜑 → (𝐹‘𝐴) = ((𝐺‘𝐴) / (𝐴↑𝑀)))
256		elaa2lem.ga	. . . . 5 ⊢ (𝜑 → (𝐺‘𝐴) = 0)
257	256	oveq1d 7402	. . . 4 ⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = (0 / (𝐴↑𝑀)))
258	255, 257, 227	3eqtrd 2768	. . 3 ⊢ (𝜑 → (𝐹‘𝐴) = 0)
259	122, 258	jca 511	. 2 ⊢ (𝜑 → (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0))
260		fveq2 6858	. . . . . 6 ⊢ (𝑓 = 𝐹 → (coeff‘𝑓) = (coeff‘𝐹))
261	260	fveq1d 6860	. . . . 5 ⊢ (𝑓 = 𝐹 → ((coeff‘𝑓)‘0) = ((coeff‘𝐹)‘0))
262	261	neeq1d 2984	. . . 4 ⊢ (𝑓 = 𝐹 → (((coeff‘𝑓)‘0) ≠ 0 ↔ ((coeff‘𝐹)‘0) ≠ 0))
263		fveq1 6857	. . . . 5 ⊢ (𝑓 = 𝐹 → (𝑓‘𝐴) = (𝐹‘𝐴))
264	263	eqeq1d 2731	. . . 4 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝐴) = 0 ↔ (𝐹‘𝐴) = 0))
265	262, 264	anbi12d 632	. . 3 ⊢ (𝑓 = 𝐹 → ((((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0) ↔ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0)))
266	265	rspcev 3588	. 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 1540   ∈ wcel 2109   ≠ wne 2925  ∃wrex 3053  {crab 3405   ∖ cdif 3911   ⊆ wss 3914  ∅c0 4296  ifcif 4488   class class class wbr 5107   ↦ cmpt 5188  ⟶wf 6507  ‘cfv 6511  (class class class)co 7387  infcinf 9392  ℂcc 11066  ℝcr 11067  0cc0 11068   + caddc 11071   · cmul 11073   < clt 11208   ≤ cle 11209   − cmin 11405   / cdiv 11835  ℕ₀cn0 12442  ℤcz 12529  ℤ_≥cuz 12793  ...cfz 13468  ↑cexp 14026  Σcsu 15652  0_𝑝c0p 25570  Polycply 26089  coeffccoe 26091  degcdgr 26092  𝔸caa 26222

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-inf2 9594  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145  ax-pre-sup 11146

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-se 5592  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-of 7653  df-om 7843  df-1st 7968  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-er 8671  df-map 8801  df-pm 8802  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-sup 9393  df-inf 9394  df-oi 9463  df-card 9892  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-div 11836  df-nn 12187  df-2 12249  df-3 12250  df-n0 12443  df-z 12530  df-uz 12794  df-rp 12952  df-fz 13469  df-fzo 13616  df-fl 13754  df-seq 13967  df-exp 14027  df-hash 14296  df-cj 15065  df-re 15066  df-im 15067  df-sqrt 15201  df-abs 15202  df-clim 15454  df-rlim 15455  df-sum 15653  df-0p 25571  df-ply 26093  df-coe 26095  df-dgr 26096  df-aa 26223

This theorem is referenced by:  elaa2  46232