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

Theorem dvferm 24089
Description: Fermat's theorem on stationary points. A point 𝑈 which is a local maximum has derivative equal to zero. (Contributed by Mario Carneiro, 1-Sep-2014.)
Hypotheses
Ref Expression
dvferm.a (𝜑𝐹:𝑋⟶ℝ)
dvferm.b (𝜑𝑋 ⊆ ℝ)
dvferm.u (𝜑𝑈 ∈ (𝐴(,)𝐵))
dvferm.s (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋)
dvferm.d (𝜑𝑈 ∈ dom (ℝ D 𝐹))
dvferm.r (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(𝐹𝑦) ≤ (𝐹𝑈))
Assertion
Ref Expression
dvferm (𝜑 → ((ℝ D 𝐹)‘𝑈) = 0)
Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑦,𝐹   𝑦,𝑈   𝑦,𝑋   𝜑,𝑦

Proof of Theorem dvferm
StepHypRef Expression
1 dvferm.a . . 3 (𝜑𝐹:𝑋⟶ℝ)
2 dvferm.b . . 3 (𝜑𝑋 ⊆ ℝ)
3 dvferm.u . . 3 (𝜑𝑈 ∈ (𝐴(,)𝐵))
4 dvferm.s . . 3 (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋)
5 dvferm.d . . 3 (𝜑𝑈 ∈ dom (ℝ D 𝐹))
6 ne0i 4120 . . . . . . 7 (𝑈 ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
7 ndmioo 12448 . . . . . . . 8 (¬ (𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = ∅)
87necon1ai 2997 . . . . . . 7 ((𝐴(,)𝐵) ≠ ∅ → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*))
93, 6, 83syl 18 . . . . . 6 (𝜑 → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*))
109simpld 489 . . . . 5 (𝜑𝐴 ∈ ℝ*)
11 ioossre 12481 . . . . . . . 8 (𝐴(,)𝐵) ⊆ ℝ
1211, 3sseldi 3795 . . . . . . 7 (𝜑𝑈 ∈ ℝ)
1312rexrd 10377 . . . . . 6 (𝜑𝑈 ∈ ℝ*)
14 eliooord 12479 . . . . . . . 8 (𝑈 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑈𝑈 < 𝐵))
153, 14syl 17 . . . . . . 7 (𝜑 → (𝐴 < 𝑈𝑈 < 𝐵))
1615simpld 489 . . . . . 6 (𝜑𝐴 < 𝑈)
1710, 13, 16xrltled 12227 . . . . 5 (𝜑𝐴𝑈)
18 iooss1 12456 . . . . 5 ((𝐴 ∈ ℝ*𝐴𝑈) → (𝑈(,)𝐵) ⊆ (𝐴(,)𝐵))
1910, 17, 18syl2anc 580 . . . 4 (𝜑 → (𝑈(,)𝐵) ⊆ (𝐴(,)𝐵))
20 dvferm.r . . . 4 (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(𝐹𝑦) ≤ (𝐹𝑈))
21 ssralv 3861 . . . 4 ((𝑈(,)𝐵) ⊆ (𝐴(,)𝐵) → (∀𝑦 ∈ (𝐴(,)𝐵)(𝐹𝑦) ≤ (𝐹𝑈) → ∀𝑦 ∈ (𝑈(,)𝐵)(𝐹𝑦) ≤ (𝐹𝑈)))
2219, 20, 21sylc 65 . . 3 (𝜑 → ∀𝑦 ∈ (𝑈(,)𝐵)(𝐹𝑦) ≤ (𝐹𝑈))
231, 2, 3, 4, 5, 22dvferm1 24086 . 2 (𝜑 → ((ℝ D 𝐹)‘𝑈) ≤ 0)
249simprd 490 . . . . 5 (𝜑𝐵 ∈ ℝ*)
2515simprd 490 . . . . . 6 (𝜑𝑈 < 𝐵)
2613, 24, 25xrltled 12227 . . . . 5 (𝜑𝑈𝐵)
27 iooss2 12457 . . . . 5 ((𝐵 ∈ ℝ*𝑈𝐵) → (𝐴(,)𝑈) ⊆ (𝐴(,)𝐵))
2824, 26, 27syl2anc 580 . . . 4 (𝜑 → (𝐴(,)𝑈) ⊆ (𝐴(,)𝐵))
29 ssralv 3861 . . . 4 ((𝐴(,)𝑈) ⊆ (𝐴(,)𝐵) → (∀𝑦 ∈ (𝐴(,)𝐵)(𝐹𝑦) ≤ (𝐹𝑈) → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹𝑦) ≤ (𝐹𝑈)))
3028, 20, 29sylc 65 . . 3 (𝜑 → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹𝑦) ≤ (𝐹𝑈))
311, 2, 3, 4, 5, 30dvferm2 24088 . 2 (𝜑 → 0 ≤ ((ℝ D 𝐹)‘𝑈))
32 dvfre 24052 . . . . 5 ((𝐹:𝑋⟶ℝ ∧ 𝑋 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
331, 2, 32syl2anc 580 . . . 4 (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
3433, 5ffvelrnd 6585 . . 3 (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℝ)
35 0re 10329 . . 3 0 ∈ ℝ
36 letri3 10412 . . 3 ((((ℝ D 𝐹)‘𝑈) ∈ ℝ ∧ 0 ∈ ℝ) → (((ℝ D 𝐹)‘𝑈) = 0 ↔ (((ℝ D 𝐹)‘𝑈) ≤ 0 ∧ 0 ≤ ((ℝ D 𝐹)‘𝑈))))
3734, 35, 36sylancl 581 . 2 (𝜑 → (((ℝ D 𝐹)‘𝑈) = 0 ↔ (((ℝ D 𝐹)‘𝑈) ≤ 0 ∧ 0 ≤ ((ℝ D 𝐹)‘𝑈))))
3823, 31, 37mpbir2and 705 1 (𝜑 → ((ℝ D 𝐹)‘𝑈) = 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385   = wceq 1653  wcel 2157  wne 2970  wral 3088  wss 3768  c0 4114   class class class wbr 4842  dom cdm 5311  wf 6096  cfv 6100  (class class class)co 6877  cr 10222  0cc0 10223  *cxr 10361   < clt 10362  cle 10363  (,)cioo 12421   D cdv 23965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-rep 4963  ax-sep 4974  ax-nul 4982  ax-pow 5034  ax-pr 5096  ax-un 7182  ax-cnex 10279  ax-resscn 10280  ax-1cn 10281  ax-icn 10282  ax-addcl 10283  ax-addrcl 10284  ax-mulcl 10285  ax-mulrcl 10286  ax-mulcom 10287  ax-addass 10288  ax-mulass 10289  ax-distr 10290  ax-i2m1 10291  ax-1ne0 10292  ax-1rid 10293  ax-rnegex 10294  ax-rrecex 10295  ax-cnre 10296  ax-pre-lttri 10297  ax-pre-lttrn 10298  ax-pre-ltadd 10299  ax-pre-mulgt0 10300  ax-pre-sup 10301
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ne 2971  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3386  df-sbc 3633  df-csb 3728  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-pss 3784  df-nul 4115  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4628  df-int 4667  df-iun 4711  df-iin 4712  df-br 4843  df-opab 4905  df-mpt 4922  df-tr 4945  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5897  df-ord 5943  df-on 5944  df-lim 5945  df-suc 5946  df-iota 6063  df-fun 6102  df-fn 6103  df-f 6104  df-f1 6105  df-fo 6106  df-f1o 6107  df-fv 6108  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-1st 7400  df-2nd 7401  df-wrecs 7644  df-recs 7706  df-rdg 7744  df-1o 7798  df-oadd 7802  df-er 7981  df-map 8096  df-pm 8097  df-en 8195  df-dom 8196  df-sdom 8197  df-fin 8198  df-fi 8558  df-sup 8589  df-inf 8590  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10557  df-neg 10558  df-div 10976  df-nn 11312  df-2 11373  df-3 11374  df-4 11375  df-5 11376  df-6 11377  df-7 11378  df-8 11379  df-9 11380  df-n0 11578  df-z 11664  df-dec 11781  df-uz 11928  df-q 12031  df-rp 12072  df-xneg 12190  df-xadd 12191  df-xmul 12192  df-ioo 12425  df-icc 12428  df-fz 12578  df-seq 13053  df-exp 13112  df-cj 14177  df-re 14178  df-im 14179  df-sqrt 14313  df-abs 14314  df-struct 16183  df-ndx 16184  df-slot 16185  df-base 16187  df-plusg 16277  df-mulr 16278  df-starv 16279  df-tset 16283  df-ple 16284  df-ds 16286  df-unif 16287  df-rest 16395  df-topn 16396  df-topgen 16416  df-psmet 20057  df-xmet 20058  df-met 20059  df-bl 20060  df-mopn 20061  df-fbas 20062  df-fg 20063  df-cnfld 20066  df-top 21024  df-topon 21041  df-topsp 21063  df-bases 21076  df-cld 21149  df-ntr 21150  df-cls 21151  df-nei 21228  df-lp 21266  df-perf 21267  df-cn 21357  df-cnp 21358  df-haus 21445  df-fil 21975  df-fm 22067  df-flim 22068  df-flf 22069  df-xms 22450  df-ms 22451  df-cncf 23006  df-limc 23968  df-dv 23969
This theorem is referenced by:  rollelem  24090  dvivthlem1  24109
  Copyright terms: Public domain W3C validator