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

Theorem dvlt0 25974
Description: A function on a closed interval with negative derivative is decreasing. (Contributed by Mario Carneiro, 19-Feb-2015.)
Hypotheses
Ref Expression
dvgt0.a (𝜑𝐴 ∈ ℝ)
dvgt0.b (𝜑𝐵 ∈ ℝ)
dvgt0.f (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))
dvlt0.d (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶(-∞(,)0))
Assertion
Ref Expression
dvlt0 (𝜑𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹))

Proof of Theorem dvlt0
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvgt0.a . 2 (𝜑𝐴 ∈ ℝ)
2 dvgt0.b . 2 (𝜑𝐵 ∈ ℝ)
3 dvgt0.f . 2 (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))
4 dvlt0.d . 2 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶(-∞(,)0))
5 gtso 11229 . 2 < Or ℝ
61, 2, 3, 4dvgt0lem1 25971 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((𝐹𝑦) − (𝐹𝑥)) / (𝑦𝑥)) ∈ (-∞(,)0))
7 eliooord 13360 . . . . . . . . 9 ((((𝐹𝑦) − (𝐹𝑥)) / (𝑦𝑥)) ∈ (-∞(,)0) → (-∞ < (((𝐹𝑦) − (𝐹𝑥)) / (𝑦𝑥)) ∧ (((𝐹𝑦) − (𝐹𝑥)) / (𝑦𝑥)) < 0))
86, 7syl 17 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (-∞ < (((𝐹𝑦) − (𝐹𝑥)) / (𝑦𝑥)) ∧ (((𝐹𝑦) − (𝐹𝑥)) / (𝑦𝑥)) < 0))
98simprd 495 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((𝐹𝑦) − (𝐹𝑥)) / (𝑦𝑥)) < 0)
10 cncff 24862 . . . . . . . . . . . 12 (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐹:(𝐴[,]𝐵)⟶ℝ)
113, 10syl 17 . . . . . . . . . . 11 (𝜑𝐹:(𝐴[,]𝐵)⟶ℝ)
1211ad2antrr 727 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝐹:(𝐴[,]𝐵)⟶ℝ)
13 simplrr 778 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑦 ∈ (𝐴[,]𝐵))
1412, 13ffvelcdmd 7039 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹𝑦) ∈ ℝ)
15 simplrl 777 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ∈ (𝐴[,]𝐵))
1612, 15ffvelcdmd 7039 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹𝑥) ∈ ℝ)
1714, 16resubcld 11580 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹𝑦) − (𝐹𝑥)) ∈ ℝ)
18 0red 11149 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 0 ∈ ℝ)
19 iccssre 13384 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
201, 2, 19syl2anc 585 . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
2120ad2antrr 727 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐴[,]𝐵) ⊆ ℝ)
2221, 13sseldd 3923 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℝ)
2321, 15sseldd 3923 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℝ)
2422, 23resubcld 11580 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑦𝑥) ∈ ℝ)
25 simpr 484 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 < 𝑦)
2623, 22posdifd 11739 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥 < 𝑦 ↔ 0 < (𝑦𝑥)))
2725, 26mpbid 232 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 0 < (𝑦𝑥))
28 ltdivmul 12033 . . . . . . . 8 ((((𝐹𝑦) − (𝐹𝑥)) ∈ ℝ ∧ 0 ∈ ℝ ∧ ((𝑦𝑥) ∈ ℝ ∧ 0 < (𝑦𝑥))) → ((((𝐹𝑦) − (𝐹𝑥)) / (𝑦𝑥)) < 0 ↔ ((𝐹𝑦) − (𝐹𝑥)) < ((𝑦𝑥) · 0)))
2917, 18, 24, 27, 28syl112anc 1377 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((((𝐹𝑦) − (𝐹𝑥)) / (𝑦𝑥)) < 0 ↔ ((𝐹𝑦) − (𝐹𝑥)) < ((𝑦𝑥) · 0)))
309, 29mpbid 232 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹𝑦) − (𝐹𝑥)) < ((𝑦𝑥) · 0))
3124recnd 11175 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑦𝑥) ∈ ℂ)
3231mul01d 11347 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝑦𝑥) · 0) = 0)
3330, 32breqtrd 5112 . . . . 5 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹𝑦) − (𝐹𝑥)) < 0)
3414, 16, 18ltsubaddd 11748 . . . . 5 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((𝐹𝑦) − (𝐹𝑥)) < 0 ↔ (𝐹𝑦) < (0 + (𝐹𝑥))))
3533, 34mpbid 232 . . . 4 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹𝑦) < (0 + (𝐹𝑥)))
3616recnd 11175 . . . . 5 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹𝑥) ∈ ℂ)
3736addlidd 11349 . . . 4 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (0 + (𝐹𝑥)) = (𝐹𝑥))
3835, 37breqtrd 5112 . . 3 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹𝑦) < (𝐹𝑥))
39 fvex 6855 . . . 4 (𝐹𝑥) ∈ V
40 fvex 6855 . . . 4 (𝐹𝑦) ∈ V
4139, 40brcnv 5839 . . 3 ((𝐹𝑥) < (𝐹𝑦) ↔ (𝐹𝑦) < (𝐹𝑥))
4238, 41sylibr 234 . 2 (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹𝑥) < (𝐹𝑦))
431, 2, 3, 4, 5, 42dvgt0lem2 25972 1 (𝜑𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wcel 2114  wss 3890   class class class wbr 5086  ccnv 5631  ran crn 5633  wf 6496  cfv 6500   Isom wiso 6501  (class class class)co 7369  cr 11039  0cc0 11040   + caddc 11043   · cmul 11045  -∞cmnf 11179   < clt 11181  cmin 11379   / cdiv 11809  (,)cioo 13300  [,]cicc 13303  cnccncf 24845   D cdv 25832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376  ax-un 7691  ax-cnex 11096  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116  ax-pre-mulgt0 11117  ax-pre-sup 11118  ax-addf 11119
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-se 5586  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-of 7633  df-om 7820  df-1st 7944  df-2nd 7945  df-supp 8113  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-2o 8408  df-er 8645  df-map 8777  df-pm 8778  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9277  df-fi 9326  df-sup 9357  df-inf 9358  df-oi 9427  df-card 9865  df-pnf 11183  df-mnf 11184  df-xr 11185  df-ltxr 11186  df-le 11187  df-sub 11381  df-neg 11382  df-div 11810  df-nn 12177  df-2 12246  df-3 12247  df-4 12248  df-5 12249  df-6 12250  df-7 12251  df-8 12252  df-9 12253  df-n0 12440  df-z 12527  df-dec 12647  df-uz 12791  df-q 12901  df-rp 12945  df-xneg 13065  df-xadd 13066  df-xmul 13067  df-ioo 13304  df-ico 13306  df-icc 13307  df-fz 13464  df-fzo 13611  df-seq 13966  df-exp 14026  df-hash 14295  df-cj 15063  df-re 15064  df-im 15065  df-sqrt 15199  df-abs 15200  df-struct 17119  df-sets 17136  df-slot 17154  df-ndx 17166  df-base 17182  df-ress 17203  df-plusg 17235  df-mulr 17236  df-starv 17237  df-sca 17238  df-vsca 17239  df-ip 17240  df-tset 17241  df-ple 17242  df-ds 17244  df-unif 17245  df-hom 17246  df-cco 17247  df-rest 17387  df-topn 17388  df-0g 17406  df-gsum 17407  df-topgen 17408  df-pt 17409  df-prds 17412  df-xrs 17468  df-qtop 17473  df-imas 17474  df-xps 17476  df-mre 17550  df-mrc 17551  df-acs 17553  df-mgm 18610  df-sgrp 18689  df-mnd 18705  df-submnd 18754  df-mulg 19046  df-cntz 19294  df-cmn 19759  df-psmet 21346  df-xmet 21347  df-met 21348  df-bl 21349  df-mopn 21350  df-fbas 21351  df-fg 21352  df-cnfld 21355  df-top 22861  df-topon 22878  df-topsp 22900  df-bases 22913  df-cld 22986  df-ntr 22987  df-cls 22988  df-nei 23065  df-lp 23103  df-perf 23104  df-cn 23194  df-cnp 23195  df-haus 23282  df-cmp 23354  df-tx 23529  df-hmeo 23722  df-fil 23813  df-fm 23905  df-flim 23906  df-flf 23907  df-xms 24287  df-ms 24288  df-tms 24289  df-cncf 24847  df-limc 25835  df-dv 25836
This theorem is referenced by:  dvne0  25980
  Copyright terms: Public domain W3C validator