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

Theorem dvcvx 25966
Description: A real function with strictly increasing derivative is strictly convex. (Contributed by Mario Carneiro, 20-Jun-2015.)
Hypotheses
Ref Expression
dvcvx.a (πœ‘ β†’ 𝐴 ∈ ℝ)
dvcvx.b (πœ‘ β†’ 𝐡 ∈ ℝ)
dvcvx.l (πœ‘ β†’ 𝐴 < 𝐡)
dvcvx.f (πœ‘ β†’ 𝐹 ∈ ((𝐴[,]𝐡)–cn→ℝ))
dvcvx.d (πœ‘ β†’ (ℝ D 𝐹) Isom < , < ((𝐴(,)𝐡), π‘Š))
dvcvx.t (πœ‘ β†’ 𝑇 ∈ (0(,)1))
dvcvx.c 𝐢 = ((𝑇 Β· 𝐴) + ((1 βˆ’ 𝑇) Β· 𝐡))
Assertion
Ref Expression
dvcvx (πœ‘ β†’ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅))))

Proof of Theorem dvcvx
Dummy variables π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvcvx.a . . 3 (πœ‘ β†’ 𝐴 ∈ ℝ)
2 dvcvx.c . . . 4 𝐢 = ((𝑇 Β· 𝐴) + ((1 βˆ’ 𝑇) Β· 𝐡))
3 dvcvx.t . . . . . . 7 (πœ‘ β†’ 𝑇 ∈ (0(,)1))
4 elioore 13387 . . . . . . 7 (𝑇 ∈ (0(,)1) β†’ 𝑇 ∈ ℝ)
53, 4syl 17 . . . . . 6 (πœ‘ β†’ 𝑇 ∈ ℝ)
65, 1remulcld 11275 . . . . 5 (πœ‘ β†’ (𝑇 Β· 𝐴) ∈ ℝ)
7 1re 11245 . . . . . . 7 1 ∈ ℝ
8 resubcl 11555 . . . . . . 7 ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) β†’ (1 βˆ’ 𝑇) ∈ ℝ)
97, 5, 8sylancr 586 . . . . . 6 (πœ‘ β†’ (1 βˆ’ 𝑇) ∈ ℝ)
10 dvcvx.b . . . . . 6 (πœ‘ β†’ 𝐡 ∈ ℝ)
119, 10remulcld 11275 . . . . 5 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐡) ∈ ℝ)
126, 11readdcld 11274 . . . 4 (πœ‘ β†’ ((𝑇 Β· 𝐴) + ((1 βˆ’ 𝑇) Β· 𝐡)) ∈ ℝ)
132, 12eqeltrid 2833 . . 3 (πœ‘ β†’ 𝐢 ∈ ℝ)
14 1cnd 11240 . . . . . . . 8 (πœ‘ β†’ 1 ∈ β„‚)
155recnd 11273 . . . . . . . 8 (πœ‘ β†’ 𝑇 ∈ β„‚)
161recnd 11273 . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ β„‚)
1714, 15, 16subdird 11702 . . . . . . 7 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐴) = ((1 Β· 𝐴) βˆ’ (𝑇 Β· 𝐴)))
1816mullidd 11263 . . . . . . . 8 (πœ‘ β†’ (1 Β· 𝐴) = 𝐴)
1918oveq1d 7435 . . . . . . 7 (πœ‘ β†’ ((1 Β· 𝐴) βˆ’ (𝑇 Β· 𝐴)) = (𝐴 βˆ’ (𝑇 Β· 𝐴)))
2017, 19eqtrd 2768 . . . . . 6 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐴) = (𝐴 βˆ’ (𝑇 Β· 𝐴)))
21 dvcvx.l . . . . . . 7 (πœ‘ β†’ 𝐴 < 𝐡)
22 eliooord 13416 . . . . . . . . . . 11 (𝑇 ∈ (0(,)1) β†’ (0 < 𝑇 ∧ 𝑇 < 1))
233, 22syl 17 . . . . . . . . . 10 (πœ‘ β†’ (0 < 𝑇 ∧ 𝑇 < 1))
2423simprd 495 . . . . . . . . 9 (πœ‘ β†’ 𝑇 < 1)
25 posdif 11738 . . . . . . . . . 10 ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) β†’ (𝑇 < 1 ↔ 0 < (1 βˆ’ 𝑇)))
265, 7, 25sylancl 585 . . . . . . . . 9 (πœ‘ β†’ (𝑇 < 1 ↔ 0 < (1 βˆ’ 𝑇)))
2724, 26mpbid 231 . . . . . . . 8 (πœ‘ β†’ 0 < (1 βˆ’ 𝑇))
28 ltmul2 12096 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ ((1 βˆ’ 𝑇) ∈ ℝ ∧ 0 < (1 βˆ’ 𝑇))) β†’ (𝐴 < 𝐡 ↔ ((1 βˆ’ 𝑇) Β· 𝐴) < ((1 βˆ’ 𝑇) Β· 𝐡)))
291, 10, 9, 27, 28syl112anc 1372 . . . . . . 7 (πœ‘ β†’ (𝐴 < 𝐡 ↔ ((1 βˆ’ 𝑇) Β· 𝐴) < ((1 βˆ’ 𝑇) Β· 𝐡)))
3021, 29mpbid 231 . . . . . 6 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐴) < ((1 βˆ’ 𝑇) Β· 𝐡))
3120, 30eqbrtrrd 5172 . . . . 5 (πœ‘ β†’ (𝐴 βˆ’ (𝑇 Β· 𝐴)) < ((1 βˆ’ 𝑇) Β· 𝐡))
321, 6, 11ltsubadd2d 11843 . . . . 5 (πœ‘ β†’ ((𝐴 βˆ’ (𝑇 Β· 𝐴)) < ((1 βˆ’ 𝑇) Β· 𝐡) ↔ 𝐴 < ((𝑇 Β· 𝐴) + ((1 βˆ’ 𝑇) Β· 𝐡))))
3331, 32mpbid 231 . . . 4 (πœ‘ β†’ 𝐴 < ((𝑇 Β· 𝐴) + ((1 βˆ’ 𝑇) Β· 𝐡)))
3433, 2breqtrrdi 5190 . . 3 (πœ‘ β†’ 𝐴 < 𝐢)
351leidd 11811 . . . . 5 (πœ‘ β†’ 𝐴 ≀ 𝐴)
3610recnd 11273 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ∈ β„‚)
3714, 15, 36subdird 11702 . . . . . . . . . 10 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐡) = ((1 Β· 𝐡) βˆ’ (𝑇 Β· 𝐡)))
3836mullidd 11263 . . . . . . . . . . 11 (πœ‘ β†’ (1 Β· 𝐡) = 𝐡)
3938oveq1d 7435 . . . . . . . . . 10 (πœ‘ β†’ ((1 Β· 𝐡) βˆ’ (𝑇 Β· 𝐡)) = (𝐡 βˆ’ (𝑇 Β· 𝐡)))
4037, 39eqtrd 2768 . . . . . . . . 9 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐡) = (𝐡 βˆ’ (𝑇 Β· 𝐡)))
415, 10remulcld 11275 . . . . . . . . . 10 (πœ‘ β†’ (𝑇 Β· 𝐡) ∈ ℝ)
4223simpld 494 . . . . . . . . . . . 12 (πœ‘ β†’ 0 < 𝑇)
43 ltmul2 12096 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇)) β†’ (𝐴 < 𝐡 ↔ (𝑇 Β· 𝐴) < (𝑇 Β· 𝐡)))
441, 10, 5, 42, 43syl112anc 1372 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 < 𝐡 ↔ (𝑇 Β· 𝐴) < (𝑇 Β· 𝐡)))
4521, 44mpbid 231 . . . . . . . . . 10 (πœ‘ β†’ (𝑇 Β· 𝐴) < (𝑇 Β· 𝐡))
466, 41, 10, 45ltsub2dd 11858 . . . . . . . . 9 (πœ‘ β†’ (𝐡 βˆ’ (𝑇 Β· 𝐡)) < (𝐡 βˆ’ (𝑇 Β· 𝐴)))
4740, 46eqbrtrd 5170 . . . . . . . 8 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐡) < (𝐡 βˆ’ (𝑇 Β· 𝐴)))
486, 11, 10ltaddsub2d 11846 . . . . . . . 8 (πœ‘ β†’ (((𝑇 Β· 𝐴) + ((1 βˆ’ 𝑇) Β· 𝐡)) < 𝐡 ↔ ((1 βˆ’ 𝑇) Β· 𝐡) < (𝐡 βˆ’ (𝑇 Β· 𝐴))))
4947, 48mpbird 257 . . . . . . 7 (πœ‘ β†’ ((𝑇 Β· 𝐴) + ((1 βˆ’ 𝑇) Β· 𝐡)) < 𝐡)
502, 49eqbrtrid 5183 . . . . . 6 (πœ‘ β†’ 𝐢 < 𝐡)
5113, 10, 50ltled 11393 . . . . 5 (πœ‘ β†’ 𝐢 ≀ 𝐡)
52 iccss 13425 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) ∧ (𝐴 ≀ 𝐴 ∧ 𝐢 ≀ 𝐡)) β†’ (𝐴[,]𝐢) βŠ† (𝐴[,]𝐡))
531, 10, 35, 51, 52syl22anc 838 . . . 4 (πœ‘ β†’ (𝐴[,]𝐢) βŠ† (𝐴[,]𝐡))
54 dvcvx.f . . . 4 (πœ‘ β†’ 𝐹 ∈ ((𝐴[,]𝐡)–cn→ℝ))
55 rescncf 24830 . . . 4 ((𝐴[,]𝐢) βŠ† (𝐴[,]𝐡) β†’ (𝐹 ∈ ((𝐴[,]𝐡)–cn→ℝ) β†’ (𝐹 β†Ύ (𝐴[,]𝐢)) ∈ ((𝐴[,]𝐢)–cn→ℝ)))
5653, 54, 55sylc 65 . . 3 (πœ‘ β†’ (𝐹 β†Ύ (𝐴[,]𝐢)) ∈ ((𝐴[,]𝐢)–cn→ℝ))
57 ax-resscn 11196 . . . . . . . 8 ℝ βŠ† β„‚
5857a1i 11 . . . . . . 7 (πœ‘ β†’ ℝ βŠ† β„‚)
59 cncff 24826 . . . . . . . . 9 (𝐹 ∈ ((𝐴[,]𝐡)–cn→ℝ) β†’ 𝐹:(𝐴[,]𝐡)βŸΆβ„)
6054, 59syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐹:(𝐴[,]𝐡)βŸΆβ„)
61 fss 6739 . . . . . . . 8 ((𝐹:(𝐴[,]𝐡)βŸΆβ„ ∧ ℝ βŠ† β„‚) β†’ 𝐹:(𝐴[,]𝐡)βŸΆβ„‚)
6260, 57, 61sylancl 585 . . . . . . 7 (πœ‘ β†’ 𝐹:(𝐴[,]𝐡)βŸΆβ„‚)
63 iccssre 13439 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴[,]𝐡) βŠ† ℝ)
641, 10, 63syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† ℝ)
65 iccssre 13439 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ (𝐴[,]𝐢) βŠ† ℝ)
661, 13, 65syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝐴[,]𝐢) βŠ† ℝ)
67 eqid 2728 . . . . . . . 8 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
6867tgioo2 24732 . . . . . . . 8 (topGenβ€˜ran (,)) = ((TopOpenβ€˜β„‚fld) β†Ύt ℝ)
6967, 68dvres 25853 . . . . . . 7 (((ℝ βŠ† β„‚ ∧ 𝐹:(𝐴[,]𝐡)βŸΆβ„‚) ∧ ((𝐴[,]𝐡) βŠ† ℝ ∧ (𝐴[,]𝐢) βŠ† ℝ)) β†’ (ℝ D (𝐹 β†Ύ (𝐴[,]𝐢))) = ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴[,]𝐢))))
7058, 62, 64, 66, 69syl22anc 838 . . . . . 6 (πœ‘ β†’ (ℝ D (𝐹 β†Ύ (𝐴[,]𝐢))) = ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴[,]𝐢))))
71 iccntr 24750 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴[,]𝐢)) = (𝐴(,)𝐢))
721, 13, 71syl2anc 583 . . . . . . 7 (πœ‘ β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴[,]𝐢)) = (𝐴(,)𝐢))
7372reseq2d 5985 . . . . . 6 (πœ‘ β†’ ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴[,]𝐢))) = ((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢)))
7470, 73eqtrd 2768 . . . . 5 (πœ‘ β†’ (ℝ D (𝐹 β†Ύ (𝐴[,]𝐢))) = ((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢)))
7574dmeqd 5908 . . . 4 (πœ‘ β†’ dom (ℝ D (𝐹 β†Ύ (𝐴[,]𝐢))) = dom ((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢)))
76 dmres 6007 . . . . 5 dom ((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢)) = ((𝐴(,)𝐢) ∩ dom (ℝ D 𝐹))
7710rexrd 11295 . . . . . . . 8 (πœ‘ β†’ 𝐡 ∈ ℝ*)
78 iooss2 13393 . . . . . . . 8 ((𝐡 ∈ ℝ* ∧ 𝐢 ≀ 𝐡) β†’ (𝐴(,)𝐢) βŠ† (𝐴(,)𝐡))
7977, 51, 78syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝐴(,)𝐢) βŠ† (𝐴(,)𝐡))
80 dvcvx.d . . . . . . . 8 (πœ‘ β†’ (ℝ D 𝐹) Isom < , < ((𝐴(,)𝐡), π‘Š))
81 isof1o 7331 . . . . . . . 8 ((ℝ D 𝐹) Isom < , < ((𝐴(,)𝐡), π‘Š) β†’ (ℝ D 𝐹):(𝐴(,)𝐡)–1-1-ontoβ†’π‘Š)
82 f1odm 6843 . . . . . . . 8 ((ℝ D 𝐹):(𝐴(,)𝐡)–1-1-ontoβ†’π‘Š β†’ dom (ℝ D 𝐹) = (𝐴(,)𝐡))
8380, 81, 823syl 18 . . . . . . 7 (πœ‘ β†’ dom (ℝ D 𝐹) = (𝐴(,)𝐡))
8479, 83sseqtrrd 4021 . . . . . 6 (πœ‘ β†’ (𝐴(,)𝐢) βŠ† dom (ℝ D 𝐹))
85 df-ss 3964 . . . . . 6 ((𝐴(,)𝐢) βŠ† dom (ℝ D 𝐹) ↔ ((𝐴(,)𝐢) ∩ dom (ℝ D 𝐹)) = (𝐴(,)𝐢))
8684, 85sylib 217 . . . . 5 (πœ‘ β†’ ((𝐴(,)𝐢) ∩ dom (ℝ D 𝐹)) = (𝐴(,)𝐢))
8776, 86eqtrid 2780 . . . 4 (πœ‘ β†’ dom ((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢)) = (𝐴(,)𝐢))
8875, 87eqtrd 2768 . . 3 (πœ‘ β†’ dom (ℝ D (𝐹 β†Ύ (𝐴[,]𝐢))) = (𝐴(,)𝐢))
891, 13, 34, 56, 88mvth 25938 . 2 (πœ‘ β†’ βˆƒπ‘₯ ∈ (𝐴(,)𝐢)((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)))
901, 13, 34ltled 11393 . . . . 5 (πœ‘ β†’ 𝐴 ≀ 𝐢)
9110leidd 11811 . . . . 5 (πœ‘ β†’ 𝐡 ≀ 𝐡)
92 iccss 13425 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) ∧ (𝐴 ≀ 𝐢 ∧ 𝐡 ≀ 𝐡)) β†’ (𝐢[,]𝐡) βŠ† (𝐴[,]𝐡))
931, 10, 90, 91, 92syl22anc 838 . . . 4 (πœ‘ β†’ (𝐢[,]𝐡) βŠ† (𝐴[,]𝐡))
94 rescncf 24830 . . . 4 ((𝐢[,]𝐡) βŠ† (𝐴[,]𝐡) β†’ (𝐹 ∈ ((𝐴[,]𝐡)–cn→ℝ) β†’ (𝐹 β†Ύ (𝐢[,]𝐡)) ∈ ((𝐢[,]𝐡)–cn→ℝ)))
9593, 54, 94sylc 65 . . 3 (πœ‘ β†’ (𝐹 β†Ύ (𝐢[,]𝐡)) ∈ ((𝐢[,]𝐡)–cn→ℝ))
96 iccssre 13439 . . . . . . . 8 ((𝐢 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐢[,]𝐡) βŠ† ℝ)
9713, 10, 96syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝐢[,]𝐡) βŠ† ℝ)
9867, 68dvres 25853 . . . . . . 7 (((ℝ βŠ† β„‚ ∧ 𝐹:(𝐴[,]𝐡)βŸΆβ„‚) ∧ ((𝐴[,]𝐡) βŠ† ℝ ∧ (𝐢[,]𝐡) βŠ† ℝ)) β†’ (ℝ D (𝐹 β†Ύ (𝐢[,]𝐡))) = ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐢[,]𝐡))))
9958, 62, 64, 97, 98syl22anc 838 . . . . . 6 (πœ‘ β†’ (ℝ D (𝐹 β†Ύ (𝐢[,]𝐡))) = ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐢[,]𝐡))))
100 iccntr 24750 . . . . . . . 8 ((𝐢 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐢[,]𝐡)) = (𝐢(,)𝐡))
10113, 10, 100syl2anc 583 . . . . . . 7 (πœ‘ β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐢[,]𝐡)) = (𝐢(,)𝐡))
102101reseq2d 5985 . . . . . 6 (πœ‘ β†’ ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐢[,]𝐡))) = ((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡)))
10399, 102eqtrd 2768 . . . . 5 (πœ‘ β†’ (ℝ D (𝐹 β†Ύ (𝐢[,]𝐡))) = ((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡)))
104103dmeqd 5908 . . . 4 (πœ‘ β†’ dom (ℝ D (𝐹 β†Ύ (𝐢[,]𝐡))) = dom ((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡)))
105 dmres 6007 . . . . 5 dom ((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡)) = ((𝐢(,)𝐡) ∩ dom (ℝ D 𝐹))
1061rexrd 11295 . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ ℝ*)
107 iooss1 13392 . . . . . . . 8 ((𝐴 ∈ ℝ* ∧ 𝐴 ≀ 𝐢) β†’ (𝐢(,)𝐡) βŠ† (𝐴(,)𝐡))
108106, 90, 107syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝐢(,)𝐡) βŠ† (𝐴(,)𝐡))
109108, 83sseqtrrd 4021 . . . . . 6 (πœ‘ β†’ (𝐢(,)𝐡) βŠ† dom (ℝ D 𝐹))
110 df-ss 3964 . . . . . 6 ((𝐢(,)𝐡) βŠ† dom (ℝ D 𝐹) ↔ ((𝐢(,)𝐡) ∩ dom (ℝ D 𝐹)) = (𝐢(,)𝐡))
111109, 110sylib 217 . . . . 5 (πœ‘ β†’ ((𝐢(,)𝐡) ∩ dom (ℝ D 𝐹)) = (𝐢(,)𝐡))
112105, 111eqtrid 2780 . . . 4 (πœ‘ β†’ dom ((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡)) = (𝐢(,)𝐡))
113104, 112eqtrd 2768 . . 3 (πœ‘ β†’ dom (ℝ D (𝐹 β†Ύ (𝐢[,]𝐡))) = (𝐢(,)𝐡))
11413, 10, 50, 95, 113mvth 25938 . 2 (πœ‘ β†’ βˆƒπ‘¦ ∈ (𝐢(,)𝐡)((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢)))
115 reeanv 3223 . . 3 (βˆƒπ‘₯ ∈ (𝐴(,)𝐢)βˆƒπ‘¦ ∈ (𝐢(,)𝐡)(((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ ((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢))) ↔ (βˆƒπ‘₯ ∈ (𝐴(,)𝐢)((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ βˆƒπ‘¦ ∈ (𝐢(,)𝐡)((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢))))
11674fveq1d 6899 . . . . . . . 8 (πœ‘ β†’ ((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = (((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢))β€˜π‘₯))
117 fvres 6916 . . . . . . . . 9 (π‘₯ ∈ (𝐴(,)𝐢) β†’ (((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢))β€˜π‘₯) = ((ℝ D 𝐹)β€˜π‘₯))
118117adantr 480 . . . . . . . 8 ((π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡)) β†’ (((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢))β€˜π‘₯) = ((ℝ D 𝐹)β€˜π‘₯))
119116, 118sylan9eq 2788 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((ℝ D 𝐹)β€˜π‘₯))
12013rexrd 11295 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐢 ∈ ℝ*)
121 ubicc2 13475 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ* ∧ 𝐢 ∈ ℝ* ∧ 𝐴 ≀ 𝐢) β†’ 𝐢 ∈ (𝐴[,]𝐢))
122106, 120, 90, 121syl3anc 1369 . . . . . . . . . . 11 (πœ‘ β†’ 𝐢 ∈ (𝐴[,]𝐢))
123122fvresd 6917 . . . . . . . . . 10 (πœ‘ β†’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) = (πΉβ€˜πΆ))
124 lbicc2 13474 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ* ∧ 𝐢 ∈ ℝ* ∧ 𝐴 ≀ 𝐢) β†’ 𝐴 ∈ (𝐴[,]𝐢))
125106, 120, 90, 124syl3anc 1369 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ (𝐴[,]𝐢))
126125fvresd 6917 . . . . . . . . . 10 (πœ‘ β†’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄) = (πΉβ€˜π΄))
127123, 126oveq12d 7438 . . . . . . . . 9 (πœ‘ β†’ (((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) = ((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)))
128127oveq1d 7435 . . . . . . . 8 (πœ‘ β†’ ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)))
129128adantr 480 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)))
130119, 129eqeq12d 2744 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ (((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) ↔ ((ℝ D 𝐹)β€˜π‘₯) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴))))
131103fveq1d 6899 . . . . . . . 8 (πœ‘ β†’ ((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = (((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡))β€˜π‘¦))
132 fvres 6916 . . . . . . . . 9 (𝑦 ∈ (𝐢(,)𝐡) β†’ (((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡))β€˜π‘¦) = ((ℝ D 𝐹)β€˜π‘¦))
133132adantl 481 . . . . . . . 8 ((π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡)) β†’ (((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡))β€˜π‘¦) = ((ℝ D 𝐹)β€˜π‘¦))
134131, 133sylan9eq 2788 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((ℝ D 𝐹)β€˜π‘¦))
135 ubicc2 13475 . . . . . . . . . . . 12 ((𝐢 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝐢 ≀ 𝐡) β†’ 𝐡 ∈ (𝐢[,]𝐡))
136120, 77, 51, 135syl3anc 1369 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ∈ (𝐢[,]𝐡))
137136fvresd 6917 . . . . . . . . . 10 (πœ‘ β†’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) = (πΉβ€˜π΅))
138 lbicc2 13474 . . . . . . . . . . . 12 ((𝐢 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝐢 ≀ 𝐡) β†’ 𝐢 ∈ (𝐢[,]𝐡))
139120, 77, 51, 138syl3anc 1369 . . . . . . . . . . 11 (πœ‘ β†’ 𝐢 ∈ (𝐢[,]𝐡))
140139fvresd 6917 . . . . . . . . . 10 (πœ‘ β†’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ) = (πΉβ€˜πΆ))
141137, 140oveq12d 7438 . . . . . . . . 9 (πœ‘ β†’ (((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) = ((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)))
142141oveq1d 7435 . . . . . . . 8 (πœ‘ β†’ ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢)) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢)))
143142adantr 480 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢)) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢)))
144134, 143eqeq12d 2744 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ (((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢)) ↔ ((ℝ D 𝐹)β€˜π‘¦) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢))))
145130, 144anbi12d 631 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ ((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢))) ↔ (((ℝ D 𝐹)β€˜π‘₯) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ ((ℝ D 𝐹)β€˜π‘¦) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢)))))
146 elioore 13387 . . . . . . . . . 10 (π‘₯ ∈ (𝐴(,)𝐢) β†’ π‘₯ ∈ ℝ)
147146ad2antrl 727 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ π‘₯ ∈ ℝ)
14813adantr 480 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ 𝐢 ∈ ℝ)
149 elioore 13387 . . . . . . . . . 10 (𝑦 ∈ (𝐢(,)𝐡) β†’ 𝑦 ∈ ℝ)
150149ad2antll 728 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ 𝑦 ∈ ℝ)
151 eliooord 13416 . . . . . . . . . . 11 (π‘₯ ∈ (𝐴(,)𝐢) β†’ (𝐴 < π‘₯ ∧ π‘₯ < 𝐢))
152151ad2antrl 727 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ (𝐴 < π‘₯ ∧ π‘₯ < 𝐢))
153152simprd 495 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ π‘₯ < 𝐢)
154 eliooord 13416 . . . . . . . . . . 11 (𝑦 ∈ (𝐢(,)𝐡) β†’ (𝐢 < 𝑦 ∧ 𝑦 < 𝐡))
155154ad2antll 728 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ (𝐢 < 𝑦 ∧ 𝑦 < 𝐡))
156155simpld 494 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ 𝐢 < 𝑦)
157147, 148, 150, 153, 156lttrd 11406 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ π‘₯ < 𝑦)
15880adantr 480 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ (ℝ D 𝐹) Isom < , < ((𝐴(,)𝐡), π‘Š))
15979sselda 3980 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐢)) β†’ π‘₯ ∈ (𝐴(,)𝐡))
160159adantrr 716 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ π‘₯ ∈ (𝐴(,)𝐡))
161108sselda 3980 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ (𝐢(,)𝐡)) β†’ 𝑦 ∈ (𝐴(,)𝐡))
162161adantrl 715 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ 𝑦 ∈ (𝐴(,)𝐡))
163 isorel 7334 . . . . . . . . 9 (((ℝ D 𝐹) Isom < , < ((𝐴(,)𝐡), π‘Š) ∧ (π‘₯ ∈ (𝐴(,)𝐡) ∧ 𝑦 ∈ (𝐴(,)𝐡))) β†’ (π‘₯ < 𝑦 ↔ ((ℝ D 𝐹)β€˜π‘₯) < ((ℝ D 𝐹)β€˜π‘¦)))
164158, 160, 162, 163syl12anc 836 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ (π‘₯ < 𝑦 ↔ ((ℝ D 𝐹)β€˜π‘₯) < ((ℝ D 𝐹)β€˜π‘¦)))
165157, 164mpbid 231 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((ℝ D 𝐹)β€˜π‘₯) < ((ℝ D 𝐹)β€˜π‘¦))
166 breq12 5153 . . . . . . 7 ((((ℝ D 𝐹)β€˜π‘₯) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ ((ℝ D 𝐹)β€˜π‘¦) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢))) β†’ (((ℝ D 𝐹)β€˜π‘₯) < ((ℝ D 𝐹)β€˜π‘¦) ↔ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢))))
167165, 166syl5ibcom 244 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((((ℝ D 𝐹)β€˜π‘₯) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ ((ℝ D 𝐹)β€˜π‘¦) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢))) β†’ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢))))
16853, 122sseldd 3981 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐢 ∈ (𝐴[,]𝐡))
16960, 168ffvelcdmd 7095 . . . . . . . . . . 11 (πœ‘ β†’ (πΉβ€˜πΆ) ∈ ℝ)
17053, 125sseldd 3981 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 ∈ (𝐴[,]𝐡))
17160, 170ffvelcdmd 7095 . . . . . . . . . . 11 (πœ‘ β†’ (πΉβ€˜π΄) ∈ ℝ)
172169, 171resubcld 11673 . . . . . . . . . 10 (πœ‘ β†’ ((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) ∈ ℝ)
17327gt0ne0d 11809 . . . . . . . . . 10 (πœ‘ β†’ (1 βˆ’ 𝑇) β‰  0)
174172, 9, 173redivcld 12073 . . . . . . . . 9 (πœ‘ β†’ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) ∈ ℝ)
17593, 136sseldd 3981 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ (𝐴[,]𝐡))
17660, 175ffvelcdmd 7095 . . . . . . . . . . 11 (πœ‘ β†’ (πΉβ€˜π΅) ∈ ℝ)
177176, 169resubcld 11673 . . . . . . . . . 10 (πœ‘ β†’ ((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) ∈ ℝ)
17842gt0ne0d 11809 . . . . . . . . . 10 (πœ‘ β†’ 𝑇 β‰  0)
179177, 5, 178redivcld 12073 . . . . . . . . 9 (πœ‘ β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) ∈ ℝ)
18010, 1resubcld 11673 . . . . . . . . 9 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ∈ ℝ)
1811, 10posdifd 11832 . . . . . . . . . 10 (πœ‘ β†’ (𝐴 < 𝐡 ↔ 0 < (𝐡 βˆ’ 𝐴)))
18221, 181mpbid 231 . . . . . . . . 9 (πœ‘ β†’ 0 < (𝐡 βˆ’ 𝐴))
183 ltdiv1 12109 . . . . . . . . 9 (((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) ∈ ℝ ∧ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) ∈ ℝ ∧ ((𝐡 βˆ’ 𝐴) ∈ ℝ ∧ 0 < (𝐡 βˆ’ 𝐴))) β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) ↔ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) / (𝐡 βˆ’ 𝐴)) < ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) / (𝐡 βˆ’ 𝐴))))
184174, 179, 180, 182, 183syl112anc 1372 . . . . . . . 8 (πœ‘ β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) ↔ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) / (𝐡 βˆ’ 𝐴)) < ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) / (𝐡 βˆ’ 𝐴))))
185172recnd 11273 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) ∈ β„‚)
186185, 15mulcomd 11266 . . . . . . . . . . 11 (πœ‘ β†’ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) Β· 𝑇) = (𝑇 Β· ((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄))))
187169recnd 11273 . . . . . . . . . . . 12 (πœ‘ β†’ (πΉβ€˜πΆ) ∈ β„‚)
188171recnd 11273 . . . . . . . . . . . 12 (πœ‘ β†’ (πΉβ€˜π΄) ∈ β„‚)
18915, 187, 188subdid 11701 . . . . . . . . . . 11 (πœ‘ β†’ (𝑇 Β· ((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄))) = ((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))))
190186, 189eqtrd 2768 . . . . . . . . . 10 (πœ‘ β†’ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) Β· 𝑇) = ((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))))
191177recnd 11273 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) ∈ β„‚)
1929recnd 11273 . . . . . . . . . . . 12 (πœ‘ β†’ (1 βˆ’ 𝑇) ∈ β„‚)
193191, 192mulcomd 11266 . . . . . . . . . . 11 (πœ‘ β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) Β· (1 βˆ’ 𝑇)) = ((1 βˆ’ 𝑇) Β· ((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ))))
194176recnd 11273 . . . . . . . . . . . 12 (πœ‘ β†’ (πΉβ€˜π΅) ∈ β„‚)
195192, 194, 187subdid 11701 . . . . . . . . . . 11 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· ((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ))) = (((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) βˆ’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))))
196193, 195eqtrd 2768 . . . . . . . . . 10 (πœ‘ β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) Β· (1 βˆ’ 𝑇)) = (((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) βˆ’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))))
197190, 196breq12d 5161 . . . . . . . . 9 (πœ‘ β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) Β· 𝑇) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) Β· (1 βˆ’ 𝑇)) ↔ ((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) < (((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) βˆ’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ)))))
1985, 42jca 511 . . . . . . . . . 10 (πœ‘ β†’ (𝑇 ∈ ℝ ∧ 0 < 𝑇))
1999, 27jca 511 . . . . . . . . . 10 (πœ‘ β†’ ((1 βˆ’ 𝑇) ∈ ℝ ∧ 0 < (1 βˆ’ 𝑇)))
200 lt2mul2div 12123 . . . . . . . . . 10 (((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) ∈ ℝ ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇)) ∧ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) ∈ ℝ ∧ ((1 βˆ’ 𝑇) ∈ ℝ ∧ 0 < (1 βˆ’ 𝑇)))) β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) Β· 𝑇) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) Β· (1 βˆ’ 𝑇)) ↔ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇)))
201172, 198, 177, 199, 200syl22anc 838 . . . . . . . . 9 (πœ‘ β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) Β· 𝑇) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) Β· (1 βˆ’ 𝑇)) ↔ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇)))
2025, 169remulcld 11275 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑇 Β· (πΉβ€˜πΆ)) ∈ ℝ)
203202recnd 11273 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑇 Β· (πΉβ€˜πΆ)) ∈ β„‚)
2049, 169remulcld 11275 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ)) ∈ ℝ)
205204recnd 11273 . . . . . . . . . . . . 13 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ)) ∈ β„‚)
2065, 171remulcld 11275 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑇 Β· (πΉβ€˜π΄)) ∈ ℝ)
207206recnd 11273 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑇 Β· (πΉβ€˜π΄)) ∈ β„‚)
208203, 205, 207addsubd 11623 . . . . . . . . . . . 12 (πœ‘ β†’ (((𝑇 Β· (πΉβ€˜πΆ)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) = (((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))))
209 ax-1cn 11197 . . . . . . . . . . . . . . . 16 1 ∈ β„‚
210 pncan3 11499 . . . . . . . . . . . . . . . 16 ((𝑇 ∈ β„‚ ∧ 1 ∈ β„‚) β†’ (𝑇 + (1 βˆ’ 𝑇)) = 1)
21115, 209, 210sylancl 585 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑇 + (1 βˆ’ 𝑇)) = 1)
212211oveq1d 7435 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑇 + (1 βˆ’ 𝑇)) Β· (πΉβ€˜πΆ)) = (1 Β· (πΉβ€˜πΆ)))
21315, 192, 187adddird 11270 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑇 + (1 βˆ’ 𝑇)) Β· (πΉβ€˜πΆ)) = ((𝑇 Β· (πΉβ€˜πΆ)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))))
214187mullidd 11263 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1 Β· (πΉβ€˜πΆ)) = (πΉβ€˜πΆ))
215212, 213, 2143eqtr3d 2776 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝑇 Β· (πΉβ€˜πΆ)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))) = (πΉβ€˜πΆ))
216215oveq1d 7435 . . . . . . . . . . . 12 (πœ‘ β†’ (((𝑇 Β· (πΉβ€˜πΆ)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) = ((πΉβ€˜πΆ) βˆ’ (𝑇 Β· (πΉβ€˜π΄))))
217208, 216eqtr3d 2770 . . . . . . . . . . 11 (πœ‘ β†’ (((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))) = ((πΉβ€˜πΆ) βˆ’ (𝑇 Β· (πΉβ€˜π΄))))
218217breq1d 5158 . . . . . . . . . 10 (πœ‘ β†’ ((((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))) < ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) ↔ ((πΉβ€˜πΆ) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) < ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅))))
219202, 206resubcld 11673 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) ∈ ℝ)
2209, 176remulcld 11275 . . . . . . . . . . 11 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) ∈ ℝ)
221219, 204, 220ltaddsubd 11845 . . . . . . . . . 10 (πœ‘ β†’ ((((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))) < ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) ↔ ((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) < (((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) βˆ’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ)))))
222169, 206, 220ltsubadd2d 11843 . . . . . . . . . 10 (πœ‘ β†’ (((πΉβ€˜πΆ) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) < ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) ↔ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)))))
223218, 221, 2223bitr3d 309 . . . . . . . . 9 (πœ‘ β†’ (((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) < (((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) βˆ’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))) ↔ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)))))
224197, 201, 2233bitr3d 309 . . . . . . . 8 (πœ‘ β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) ↔ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)))))
225180recnd 11273 . . . . . . . . . . 11 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ∈ β„‚)
226182gt0ne0d 11809 . . . . . . . . . . 11 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) β‰  0)
227185, 192, 225, 173, 226divdiv1d 12052 . . . . . . . . . 10 (πœ‘ β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) / (𝐡 βˆ’ 𝐴)) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / ((1 βˆ’ 𝑇) Β· (𝐡 βˆ’ 𝐴))))
22820oveq2d 7436 . . . . . . . . . . . . 13 (πœ‘ β†’ (((1 βˆ’ 𝑇) Β· 𝐡) βˆ’ ((1 βˆ’ 𝑇) Β· 𝐴)) = (((1 βˆ’ 𝑇) Β· 𝐡) βˆ’ (𝐴 βˆ’ (𝑇 Β· 𝐴))))
22911recnd 11273 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐡) ∈ β„‚)
2306recnd 11273 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑇 Β· 𝐴) ∈ β„‚)
231229, 16, 230subsub3d 11632 . . . . . . . . . . . . 13 (πœ‘ β†’ (((1 βˆ’ 𝑇) Β· 𝐡) βˆ’ (𝐴 βˆ’ (𝑇 Β· 𝐴))) = ((((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴)) βˆ’ 𝐴))
232228, 231eqtrd 2768 . . . . . . . . . . . 12 (πœ‘ β†’ (((1 βˆ’ 𝑇) Β· 𝐡) βˆ’ ((1 βˆ’ 𝑇) Β· 𝐴)) = ((((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴)) βˆ’ 𝐴))
233192, 36, 16subdid 11701 . . . . . . . . . . . 12 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· (𝐡 βˆ’ 𝐴)) = (((1 βˆ’ 𝑇) Β· 𝐡) βˆ’ ((1 βˆ’ 𝑇) Β· 𝐴)))
234230, 229addcomd 11447 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑇 Β· 𝐴) + ((1 βˆ’ 𝑇) Β· 𝐡)) = (((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴)))
2352, 234eqtrid 2780 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐢 = (((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴)))
236235oveq1d 7435 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐢 βˆ’ 𝐴) = ((((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴)) βˆ’ 𝐴))
237232, 233, 2363eqtr4d 2778 . . . . . . . . . . 11 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· (𝐡 βˆ’ 𝐴)) = (𝐢 βˆ’ 𝐴))
238237oveq2d 7436 . . . . . . . . . 10 (πœ‘ β†’ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / ((1 βˆ’ 𝑇) Β· (𝐡 βˆ’ 𝐴))) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)))
239227, 238eqtrd 2768 . . . . . . . . 9 (πœ‘ β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) / (𝐡 βˆ’ 𝐴)) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)))
240191, 15, 225, 178, 226divdiv1d 12052 . . . . . . . . . 10 (πœ‘ β†’ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) / (𝐡 βˆ’ 𝐴)) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝑇 Β· (𝐡 βˆ’ 𝐴))))
24136, 229, 230subsub4d 11633 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐡 βˆ’ ((1 βˆ’ 𝑇) Β· 𝐡)) βˆ’ (𝑇 Β· 𝐴)) = (𝐡 βˆ’ (((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴))))
24240oveq2d 7436 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐡 βˆ’ ((1 βˆ’ 𝑇) Β· 𝐡)) = (𝐡 βˆ’ (𝐡 βˆ’ (𝑇 Β· 𝐡))))
24341recnd 11273 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑇 Β· 𝐡) ∈ β„‚)
24436, 243nncand 11607 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐡 βˆ’ (𝐡 βˆ’ (𝑇 Β· 𝐡))) = (𝑇 Β· 𝐡))
245242, 244eqtrd 2768 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐡 βˆ’ ((1 βˆ’ 𝑇) Β· 𝐡)) = (𝑇 Β· 𝐡))
246245oveq1d 7435 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐡 βˆ’ ((1 βˆ’ 𝑇) Β· 𝐡)) βˆ’ (𝑇 Β· 𝐴)) = ((𝑇 Β· 𝐡) βˆ’ (𝑇 Β· 𝐴)))
247241, 246eqtr3d 2770 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐡 βˆ’ (((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴))) = ((𝑇 Β· 𝐡) βˆ’ (𝑇 Β· 𝐴)))
248235oveq2d 7436 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐡 βˆ’ 𝐢) = (𝐡 βˆ’ (((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴))))
24915, 36, 16subdid 11701 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑇 Β· (𝐡 βˆ’ 𝐴)) = ((𝑇 Β· 𝐡) βˆ’ (𝑇 Β· 𝐴)))
250247, 248, 2493eqtr4d 2778 . . . . . . . . . . 11 (πœ‘ β†’ (𝐡 βˆ’ 𝐢) = (𝑇 Β· (𝐡 βˆ’ 𝐴)))
251250oveq2d 7436 . . . . . . . . . 10 (πœ‘ β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢)) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝑇 Β· (𝐡 βˆ’ 𝐴))))
252240, 251eqtr4d 2771 . . . . . . . . 9 (πœ‘ β†’ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) / (𝐡 βˆ’ 𝐴)) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢)))
253239, 252breq12d 5161 . . . . . . . 8 (πœ‘ β†’ (((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) / (𝐡 βˆ’ 𝐴)) < ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) / (𝐡 βˆ’ 𝐴)) ↔ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢))))
254184, 224, 2533bitr3rd 310 . . . . . . 7 (πœ‘ β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢)) ↔ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)))))
255254adantr 480 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢)) ↔ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)))))
256167, 255sylibd 238 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((((ℝ D 𝐹)β€˜π‘₯) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ ((ℝ D 𝐹)β€˜π‘¦) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢))) β†’ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)))))
257145, 256sylbid 239 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ ((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢))) β†’ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)))))
258257rexlimdvva 3208 . . 3 (πœ‘ β†’ (βˆƒπ‘₯ ∈ (𝐴(,)𝐢)βˆƒπ‘¦ ∈ (𝐢(,)𝐡)(((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ ((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢))) β†’ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)))))
259115, 258biimtrrid 242 . 2 (πœ‘ β†’ ((βˆƒπ‘₯ ∈ (𝐴(,)𝐢)((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ βˆƒπ‘¦ ∈ (𝐢(,)𝐡)((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢))) β†’ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)))))
26089, 114, 259mp2and 698 1 (πœ‘ β†’ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ∈ wcel 2099  βˆƒwrex 3067   ∩ cin 3946   βŠ† wss 3947   class class class wbr 5148  dom cdm 5678  ran crn 5679   β†Ύ cres 5680  βŸΆwf 6544  β€“1-1-ontoβ†’wf1o 6547  β€˜cfv 6548   Isom wiso 6549  (class class class)co 7420  β„‚cc 11137  β„cr 11138  0cc0 11139  1c1 11140   + caddc 11142   Β· cmul 11144  β„*cxr 11278   < clt 11279   ≀ cle 11280   βˆ’ cmin 11475   / cdiv 11902  (,)cioo 13357  [,]cicc 13360  TopOpenctopn 17403  topGenctg 17419  β„‚fldccnfld 21279  intcnt 22934  β€“cnβ†’ccncf 24809   D cdv 25805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-cnex 11195  ax-resscn 11196  ax-1cn 11197  ax-icn 11198  ax-addcl 11199  ax-addrcl 11200  ax-mulcl 11201  ax-mulrcl 11202  ax-mulcom 11203  ax-addass 11204  ax-mulass 11205  ax-distr 11206  ax-i2m1 11207  ax-1ne0 11208  ax-1rid 11209  ax-rnegex 11210  ax-rrecex 11211  ax-cnre 11212  ax-pre-lttri 11213  ax-pre-lttrn 11214  ax-pre-ltadd 11215  ax-pre-mulgt0 11216  ax-pre-sup 11217  ax-addf 11218
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-isom 6557  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7685  df-om 7871  df-1st 7993  df-2nd 7994  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-er 8725  df-map 8847  df-pm 8848  df-ixp 8917  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9387  df-fi 9435  df-sup 9466  df-inf 9467  df-oi 9534  df-card 9963  df-pnf 11281  df-mnf 11282  df-xr 11283  df-ltxr 11284  df-le 11285  df-sub 11477  df-neg 11478  df-div 11903  df-nn 12244  df-2 12306  df-3 12307  df-4 12308  df-5 12309  df-6 12310  df-7 12311  df-8 12312  df-9 12313  df-n0 12504  df-z 12590  df-dec 12709  df-uz 12854  df-q 12964  df-rp 13008  df-xneg 13125  df-xadd 13126  df-xmul 13127  df-ioo 13361  df-ico 13363  df-icc 13364  df-fz 13518  df-fzo 13661  df-seq 14000  df-exp 14060  df-hash 14323  df-cj 15079  df-re 15080  df-im 15081  df-sqrt 15215  df-abs 15216  df-struct 17116  df-sets 17133  df-slot 17151  df-ndx 17163  df-base 17181  df-ress 17210  df-plusg 17246  df-mulr 17247  df-starv 17248  df-sca 17249  df-vsca 17250  df-ip 17251  df-tset 17252  df-ple 17253  df-ds 17255  df-unif 17256  df-hom 17257  df-cco 17258  df-rest 17404  df-topn 17405  df-0g 17423  df-gsum 17424  df-topgen 17425  df-pt 17426  df-prds 17429  df-xrs 17484  df-qtop 17489  df-imas 17490  df-xps 17492  df-mre 17566  df-mrc 17567  df-acs 17569  df-mgm 18600  df-sgrp 18679  df-mnd 18695  df-submnd 18741  df-mulg 19024  df-cntz 19268  df-cmn 19737  df-psmet 21271  df-xmet 21272  df-met 21273  df-bl 21274  df-mopn 21275  df-fbas 21276  df-fg 21277  df-cnfld 21280  df-top 22809  df-topon 22826  df-topsp 22848  df-bases 22862  df-cld 22936  df-ntr 22937  df-cls 22938  df-nei 23015  df-lp 23053  df-perf 23054  df-cn 23144  df-cnp 23145  df-haus 23232  df-cmp 23304  df-tx 23479  df-hmeo 23672  df-fil 23763  df-fm 23855  df-flim 23856  df-flf 23857  df-xms 24239  df-ms 24240  df-tms 24241  df-cncf 24811  df-limc 25808  df-dv 25809
This theorem is referenced by:  efcvx  26399  logccv  26610
  Copyright terms: Public domain W3C validator