MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ftalem2 Structured version   Visualization version   GIF version

Theorem ftalem2 26910
Description: Lemma for fta 26916. There exists some 𝑟 such that 𝐹 has magnitude greater than 𝐹(0) outside the closed ball B(0,r). (Contributed by Mario Carneiro, 14-Sep-2014.)
Hypotheses
Ref Expression
ftalem.1 𝐴 = (coeff‘𝐹)
ftalem.2 𝑁 = (deg‘𝐹)
ftalem.3 (𝜑𝐹 ∈ (Poly‘𝑆))
ftalem.4 (𝜑𝑁 ∈ ℕ)
ftalem2.5 𝑈 = if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1))
ftalem2.6 𝑇 = ((abs‘(𝐹‘0)) / ((abs‘(𝐴𝑁)) / 2))
Assertion
Ref Expression
ftalem2 (𝜑 → ∃𝑟 ∈ ℝ+𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))))
Distinct variable groups:   𝑠,𝑟,𝑥,𝐴   𝑁,𝑟,𝑠,𝑥   𝐹,𝑟,𝑠,𝑥   𝜑,𝑠,𝑥   𝑆,𝑠   𝑇,𝑟,𝑥   𝑈,𝑟,𝑥
Allowed substitution hints:   𝜑(𝑟)   𝑆(𝑥,𝑟)   𝑇(𝑠)   𝑈(𝑠)

Proof of Theorem ftalem2
Dummy variables 𝑘 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ftalem.1 . . 3 𝐴 = (coeff‘𝐹)
2 ftalem.2 . . 3 𝑁 = (deg‘𝐹)
3 ftalem.3 . . 3 (𝜑𝐹 ∈ (Poly‘𝑆))
4 ftalem.4 . . 3 (𝜑𝑁 ∈ ℕ)
51coef3 26074 . . . . . . 7 (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ)
63, 5syl 17 . . . . . 6 (𝜑𝐴:ℕ0⟶ℂ)
74nnnn0d 12528 . . . . . 6 (𝜑𝑁 ∈ ℕ0)
86, 7ffvelcdmd 7077 . . . . 5 (𝜑 → (𝐴𝑁) ∈ ℂ)
94nnne0d 12258 . . . . . 6 (𝜑𝑁 ≠ 0)
102, 1dgreq0 26108 . . . . . . . . 9 (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
11 fveq2 6881 . . . . . . . . . . 11 (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
12 dgr0 26105 . . . . . . . . . . 11 (deg‘0𝑝) = 0
1311, 12eqtrdi 2780 . . . . . . . . . 10 (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
142, 13eqtrid 2776 . . . . . . . . 9 (𝐹 = 0𝑝𝑁 = 0)
1510, 14syl6bir 254 . . . . . . . 8 (𝐹 ∈ (Poly‘𝑆) → ((𝐴𝑁) = 0 → 𝑁 = 0))
163, 15syl 17 . . . . . . 7 (𝜑 → ((𝐴𝑁) = 0 → 𝑁 = 0))
1716necon3d 2953 . . . . . 6 (𝜑 → (𝑁 ≠ 0 → (𝐴𝑁) ≠ 0))
189, 17mpd 15 . . . . 5 (𝜑 → (𝐴𝑁) ≠ 0)
198, 18absrpcld 15391 . . . 4 (𝜑 → (abs‘(𝐴𝑁)) ∈ ℝ+)
2019rphalfcld 13024 . . 3 (𝜑 → ((abs‘(𝐴𝑁)) / 2) ∈ ℝ+)
21 2fveq3 6886 . . . . 5 (𝑛 = 𝑘 → (abs‘(𝐴𝑛)) = (abs‘(𝐴𝑘)))
2221cbvsumv 15638 . . . 4 Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(𝐴𝑛)) = Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴𝑘))
2322oveq1i 7411 . . 3 𝑛 ∈ (0...(𝑁 − 1))(abs‘(𝐴𝑛)) / ((abs‘(𝐴𝑁)) / 2)) = (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴𝑘)) / ((abs‘(𝐴𝑁)) / 2))
241, 2, 3, 4, 20, 23ftalem1 26909 . 2 (𝜑 → ∃𝑠 ∈ ℝ ∀𝑥 ∈ ℂ (𝑠 < (abs‘𝑥) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))))
25 ftalem2.5 . . . . . 6 𝑈 = if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1))
26 ftalem2.6 . . . . . . . . 9 𝑇 = ((abs‘(𝐹‘0)) / ((abs‘(𝐴𝑁)) / 2))
27 plyf 26040 . . . . . . . . . . . . 13 (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
283, 27syl 17 . . . . . . . . . . . 12 (𝜑𝐹:ℂ⟶ℂ)
29 0cn 11202 . . . . . . . . . . . 12 0 ∈ ℂ
30 ffvelcdm 7073 . . . . . . . . . . . 12 ((𝐹:ℂ⟶ℂ ∧ 0 ∈ ℂ) → (𝐹‘0) ∈ ℂ)
3128, 29, 30sylancl 585 . . . . . . . . . . 11 (𝜑 → (𝐹‘0) ∈ ℂ)
3231abscld 15379 . . . . . . . . . 10 (𝜑 → (abs‘(𝐹‘0)) ∈ ℝ)
3332, 20rerpdivcld 13043 . . . . . . . . 9 (𝜑 → ((abs‘(𝐹‘0)) / ((abs‘(𝐴𝑁)) / 2)) ∈ ℝ)
3426, 33eqeltrid 2829 . . . . . . . 8 (𝜑𝑇 ∈ ℝ)
3534adantr 480 . . . . . . 7 ((𝜑𝑠 ∈ ℝ) → 𝑇 ∈ ℝ)
36 simpr 484 . . . . . . . 8 ((𝜑𝑠 ∈ ℝ) → 𝑠 ∈ ℝ)
37 1re 11210 . . . . . . . 8 1 ∈ ℝ
38 ifcl 4565 . . . . . . . 8 ((𝑠 ∈ ℝ ∧ 1 ∈ ℝ) → if(1 ≤ 𝑠, 𝑠, 1) ∈ ℝ)
3936, 37, 38sylancl 585 . . . . . . 7 ((𝜑𝑠 ∈ ℝ) → if(1 ≤ 𝑠, 𝑠, 1) ∈ ℝ)
4035, 39ifcld 4566 . . . . . 6 ((𝜑𝑠 ∈ ℝ) → if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1)) ∈ ℝ)
4125, 40eqeltrid 2829 . . . . 5 ((𝜑𝑠 ∈ ℝ) → 𝑈 ∈ ℝ)
42 0red 11213 . . . . . 6 ((𝜑𝑠 ∈ ℝ) → 0 ∈ ℝ)
43 1red 11211 . . . . . 6 ((𝜑𝑠 ∈ ℝ) → 1 ∈ ℝ)
44 0lt1 11732 . . . . . . 7 0 < 1
4544a1i 11 . . . . . 6 ((𝜑𝑠 ∈ ℝ) → 0 < 1)
46 max1 13160 . . . . . . . 8 ((1 ∈ ℝ ∧ 𝑠 ∈ ℝ) → 1 ≤ if(1 ≤ 𝑠, 𝑠, 1))
4737, 36, 46sylancr 586 . . . . . . 7 ((𝜑𝑠 ∈ ℝ) → 1 ≤ if(1 ≤ 𝑠, 𝑠, 1))
48 max1 13160 . . . . . . . . 9 ((if(1 ≤ 𝑠, 𝑠, 1) ∈ ℝ ∧ 𝑇 ∈ ℝ) → if(1 ≤ 𝑠, 𝑠, 1) ≤ if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1)))
4939, 35, 48syl2anc 583 . . . . . . . 8 ((𝜑𝑠 ∈ ℝ) → if(1 ≤ 𝑠, 𝑠, 1) ≤ if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1)))
5049, 25breqtrrdi 5180 . . . . . . 7 ((𝜑𝑠 ∈ ℝ) → if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑈)
5143, 39, 41, 47, 50letrd 11367 . . . . . 6 ((𝜑𝑠 ∈ ℝ) → 1 ≤ 𝑈)
5242, 43, 41, 45, 51ltletrd 11370 . . . . 5 ((𝜑𝑠 ∈ ℝ) → 0 < 𝑈)
5341, 52elrpd 13009 . . . 4 ((𝜑𝑠 ∈ ℝ) → 𝑈 ∈ ℝ+)
54 max2 13162 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 𝑠 ∈ ℝ) → 𝑠 ≤ if(1 ≤ 𝑠, 𝑠, 1))
5537, 36, 54sylancr 586 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℝ) → 𝑠 ≤ if(1 ≤ 𝑠, 𝑠, 1))
5636, 39, 41, 55, 50letrd 11367 . . . . . . . . 9 ((𝜑𝑠 ∈ ℝ) → 𝑠𝑈)
5756adantr 480 . . . . . . . 8 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → 𝑠𝑈)
58 abscl 15221 . . . . . . . . 9 (𝑥 ∈ ℂ → (abs‘𝑥) ∈ ℝ)
59 lelttr 11300 . . . . . . . . 9 ((𝑠 ∈ ℝ ∧ 𝑈 ∈ ℝ ∧ (abs‘𝑥) ∈ ℝ) → ((𝑠𝑈𝑈 < (abs‘𝑥)) → 𝑠 < (abs‘𝑥)))
6036, 41, 58, 59syl2an3an 1419 . . . . . . . 8 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → ((𝑠𝑈𝑈 < (abs‘𝑥)) → 𝑠 < (abs‘𝑥)))
6157, 60mpand 692 . . . . . . 7 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → (𝑈 < (abs‘𝑥) → 𝑠 < (abs‘𝑥)))
6261imim1d 82 . . . . . 6 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → ((𝑠 < (abs‘𝑥) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → (𝑈 < (abs‘𝑥) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)))))
6328ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝐹:ℂ⟶ℂ)
64 simprl 768 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑥 ∈ ℂ)
6563, 64ffvelcdmd 7077 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (𝐹𝑥) ∈ ℂ)
668ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (𝐴𝑁) ∈ ℂ)
677ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑁 ∈ ℕ0)
6864, 67expcld 14107 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (𝑥𝑁) ∈ ℂ)
6966, 68mulcld 11230 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((𝐴𝑁) · (𝑥𝑁)) ∈ ℂ)
7065, 69subcld 11567 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))) ∈ ℂ)
7170abscld 15379 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) ∈ ℝ)
7269abscld 15379 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘((𝐴𝑁) · (𝑥𝑁))) ∈ ℝ)
7372rehalfcld 12455 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ∈ ℝ)
7471, 73, 72ltsub2d 11820 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ↔ ((abs‘((𝐴𝑁) · (𝑥𝑁))) − ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))))))
7566, 68absmuld 15397 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘((𝐴𝑁) · (𝑥𝑁))) = ((abs‘(𝐴𝑁)) · (abs‘(𝑥𝑁))))
7664, 67absexpd 15395 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝑥𝑁)) = ((abs‘𝑥)↑𝑁))
7776oveq2d 7417 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘(𝐴𝑁)) · (abs‘(𝑥𝑁))) = ((abs‘(𝐴𝑁)) · ((abs‘𝑥)↑𝑁)))
7875, 77eqtrd 2764 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘((𝐴𝑁) · (𝑥𝑁))) = ((abs‘(𝐴𝑁)) · ((abs‘𝑥)↑𝑁)))
7978oveq1d 7416 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) = (((abs‘(𝐴𝑁)) · ((abs‘𝑥)↑𝑁)) / 2))
8066abscld 15379 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐴𝑁)) ∈ ℝ)
8180recnd 11238 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐴𝑁)) ∈ ℂ)
8258ad2antrl 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘𝑥) ∈ ℝ)
8382, 67reexpcld 14124 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘𝑥)↑𝑁) ∈ ℝ)
8483recnd 11238 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘𝑥)↑𝑁) ∈ ℂ)
85 2cnd 12286 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 2 ∈ ℂ)
86 2ne0 12312 . . . . . . . . . . . . . . 15 2 ≠ 0
8786a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 2 ≠ 0)
8881, 84, 85, 87div23d 12023 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐴𝑁)) · ((abs‘𝑥)↑𝑁)) / 2) = (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)))
8979, 88eqtrd 2764 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) = (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)))
9089breq2d 5150 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ↔ (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))))
9172recnd 11238 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘((𝐴𝑁) · (𝑥𝑁))) ∈ ℂ)
92912halvesd 12454 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) + ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) = (abs‘((𝐴𝑁) · (𝑥𝑁))))
9392oveq1d 7416 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) + ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) − ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) = ((abs‘((𝐴𝑁) · (𝑥𝑁))) − ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)))
9473recnd 11238 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ∈ ℂ)
9594, 94pncand 11568 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) + ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) − ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) = ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2))
9693, 95eqtr3d 2766 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) − ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) = ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2))
9796breq1d 5148 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘((𝐴𝑁) · (𝑥𝑁))) − ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ↔ ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))))))
9874, 90, 973bitr3d 309 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)) ↔ ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))))))
9969, 65subcld 11567 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((𝐴𝑁) · (𝑥𝑁)) − (𝐹𝑥)) ∈ ℂ)
10069, 99abs2difd 15400 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘(((𝐴𝑁) · (𝑥𝑁)) − (𝐹𝑥)))) ≤ (abs‘(((𝐴𝑁) · (𝑥𝑁)) − (((𝐴𝑁) · (𝑥𝑁)) − (𝐹𝑥)))))
10169, 65abssubd 15396 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(((𝐴𝑁) · (𝑥𝑁)) − (𝐹𝑥))) = (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))))
102101oveq2d 7417 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘(((𝐴𝑁) · (𝑥𝑁)) − (𝐹𝑥)))) = ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))))
10369, 65nncand 11572 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((𝐴𝑁) · (𝑥𝑁)) − (((𝐴𝑁) · (𝑥𝑁)) − (𝐹𝑥))) = (𝐹𝑥))
104103fveq2d 6885 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(((𝐴𝑁) · (𝑥𝑁)) − (((𝐴𝑁) · (𝑥𝑁)) − (𝐹𝑥)))) = (abs‘(𝐹𝑥)))
105100, 102, 1043brtr3d 5169 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ≤ (abs‘(𝐹𝑥)))
10672, 71resubcld 11638 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ∈ ℝ)
10765abscld 15379 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐹𝑥)) ∈ ℝ)
108 ltletr 11302 . . . . . . . . . . . 12 ((((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ∈ ℝ ∧ ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ∈ ℝ ∧ (abs‘(𝐹𝑥)) ∈ ℝ) → ((((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ∧ ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ≤ (abs‘(𝐹𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < (abs‘(𝐹𝑥))))
10973, 106, 107, 108syl3anc 1368 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ∧ ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ≤ (abs‘(𝐹𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < (abs‘(𝐹𝑥))))
110105, 109mpan2d 691 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < (abs‘(𝐹𝑥))))
11198, 110sylbid 239 . . . . . . . . 9 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < (abs‘(𝐹𝑥))))
11232ad2antrr 723 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐹‘0)) ∈ ℝ)
11320ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘(𝐴𝑁)) / 2) ∈ ℝ+)
114113rpred 13012 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘(𝐴𝑁)) / 2) ∈ ℝ)
115114, 82remulcld 11240 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐴𝑁)) / 2) · (abs‘𝑥)) ∈ ℝ)
11689, 73eqeltrrd 2826 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)) ∈ ℝ)
11735adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑇 ∈ ℝ)
11841adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑈 ∈ ℝ)
119 max2 13162 . . . . . . . . . . . . . . . . . 18 ((if(1 ≤ 𝑠, 𝑠, 1) ∈ ℝ ∧ 𝑇 ∈ ℝ) → 𝑇 ≤ if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1)))
12039, 35, 119syl2anc 583 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ ℝ) → 𝑇 ≤ if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1)))
121120, 25breqtrrdi 5180 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ ℝ) → 𝑇𝑈)
122121adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑇𝑈)
123 simprr 770 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑈 < (abs‘𝑥))
124117, 118, 82, 122, 123lelttrd 11368 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑇 < (abs‘𝑥))
12526, 124eqbrtrrid 5174 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘(𝐹‘0)) / ((abs‘(𝐴𝑁)) / 2)) < (abs‘𝑥))
126112, 82, 113ltdivmuld 13063 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐹‘0)) / ((abs‘(𝐴𝑁)) / 2)) < (abs‘𝑥) ↔ (abs‘(𝐹‘0)) < (((abs‘(𝐴𝑁)) / 2) · (abs‘𝑥))))
127125, 126mpbid 231 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐹‘0)) < (((abs‘(𝐴𝑁)) / 2) · (abs‘𝑥)))
12882recnd 11238 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘𝑥) ∈ ℂ)
129128exp1d 14102 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘𝑥)↑1) = (abs‘𝑥))
130 1red 11211 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 1 ∈ ℝ)
13151adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 1 ≤ 𝑈)
132130, 118, 82, 131, 123lelttrd 11368 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 1 < (abs‘𝑥))
133130, 82, 132ltled 11358 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 1 ≤ (abs‘𝑥))
1344ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑁 ∈ ℕ)
135 nnuz 12861 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
136134, 135eleqtrdi 2835 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑁 ∈ (ℤ‘1))
13782, 133, 136leexp2ad 14213 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘𝑥)↑1) ≤ ((abs‘𝑥)↑𝑁))
138129, 137eqbrtrrd 5162 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘𝑥) ≤ ((abs‘𝑥)↑𝑁))
13982, 83, 113lemul2d 13056 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘𝑥) ≤ ((abs‘𝑥)↑𝑁) ↔ (((abs‘(𝐴𝑁)) / 2) · (abs‘𝑥)) ≤ (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))))
140138, 139mpbid 231 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐴𝑁)) / 2) · (abs‘𝑥)) ≤ (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)))
141112, 115, 116, 127, 140ltletrd 11370 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐹‘0)) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)))
142141, 89breqtrrd 5166 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐹‘0)) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2))
143 lttr 11286 . . . . . . . . . . 11 (((abs‘(𝐹‘0)) ∈ ℝ ∧ ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ∈ ℝ ∧ (abs‘(𝐹𝑥)) ∈ ℝ) → (((abs‘(𝐹‘0)) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ∧ ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < (abs‘(𝐹𝑥))) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))))
144112, 73, 107, 143syl3anc 1368 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐹‘0)) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ∧ ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < (abs‘(𝐹𝑥))) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))))
145142, 144mpand 692 . . . . . . . . 9 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < (abs‘(𝐹𝑥)) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))))
146111, 145syld 47 . . . . . . . 8 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))))
147146expr 456 . . . . . . 7 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → (𝑈 < (abs‘𝑥) → ((abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))))
148147a2d 29 . . . . . 6 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → ((𝑈 < (abs‘𝑥) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → (𝑈 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))))
14962, 148syld 47 . . . . 5 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → ((𝑠 < (abs‘𝑥) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → (𝑈 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))))
150149ralimdva 3159 . . . 4 ((𝜑𝑠 ∈ ℝ) → (∀𝑥 ∈ ℂ (𝑠 < (abs‘𝑥) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → ∀𝑥 ∈ ℂ (𝑈 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))))
151 breq1 5141 . . . . 5 (𝑟 = 𝑈 → (𝑟 < (abs‘𝑥) ↔ 𝑈 < (abs‘𝑥)))
152151rspceaimv 3609 . . . 4 ((𝑈 ∈ ℝ+ ∧ ∀𝑥 ∈ ℂ (𝑈 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))) → ∃𝑟 ∈ ℝ+𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))))
15353, 150, 152syl6an 681 . . 3 ((𝜑𝑠 ∈ ℝ) → (∀𝑥 ∈ ℂ (𝑠 < (abs‘𝑥) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → ∃𝑟 ∈ ℝ+𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))))
154153rexlimdva 3147 . 2 (𝜑 → (∃𝑠 ∈ ℝ ∀𝑥 ∈ ℂ (𝑠 < (abs‘𝑥) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → ∃𝑟 ∈ ℝ+𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))))
15524, 154mpd 15 1 (𝜑 → ∃𝑟 ∈ ℝ+𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1533  wcel 2098  wne 2932  wral 3053  wrex 3062  ifcif 4520   class class class wbr 5138  wf 6529  cfv 6533  (class class class)co 7401  cc 11103  cr 11104  0cc0 11105  1c1 11106   + caddc 11108   · cmul 11110   < clt 11244  cle 11245  cmin 11440   / cdiv 11867  cn 12208  2c2 12263  0cn0 12468  cuz 12818  +crp 12970  ...cfz 13480  cexp 14023  abscabs 15177  Σcsu 15628  0𝑝c0p 25508  Polycply 26026  coeffccoe 26028  degcdgr 26029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9631  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182  ax-pre-sup 11183
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-er 8698  df-map 8817  df-pm 8818  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-sup 9432  df-inf 9433  df-oi 9500  df-card 9929  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-n0 12469  df-z 12555  df-uz 12819  df-rp 12971  df-ico 13326  df-fz 13481  df-fzo 13624  df-fl 13753  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428  df-rlim 15429  df-sum 15629  df-0p 25509  df-ply 26030  df-coe 26032  df-dgr 26033
This theorem is referenced by:  fta  26916
  Copyright terms: Public domain W3C validator