Theorem elaa2lem 46661

Description: Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 46662. (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 12532	. . . . 5 ⊢ ℤ ⊆ ℂ
4	3	a1i 11	. . . 4 ⊢ (𝜑 → ℤ ⊆ ℂ)
5		elaa2lem.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ (Poly‘ℤ))
6		dgrcl 26198	. . . . . . . . 9 ⊢ (𝐺 ∈ (Poly‘ℤ) → (deg‘𝐺) ∈ ℕ0)
7	5, 6	syl 17	. . . . . . . 8 ⊢ (𝜑 → (deg‘𝐺) ∈ ℕ0)
8	7	nn0zd 12549	. . . . . . 7 ⊢ (𝜑 → (deg‘𝐺) ∈ ℤ)
9		elaa2lem.m	. . . . . . . . 9 ⊢ 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )
10		ssrab2 4020	. . . . . . . . . 10 ⊢ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ ℕ0
11		nn0uz 12826	. . . . . . . . . . . . 13 ⊢ ℕ0 = (ℤ≥‘0)
12	10, 11	sseqtri 3970	. . . . . . . . . . . 12 ⊢ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ≥‘0)
13	12	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ≥‘0))
14		elaa2lem.gn0	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺 ≠ 0𝑝)
15	14	neneqd 2937	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝐺 = 0𝑝)
16		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (deg‘𝐺) = (deg‘𝐺)
17		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (coeff‘𝐺) = (coeff‘𝐺)
18	16, 17	dgreq0 26230	. . . . . . . . . . . . . . . . 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 2939	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0)
22	7, 21	jca 511	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((deg‘𝐺) ∈ ℕ0 ∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
23		fveq2 6840	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (deg‘𝐺) → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘(deg‘𝐺)))
24	23	neeq1d 2991	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (deg‘𝐺) → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
25	24	elrab 3634	. . . . . . . . . . . . 13 ⊢ ((deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ ((deg‘𝐺) ∈ ℕ0 ∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
26	22, 25	sylibr 234	. . . . . . . . . . . 12 ⊢ (𝜑 → (deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
27	26	ne0d 4282	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅)
28		infssuzcl 12882	. . . . . . . . . . 11 ⊢ (({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ≥‘0) ∧ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
29	13, 27, 28	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
30	10, 29	sselid 3919	. . . . . . . . 9 ⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ ℕ0)
31	9, 30	eqeltrid 2840	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
32	31	nn0zd 12549	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℤ)
33	8, 32	zsubcld 12638	. . . . . 6 ⊢ (𝜑 → ((deg‘𝐺) − 𝑀) ∈ ℤ)
34	9	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ))
35		infssuzle 12881	. . . . . . . . 9 ⊢ (({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ≥‘0) ∧ (deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ (deg‘𝐺))
36	13, 26, 35	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ (deg‘𝐺))
37	34, 36	eqbrtrd 5107	. . . . . . 7 ⊢ (𝜑 → 𝑀 ≤ (deg‘𝐺))
38	7	nn0red 12499	. . . . . . . 8 ⊢ (𝜑 → (deg‘𝐺) ∈ ℝ)
39	31	nn0red 12499	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℝ)
40	38, 39	subge0d 11740	. . . . . . 7 ⊢ (𝜑 → (0 ≤ ((deg‘𝐺) − 𝑀) ↔ 𝑀 ≤ (deg‘𝐺)))
41	37, 40	mpbird 257	. . . . . 6 ⊢ (𝜑 → 0 ≤ ((deg‘𝐺) − 𝑀))
42	33, 41	jca 511	. . . . 5 ⊢ (𝜑 → (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤ ((deg‘𝐺) − 𝑀)))
43		elnn0z 12537	. . . . 5 ⊢ (((deg‘𝐺) − 𝑀) ∈ ℕ0 ↔ (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤ ((deg‘𝐺) − 𝑀)))
44	42, 43	sylibr 234	. . . 4 ⊢ (𝜑 → ((deg‘𝐺) − 𝑀) ∈ ℕ0)
45		0zd 12536	. . . . . . . 8 ⊢ (𝐺 ∈ (Poly‘ℤ) → 0 ∈ ℤ)
46	17	coef2 26196	. . . . . . . 8 ⊢ ((𝐺 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → (coeff‘𝐺):ℕ0⟶ℤ)
47	5, 45, 46	syl2anc2 586	. . . . . . 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 12502	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 𝑀) ∈ ℕ0)
52	48, 51	ffvelcdmd 7037	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ)
53		elaa2lem.i	. . . . 5 ⊢ 𝐼 = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀)))
54	52, 53	fmptd 7066	. . . 4 ⊢ (𝜑 → 𝐼:ℕ0⟶ℤ)
55		elplyr 26166	. . . 4 ⊢ ((ℤ ⊆ ℂ ∧ ((deg‘𝐺) − 𝑀) ∈ ℕ0 ∧ 𝐼:ℕ0⟶ℤ) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘ℤ))
56	4, 44, 54, 55	syl3anc 1374	. . 3 ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘ℤ))
57	2, 56	eqeltrd 2836	. 2 ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))
58		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ≤ ((deg‘𝐺) − 𝑀))
59	58	iftrued 4474	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
60		iffalse 4475	. . . . . . . . . . 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 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) ∈ ℝ)
64	39	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑀 ∈ ℝ)
65	63, 64	resubcld 11578	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) ∈ ℝ)
66		nn0re 12446	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ)
67	66	ad2antlr 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℝ)
68	65, 67	ltnled 11293	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)))
69	62, 68	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) < 𝑘)
70	63, 64, 67	ltsubaddd 11746	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ (deg‘𝐺) < (𝑘 + 𝑀)))
71	69, 70	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) < (𝑘 + 𝑀))
72		olc 869	. . . . . . . . . . . . 13 ⊢ ((deg‘𝐺) < (𝑘 + 𝑀) → (𝐺 = 0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)))
73	71, 72	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝐺 = 0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)))
74	5	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝐺 ∈ (Poly‘ℤ))
75	51	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝑘 + 𝑀) ∈ ℕ0)
76	16, 17	dgrlt 26231	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ (Poly‘ℤ) ∧ (𝑘 + 𝑀) ∈ ℕ0) → ((𝐺 = 0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)) ↔ ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)))
77	74, 75, 76	syl2anc 585	. . . . . . . . . . . 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 2774	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
81	59, 80	pm2.61dan 813	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
82	81	mpteq2dva 5178	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0)) = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀))))
83	47, 4	fssd 6685	. . . . . . . . . 10 ⊢ (𝜑 → (coeff‘𝐺):ℕ0⟶ℂ)
84	83	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (coeff‘𝐺):ℕ0⟶ℂ)
85		elfznn0 13574	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℕ0)
86	85	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑘 ∈ ℕ0)
87	31	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑀 ∈ ℕ0)
88	86, 87	nn0addcld 12502	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑘 + 𝑀) ∈ ℕ0)
89	84, 88	ffvelcdmd 7037	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℂ)
90		eqidd 2737	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...((deg‘𝐺) − 𝑀)) = (0...((deg‘𝐺) − 𝑀)))
91		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝜑)
92	53	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀))))
93	92, 52	fvmpt2d 6961	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
94	91, 86, 93	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
95	94	adantlr 716	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
96	95	oveq1d 7382	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘)))
97	90, 96	sumeq12rdv 15669	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘)))
98	97	mpteq2dva 5178	. . . . . . . . 9 ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘))))
99	2, 98	eqtrd 2771	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘))))
100	57, 44, 89, 99	coeeq2 26207	. . . . . . 7 ⊢ (𝜑 → (coeff‘𝐹) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0)))
101	82, 100, 92	3eqtr4d 2781	. . . . . 6 ⊢ (𝜑 → (coeff‘𝐹) = 𝐼)
102	101	fveq1d 6842	. . . . 5 ⊢ (𝜑 → ((coeff‘𝐹)‘0) = (𝐼‘0))
103		oveq1 7374	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑘 + 𝑀) = (0 + 𝑀))
104	103	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑘 + 𝑀) = (0 + 𝑀))
105	3, 32	sselid 3919	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℂ)
106	105	addlidd 11347	. . . . . . . . 9 ⊢ (𝜑 → (0 + 𝑀) = 𝑀)
107	106	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 = 0) → (0 + 𝑀) = 𝑀)
108	104, 107	eqtrd 2771	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑘 + 𝑀) = 𝑀)
109	108	fveq2d 6844	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 = 0) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘𝑀))
110		0nn0 12452	. . . . . . 7 ⊢ 0 ∈ ℕ0
111	110	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℕ0)
112	47, 31	ffvelcdmd 7037	. . . . . 6 ⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) ∈ ℤ)
113	92, 109, 111, 112	fvmptd 6955	. . . . 5 ⊢ (𝜑 → (𝐼‘0) = ((coeff‘𝐺)‘𝑀))
114		eqidd 2737	. . . . 5 ⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) = ((coeff‘𝐺)‘𝑀))
115	102, 113, 114	3eqtrd 2775	. . . 4 ⊢ (𝜑 → ((coeff‘𝐹)‘0) = ((coeff‘𝐺)‘𝑀))
116	34, 29	eqeltrd 2836	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
117		fveq2 6840	. . . . . . . 8 ⊢ (𝑛 = 𝑀 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑀))
118	117	neeq1d 2991	. . . . . . 7 ⊢ (𝑛 = 𝑀 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑀) ≠ 0))
119	118	elrab 3634	. . . . . 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 2999	. . 3 ⊢ (𝜑 → ((coeff‘𝐹)‘0) ≠ 0)
123	5, 45	syl 17	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
124		aasscn 26284	. . . . . . . . . . 11 ⊢ 𝔸 ⊆ ℂ
125		elaa2lem.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ 𝔸)
126	124, 125	sselid 3919	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
127	91, 126	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝐴 ∈ ℂ)
128	127, 86	expcld 14108	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐴↑𝑘) ∈ ℂ)
129	89, 128	mulcld 11165	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) ∈ ℂ)
130		fvoveq1 7390	. . . . . . . 8 ⊢ (𝑘 = (𝑗 − 𝑀) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)))
131		oveq2 7375	. . . . . . . 8 ⊢ (𝑘 = (𝑗 − 𝑀) → (𝐴↑𝑘) = (𝐴↑(𝑗 − 𝑀)))
132	130, 131	oveq12d 7385	. . . . . . 7 ⊢ (𝑘 = (𝑗 − 𝑀) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))))
133	32, 123, 33, 129, 132	fsumshft 15742	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))))
134	3, 8	sselid 3919	. . . . . . . . . 10 ⊢ (𝜑 → (deg‘𝐺) ∈ ℂ)
135	134, 105	npcand 11509	. . . . . . . . 9 ⊢ (𝜑 → (((deg‘𝐺) − 𝑀) + 𝑀) = (deg‘𝐺))
136	106, 135	oveq12d 7385	. . . . . . . 8 ⊢ (𝜑 → ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀)) = (𝑀...(deg‘𝐺)))
137	136	sumeq1d 15662	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))))
138		elfzelz 13478	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑗 ∈ ℤ)
139	138	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ)
140	3, 139	sselid 3919	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℂ)
141	105	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℂ)
142	140, 141	npcand 11509	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((𝑗 − 𝑀) + 𝑀) = 𝑗)
143	142	fveq2d 6844	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) = ((coeff‘𝐺)‘𝑗))
144	143	oveq1d 7382	. . . . . . . . 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 14119	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑(𝑗 − 𝑀)) = ((𝐴↑𝑗) / (𝐴↑𝑀)))
150	149	oveq2d 7383	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀))) = (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀))))
151	83	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (coeff‘𝐺):ℕ0⟶ℂ)
152		0red 11147	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ∈ ℝ)
153	39	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℝ)
154	139	zred 12633	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ)
155	31	nn0ge0d 12501	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ≤ 𝑀)
156	155	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑀)
157		elfzle1 13481	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑀 ≤ 𝑗)
158	157	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ≤ 𝑗)
159	152, 153, 154, 156, 158	letrd 11303	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑗)
160	139, 159	jca 511	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
161		elnn0z 12537	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ0 ↔ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
162	160, 161	sylibr 234	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ0)
163	151, 162	ffvelcdmd 7037	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ)
164	145, 162	expcld 14108	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑗) ∈ ℂ)
165	126, 31	expcld 14108	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴↑𝑀) ∈ ℂ)
166	165	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑀) ∈ ℂ)
167	145, 147, 148	expne0d 14114	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑀) ≠ 0)
168	163, 164, 166, 167	divassd 11966	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀))))
169	168	eqcomd 2742	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
170	150, 169	eqtr2d 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀))))
171	144, 170	eqtr4d 2774	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
172	171	sumeq2dv 15664	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
173	137, 172	eqtrd 2771	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
174	31, 11	eleqtrdi 2846	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘0))
175		fzss1 13517	. . . . . . . 8 ⊢ (𝑀 ∈ (ℤ≥‘0) → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺)))
176	174, 175	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺)))
177	163, 164	mulcld 11165	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) ∈ ℂ)
178	177, 166, 167	divcld 11931	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) ∈ ℂ)
179	32	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℤ)
180	8	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (deg‘𝐺) ∈ ℤ)
181		eldifi 4071	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ (0...(deg‘𝐺)))
182	181	elfzelzd 13479	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ)
183	182	ad2antlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℤ)
184		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ¬ 𝑗 < 𝑀)
185	39	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℝ)
186	183	zred 12633	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℝ)
187	185, 186	lenltd 11292	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (𝑀 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑀))
188	184, 187	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ≤ 𝑗)
189		elfzle2 13482	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ≤ (deg‘𝐺))
190	181, 189	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ≤ (deg‘𝐺))
191	190	ad2antlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ≤ (deg‘𝐺))
192	179, 180, 183, 188, 191	elfzd 13469	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ (𝑀...(deg‘𝐺)))
193		eldifn 4072	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → ¬ 𝑗 ∈ (𝑀...(deg‘𝐺)))
194	193	ad2antlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ¬ 𝑗 ∈ (𝑀...(deg‘𝐺)))
195	192, 194	condan 818	. . . . . . . . . . . . 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 13574	. . . . . . . . . . . . . . . . . . . 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 2940	. . . . . . . . . . . . . . . . . . 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 6840	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑗))
206	205	neeq1d 2991	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑗) ≠ 0))
207	206	elrab 3634	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ (𝑗 ∈ ℕ0 ∧ ((coeff‘𝐺)‘𝑗) ≠ 0))
208	204, 207	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
209	208	adantll 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
210		infssuzle 12881	. . . . . . . . . . . . . . 15 ⊢ (({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ≥‘0) ∧ 𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗)
211	198, 209, 210	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗)
212	197, 211	eqbrtrd 5107	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ≤ 𝑗)
213	39	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ∈ ℝ)
214	182	zred 12633	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ)
215	214	ad2antlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℝ)
216	213, 215	lenltd 11292	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → (𝑀 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑀))
217	212, 216	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → ¬ 𝑗 < 𝑀)
218	196, 217	condan 818	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((coeff‘𝐺)‘𝑗) = 0)
219	218	oveq1d 7382	. . . . . . . . . 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 14108	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (𝐴↑𝑗) ∈ ℂ)
223	222	mul02d 11344	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 · (𝐴↑𝑗)) = 0)
224	219, 223	eqtrd 2771	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) = 0)
225	224	oveq1d 7382	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (0 / (𝐴↑𝑀)))
226	126, 146, 32	expne0d 14114	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴↑𝑀) ≠ 0)
227	165, 226	div0d 11930	. . . . . . . . 9 ⊢ (𝜑 → (0 / (𝐴↑𝑀)) = 0)
228	227	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 / (𝐴↑𝑀)) = 0)
229	225, 228	eqtrd 2771	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = 0)
230		fzfid 13935	. . . . . . 7 ⊢ (𝜑 → (0...(deg‘𝐺)) ∈ Fin)
231	176, 178, 229, 230	fsumss 15687	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
232	133, 173, 231	3eqtrd 2775	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
233	86, 52	syldan 592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ)
234	53	fvmpt2 6959	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ0 ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
235	86, 233, 234	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
236	235	adantlr 716	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
237		oveq1 7374	. . . . . . . . 9 ⊢ (𝑧 = 𝐴 → (𝑧↑𝑘) = (𝐴↑𝑘))
238	237	ad2antlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑧↑𝑘) = (𝐴↑𝑘))
239	236, 238	oveq12d 7385	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)))
240	239	sumeq2dv 15664	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 = 𝐴) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)))
241		fzfid 13935	. . . . . . 7 ⊢ (𝜑 → (0...((deg‘𝐺) − 𝑀)) ∈ Fin)
242	241, 129	fsumcl 15695	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) ∈ ℂ)
243	2, 240, 126, 242	fvmptd 6955	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐴) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)))
244	17, 16	coeid2 26204	. . . . . . . 8 ⊢ ((𝐺 ∈ (Poly‘ℤ) ∧ 𝐴 ∈ ℂ) → (𝐺‘𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)))
245	5, 126, 244	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)))
246	245	oveq1d 7382	. . . . . 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 7037	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ)
250	126	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → 𝐴 ∈ ℂ)
251	250, 248	expcld 14108	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (𝐴↑𝑗) ∈ ℂ)
252	249, 251	mulcld 11165	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) ∈ ℂ)
253	230, 165, 252, 226	fsumdivc 15748	. . . . . 6 ⊢ (𝜑 → (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
254	246, 253	eqtrd 2771	. . . . 5 ⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
255	232, 243, 254	3eqtr4d 2781	. . . 4 ⊢ (𝜑 → (𝐹‘𝐴) = ((𝐺‘𝐴) / (𝐴↑𝑀)))
256		elaa2lem.ga	. . . . 5 ⊢ (𝜑 → (𝐺‘𝐴) = 0)
257	256	oveq1d 7382	. . . 4 ⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = (0 / (𝐴↑𝑀)))
258	255, 257, 227	3eqtrd 2775	. . 3 ⊢ (𝜑 → (𝐹‘𝐴) = 0)
259	122, 258	jca 511	. 2 ⊢ (𝜑 → (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0))
260		fveq2 6840	. . . . . 6 ⊢ (𝑓 = 𝐹 → (coeff‘𝑓) = (coeff‘𝐹))
261	260	fveq1d 6842	. . . . 5 ⊢ (𝑓 = 𝐹 → ((coeff‘𝑓)‘0) = ((coeff‘𝐹)‘0))
262	261	neeq1d 2991	. . . 4 ⊢ (𝑓 = 𝐹 → (((coeff‘𝑓)‘0) ≠ 0 ↔ ((coeff‘𝐹)‘0) ≠ 0))
263		fveq1 6839	. . . . 5 ⊢ (𝑓 = 𝐹 → (𝑓‘𝐴) = (𝐹‘𝐴))
264	263	eqeq1d 2738	. . . 4 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝐴) = 0 ↔ (𝐹‘𝐴) = 0))
265	262, 264	anbi12d 633	. . 3 ⊢ (𝑓 = 𝐹 → ((((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0) ↔ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0)))
266	265	rspcev 3564	. 2 ⊢ ((𝐹 ∈ (Poly‘ℤ) ∧ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0)) → ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0))
267	57, 259, 266	syl2anc 585	1 ⊢ (𝜑 → ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ≠ wne 2932  ∃wrex 3061  {crab 3389   ∖ cdif 3886   ⊆ wss 3889  ∅c0 4273  ifcif 4466   class class class wbr 5085   ↦ cmpt 5166  ⟶wf 6494  ‘cfv 6498  (class class class)co 7367  infcinf 9354  ℂcc 11036  ℝcr 11037  0cc0 11038   + caddc 11041   · cmul 11043   < clt 11179   ≤ cle 11180   − cmin 11377   / cdiv 11807  ℕ₀cn0 12437  ℤcz 12524  ℤ_≥cuz 12788  ...cfz 13461  ↑cexp 14023  Σcsu 15648  0_𝑝c0p 25636  Polycply 26149  coeffccoe 26151  degcdgr 26152  𝔸caa 26280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-inf2 9562  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-isom 6507  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-of 7631  df-om 7818  df-1st 7942  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-er 8643  df-map 8775  df-pm 8776  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-sup 9355  df-inf 9356  df-oi 9425  df-card 9863  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808  df-nn 12175  df-2 12244  df-3 12245  df-n0 12438  df-z 12525  df-uz 12789  df-rp 12943  df-fz 13462  df-fzo 13609  df-fl 13751  df-seq 13964  df-exp 14024  df-hash 14293  df-cj 15061  df-re 15062  df-im 15063  df-sqrt 15197  df-abs 15198  df-clim 15450  df-rlim 15451  df-sum 15649  df-0p 25637  df-ply 26153  df-coe 26155  df-dgr 26156  df-aa 26281

This theorem is referenced by:  elaa2  46662