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

Theorem ftalem2 26578
Description: Lemma for fta 26584. 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 25746 . . . . . . 7 (𝐹 ∈ (Polyβ€˜π‘†) β†’ 𝐴:β„•0βŸΆβ„‚)
63, 5syl 17 . . . . . 6 (πœ‘ β†’ 𝐴:β„•0βŸΆβ„‚)
74nnnn0d 12532 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ β„•0)
86, 7ffvelcdmd 7088 . . . . 5 (πœ‘ β†’ (π΄β€˜π‘) ∈ β„‚)
94nnne0d 12262 . . . . . 6 (πœ‘ β†’ 𝑁 β‰  0)
102, 1dgreq0 25779 . . . . . . . . 9 (𝐹 ∈ (Polyβ€˜π‘†) β†’ (𝐹 = 0𝑝 ↔ (π΄β€˜π‘) = 0))
11 fveq2 6892 . . . . . . . . . . 11 (𝐹 = 0𝑝 β†’ (degβ€˜πΉ) = (degβ€˜0𝑝))
12 dgr0 25776 . . . . . . . . . . 11 (degβ€˜0𝑝) = 0
1311, 12eqtrdi 2789 . . . . . . . . . 10 (𝐹 = 0𝑝 β†’ (degβ€˜πΉ) = 0)
142, 13eqtrid 2785 . . . . . . . . 9 (𝐹 = 0𝑝 β†’ 𝑁 = 0)
1510, 14syl6bir 254 . . . . . . . 8 (𝐹 ∈ (Polyβ€˜π‘†) β†’ ((π΄β€˜π‘) = 0 β†’ 𝑁 = 0))
163, 15syl 17 . . . . . . 7 (πœ‘ β†’ ((π΄β€˜π‘) = 0 β†’ 𝑁 = 0))
1716necon3d 2962 . . . . . 6 (πœ‘ β†’ (𝑁 β‰  0 β†’ (π΄β€˜π‘) β‰  0))
189, 17mpd 15 . . . . 5 (πœ‘ β†’ (π΄β€˜π‘) β‰  0)
198, 18absrpcld 15395 . . . 4 (πœ‘ β†’ (absβ€˜(π΄β€˜π‘)) ∈ ℝ+)
2019rphalfcld 13028 . . 3 (πœ‘ β†’ ((absβ€˜(π΄β€˜π‘)) / 2) ∈ ℝ+)
21 2fveq3 6897 . . . . 5 (𝑛 = π‘˜ β†’ (absβ€˜(π΄β€˜π‘›)) = (absβ€˜(π΄β€˜π‘˜)))
2221cbvsumv 15642 . . . 4 Σ𝑛 ∈ (0...(𝑁 βˆ’ 1))(absβ€˜(π΄β€˜π‘›)) = Ξ£π‘˜ ∈ (0...(𝑁 βˆ’ 1))(absβ€˜(π΄β€˜π‘˜))
2322oveq1i 7419 . . 3 (Σ𝑛 ∈ (0...(𝑁 βˆ’ 1))(absβ€˜(π΄β€˜π‘›)) / ((absβ€˜(π΄β€˜π‘)) / 2)) = (Ξ£π‘˜ ∈ (0...(𝑁 βˆ’ 1))(absβ€˜(π΄β€˜π‘˜)) / ((absβ€˜(π΄β€˜π‘)) / 2))
241, 2, 3, 4, 20, 23ftalem1 26577 . 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 25712 . . . . . . . . . . . . 13 (𝐹 ∈ (Polyβ€˜π‘†) β†’ 𝐹:β„‚βŸΆβ„‚)
283, 27syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹:β„‚βŸΆβ„‚)
29 0cn 11206 . . . . . . . . . . . 12 0 ∈ β„‚
30 ffvelcdm 7084 . . . . . . . . . . . 12 ((𝐹:β„‚βŸΆβ„‚ ∧ 0 ∈ β„‚) β†’ (πΉβ€˜0) ∈ β„‚)
3128, 29, 30sylancl 587 . . . . . . . . . . 11 (πœ‘ β†’ (πΉβ€˜0) ∈ β„‚)
3231abscld 15383 . . . . . . . . . 10 (πœ‘ β†’ (absβ€˜(πΉβ€˜0)) ∈ ℝ)
3332, 20rerpdivcld 13047 . . . . . . . . 9 (πœ‘ β†’ ((absβ€˜(πΉβ€˜0)) / ((absβ€˜(π΄β€˜π‘)) / 2)) ∈ ℝ)
3426, 33eqeltrid 2838 . . . . . . . 8 (πœ‘ β†’ 𝑇 ∈ ℝ)
3534adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ 𝑇 ∈ ℝ)
36 simpr 486 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ 𝑠 ∈ ℝ)
37 1re 11214 . . . . . . . 8 1 ∈ ℝ
38 ifcl 4574 . . . . . . . 8 ((𝑠 ∈ ℝ ∧ 1 ∈ ℝ) β†’ if(1 ≀ 𝑠, 𝑠, 1) ∈ ℝ)
3936, 37, 38sylancl 587 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ if(1 ≀ 𝑠, 𝑠, 1) ∈ ℝ)
4035, 39ifcld 4575 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ if(if(1 ≀ 𝑠, 𝑠, 1) ≀ 𝑇, 𝑇, if(1 ≀ 𝑠, 𝑠, 1)) ∈ ℝ)
4125, 40eqeltrid 2838 . . . . 5 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ π‘ˆ ∈ ℝ)
42 0red 11217 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ 0 ∈ ℝ)
43 1red 11215 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ 1 ∈ ℝ)
44 0lt1 11736 . . . . . . 7 0 < 1
4544a1i 11 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ 0 < 1)
46 max1 13164 . . . . . . . 8 ((1 ∈ ℝ ∧ 𝑠 ∈ ℝ) β†’ 1 ≀ if(1 ≀ 𝑠, 𝑠, 1))
4737, 36, 46sylancr 588 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ 1 ≀ if(1 ≀ 𝑠, 𝑠, 1))
48 max1 13164 . . . . . . . . 9 ((if(1 ≀ 𝑠, 𝑠, 1) ∈ ℝ ∧ 𝑇 ∈ ℝ) β†’ if(1 ≀ 𝑠, 𝑠, 1) ≀ if(if(1 ≀ 𝑠, 𝑠, 1) ≀ 𝑇, 𝑇, if(1 ≀ 𝑠, 𝑠, 1)))
4939, 35, 48syl2anc 585 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ if(1 ≀ 𝑠, 𝑠, 1) ≀ if(if(1 ≀ 𝑠, 𝑠, 1) ≀ 𝑇, 𝑇, if(1 ≀ 𝑠, 𝑠, 1)))
5049, 25breqtrrdi 5191 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ if(1 ≀ 𝑠, 𝑠, 1) ≀ π‘ˆ)
5143, 39, 41, 47, 50letrd 11371 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ 1 ≀ π‘ˆ)
5242, 43, 41, 45, 51ltletrd 11374 . . . . 5 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ 0 < π‘ˆ)
5341, 52elrpd 13013 . . . 4 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ π‘ˆ ∈ ℝ+)
54 max2 13166 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 𝑠 ∈ ℝ) β†’ 𝑠 ≀ if(1 ≀ 𝑠, 𝑠, 1))
5537, 36, 54sylancr 588 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ 𝑠 ≀ if(1 ≀ 𝑠, 𝑠, 1))
5636, 39, 41, 55, 50letrd 11371 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ 𝑠 ≀ π‘ˆ)
5756adantr 482 . . . . . . . 8 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ π‘₯ ∈ β„‚) β†’ 𝑠 ≀ π‘ˆ)
58 abscl 15225 . . . . . . . . 9 (π‘₯ ∈ β„‚ β†’ (absβ€˜π‘₯) ∈ ℝ)
59 lelttr 11304 . . . . . . . . 9 ((𝑠 ∈ ℝ ∧ π‘ˆ ∈ ℝ ∧ (absβ€˜π‘₯) ∈ ℝ) β†’ ((𝑠 ≀ π‘ˆ ∧ π‘ˆ < (absβ€˜π‘₯)) β†’ 𝑠 < (absβ€˜π‘₯)))
6036, 41, 58, 59syl2an3an 1423 . . . . . . . 8 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ π‘₯ ∈ β„‚) β†’ ((𝑠 ≀ π‘ˆ ∧ π‘ˆ < (absβ€˜π‘₯)) β†’ 𝑠 < (absβ€˜π‘₯)))
6157, 60mpand 694 . . . . . . 7 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ π‘₯ ∈ β„‚) β†’ (π‘ˆ < (absβ€˜π‘₯) β†’ 𝑠 < (absβ€˜π‘₯)))
6261imim1d 82 . . . . . 6 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ π‘₯ ∈ β„‚) β†’ ((𝑠 < (absβ€˜π‘₯) β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁)))) < (((absβ€˜(π΄β€˜π‘)) / 2) Β· ((absβ€˜π‘₯)↑𝑁))) β†’ (π‘ˆ < (absβ€˜π‘₯) β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁)))) < (((absβ€˜(π΄β€˜π‘)) / 2) Β· ((absβ€˜π‘₯)↑𝑁)))))
6328ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ 𝐹:β„‚βŸΆβ„‚)
64 simprl 770 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ π‘₯ ∈ β„‚)
6563, 64ffvelcdmd 7088 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
668ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (π΄β€˜π‘) ∈ β„‚)
677ad2antrr 725 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ 𝑁 ∈ β„•0)
6864, 67expcld 14111 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (π‘₯↑𝑁) ∈ β„‚)
6966, 68mulcld 11234 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁)) ∈ β„‚)
7065, 69subcld 11571 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁))) ∈ β„‚)
7170abscld 15383 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁)))) ∈ ℝ)
7269abscld 15383 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) ∈ ℝ)
7372rehalfcld 12459 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) ∈ ℝ)
7471, 73, 72ltsub2d 11824 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁)))) < ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) ↔ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) βˆ’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2)) < ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) βˆ’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁)))))))
7566, 68absmuld 15401 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) = ((absβ€˜(π΄β€˜π‘)) Β· (absβ€˜(π‘₯↑𝑁))))
7664, 67absexpd 15399 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜(π‘₯↑𝑁)) = ((absβ€˜π‘₯)↑𝑁))
7776oveq2d 7425 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜(π΄β€˜π‘)) Β· (absβ€˜(π‘₯↑𝑁))) = ((absβ€˜(π΄β€˜π‘)) Β· ((absβ€˜π‘₯)↑𝑁)))
7875, 77eqtrd 2773 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) = ((absβ€˜(π΄β€˜π‘)) Β· ((absβ€˜π‘₯)↑𝑁)))
7978oveq1d 7424 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) = (((absβ€˜(π΄β€˜π‘)) Β· ((absβ€˜π‘₯)↑𝑁)) / 2))
8066abscld 15383 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜(π΄β€˜π‘)) ∈ ℝ)
8180recnd 11242 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜(π΄β€˜π‘)) ∈ β„‚)
8258ad2antrl 727 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜π‘₯) ∈ ℝ)
8382, 67reexpcld 14128 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜π‘₯)↑𝑁) ∈ ℝ)
8483recnd 11242 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜π‘₯)↑𝑁) ∈ β„‚)
85 2cnd 12290 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ 2 ∈ β„‚)
86 2ne0 12316 . . . . . . . . . . . . . . 15 2 β‰  0
8786a1i 11 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ 2 β‰  0)
8881, 84, 85, 87div23d 12027 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (((absβ€˜(π΄β€˜π‘)) Β· ((absβ€˜π‘₯)↑𝑁)) / 2) = (((absβ€˜(π΄β€˜π‘)) / 2) Β· ((absβ€˜π‘₯)↑𝑁)))
8979, 88eqtrd 2773 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) = (((absβ€˜(π΄β€˜π‘)) / 2) Β· ((absβ€˜π‘₯)↑𝑁)))
9089breq2d 5161 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁)))) < ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) ↔ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁)))) < (((absβ€˜(π΄β€˜π‘)) / 2) Β· ((absβ€˜π‘₯)↑𝑁))))
9172recnd 11242 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) ∈ β„‚)
92912halvesd 12458 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) + ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2)) = (absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))))
9392oveq1d 7424 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) + ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2)) βˆ’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2)) = ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) βˆ’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2)))
9473recnd 11242 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) ∈ β„‚)
9594, 94pncand 11572 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) + ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2)) βˆ’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2)) = ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2))
9693, 95eqtr3d 2775 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) βˆ’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2)) = ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2))
9796breq1d 5159 . . . . . . . . . . 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 11571 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (((π΄β€˜π‘) Β· (π‘₯↑𝑁)) βˆ’ (πΉβ€˜π‘₯)) ∈ β„‚)
10069, 99abs2difd 15404 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) βˆ’ (absβ€˜(((π΄β€˜π‘) Β· (π‘₯↑𝑁)) βˆ’ (πΉβ€˜π‘₯)))) ≀ (absβ€˜(((π΄β€˜π‘) Β· (π‘₯↑𝑁)) βˆ’ (((π΄β€˜π‘) Β· (π‘₯↑𝑁)) βˆ’ (πΉβ€˜π‘₯)))))
10169, 65abssubd 15400 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜(((π΄β€˜π‘) Β· (π‘₯↑𝑁)) βˆ’ (πΉβ€˜π‘₯))) = (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁)))))
102101oveq2d 7425 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) βˆ’ (absβ€˜(((π΄β€˜π‘) Β· (π‘₯↑𝑁)) βˆ’ (πΉβ€˜π‘₯)))) = ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) βˆ’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁))))))
10369, 65nncand 11576 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (((π΄β€˜π‘) Β· (π‘₯↑𝑁)) βˆ’ (((π΄β€˜π‘) Β· (π‘₯↑𝑁)) βˆ’ (πΉβ€˜π‘₯))) = (πΉβ€˜π‘₯))
104103fveq2d 6896 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜(((π΄β€˜π‘) Β· (π‘₯↑𝑁)) βˆ’ (((π΄β€˜π‘) Β· (π‘₯↑𝑁)) βˆ’ (πΉβ€˜π‘₯)))) = (absβ€˜(πΉβ€˜π‘₯)))
105100, 102, 1043brtr3d 5180 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) βˆ’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁))))) ≀ (absβ€˜(πΉβ€˜π‘₯)))
10672, 71resubcld 11642 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) βˆ’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁))))) ∈ ℝ)
10765abscld 15383 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜(πΉβ€˜π‘₯)) ∈ ℝ)
108 ltletr 11306 . . . . . . . . . . . 12 ((((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) ∈ ℝ ∧ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) βˆ’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁))))) ∈ ℝ ∧ (absβ€˜(πΉβ€˜π‘₯)) ∈ ℝ) β†’ ((((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) < ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) βˆ’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁))))) ∧ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) βˆ’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁))))) ≀ (absβ€˜(πΉβ€˜π‘₯))) β†’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) < (absβ€˜(πΉβ€˜π‘₯))))
10973, 106, 107, 108syl3anc 1372 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) < ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) βˆ’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁))))) ∧ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) βˆ’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁))))) ≀ (absβ€˜(πΉβ€˜π‘₯))) β†’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) < (absβ€˜(πΉβ€˜π‘₯))))
110105, 109mpan2d 693 . . . . . . . . . 10 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) < ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) βˆ’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁))))) β†’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) < (absβ€˜(πΉβ€˜π‘₯))))
11198, 110sylbid 239 . . . . . . . . 9 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁)))) < (((absβ€˜(π΄β€˜π‘)) / 2) Β· ((absβ€˜π‘₯)↑𝑁)) β†’ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) < (absβ€˜(πΉβ€˜π‘₯))))
11232ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜(πΉβ€˜0)) ∈ ℝ)
11320ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜(π΄β€˜π‘)) / 2) ∈ ℝ+)
114113rpred 13016 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜(π΄β€˜π‘)) / 2) ∈ ℝ)
115114, 82remulcld 11244 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (((absβ€˜(π΄β€˜π‘)) / 2) Β· (absβ€˜π‘₯)) ∈ ℝ)
11689, 73eqeltrrd 2835 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (((absβ€˜(π΄β€˜π‘)) / 2) Β· ((absβ€˜π‘₯)↑𝑁)) ∈ ℝ)
11735adantr 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ 𝑇 ∈ ℝ)
11841adantr 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ π‘ˆ ∈ ℝ)
119 max2 13166 . . . . . . . . . . . . . . . . . 18 ((if(1 ≀ 𝑠, 𝑠, 1) ∈ ℝ ∧ 𝑇 ∈ ℝ) β†’ 𝑇 ≀ if(if(1 ≀ 𝑠, 𝑠, 1) ≀ 𝑇, 𝑇, if(1 ≀ 𝑠, 𝑠, 1)))
12039, 35, 119syl2anc 585 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ 𝑇 ≀ if(if(1 ≀ 𝑠, 𝑠, 1) ≀ 𝑇, 𝑇, if(1 ≀ 𝑠, 𝑠, 1)))
121120, 25breqtrrdi 5191 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ 𝑇 ≀ π‘ˆ)
122121adantr 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ 𝑇 ≀ π‘ˆ)
123 simprr 772 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ π‘ˆ < (absβ€˜π‘₯))
124117, 118, 82, 122, 123lelttrd 11372 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ 𝑇 < (absβ€˜π‘₯))
12526, 124eqbrtrrid 5185 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜(πΉβ€˜0)) / ((absβ€˜(π΄β€˜π‘)) / 2)) < (absβ€˜π‘₯))
126112, 82, 113ltdivmuld 13067 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (((absβ€˜(πΉβ€˜0)) / ((absβ€˜(π΄β€˜π‘)) / 2)) < (absβ€˜π‘₯) ↔ (absβ€˜(πΉβ€˜0)) < (((absβ€˜(π΄β€˜π‘)) / 2) Β· (absβ€˜π‘₯))))
127125, 126mpbid 231 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜(πΉβ€˜0)) < (((absβ€˜(π΄β€˜π‘)) / 2) Β· (absβ€˜π‘₯)))
12882recnd 11242 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜π‘₯) ∈ β„‚)
129128exp1d 14106 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜π‘₯)↑1) = (absβ€˜π‘₯))
130 1red 11215 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ 1 ∈ ℝ)
13151adantr 482 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ 1 ≀ π‘ˆ)
132130, 118, 82, 131, 123lelttrd 11372 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ 1 < (absβ€˜π‘₯))
133130, 82, 132ltled 11362 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ 1 ≀ (absβ€˜π‘₯))
1344ad2antrr 725 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ 𝑁 ∈ β„•)
135 nnuz 12865 . . . . . . . . . . . . . . . 16 β„• = (β„€β‰₯β€˜1)
136134, 135eleqtrdi 2844 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ 𝑁 ∈ (β„€β‰₯β€˜1))
13782, 133, 136leexp2ad 14217 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜π‘₯)↑1) ≀ ((absβ€˜π‘₯)↑𝑁))
138129, 137eqbrtrrd 5173 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜π‘₯) ≀ ((absβ€˜π‘₯)↑𝑁))
13982, 83, 113lemul2d 13060 . . . . . . . . . . . . 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 11374 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜(πΉβ€˜0)) < (((absβ€˜(π΄β€˜π‘)) / 2) Β· ((absβ€˜π‘₯)↑𝑁)))
142141, 89breqtrrd 5177 . . . . . . . . . 10 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (absβ€˜(πΉβ€˜0)) < ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2))
143 lttr 11290 . . . . . . . . . . 11 (((absβ€˜(πΉβ€˜0)) ∈ ℝ ∧ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) ∈ ℝ ∧ (absβ€˜(πΉβ€˜π‘₯)) ∈ ℝ) β†’ (((absβ€˜(πΉβ€˜0)) < ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) ∧ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) < (absβ€˜(πΉβ€˜π‘₯))) β†’ (absβ€˜(πΉβ€˜0)) < (absβ€˜(πΉβ€˜π‘₯))))
144112, 73, 107, 143syl3anc 1372 . . . . . . . . . 10 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (((absβ€˜(πΉβ€˜0)) < ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) ∧ ((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) < (absβ€˜(πΉβ€˜π‘₯))) β†’ (absβ€˜(πΉβ€˜0)) < (absβ€˜(πΉβ€˜π‘₯))))
145142, 144mpand 694 . . . . . . . . 9 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ (((absβ€˜((π΄β€˜π‘) Β· (π‘₯↑𝑁))) / 2) < (absβ€˜(πΉβ€˜π‘₯)) β†’ (absβ€˜(πΉβ€˜0)) < (absβ€˜(πΉβ€˜π‘₯))))
146111, 145syld 47 . . . . . . . 8 (((πœ‘ ∧ 𝑠 ∈ ℝ) ∧ (π‘₯ ∈ β„‚ ∧ π‘ˆ < (absβ€˜π‘₯))) β†’ ((absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁)))) < (((absβ€˜(π΄β€˜π‘)) / 2) Β· ((absβ€˜π‘₯)↑𝑁)) β†’ (absβ€˜(πΉβ€˜0)) < (absβ€˜(πΉβ€˜π‘₯))))
147146expr 458 . . . . . . 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 3168 . . . 4 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ (βˆ€π‘₯ ∈ β„‚ (𝑠 < (absβ€˜π‘₯) β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁)))) < (((absβ€˜(π΄β€˜π‘)) / 2) Β· ((absβ€˜π‘₯)↑𝑁))) β†’ βˆ€π‘₯ ∈ β„‚ (π‘ˆ < (absβ€˜π‘₯) β†’ (absβ€˜(πΉβ€˜0)) < (absβ€˜(πΉβ€˜π‘₯)))))
151 breq1 5152 . . . . 5 (π‘Ÿ = π‘ˆ β†’ (π‘Ÿ < (absβ€˜π‘₯) ↔ π‘ˆ < (absβ€˜π‘₯)))
152151rspceaimv 3618 . . . 4 ((π‘ˆ ∈ ℝ+ ∧ βˆ€π‘₯ ∈ β„‚ (π‘ˆ < (absβ€˜π‘₯) β†’ (absβ€˜(πΉβ€˜0)) < (absβ€˜(πΉβ€˜π‘₯)))) β†’ βˆƒπ‘Ÿ ∈ ℝ+ βˆ€π‘₯ ∈ β„‚ (π‘Ÿ < (absβ€˜π‘₯) β†’ (absβ€˜(πΉβ€˜0)) < (absβ€˜(πΉβ€˜π‘₯))))
15353, 150, 152syl6an 683 . . 3 ((πœ‘ ∧ 𝑠 ∈ ℝ) β†’ (βˆ€π‘₯ ∈ β„‚ (𝑠 < (absβ€˜π‘₯) β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ ((π΄β€˜π‘) Β· (π‘₯↑𝑁)))) < (((absβ€˜(π΄β€˜π‘)) / 2) Β· ((absβ€˜π‘₯)↑𝑁))) β†’ βˆƒπ‘Ÿ ∈ ℝ+ βˆ€π‘₯ ∈ β„‚ (π‘Ÿ < (absβ€˜π‘₯) β†’ (absβ€˜(πΉβ€˜0)) < (absβ€˜(πΉβ€˜π‘₯)))))
154153rexlimdva 3156 . 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 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  ifcif 4529   class class class wbr 5149  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409  β„‚cc 11108  β„cr 11109  0cc0 11110  1c1 11111   + caddc 11113   Β· cmul 11115   < clt 11248   ≀ cle 11249   βˆ’ cmin 11444   / cdiv 11871  β„•cn 12212  2c2 12267  β„•0cn0 12472  β„€β‰₯cuz 12822  β„+crp 12974  ...cfz 13484  β†‘cexp 14027  abscabs 15181  Ξ£csu 15632  0𝑝c0p 25186  Polycply 25698  coeffccoe 25700  degcdgr 25701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-pm 8823  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9437  df-inf 9438  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-z 12559  df-uz 12823  df-rp 12975  df-ico 13330  df-fz 13485  df-fzo 13628  df-fl 13757  df-seq 13967  df-exp 14028  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-clim 15432  df-rlim 15433  df-sum 15633  df-0p 25187  df-ply 25702  df-coe 25704  df-dgr 25705
This theorem is referenced by:  fta  26584
  Copyright terms: Public domain W3C validator