signsplypnf - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > signsplypnf		Structured version Visualization version GIF version

Theorem signsplypnf 35045

Description: The quotient of a polynomial 𝐹 by a monic monomial of same degree 𝐺 converges to the highest coefficient of 𝐹. (Contributed by Thierry Arnoux, 18-Sep-2018.)

**Hypotheses**
Ref	Expression
signsply0.d	⊢ 𝐷 = (deg‘𝐹)
signsply0.c	⊢ 𝐶 = (coeff‘𝐹)
signsply0.b	⊢ 𝐵 = (𝐶‘𝐷)
signsplypnf.g	⊢ 𝐺 = (𝑥 ∈ ℝ⁺ ↦ (𝑥↑𝐷))

**Assertion**
Ref	Expression
signsplypnf	⊢ (𝐹 ∈ (Poly‘ℝ) → (𝐹 ∘_f / 𝐺) ⇝_𝑟 𝐵)

Distinct variable groups: 𝑥,𝐶 𝑥,𝐷 𝑥,𝐹 𝑥,𝐺 Allowed substitution hint: 𝐵(𝑥)

Proof of Theorem signsplypnf Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		plyf 26425	. . . . 5 ⊢ (𝐹 ∈ (Poly‘ℝ) → 𝐹:ℂ⟶ℂ)
2	1	ffnd 6707	. . . 4 ⊢ (𝐹 ∈ (Poly‘ℝ) → 𝐹 Fn ℂ)
3		ovex 7449	. . . . . 6 ⊢ (𝑥↑𝐷) ∈ V
4	3	rgenw 3082	. . . . 5 ⊢ ∀𝑥 ∈ ℝ⁺ (𝑥↑𝐷) ∈ V
5		signsplypnf.g	. . . . . 6 ⊢ 𝐺 = (𝑥 ∈ ℝ⁺ ↦ (𝑥↑𝐷))
6	5	fnmpt 6676	. . . . 5 ⊢ (∀𝑥 ∈ ℝ⁺ (𝑥↑𝐷) ∈ V → 𝐺 Fn ℝ⁺)
7	4, 6	mp1i 14	. . . 4 ⊢ (𝐹 ∈ (Poly‘ℝ) → 𝐺 Fn ℝ⁺)
8		cnex 11208	. . . . 5 ⊢ ℂ ∈ V
9	8	a1i 11	. . . 4 ⊢ (𝐹 ∈ (Poly‘ℝ) → ℂ ∈ V)
10		reex 11218	. . . . . 6 ⊢ ℝ ∈ V
11		rpssre 13052	. . . . . 6 ⊢ ℝ⁺ ⊆ ℝ
12	10, 11	ssexi 5291	. . . . 5 ⊢ ℝ⁺ ∈ V
13	12	a1i 11	. . . 4 ⊢ (𝐹 ∈ (Poly‘ℝ) → ℝ⁺ ∈ V)
14		ax-resscn 11184	. . . . . 6 ⊢ ℝ ⊆ ℂ
15	11, 14	sstri 3943	. . . . 5 ⊢ ℝ⁺ ⊆ ℂ
16		sseqin2 4172	. . . . 5 ⊢ (ℝ⁺ ⊆ ℂ ↔ (ℂ ∩ ℝ⁺) = ℝ⁺)
17	15, 16	mpbi 233	. . . 4 ⊢ (ℂ ∩ ℝ⁺) = ℝ⁺
18		signsply0.c	. . . . 5 ⊢ 𝐶 = (coeff‘𝐹)
19		signsply0.d	. . . . 5 ⊢ 𝐷 = (deg‘𝐹)
20	18, 19	coeid2 26466	. . . 4 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℂ) → (𝐹‘𝑥) = Σ𝑘 ∈ (0...𝐷)((𝐶‘𝑘) · (𝑥↑𝑘)))
21	5	fvmpt2 7002	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ∧ (𝑥↑𝐷) ∈ V) → (𝐺‘𝑥) = (𝑥↑𝐷))
22	3, 21	mpan2 704	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ → (𝐺‘𝑥) = (𝑥↑𝐷))
23	22	adantl 487	. . . 4 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → (𝐺‘𝑥) = (𝑥↑𝐷))
24	2, 7, 9, 13, 17, 20, 23	offval 7690	. . 3 ⊢ (𝐹 ∈ (Poly‘ℝ) → (𝐹 ∘_f / 𝐺) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (0...𝐷)((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))))
25		fzfid 14039	. . . . . 6 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → (0...𝐷) ∈ Fin)
26	15	a1i 11	. . . . . . . 8 ⊢ (𝐹 ∈ (Poly‘ℝ) → ℝ⁺ ⊆ ℂ)
27	26	sselda 3934	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℂ)
28		dgrcl 26460	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘ℝ) → (deg‘𝐹) ∈ ℕ₀)
29	19, 28	eqeltrid 2866	. . . . . . . 8 ⊢ (𝐹 ∈ (Poly‘ℝ) → 𝐷 ∈ ℕ₀)
30	29	adantr 486	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → 𝐷 ∈ ℕ₀)
31	27, 30	expcld 14212	. . . . . 6 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → (𝑥↑𝐷) ∈ ℂ)
32	18	coef3 26459	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘ℝ) → 𝐶:ℕ₀⟶ℂ)
33	32	ad2antrr 739	. . . . . . . 8 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑘 ∈ (0...𝐷)) → 𝐶:ℕ₀⟶ℂ)
34		elfznn0 13677	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝐷) → 𝑘 ∈ ℕ₀)
35	34	adantl 487	. . . . . . . 8 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑘 ∈ (0...𝐷)) → 𝑘 ∈ ℕ₀)
36	33, 35	ffvelcdmd 7081	. . . . . . 7 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑘 ∈ (0...𝐷)) → (𝐶‘𝑘) ∈ ℂ)
37	27	adantr 486	. . . . . . . 8 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑘 ∈ (0...𝐷)) → 𝑥 ∈ ℂ)
38	37, 35	expcld 14212	. . . . . . 7 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑘 ∈ (0...𝐷)) → (𝑥↑𝑘) ∈ ℂ)
39	36, 38	mulcld 11256	. . . . . 6 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑘 ∈ (0...𝐷)) → ((𝐶‘𝑘) · (𝑥↑𝑘)) ∈ ℂ)
40		rpne0 13061	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ≠ 0)
41	40	adantl 487	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ≠ 0)
42	29	nn0zd 12643	. . . . . . . 8 ⊢ (𝐹 ∈ (Poly‘ℝ) → 𝐷 ∈ ℤ)
43	42	adantr 486	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → 𝐷 ∈ ℤ)
44	27, 41, 43	expne0d 14218	. . . . . 6 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → (𝑥↑𝐷) ≠ 0)
45	25, 31, 39, 44	fsumdivc 15874	. . . . 5 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑘 ∈ (0...𝐷)((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = Σ𝑘 ∈ (0...𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)))
46		fzosn 13794	. . . . . . . . 9 ⊢ (𝐷 ∈ ℤ → (𝐷..^(𝐷 + 1)) = {𝐷})
47	46	ineq2d 4169	. . . . . . . 8 ⊢ (𝐷 ∈ ℤ → ((0..^𝐷) ∩ (𝐷..^(𝐷 + 1))) = ((0..^𝐷) ∩ {𝐷}))
48		fzodisj 13751	. . . . . . . 8 ⊢ ((0..^𝐷) ∩ (𝐷..^(𝐷 + 1))) = ∅
49	47, 48	eqtr3di 2812	. . . . . . 7 ⊢ (𝐷 ∈ ℤ → ((0..^𝐷) ∩ {𝐷}) = ∅)
50	43, 49	syl 18	. . . . . 6 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → ((0..^𝐷) ∩ {𝐷}) = ∅)
51		fzval3 13792	. . . . . . . . 9 ⊢ (𝐷 ∈ ℤ → (0...𝐷) = (0..^(𝐷 + 1)))
52	42, 51	syl 18	. . . . . . . 8 ⊢ (𝐹 ∈ (Poly‘ℝ) → (0...𝐷) = (0..^(𝐷 + 1)))
53		nn0uz 12928	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
54	29, 53	eleqtrdi 2872	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘ℝ) → 𝐷 ∈ (ℤ_≥‘0))
55		fzosplitsn 13834	. . . . . . . . 9 ⊢ (𝐷 ∈ (ℤ_≥‘0) → (0..^(𝐷 + 1)) = ((0..^𝐷) ∪ {𝐷}))
56	54, 55	syl 18	. . . . . . . 8 ⊢ (𝐹 ∈ (Poly‘ℝ) → (0..^(𝐷 + 1)) = ((0..^𝐷) ∪ {𝐷}))
57	52, 56	eqtrd 2797	. . . . . . 7 ⊢ (𝐹 ∈ (Poly‘ℝ) → (0...𝐷) = ((0..^𝐷) ∪ {𝐷}))
58	57	adantr 486	. . . . . 6 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → (0...𝐷) = ((0..^𝐷) ∪ {𝐷}))
59	31	adantr 486	. . . . . . 7 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑘 ∈ (0...𝐷)) → (𝑥↑𝐷) ∈ ℂ)
60	41	adantr 486	. . . . . . . 8 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑘 ∈ (0...𝐷)) → 𝑥 ≠ 0)
61	43	adantr 486	. . . . . . . 8 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑘 ∈ (0...𝐷)) → 𝐷 ∈ ℤ)
62	37, 60, 61	expne0d 14218	. . . . . . 7 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑘 ∈ (0...𝐷)) → (𝑥↑𝐷) ≠ 0)
63	39, 59, 62	divcld 12018	. . . . . 6 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑘 ∈ (0...𝐷)) → (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ ℂ)
64	50, 58, 25, 63	fsumsplit 15829	. . . . 5 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → Σ𝑘 ∈ (0...𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))))
65	45, 64	eqtrd 2797	. . . 4 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑘 ∈ (0...𝐷)((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))))
66	65	mpteq2dva 5202	. . 3 ⊢ (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (0...𝐷)((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)))))
67	24, 66	eqtrd 2797	. 2 ⊢ (𝐹 ∈ (Poly‘ℝ) → (𝐹 ∘_f / 𝐺) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)))))
68		sumex 15777	. . . . 5 ⊢ Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V
69	68	a1i 11	. . . 4 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V)
70		sumex 15777	. . . . 5 ⊢ Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V
71	70	a1i 11	. . . 4 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V)
72	11	a1i 11	. . . . . 6 ⊢ (𝐹 ∈ (Poly‘ℝ) → ℝ⁺ ⊆ ℝ)
73		fzofi 14040	. . . . . . 7 ⊢ (0..^𝐷) ∈ Fin
74	73	a1i 11	. . . . . 6 ⊢ (𝐹 ∈ (Poly‘ℝ) → (0..^𝐷) ∈ Fin)
75		ovexd 7451	. . . . . 6 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑘 ∈ (0..^𝐷))) → (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V)
76	32	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → 𝐶:ℕ₀⟶ℂ)
77		elfzonn0 13765	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0..^𝐷) → 𝑘 ∈ ℕ₀)
78	77	ad2antlr 740	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → 𝑘 ∈ ℕ₀)
79	76, 78	ffvelcdmd 7081	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → (𝐶‘𝑘) ∈ ℂ)
80	27	adantlr 728	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℂ)
81	80, 78	expcld 14212	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → (𝑥↑𝑘) ∈ ℂ)
82	31	adantlr 728	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → (𝑥↑𝐷) ∈ ℂ)
83	40	adantl 487	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ≠ 0)
84	43	adantlr 728	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → 𝐷 ∈ ℤ)
85	80, 83, 84	expne0d 14218	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → (𝑥↑𝐷) ≠ 0)
86	79, 81, 82, 85	divassd 12053	. . . . . . . 8 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = ((𝐶‘𝑘) · ((𝑥↑𝑘) / (𝑥↑𝐷))))
87	86	mpteq2dva 5202	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ⁺ ↦ (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) = (𝑥 ∈ ℝ⁺ ↦ ((𝐶‘𝑘) · ((𝑥↑𝑘) / (𝑥↑𝐷)))))
88		fvexd 6897	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → (𝐶‘𝑘) ∈ V)
89		ovexd 7451	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → ((𝑥↑𝑘) / (𝑥↑𝐷)) ∈ V)
90	32	adantr 486	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → 𝐶:ℕ₀⟶ℂ)
91	77	adantl 487	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → 𝑘 ∈ ℕ₀)
92	90, 91	ffvelcdmd 7081	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝐶‘𝑘) ∈ ℂ)
93		rlimconst 15633	. . . . . . . . . 10 ⊢ ((ℝ⁺ ⊆ ℝ ∧ (𝐶‘𝑘) ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ (𝐶‘𝑘)) ⇝_𝑟 (𝐶‘𝑘))
94	11, 92, 93	sylancr 599	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ⁺ ↦ (𝐶‘𝑘)) ⇝_𝑟 (𝐶‘𝑘))
95	78	nn0zd 12643	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → 𝑘 ∈ ℤ)
96	84, 95	zsubcld 12733	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → (𝐷 − 𝑘) ∈ ℤ)
97	80, 83, 96	cxpexpzd 26946	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → (𝑥↑_𝑐(𝐷 − 𝑘)) = (𝑥↑(𝐷 − 𝑘)))
98	97	oveq2d 7432	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → (1 / (𝑥↑_𝑐(𝐷 − 𝑘))) = (1 / (𝑥↑(𝐷 − 𝑘))))
99	80, 83, 96	expnegd 14219	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → (𝑥↑-(𝐷 − 𝑘)) = (1 / (𝑥↑(𝐷 − 𝑘))))
100	84	zcnd 12729	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → 𝐷 ∈ ℂ)
101	78	nn0cnd 12594	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → 𝑘 ∈ ℂ)
102	100, 101	negsubdi2d 11612	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → -(𝐷 − 𝑘) = (𝑘 − 𝐷))
103	102	oveq2d 7432	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → (𝑥↑-(𝐷 − 𝑘)) = (𝑥↑(𝑘 − 𝐷)))
104	98, 99, 103	3eqtr2d 2803	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → (1 / (𝑥↑_𝑐(𝐷 − 𝑘))) = (𝑥↑(𝑘 − 𝐷)))
105	80, 83, 84, 95	expsubd 14223	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → (𝑥↑(𝑘 − 𝐷)) = ((𝑥↑𝑘) / (𝑥↑𝐷)))
106	104, 105	eqtrd 2797	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ⁺) → (1 / (𝑥↑_𝑐(𝐷 − 𝑘))) = ((𝑥↑𝑘) / (𝑥↑𝐷)))
107	106	mpteq2dva 5202	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ⁺ ↦ (1 / (𝑥↑_𝑐(𝐷 − 𝑘)))) = (𝑥 ∈ ℝ⁺ ↦ ((𝑥↑𝑘) / (𝑥↑𝐷))))
108	91	nn0red 12593	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → 𝑘 ∈ ℝ)
109	29	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → 𝐷 ∈ ℕ₀)
110	109	nn0red 12593	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → 𝐷 ∈ ℝ)
111		elfzolt2 13726	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0..^𝐷) → 𝑘 < 𝐷)
112	111	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → 𝑘 < 𝐷)
113		difrp 13084	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑘 < 𝐷 ↔ (𝐷 − 𝑘) ∈ ℝ⁺))
114	113	biimpa 482	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ 𝑘 < 𝐷) → (𝐷 − 𝑘) ∈ ℝ⁺)
115	108, 110, 112, 114	syl21anc 851	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝐷 − 𝑘) ∈ ℝ⁺)
116		cxplim 27206	. . . . . . . . . . 11 ⊢ ((𝐷 − 𝑘) ∈ ℝ⁺ → (𝑥 ∈ ℝ⁺ ↦ (1 / (𝑥↑_𝑐(𝐷 − 𝑘)))) ⇝_𝑟 0)
117	115, 116	syl 18	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ⁺ ↦ (1 / (𝑥↑_𝑐(𝐷 − 𝑘)))) ⇝_𝑟 0)
118	107, 117	eqbrtrrd 5133	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ⁺ ↦ ((𝑥↑𝑘) / (𝑥↑𝐷))) ⇝_𝑟 0)
119	88, 89, 94, 118	rlimmul 15734	. . . . . . . 8 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ⁺ ↦ ((𝐶‘𝑘) · ((𝑥↑𝑘) / (𝑥↑𝐷)))) ⇝_𝑟 ((𝐶‘𝑘) · 0))
120	92	mul01d 11436	. . . . . . . 8 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → ((𝐶‘𝑘) · 0) = 0)
121	119, 120	breqtrd 5135	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ⁺ ↦ ((𝐶‘𝑘) · ((𝑥↑𝑘) / (𝑥↑𝐷)))) ⇝_𝑟 0)
122	87, 121	eqbrtrd 5131	. . . . . 6 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ⁺ ↦ (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) ⇝_𝑟 0)
123	72, 74, 75, 122	fsumrlim 15900	. . . . 5 ⊢ (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ⁺ ↦ Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) ⇝_𝑟 Σ𝑘 ∈ (0..^𝐷)0)
124	74	olcd 888	. . . . . 6 ⊢ (𝐹 ∈ (Poly‘ℝ) → ((0..^𝐷) ⊆ (ℤ_≥‘0) ∨ (0..^𝐷) ∈ Fin))
125		sumz 15810	. . . . . 6 ⊢ (((0..^𝐷) ⊆ (ℤ_≥‘0) ∨ (0..^𝐷) ∈ Fin) → Σ𝑘 ∈ (0..^𝐷)0 = 0)
126	124, 125	syl 18	. . . . 5 ⊢ (𝐹 ∈ (Poly‘ℝ) → Σ𝑘 ∈ (0..^𝐷)0 = 0)
127	123, 126	breqtrd 5135	. . . 4 ⊢ (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ⁺ ↦ Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) ⇝_𝑟 0)
128	32, 29	ffvelcdmd 7081	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (Poly‘ℝ) → (𝐶‘𝐷) ∈ ℂ)
129	128	adantr 486	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → (𝐶‘𝐷) ∈ ℂ)
130	129, 31	mulcld 11256	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → ((𝐶‘𝐷) · (𝑥↑𝐷)) ∈ ℂ)
131	130, 31, 44	divcld 12018	. . . . . . . 8 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷)) ∈ ℂ)
132		fveq2 6882	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐷 → (𝐶‘𝑘) = (𝐶‘𝐷))
133		oveq2 7424	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐷 → (𝑥↑𝑘) = (𝑥↑𝐷))
134	132, 133	oveq12d 7434	. . . . . . . . . 10 ⊢ (𝑘 = 𝐷 → ((𝐶‘𝑘) · (𝑥↑𝑘)) = ((𝐶‘𝐷) · (𝑥↑𝐷)))
135	134	oveq1d 7431	. . . . . . . . 9 ⊢ (𝑘 = 𝐷 → (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷)))
136	135	sumsn 15834	. . . . . . . 8 ⊢ ((𝐷 ∈ ℕ₀ ∧ (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷)) ∈ ℂ) → Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷)))
137	30, 131, 136	syl2anc 596	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷)))
138	129, 31, 44	divcan4d 12024	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷)) = (𝐶‘𝐷))
139	137, 138	eqtrd 2797	. . . . . 6 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ⁺) → Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (𝐶‘𝐷))
140	139	mpteq2dva 5202	. . . . 5 ⊢ (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ⁺ ↦ Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) = (𝑥 ∈ ℝ⁺ ↦ (𝐶‘𝐷)))
141		rlimconst 15633	. . . . . 6 ⊢ ((ℝ⁺ ⊆ ℝ ∧ (𝐶‘𝐷) ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ (𝐶‘𝐷)) ⇝_𝑟 (𝐶‘𝐷))
142	11, 128, 141	sylancr 599	. . . . 5 ⊢ (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ⁺ ↦ (𝐶‘𝐷)) ⇝_𝑟 (𝐶‘𝐷))
143	140, 142	eqbrtrd 5131	. . . 4 ⊢ (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ⁺ ↦ Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) ⇝_𝑟 (𝐶‘𝐷))
144	69, 71, 127, 143	rlimadd 15732	. . 3 ⊢ (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)))) ⇝_𝑟 (0 + (𝐶‘𝐷)))
145	128	addlidd 11438	. . . 4 ⊢ (𝐹 ∈ (Poly‘ℝ) → (0 + (𝐶‘𝐷)) = (𝐶‘𝐷))
146		signsply0.b	. . . 4 ⊢ 𝐵 = (𝐶‘𝐷)
147	145, 146	eqtr4di 2815	. . 3 ⊢ (𝐹 ∈ (Poly‘ℝ) → (0 + (𝐶‘𝐷)) = 𝐵)
148	144, 147	breqtrd 5135	. 2 ⊢ (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)))) ⇝_𝑟 𝐵)
149	67, 148	eqbrtrd 5131	1 ⊢ (𝐹 ∈ (Poly‘ℝ) → (𝐹 ∘_f / 𝐺) ⇝_𝑟 𝐵)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∀wral 3078 Vcvv 3453 ∪ cun 3900 ∩ cin 3901 ⊆ wss 3902 ∅c0 4282 {csn 4587 class class class wbr 5107 ↦ cmpt 5190 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7416 ∘_f cof 7679 Fincfn 8955 ℂcc 11125 ℝcr 11126 0cc0 11127 1c1 11128 + caddc 11130 · cmul 11132 < clt 11270 − cmin 11468 -cneg 11469 / cdiv 11898 ℕ₀cn0 12531 ℤcz 12618 ℤ_≥cuz 12890 ℝ⁺crp 13044 ...cfz 13563 ..^cfzo 13711 ↑cexp 14127 ⇝_𝑟 crli 15574 Σcsu 15775 Polycply 26411 coeffccoe 26413 degcdgr 26414 ↑_𝑐ccxp 26790

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-inf2 9623 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205 ax-addf 11206

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7681 df-om 7866 df-1st 7989 df-2nd 7990 df-supp 8162 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-2o 8459 df-er 8699 df-map 8831 df-pm 8832 df-ixp 8908 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-fsupp 9335 df-fi 9384 df-sup 9415 df-inf 9416 df-oi 9485 df-card 9947 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-q 13001 df-rp 13045 df-xneg 13165 df-xadd 13166 df-xmul 13167 df-ioo 13404 df-ioc 13405 df-ico 13406 df-icc 13407 df-fz 13564 df-fzo 13712 df-fl 13855 df-mod 13933 df-seq 14068 df-exp 14128 df-fac 14340 df-bc 14369 df-hash 14397 df-shft 15142 df-cj 15188 df-re 15189 df-im 15190 df-sqrt 15324 df-abs 15325 df-limsup 15560 df-clim 15577 df-rlim 15578 df-sum 15776 df-ef 16157 df-sin 16159 df-cos 16160 df-pi 16162 df-struct 17243 df-sets 17260 df-slot 17278 df-ndx 17290 df-base 17306 df-ress 17327 df-plusg 17359 df-mulr 17360 df-starv 17361 df-sca 17362 df-vsca 17363 df-ip 17364 df-tset 17365 df-ple 17366 df-ds 17368 df-unif 17369 df-hom 17370 df-cco 17371 df-rest 17511 df-topn 17512 df-0g 17530 df-gsum 17531 df-topgen 17532 df-pt 17533 df-prds 17536 df-xrs 17592 df-qtop 17597 df-imas 17598 df-xps 17600 df-mre 17674 df-mrc 17675 df-acs 17677 df-mgm 18734 df-sgrp 18823 df-mnd 18839 df-submnd 18893 df-mulg 19192 df-cntz 19445 df-cmn 19910 df-psmet 21578 df-xmet 21579 df-met 21580 df-bl 21581 df-mopn 21582 df-fbas 21583 df-fg 21584 df-cnfld 21587 df-top 23120 df-topon 23137 df-topsp 23159 df-bases 23172 df-cld 23245 df-ntr 23246 df-cls 23247 df-nei 23324 df-lp 23362 df-perf 23363 df-cn 23453 df-cnp 23454 df-haus 23541 df-tx 23789 df-hmeo 23982 df-fil 24073 df-fm 24165 df-flim 24166 df-flf 24167 df-xms 24547 df-ms 24548 df-tms 24549 df-cncf 25107 df-0p 25899 df-limc 26095 df-dv 26096 df-ply 26415 df-coe 26417 df-dgr 26418 df-log 26791 df-cxp 26792

This theorem is used by: signsply0 35046

W3C validator