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

Theorem ftalem2 25252
 Description: Lemma for fta 25258. 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 24425 . . . . . . 7 (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ)
63, 5syl 17 . . . . . 6 (𝜑𝐴:ℕ0⟶ℂ)
74nnnn0d 11702 . . . . . 6 (𝜑𝑁 ∈ ℕ0)
86, 7ffvelrnd 6624 . . . . 5 (𝜑 → (𝐴𝑁) ∈ ℂ)
94nnne0d 11425 . . . . . 6 (𝜑𝑁 ≠ 0)
102, 1dgreq0 24458 . . . . . . . . 9 (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
11 fveq2 6446 . . . . . . . . . . 11 (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
12 dgr0 24455 . . . . . . . . . . 11 (deg‘0𝑝) = 0
1311, 12syl6eq 2830 . . . . . . . . . 10 (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
142, 13syl5eq 2826 . . . . . . . . 9 (𝐹 = 0𝑝𝑁 = 0)
1510, 14syl6bir 246 . . . . . . . 8 (𝐹 ∈ (Poly‘𝑆) → ((𝐴𝑁) = 0 → 𝑁 = 0))
163, 15syl 17 . . . . . . 7 (𝜑 → ((𝐴𝑁) = 0 → 𝑁 = 0))
1716necon3d 2990 . . . . . 6 (𝜑 → (𝑁 ≠ 0 → (𝐴𝑁) ≠ 0))
189, 17mpd 15 . . . . 5 (𝜑 → (𝐴𝑁) ≠ 0)
198, 18absrpcld 14595 . . . 4 (𝜑 → (abs‘(𝐴𝑁)) ∈ ℝ+)
2019rphalfcld 12193 . . 3 (𝜑 → ((abs‘(𝐴𝑁)) / 2) ∈ ℝ+)
21 2fveq3 6451 . . . . 5 (𝑛 = 𝑘 → (abs‘(𝐴𝑛)) = (abs‘(𝐴𝑘)))
2221cbvsumv 14834 . . . 4 Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(𝐴𝑛)) = Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴𝑘))
2322oveq1i 6932 . . 3 𝑛 ∈ (0...(𝑁 − 1))(abs‘(𝐴𝑛)) / ((abs‘(𝐴𝑁)) / 2)) = (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴𝑘)) / ((abs‘(𝐴𝑁)) / 2))
241, 2, 3, 4, 20, 23ftalem1 25251 . 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 24391 . . . . . . . . . . . . 13 (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
283, 27syl 17 . . . . . . . . . . . 12 (𝜑𝐹:ℂ⟶ℂ)
29 0cn 10368 . . . . . . . . . . . 12 0 ∈ ℂ
30 ffvelrn 6621 . . . . . . . . . . . 12 ((𝐹:ℂ⟶ℂ ∧ 0 ∈ ℂ) → (𝐹‘0) ∈ ℂ)
3128, 29, 30sylancl 580 . . . . . . . . . . 11 (𝜑 → (𝐹‘0) ∈ ℂ)
3231abscld 14583 . . . . . . . . . 10 (𝜑 → (abs‘(𝐹‘0)) ∈ ℝ)
3332, 20rerpdivcld 12212 . . . . . . . . 9 (𝜑 → ((abs‘(𝐹‘0)) / ((abs‘(𝐴𝑁)) / 2)) ∈ ℝ)
3426, 33syl5eqel 2863 . . . . . . . 8 (𝜑𝑇 ∈ ℝ)
3534adantr 474 . . . . . . 7 ((𝜑𝑠 ∈ ℝ) → 𝑇 ∈ ℝ)
36 simpr 479 . . . . . . . 8 ((𝜑𝑠 ∈ ℝ) → 𝑠 ∈ ℝ)
37 1re 10376 . . . . . . . 8 1 ∈ ℝ
38 ifcl 4351 . . . . . . . 8 ((𝑠 ∈ ℝ ∧ 1 ∈ ℝ) → if(1 ≤ 𝑠, 𝑠, 1) ∈ ℝ)
3936, 37, 38sylancl 580 . . . . . . 7 ((𝜑𝑠 ∈ ℝ) → if(1 ≤ 𝑠, 𝑠, 1) ∈ ℝ)
4035, 39ifcld 4352 . . . . . 6 ((𝜑𝑠 ∈ ℝ) → if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1)) ∈ ℝ)
4125, 40syl5eqel 2863 . . . . 5 ((𝜑𝑠 ∈ ℝ) → 𝑈 ∈ ℝ)
42 0red 10380 . . . . . 6 ((𝜑𝑠 ∈ ℝ) → 0 ∈ ℝ)
43 1red 10377 . . . . . 6 ((𝜑𝑠 ∈ ℝ) → 1 ∈ ℝ)
44 0lt1 10897 . . . . . . 7 0 < 1
4544a1i 11 . . . . . 6 ((𝜑𝑠 ∈ ℝ) → 0 < 1)
46 max1 12328 . . . . . . . 8 ((1 ∈ ℝ ∧ 𝑠 ∈ ℝ) → 1 ≤ if(1 ≤ 𝑠, 𝑠, 1))
4737, 36, 46sylancr 581 . . . . . . 7 ((𝜑𝑠 ∈ ℝ) → 1 ≤ if(1 ≤ 𝑠, 𝑠, 1))
48 max1 12328 . . . . . . . . 9 ((if(1 ≤ 𝑠, 𝑠, 1) ∈ ℝ ∧ 𝑇 ∈ ℝ) → if(1 ≤ 𝑠, 𝑠, 1) ≤ if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1)))
4939, 35, 48syl2anc 579 . . . . . . . 8 ((𝜑𝑠 ∈ ℝ) → if(1 ≤ 𝑠, 𝑠, 1) ≤ if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1)))
5049, 25syl6breqr 4928 . . . . . . 7 ((𝜑𝑠 ∈ ℝ) → if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑈)
5143, 39, 41, 47, 50letrd 10533 . . . . . 6 ((𝜑𝑠 ∈ ℝ) → 1 ≤ 𝑈)
5242, 43, 41, 45, 51ltletrd 10536 . . . . 5 ((𝜑𝑠 ∈ ℝ) → 0 < 𝑈)
5341, 52elrpd 12178 . . . 4 ((𝜑𝑠 ∈ ℝ) → 𝑈 ∈ ℝ+)
54 max2 12330 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 𝑠 ∈ ℝ) → 𝑠 ≤ if(1 ≤ 𝑠, 𝑠, 1))
5537, 36, 54sylancr 581 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℝ) → 𝑠 ≤ if(1 ≤ 𝑠, 𝑠, 1))
5636, 39, 41, 55, 50letrd 10533 . . . . . . . . 9 ((𝜑𝑠 ∈ ℝ) → 𝑠𝑈)
5756adantr 474 . . . . . . . 8 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → 𝑠𝑈)
5836adantr 474 . . . . . . . . 9 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → 𝑠 ∈ ℝ)
5941adantr 474 . . . . . . . . 9 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → 𝑈 ∈ ℝ)
60 abscl 14425 . . . . . . . . . 10 (𝑥 ∈ ℂ → (abs‘𝑥) ∈ ℝ)
6160adantl 475 . . . . . . . . 9 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → (abs‘𝑥) ∈ ℝ)
62 lelttr 10467 . . . . . . . . 9 ((𝑠 ∈ ℝ ∧ 𝑈 ∈ ℝ ∧ (abs‘𝑥) ∈ ℝ) → ((𝑠𝑈𝑈 < (abs‘𝑥)) → 𝑠 < (abs‘𝑥)))
6358, 59, 61, 62syl3anc 1439 . . . . . . . 8 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → ((𝑠𝑈𝑈 < (abs‘𝑥)) → 𝑠 < (abs‘𝑥)))
6457, 63mpand 685 . . . . . . 7 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → (𝑈 < (abs‘𝑥) → 𝑠 < (abs‘𝑥)))
6564imim1d 82 . . . . . 6 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → ((𝑠 < (abs‘𝑥) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → (𝑈 < (abs‘𝑥) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)))))
6628ad2antrr 716 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝐹:ℂ⟶ℂ)
67 simprl 761 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑥 ∈ ℂ)
6866, 67ffvelrnd 6624 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (𝐹𝑥) ∈ ℂ)
698ad2antrr 716 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (𝐴𝑁) ∈ ℂ)
707ad2antrr 716 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑁 ∈ ℕ0)
7167, 70expcld 13327 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (𝑥𝑁) ∈ ℂ)
7269, 71mulcld 10397 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((𝐴𝑁) · (𝑥𝑁)) ∈ ℂ)
7368, 72subcld 10734 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))) ∈ ℂ)
7473abscld 14583 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) ∈ ℝ)
7572abscld 14583 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘((𝐴𝑁) · (𝑥𝑁))) ∈ ℝ)
7675rehalfcld 11629 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ∈ ℝ)
7774, 76, 75ltsub2d 10985 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ↔ ((abs‘((𝐴𝑁) · (𝑥𝑁))) − ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))))))
7869, 71absmuld 14601 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘((𝐴𝑁) · (𝑥𝑁))) = ((abs‘(𝐴𝑁)) · (abs‘(𝑥𝑁))))
7967, 70absexpd 14599 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝑥𝑁)) = ((abs‘𝑥)↑𝑁))
8079oveq2d 6938 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘(𝐴𝑁)) · (abs‘(𝑥𝑁))) = ((abs‘(𝐴𝑁)) · ((abs‘𝑥)↑𝑁)))
8178, 80eqtrd 2814 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘((𝐴𝑁) · (𝑥𝑁))) = ((abs‘(𝐴𝑁)) · ((abs‘𝑥)↑𝑁)))
8281oveq1d 6937 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) = (((abs‘(𝐴𝑁)) · ((abs‘𝑥)↑𝑁)) / 2))
8369abscld 14583 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐴𝑁)) ∈ ℝ)
8483recnd 10405 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐴𝑁)) ∈ ℂ)
8561adantrr 707 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘𝑥) ∈ ℝ)
8685, 70reexpcld 13344 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘𝑥)↑𝑁) ∈ ℝ)
8786recnd 10405 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘𝑥)↑𝑁) ∈ ℂ)
88 2cnd 11453 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 2 ∈ ℂ)
89 2ne0 11486 . . . . . . . . . . . . . . 15 2 ≠ 0
9089a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 2 ≠ 0)
9184, 87, 88, 90div23d 11188 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐴𝑁)) · ((abs‘𝑥)↑𝑁)) / 2) = (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)))
9282, 91eqtrd 2814 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) = (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)))
9392breq2d 4898 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ↔ (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))))
9475recnd 10405 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘((𝐴𝑁) · (𝑥𝑁))) ∈ ℂ)
95942halvesd 11628 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) + ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) = (abs‘((𝐴𝑁) · (𝑥𝑁))))
9695oveq1d 6937 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) + ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) − ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) = ((abs‘((𝐴𝑁) · (𝑥𝑁))) − ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)))
9776recnd 10405 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ∈ ℂ)
9897, 97pncand 10735 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) + ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) − ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) = ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2))
9996, 98eqtr3d 2816 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) − ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) = ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2))
10099breq1d 4896 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘((𝐴𝑁) · (𝑥𝑁))) − ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2)) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ↔ ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))))))
10177, 93, 1003bitr3d 301 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)) ↔ ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))))))
10272, 68subcld 10734 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((𝐴𝑁) · (𝑥𝑁)) − (𝐹𝑥)) ∈ ℂ)
10372, 102abs2difd 14604 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘(((𝐴𝑁) · (𝑥𝑁)) − (𝐹𝑥)))) ≤ (abs‘(((𝐴𝑁) · (𝑥𝑁)) − (((𝐴𝑁) · (𝑥𝑁)) − (𝐹𝑥)))))
10472, 68abssubd 14600 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(((𝐴𝑁) · (𝑥𝑁)) − (𝐹𝑥))) = (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))))
105104oveq2d 6938 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘(((𝐴𝑁) · (𝑥𝑁)) − (𝐹𝑥)))) = ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))))
10672, 68nncand 10739 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((𝐴𝑁) · (𝑥𝑁)) − (((𝐴𝑁) · (𝑥𝑁)) − (𝐹𝑥))) = (𝐹𝑥))
107106fveq2d 6450 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(((𝐴𝑁) · (𝑥𝑁)) − (((𝐴𝑁) · (𝑥𝑁)) − (𝐹𝑥)))) = (abs‘(𝐹𝑥)))
108103, 105, 1073brtr3d 4917 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ≤ (abs‘(𝐹𝑥)))
10975, 74resubcld 10803 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ∈ ℝ)
11068abscld 14583 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐹𝑥)) ∈ ℝ)
111 ltletr 10468 . . . . . . . . . . . 12 ((((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ∈ ℝ ∧ ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ∈ ℝ ∧ (abs‘(𝐹𝑥)) ∈ ℝ) → ((((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ∧ ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ≤ (abs‘(𝐹𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < (abs‘(𝐹𝑥))))
11276, 109, 110, 111syl3anc 1439 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ∧ ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) ≤ (abs‘(𝐹𝑥))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < (abs‘(𝐹𝑥))))
113108, 112mpan2d 684 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) − (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁))))) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < (abs‘(𝐹𝑥))))
114101, 113sylbid 232 . . . . . . . . 9 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)) → ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < (abs‘(𝐹𝑥))))
11532ad2antrr 716 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐹‘0)) ∈ ℝ)
11620ad2antrr 716 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘(𝐴𝑁)) / 2) ∈ ℝ+)
117116rpred 12181 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘(𝐴𝑁)) / 2) ∈ ℝ)
118117, 85remulcld 10407 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐴𝑁)) / 2) · (abs‘𝑥)) ∈ ℝ)
11992, 76eqeltrrd 2860 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)) ∈ ℝ)
12035adantr 474 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑇 ∈ ℝ)
12141adantr 474 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑈 ∈ ℝ)
122 max2 12330 . . . . . . . . . . . . . . . . . 18 ((if(1 ≤ 𝑠, 𝑠, 1) ∈ ℝ ∧ 𝑇 ∈ ℝ) → 𝑇 ≤ if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1)))
12339, 35, 122syl2anc 579 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ ℝ) → 𝑇 ≤ if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1)))
124123, 25syl6breqr 4928 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ ℝ) → 𝑇𝑈)
125124adantr 474 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑇𝑈)
126 simprr 763 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑈 < (abs‘𝑥))
127120, 121, 85, 125, 126lelttrd 10534 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑇 < (abs‘𝑥))
12826, 127syl5eqbrr 4922 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘(𝐹‘0)) / ((abs‘(𝐴𝑁)) / 2)) < (abs‘𝑥))
129115, 85, 116ltdivmuld 12232 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐹‘0)) / ((abs‘(𝐴𝑁)) / 2)) < (abs‘𝑥) ↔ (abs‘(𝐹‘0)) < (((abs‘(𝐴𝑁)) / 2) · (abs‘𝑥))))
130128, 129mpbid 224 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐹‘0)) < (((abs‘(𝐴𝑁)) / 2) · (abs‘𝑥)))
13185recnd 10405 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘𝑥) ∈ ℂ)
132131exp1d 13322 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘𝑥)↑1) = (abs‘𝑥))
133 1red 10377 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 1 ∈ ℝ)
13451adantr 474 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 1 ≤ 𝑈)
135133, 121, 85, 134, 126lelttrd 10534 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 1 < (abs‘𝑥))
136133, 85, 135ltled 10524 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 1 ≤ (abs‘𝑥))
1374ad2antrr 716 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑁 ∈ ℕ)
138 nnuz 12029 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
139137, 138syl6eleq 2869 . . . . . . . . . . . . . . 15 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑁 ∈ (ℤ‘1))
14085, 136, 139leexp2ad 13362 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘𝑥)↑1) ≤ ((abs‘𝑥)↑𝑁))
141132, 140eqbrtrrd 4910 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘𝑥) ≤ ((abs‘𝑥)↑𝑁))
14285, 86, 116lemul2d 12225 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘𝑥) ≤ ((abs‘𝑥)↑𝑁) ↔ (((abs‘(𝐴𝑁)) / 2) · (abs‘𝑥)) ≤ (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))))
143141, 142mpbid 224 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐴𝑁)) / 2) · (abs‘𝑥)) ≤ (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)))
144115, 118, 119, 130, 143ltletrd 10536 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐹‘0)) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)))
145144, 92breqtrrd 4914 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐹‘0)) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2))
146 lttr 10453 . . . . . . . . . . 11 (((abs‘(𝐹‘0)) ∈ ℝ ∧ ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ∈ ℝ ∧ (abs‘(𝐹𝑥)) ∈ ℝ) → (((abs‘(𝐹‘0)) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ∧ ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < (abs‘(𝐹𝑥))) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))))
147115, 76, 110, 146syl3anc 1439 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐹‘0)) < ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) ∧ ((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < (abs‘(𝐹𝑥))) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))))
148145, 147mpand 685 . . . . . . . . 9 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘((𝐴𝑁) · (𝑥𝑁))) / 2) < (abs‘(𝐹𝑥)) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))))
149114, 148syld 47 . . . . . . . 8 (((𝜑𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))))
150149expr 450 . . . . . . 7 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → (𝑈 < (abs‘𝑥) → ((abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁)) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))))
151150a2d 29 . . . . . 6 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → ((𝑈 < (abs‘𝑥) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → (𝑈 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))))
15265, 151syld 47 . . . . 5 (((𝜑𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → ((𝑠 < (abs‘𝑥) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → (𝑈 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))))
153152ralimdva 3144 . . . 4 ((𝜑𝑠 ∈ ℝ) → (∀𝑥 ∈ ℂ (𝑠 < (abs‘𝑥) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → ∀𝑥 ∈ ℂ (𝑈 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))))
154 breq1 4889 . . . . 5 (𝑟 = 𝑈 → (𝑟 < (abs‘𝑥) ↔ 𝑈 < (abs‘𝑥)))
155154rspceaimv 3519 . . . 4 ((𝑈 ∈ ℝ+ ∧ ∀𝑥 ∈ ℂ (𝑈 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))) → ∃𝑟 ∈ ℝ+𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))))
15653, 153, 155syl6an 674 . . 3 ((𝜑𝑠 ∈ ℝ) → (∀𝑥 ∈ ℂ (𝑠 < (abs‘𝑥) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → ∃𝑟 ∈ ℝ+𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))))
157156rexlimdva 3213 . 2 (𝜑 → (∃𝑠 ∈ ℝ ∀𝑥 ∈ ℂ (𝑠 < (abs‘𝑥) → (abs‘((𝐹𝑥) − ((𝐴𝑁) · (𝑥𝑁)))) < (((abs‘(𝐴𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → ∃𝑟 ∈ ℝ+𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥)))))
15824, 157mpd 15 1 (𝜑 → ∃𝑟 ∈ ℝ+𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹𝑥))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∈ wcel 2107   ≠ wne 2969  ∀wral 3090  ∃wrex 3091  ifcif 4307   class class class wbr 4886  ⟶wf 6131  ‘cfv 6135  (class class class)co 6922  ℂcc 10270  ℝcr 10271  0cc0 10272  1c1 10273   + caddc 10275   · cmul 10277   < clt 10411   ≤ cle 10412   − cmin 10606   / cdiv 11032  ℕcn 11374  2c2 11430  ℕ0cn0 11642  ℤ≥cuz 11992  ℝ+crp 12137  ...cfz 12643  ↑cexp 13178  abscabs 14381  Σcsu 14824  0𝑝c0p 23873  Polycply 24377  coeffccoe 24379  degcdgr 24380 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350  ax-addf 10351 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-of 7174  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-n0 11643  df-z 11729  df-uz 11993  df-rp 12138  df-ico 12493  df-fz 12644  df-fzo 12785  df-fl 12912  df-seq 13120  df-exp 13179  df-hash 13436  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-clim 14627  df-rlim 14628  df-sum 14825  df-0p 23874  df-ply 24381  df-coe 24383  df-dgr 24384 This theorem is referenced by:  fta  25258
 Copyright terms: Public domain W3C validator