elaa2lem - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > elaa2lem		Structured version Visualization version GIF version

Theorem elaa2lem 45621

Description: Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 45622. (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({𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )
elaa2lem.i	⊢ 𝐼 = (𝑘 ∈ ℕ₀ ↦ ((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 12596	. . . . 5 ⊢ ℤ ⊆ ℂ
4	3	a1i 11	. . . 4 ⊢ (𝜑 → ℤ ⊆ ℂ)
5		elaa2lem.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ (Poly‘ℤ))
6		dgrcl 26166	. . . . . . . . 9 ⊢ (𝐺 ∈ (Poly‘ℤ) → (deg‘𝐺) ∈ ℕ₀)
7	5, 6	syl 17	. . . . . . . 8 ⊢ (𝜑 → (deg‘𝐺) ∈ ℕ₀)
8	7	nn0zd 12614	. . . . . . 7 ⊢ (𝜑 → (deg‘𝐺) ∈ ℤ)
9		elaa2lem.m	. . . . . . . . 9 ⊢ 𝑀 = inf({𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )
10		ssrab2 4075	. . . . . . . . . 10 ⊢ {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ ℕ₀
11		nn0uz 12894	. . . . . . . . . . . . 13 ⊢ ℕ₀ = (ℤ_≥‘0)
12	10, 11	sseqtri 4016	. . . . . . . . . . . 12 ⊢ {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ_≥‘0)
13	12	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ_≥‘0))
14		elaa2lem.gn0	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺 ≠ 0_𝑝)
15	14	neneqd 2942	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝐺 = 0_𝑝)
16		eqid 2728	. . . . . . . . . . . . . . . . . 18 ⊢ (deg‘𝐺) = (deg‘𝐺)
17		eqid 2728	. . . . . . . . . . . . . . . . . 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 2944	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0)
22	7, 21	jca 511	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((deg‘𝐺) ∈ ℕ₀ ∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
23		fveq2 6897	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (deg‘𝐺) → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘(deg‘𝐺)))
24	23	neeq1d 2997	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (deg‘𝐺) → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
25	24	elrab 3682	. . . . . . . . . . . . 13 ⊢ ((deg‘𝐺) ∈ {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ ((deg‘𝐺) ∈ ℕ₀ ∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
26	22, 25	sylibr 233	. . . . . . . . . . . 12 ⊢ (𝜑 → (deg‘𝐺) ∈ {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
27	26	ne0d 4336	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅)
28		infssuzcl 12946	. . . . . . . . . . 11 ⊢ (({𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ_≥‘0) ∧ {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
29	13, 27, 28	syl2anc 583	. . . . . . . . . 10 ⊢ (𝜑 → inf({𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
30	10, 29	sselid 3978	. . . . . . . . 9 ⊢ (𝜑 → inf({𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ ℕ₀)
31	9, 30	eqeltrid 2833	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
32	31	nn0zd 12614	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℤ)
33	8, 32	zsubcld 12701	. . . . . 6 ⊢ (𝜑 → ((deg‘𝐺) − 𝑀) ∈ ℤ)
34	9	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑀 = inf({𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ))
35		infssuzle 12945	. . . . . . . . 9 ⊢ (({𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ_≥‘0) ∧ (deg‘𝐺) ∈ {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ (deg‘𝐺))
36	13, 26, 35	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → inf({𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ (deg‘𝐺))
37	34, 36	eqbrtrd 5170	. . . . . . 7 ⊢ (𝜑 → 𝑀 ≤ (deg‘𝐺))
38	7	nn0red 12563	. . . . . . . 8 ⊢ (𝜑 → (deg‘𝐺) ∈ ℝ)
39	31	nn0red 12563	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℝ)
40	38, 39	subge0d 11834	. . . . . . 7 ⊢ (𝜑 → (0 ≤ ((deg‘𝐺) − 𝑀) ↔ 𝑀 ≤ (deg‘𝐺)))
41	37, 40	mpbird 257	. . . . . 6 ⊢ (𝜑 → 0 ≤ ((deg‘𝐺) − 𝑀))
42	33, 41	jca 511	. . . . 5 ⊢ (𝜑 → (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤ ((deg‘𝐺) − 𝑀)))
43		elnn0z 12601	. . . . 5 ⊢ (((deg‘𝐺) − 𝑀) ∈ ℕ₀ ↔ (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤ ((deg‘𝐺) − 𝑀)))
44	42, 43	sylibr 233	. . . 4 ⊢ (𝜑 → ((deg‘𝐺) − 𝑀) ∈ ℕ₀)
45		0zd 12600	. . . . . . . 8 ⊢ (𝐺 ∈ (Poly‘ℤ) → 0 ∈ ℤ)
46	17	coef2 26164	. . . . . . . 8 ⊢ ((𝐺 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → (coeff‘𝐺):ℕ₀⟶ℤ)
47	5, 45, 46	syl2anc2 584	. . . . . . 7 ⊢ (𝜑 → (coeff‘𝐺):ℕ₀⟶ℤ)
48	47	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (coeff‘𝐺):ℕ₀⟶ℤ)
49		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
50	31	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝑀 ∈ ℕ₀)
51	49, 50	nn0addcld 12566	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 + 𝑀) ∈ ℕ₀)
52	48, 51	ffvelcdmd 7095	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ)
53		elaa2lem.i	. . . . 5 ⊢ 𝐼 = (𝑘 ∈ ℕ₀ ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀)))
54	52, 53	fmptd 7124	. . . 4 ⊢ (𝜑 → 𝐼:ℕ₀⟶ℤ)
55		elplyr 26134	. . . 4 ⊢ ((ℤ ⊆ ℂ ∧ ((deg‘𝐺) − 𝑀) ∈ ℕ₀ ∧ 𝐼:ℕ₀⟶ℤ) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘ℤ))
56	4, 44, 54, 55	syl3anc 1369	. . 3 ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘ℤ))
57	2, 56	eqeltrd 2829	. 2 ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))
58		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ≤ ((deg‘𝐺) − 𝑀))
59	58	iftrued 4537	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
60		iffalse 4538	. . . . . . . . . . 11 ⊢ (¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = 0)
61	60	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = 0)
62		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀))
63	38	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) ∈ ℝ)
64	39	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑀 ∈ ℝ)
65	63, 64	resubcld 11672	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) ∈ ℝ)
66		nn0re 12511	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ₀ → 𝑘 ∈ ℝ)
67	66	ad2antlr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℝ)
68	65, 67	ltnled 11391	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)))
69	62, 68	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) < 𝑘)
70	63, 64, 67	ltsubaddd 11840	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ (deg‘𝐺) < (𝑘 + 𝑀)))
71	69, 70	mpbid 231	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) < (𝑘 + 𝑀))
72		olc 867	. . . . . . . . . . . . 13 ⊢ ((deg‘𝐺) < (𝑘 + 𝑀) → (𝐺 = 0_𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)))
73	71, 72	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝐺 = 0_𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)))
74	5	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝐺 ∈ (Poly‘ℤ))
75	51	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝑘 + 𝑀) ∈ ℕ₀)
76	16, 17	dgrlt 26200	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ (Poly‘ℤ) ∧ (𝑘 + 𝑀) ∈ ℕ₀) → ((𝐺 = 0_𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)) ↔ ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)))
77	74, 75, 76	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((𝐺 = 0_𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)) ↔ ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)))
78	73, 77	mpbid 231	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0))
79	78	simprd 495	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)
80	61, 79	eqtr4d 2771	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
81	59, 80	pm2.61dan 812	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
82	81	mpteq2dva 5248	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ ℕ₀ ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0)) = (𝑘 ∈ ℕ₀ ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀))))
83	47, 4	fssd 6740	. . . . . . . . . 10 ⊢ (𝜑 → (coeff‘𝐺):ℕ₀⟶ℂ)
84	83	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (coeff‘𝐺):ℕ₀⟶ℂ)
85		elfznn0 13626	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℕ₀)
86	85	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑘 ∈ ℕ₀)
87	31	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑀 ∈ ℕ₀)
88	86, 87	nn0addcld 12566	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑘 + 𝑀) ∈ ℕ₀)
89	84, 88	ffvelcdmd 7095	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℂ)
90		eqidd 2729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...((deg‘𝐺) − 𝑀)) = (0...((deg‘𝐺) − 𝑀)))
91		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝜑)
92	53	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 = (𝑘 ∈ ℕ₀ ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀))))
93	92, 52	fvmpt2d 7018	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
94	91, 86, 93	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
95	94	adantlr 714	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
96	95	oveq1d 7435	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘)))
97	90, 96	sumeq12rdv 15685	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘)))
98	97	mpteq2dva 5248	. . . . . . . . 9 ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘))))
99	2, 98	eqtrd 2768	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘))))
100	57, 44, 89, 99	coeeq2 26175	. . . . . . 7 ⊢ (𝜑 → (coeff‘𝐹) = (𝑘 ∈ ℕ₀ ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0)))
101	82, 100, 92	3eqtr4d 2778	. . . . . 6 ⊢ (𝜑 → (coeff‘𝐹) = 𝐼)
102	101	fveq1d 6899	. . . . 5 ⊢ (𝜑 → ((coeff‘𝐹)‘0) = (𝐼‘0))
103		oveq1 7427	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑘 + 𝑀) = (0 + 𝑀))
104	103	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑘 + 𝑀) = (0 + 𝑀))
105	3, 32	sselid 3978	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℂ)
106	105	addlidd 11445	. . . . . . . . 9 ⊢ (𝜑 → (0 + 𝑀) = 𝑀)
107	106	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 = 0) → (0 + 𝑀) = 𝑀)
108	104, 107	eqtrd 2768	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑘 + 𝑀) = 𝑀)
109	108	fveq2d 6901	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 = 0) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘𝑀))
110		0nn0 12517	. . . . . . 7 ⊢ 0 ∈ ℕ₀
111	110	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℕ₀)
112	47, 31	ffvelcdmd 7095	. . . . . 6 ⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) ∈ ℤ)
113	92, 109, 111, 112	fvmptd 7012	. . . . 5 ⊢ (𝜑 → (𝐼‘0) = ((coeff‘𝐺)‘𝑀))
114		eqidd 2729	. . . . 5 ⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) = ((coeff‘𝐺)‘𝑀))
115	102, 113, 114	3eqtrd 2772	. . . 4 ⊢ (𝜑 → ((coeff‘𝐹)‘0) = ((coeff‘𝐺)‘𝑀))
116	34, 29	eqeltrd 2829	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
117		fveq2 6897	. . . . . . . 8 ⊢ (𝑛 = 𝑀 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑀))
118	117	neeq1d 2997	. . . . . . 7 ⊢ (𝑛 = 𝑀 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑀) ≠ 0))
119	118	elrab 3682	. . . . . 6 ⊢ (𝑀 ∈ {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ (𝑀 ∈ ℕ₀ ∧ ((coeff‘𝐺)‘𝑀) ≠ 0))
120	116, 119	sylib 217	. . . . 5 ⊢ (𝜑 → (𝑀 ∈ ℕ₀ ∧ ((coeff‘𝐺)‘𝑀) ≠ 0))
121	120	simprd 495	. . . 4 ⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) ≠ 0)
122	115, 121	eqnetrd 3005	. . 3 ⊢ (𝜑 → ((coeff‘𝐹)‘0) ≠ 0)
123	5, 45	syl 17	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
124		aasscn 26252	. . . . . . . . . . 11 ⊢ 𝔸 ⊆ ℂ
125		elaa2lem.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ 𝔸)
126	124, 125	sselid 3978	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
127	91, 126	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝐴 ∈ ℂ)
128	127, 86	expcld 14142	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐴↑𝑘) ∈ ℂ)
129	89, 128	mulcld 11264	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) ∈ ℂ)
130		fvoveq1 7443	. . . . . . . 8 ⊢ (𝑘 = (𝑗 − 𝑀) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)))
131		oveq2 7428	. . . . . . . 8 ⊢ (𝑘 = (𝑗 − 𝑀) → (𝐴↑𝑘) = (𝐴↑(𝑗 − 𝑀)))
132	130, 131	oveq12d 7438	. . . . . . 7 ⊢ (𝑘 = (𝑗 − 𝑀) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))))
133	32, 123, 33, 129, 132	fsumshft 15758	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))))
134	3, 8	sselid 3978	. . . . . . . . . 10 ⊢ (𝜑 → (deg‘𝐺) ∈ ℂ)
135	134, 105	npcand 11605	. . . . . . . . 9 ⊢ (𝜑 → (((deg‘𝐺) − 𝑀) + 𝑀) = (deg‘𝐺))
136	106, 135	oveq12d 7438	. . . . . . . 8 ⊢ (𝜑 → ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀)) = (𝑀...(deg‘𝐺)))
137	136	sumeq1d 15679	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))))
138		elfzelz 13533	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑗 ∈ ℤ)
139	138	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ)
140	3, 139	sselid 3978	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℂ)
141	105	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℂ)
142	140, 141	npcand 11605	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((𝑗 − 𝑀) + 𝑀) = 𝑗)
143	142	fveq2d 6901	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) = ((coeff‘𝐺)‘𝑗))
144	143	oveq1d 7435	. . . . . . . . 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 14153	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑(𝑗 − 𝑀)) = ((𝐴↑𝑗) / (𝐴↑𝑀)))
150	149	oveq2d 7436	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀))) = (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀))))
151	83	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (coeff‘𝐺):ℕ₀⟶ℂ)
152		0red 11247	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ∈ ℝ)
153	39	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℝ)
154	139	zred 12696	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ)
155	31	nn0ge0d 12565	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ≤ 𝑀)
156	155	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑀)
157		elfzle1 13536	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑀 ≤ 𝑗)
158	157	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ≤ 𝑗)
159	152, 153, 154, 156, 158	letrd 11401	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑗)
160	139, 159	jca 511	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
161		elnn0z 12601	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ₀ ↔ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
162	160, 161	sylibr 233	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ₀)
163	151, 162	ffvelcdmd 7095	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ)
164	145, 162	expcld 14142	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑗) ∈ ℂ)
165	126, 31	expcld 14142	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴↑𝑀) ∈ ℂ)
166	165	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑀) ∈ ℂ)
167	145, 147, 148	expne0d 14148	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑀) ≠ 0)
168	163, 164, 166, 167	divassd 12055	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀))))
169	168	eqcomd 2734	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
170	150, 169	eqtr2d 2769	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀))))
171	144, 170	eqtr4d 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
172	171	sumeq2dv 15681	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
173	137, 172	eqtrd 2768	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
174	31, 11	eleqtrdi 2839	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
175		fzss1 13572	. . . . . . . 8 ⊢ (𝑀 ∈ (ℤ_≥‘0) → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺)))
176	174, 175	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺)))
177	163, 164	mulcld 11264	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) ∈ ℂ)
178	177, 166, 167	divcld 12020	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) ∈ ℂ)
179	32	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℤ)
180	8	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (deg‘𝐺) ∈ ℤ)
181		eldifi 4125	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ (0...(deg‘𝐺)))
182	181	elfzelzd 13534	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ)
183	182	ad2antlr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℤ)
184		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ¬ 𝑗 < 𝑀)
185	39	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℝ)
186	183	zred 12696	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℝ)
187	185, 186	lenltd 11390	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (𝑀 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑀))
188	184, 187	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ≤ 𝑗)
189		elfzle2 13537	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ≤ (deg‘𝐺))
190	181, 189	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ≤ (deg‘𝐺))
191	190	ad2antlr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ≤ (deg‘𝐺))
192	179, 180, 183, 188, 191	elfzd 13524	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ (𝑀...(deg‘𝐺)))
193		eldifn 4126	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → ¬ 𝑗 ∈ (𝑀...(deg‘𝐺)))
194	193	ad2antlr 726	. . . . . . . . . . . . . 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({𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ))
198	12	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ_≥‘0))
199		elfznn0 13626	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ∈ ℕ₀)
200	181, 199	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ₀)
201	200	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℕ₀)
202		neqne 2945	. . . . . . . . . . . . . . . . . . 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) → (𝑗 ∈ ℕ₀ ∧ ((coeff‘𝐺)‘𝑗) ≠ 0))
205		fveq2 6897	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑗))
206	205	neeq1d 2997	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑗) ≠ 0))
207	206	elrab 3682	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ (𝑗 ∈ ℕ₀ ∧ ((coeff‘𝐺)‘𝑗) ≠ 0))
208	204, 207	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
209	208	adantll 713	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
210		infssuzle 12945	. . . . . . . . . . . . . . 15 ⊢ (({𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ_≥‘0) ∧ 𝑗 ∈ {𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗)
211	198, 209, 210	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → inf({𝑛 ∈ ℕ₀ ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗)
212	197, 211	eqbrtrd 5170	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ≤ 𝑗)
213	39	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ∈ ℝ)
214	182	zred 12696	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ)
215	214	ad2antlr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℝ)
216	213, 215	lenltd 11390	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → (𝑀 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑀))
217	212, 216	mpbid 231	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → ¬ 𝑗 < 𝑀)
218	196, 217	condan 817	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((coeff‘𝐺)‘𝑗) = 0)
219	218	oveq1d 7435	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) = (0 · (𝐴↑𝑗)))
220	126	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝐴 ∈ ℂ)
221	200	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝑗 ∈ ℕ₀)
222	220, 221	expcld 14142	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (𝐴↑𝑗) ∈ ℂ)
223	222	mul02d 11442	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 · (𝐴↑𝑗)) = 0)
224	219, 223	eqtrd 2768	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) = 0)
225	224	oveq1d 7435	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (0 / (𝐴↑𝑀)))
226	126, 146, 32	expne0d 14148	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴↑𝑀) ≠ 0)
227	165, 226	div0d 12019	. . . . . . . . 9 ⊢ (𝜑 → (0 / (𝐴↑𝑀)) = 0)
228	227	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 / (𝐴↑𝑀)) = 0)
229	225, 228	eqtrd 2768	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = 0)
230		fzfid 13970	. . . . . . 7 ⊢ (𝜑 → (0...(deg‘𝐺)) ∈ Fin)
231	176, 178, 229, 230	fsumss 15703	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
232	133, 173, 231	3eqtrd 2772	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
233	86, 52	syldan 590	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ)
234	53	fvmpt2 7016	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ₀ ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
235	86, 233, 234	syl2anc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
236	235	adantlr 714	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
237		oveq1 7427	. . . . . . . . 9 ⊢ (𝑧 = 𝐴 → (𝑧↑𝑘) = (𝐴↑𝑘))
238	237	ad2antlr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑧↑𝑘) = (𝐴↑𝑘))
239	236, 238	oveq12d 7438	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)))
240	239	sumeq2dv 15681	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 = 𝐴) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)))
241		fzfid 13970	. . . . . . 7 ⊢ (𝜑 → (0...((deg‘𝐺) − 𝑀)) ∈ Fin)
242	241, 129	fsumcl 15711	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) ∈ ℂ)
243	2, 240, 126, 242	fvmptd 7012	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐴) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)))
244	17, 16	coeid2 26172	. . . . . . . 8 ⊢ ((𝐺 ∈ (Poly‘ℤ) ∧ 𝐴 ∈ ℂ) → (𝐺‘𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)))
245	5, 126, 244	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)))
246	245	oveq1d 7435	. . . . . 6 ⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
247	83	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (coeff‘𝐺):ℕ₀⟶ℂ)
248	199	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → 𝑗 ∈ ℕ₀)
249	247, 248	ffvelcdmd 7095	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ)
250	126	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → 𝐴 ∈ ℂ)
251	250, 248	expcld 14142	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (𝐴↑𝑗) ∈ ℂ)
252	249, 251	mulcld 11264	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) ∈ ℂ)
253	230, 165, 252, 226	fsumdivc 15764	. . . . . 6 ⊢ (𝜑 → (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
254	246, 253	eqtrd 2768	. . . . 5 ⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)))
255	232, 243, 254	3eqtr4d 2778	. . . 4 ⊢ (𝜑 → (𝐹‘𝐴) = ((𝐺‘𝐴) / (𝐴↑𝑀)))
256		elaa2lem.ga	. . . . 5 ⊢ (𝜑 → (𝐺‘𝐴) = 0)
257	256	oveq1d 7435	. . . 4 ⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = (0 / (𝐴↑𝑀)))
258	255, 257, 227	3eqtrd 2772	. . 3 ⊢ (𝜑 → (𝐹‘𝐴) = 0)
259	122, 258	jca 511	. 2 ⊢ (𝜑 → (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0))
260		fveq2 6897	. . . . . 6 ⊢ (𝑓 = 𝐹 → (coeff‘𝑓) = (coeff‘𝐹))
261	260	fveq1d 6899	. . . . 5 ⊢ (𝑓 = 𝐹 → ((coeff‘𝑓)‘0) = ((coeff‘𝐹)‘0))
262	261	neeq1d 2997	. . . 4 ⊢ (𝑓 = 𝐹 → (((coeff‘𝑓)‘0) ≠ 0 ↔ ((coeff‘𝐹)‘0) ≠ 0))
263		fveq1 6896	. . . . 5 ⊢ (𝑓 = 𝐹 → (𝑓‘𝐴) = (𝐹‘𝐴))
264	263	eqeq1d 2730	. . . 4 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝐴) = 0 ↔ (𝐹‘𝐴) = 0))
265	262, 264	anbi12d 631	. . 3 ⊢ (𝑓 = 𝐹 → ((((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0) ↔ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0)))
266	265	rspcev 3609	. 2 ⊢ ((𝐹 ∈ (Poly‘ℤ) ∧ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0)) → ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0))
267	57, 259, 266	syl2anc 583	1 ⊢ (𝜑 → ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 846 = wceq 1534 ∈ wcel 2099 ≠ wne 2937 ∃wrex 3067 {crab 3429 ∖ cdif 3944 ⊆ wss 3947 ∅c0 4323 ifcif 4529 class class class wbr 5148 ↦ cmpt 5231 ⟶wf 6544 ‘cfv 6548 (class class class)co 7420 infcinf 9464 ℂcc 11136 ℝcr 11137 0cc0 11138 + caddc 11141 · cmul 11143 < clt 11278 ≤ cle 11279 − cmin 11474 / cdiv 11901 ℕ₀cn0 12502 ℤcz 12588 ℤ_≥cuz 12852 ...cfz 13516 ↑cexp 14058 Σcsu 15664 0_𝑝c0p 25597 Polycply 26117 coeffccoe 26119 degcdgr 26120 𝔸caa 26248

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5365 ax-pr 5429 ax-un 7740 ax-inf2 9664 ax-cnex 11194 ax-resscn 11195 ax-1cn 11196 ax-icn 11197 ax-addcl 11198 ax-addrcl 11199 ax-mulcl 11200 ax-mulrcl 11201 ax-mulcom 11202 ax-addass 11203 ax-mulass 11204 ax-distr 11205 ax-i2m1 11206 ax-1ne0 11207 ax-1rid 11208 ax-rnegex 11209 ax-rrecex 11210 ax-cnre 11211 ax-pre-lttri 11212 ax-pre-lttrn 11213 ax-pre-ltadd 11214 ax-pre-mulgt0 11215 ax-pre-sup 11216

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3373 df-reu 3374 df-rab 3430 df-v 3473 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-int 4950 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-se 5634 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-pred 6305 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-iota 6500 df-fun 6550 df-fn 6551 df-f 6552 df-f1 6553 df-fo 6554 df-f1o 6555 df-fv 6556 df-isom 6557 df-riota 7376 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7685 df-om 7871 df-1st 7993 df-2nd 7994 df-frecs 8286 df-wrecs 8317 df-recs 8391 df-rdg 8430 df-1o 8486 df-er 8724 df-map 8846 df-pm 8847 df-en 8964 df-dom 8965 df-sdom 8966 df-fin 8967 df-sup 9465 df-inf 9466 df-oi 9533 df-card 9962 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 df-sub 11476 df-neg 11477 df-div 11902 df-nn 12243 df-2 12305 df-3 12306 df-n0 12503 df-z 12589 df-uz 12853 df-rp 13007 df-fz 13517 df-fzo 13660 df-fl 13789 df-seq 13999 df-exp 14059 df-hash 14322 df-cj 15078 df-re 15079 df-im 15080 df-sqrt 15214 df-abs 15215 df-clim 15464 df-rlim 15465 df-sum 15665 df-0p 25598 df-ply 26121 df-coe 26123 df-dgr 26124 df-aa 26249

This theorem is referenced by: elaa2 45622

W3C validator

	
		OSZAR »