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

Theorem dvcvx 25897
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 13355 . . . . . . 7 (𝑇 ∈ (0(,)1) β†’ 𝑇 ∈ ℝ)
53, 4syl 17 . . . . . 6 (πœ‘ β†’ 𝑇 ∈ ℝ)
65, 1remulcld 11243 . . . . 5 (πœ‘ β†’ (𝑇 Β· 𝐴) ∈ ℝ)
7 1re 11213 . . . . . . 7 1 ∈ ℝ
8 resubcl 11523 . . . . . . 7 ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) β†’ (1 βˆ’ 𝑇) ∈ ℝ)
97, 5, 8sylancr 586 . . . . . 6 (πœ‘ β†’ (1 βˆ’ 𝑇) ∈ ℝ)
10 dvcvx.b . . . . . 6 (πœ‘ β†’ 𝐡 ∈ ℝ)
119, 10remulcld 11243 . . . . 5 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐡) ∈ ℝ)
126, 11readdcld 11242 . . . 4 (πœ‘ β†’ ((𝑇 Β· 𝐴) + ((1 βˆ’ 𝑇) Β· 𝐡)) ∈ ℝ)
132, 12eqeltrid 2829 . . 3 (πœ‘ β†’ 𝐢 ∈ ℝ)
14 1cnd 11208 . . . . . . . 8 (πœ‘ β†’ 1 ∈ β„‚)
155recnd 11241 . . . . . . . 8 (πœ‘ β†’ 𝑇 ∈ β„‚)
161recnd 11241 . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ β„‚)
1714, 15, 16subdird 11670 . . . . . . 7 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐴) = ((1 Β· 𝐴) βˆ’ (𝑇 Β· 𝐴)))
1816mullidd 11231 . . . . . . . 8 (πœ‘ β†’ (1 Β· 𝐴) = 𝐴)
1918oveq1d 7417 . . . . . . 7 (πœ‘ β†’ ((1 Β· 𝐴) βˆ’ (𝑇 Β· 𝐴)) = (𝐴 βˆ’ (𝑇 Β· 𝐴)))
2017, 19eqtrd 2764 . . . . . 6 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐴) = (𝐴 βˆ’ (𝑇 Β· 𝐴)))
21 dvcvx.l . . . . . . 7 (πœ‘ β†’ 𝐴 < 𝐡)
22 eliooord 13384 . . . . . . . . . . 11 (𝑇 ∈ (0(,)1) β†’ (0 < 𝑇 ∧ 𝑇 < 1))
233, 22syl 17 . . . . . . . . . 10 (πœ‘ β†’ (0 < 𝑇 ∧ 𝑇 < 1))
2423simprd 495 . . . . . . . . 9 (πœ‘ β†’ 𝑇 < 1)
25 posdif 11706 . . . . . . . . . 10 ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) β†’ (𝑇 < 1 ↔ 0 < (1 βˆ’ 𝑇)))
265, 7, 25sylancl 585 . . . . . . . . 9 (πœ‘ β†’ (𝑇 < 1 ↔ 0 < (1 βˆ’ 𝑇)))
2724, 26mpbid 231 . . . . . . . 8 (πœ‘ β†’ 0 < (1 βˆ’ 𝑇))
28 ltmul2 12064 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ ((1 βˆ’ 𝑇) ∈ ℝ ∧ 0 < (1 βˆ’ 𝑇))) β†’ (𝐴 < 𝐡 ↔ ((1 βˆ’ 𝑇) Β· 𝐴) < ((1 βˆ’ 𝑇) Β· 𝐡)))
291, 10, 9, 27, 28syl112anc 1371 . . . . . . 7 (πœ‘ β†’ (𝐴 < 𝐡 ↔ ((1 βˆ’ 𝑇) Β· 𝐴) < ((1 βˆ’ 𝑇) Β· 𝐡)))
3021, 29mpbid 231 . . . . . 6 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐴) < ((1 βˆ’ 𝑇) Β· 𝐡))
3120, 30eqbrtrrd 5163 . . . . 5 (πœ‘ β†’ (𝐴 βˆ’ (𝑇 Β· 𝐴)) < ((1 βˆ’ 𝑇) Β· 𝐡))
321, 6, 11ltsubadd2d 11811 . . . . 5 (πœ‘ β†’ ((𝐴 βˆ’ (𝑇 Β· 𝐴)) < ((1 βˆ’ 𝑇) Β· 𝐡) ↔ 𝐴 < ((𝑇 Β· 𝐴) + ((1 βˆ’ 𝑇) Β· 𝐡))))
3331, 32mpbid 231 . . . 4 (πœ‘ β†’ 𝐴 < ((𝑇 Β· 𝐴) + ((1 βˆ’ 𝑇) Β· 𝐡)))
3433, 2breqtrrdi 5181 . . 3 (πœ‘ β†’ 𝐴 < 𝐢)
351leidd 11779 . . . . 5 (πœ‘ β†’ 𝐴 ≀ 𝐴)
3610recnd 11241 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ∈ β„‚)
3714, 15, 36subdird 11670 . . . . . . . . . 10 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐡) = ((1 Β· 𝐡) βˆ’ (𝑇 Β· 𝐡)))
3836mullidd 11231 . . . . . . . . . . 11 (πœ‘ β†’ (1 Β· 𝐡) = 𝐡)
3938oveq1d 7417 . . . . . . . . . 10 (πœ‘ β†’ ((1 Β· 𝐡) βˆ’ (𝑇 Β· 𝐡)) = (𝐡 βˆ’ (𝑇 Β· 𝐡)))
4037, 39eqtrd 2764 . . . . . . . . 9 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐡) = (𝐡 βˆ’ (𝑇 Β· 𝐡)))
415, 10remulcld 11243 . . . . . . . . . 10 (πœ‘ β†’ (𝑇 Β· 𝐡) ∈ ℝ)
4223simpld 494 . . . . . . . . . . . 12 (πœ‘ β†’ 0 < 𝑇)
43 ltmul2 12064 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇)) β†’ (𝐴 < 𝐡 ↔ (𝑇 Β· 𝐴) < (𝑇 Β· 𝐡)))
441, 10, 5, 42, 43syl112anc 1371 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 < 𝐡 ↔ (𝑇 Β· 𝐴) < (𝑇 Β· 𝐡)))
4521, 44mpbid 231 . . . . . . . . . 10 (πœ‘ β†’ (𝑇 Β· 𝐴) < (𝑇 Β· 𝐡))
466, 41, 10, 45ltsub2dd 11826 . . . . . . . . 9 (πœ‘ β†’ (𝐡 βˆ’ (𝑇 Β· 𝐡)) < (𝐡 βˆ’ (𝑇 Β· 𝐴)))
4740, 46eqbrtrd 5161 . . . . . . . 8 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐡) < (𝐡 βˆ’ (𝑇 Β· 𝐴)))
486, 11, 10ltaddsub2d 11814 . . . . . . . 8 (πœ‘ β†’ (((𝑇 Β· 𝐴) + ((1 βˆ’ 𝑇) Β· 𝐡)) < 𝐡 ↔ ((1 βˆ’ 𝑇) Β· 𝐡) < (𝐡 βˆ’ (𝑇 Β· 𝐴))))
4947, 48mpbird 257 . . . . . . 7 (πœ‘ β†’ ((𝑇 Β· 𝐴) + ((1 βˆ’ 𝑇) Β· 𝐡)) < 𝐡)
502, 49eqbrtrid 5174 . . . . . 6 (πœ‘ β†’ 𝐢 < 𝐡)
5113, 10, 50ltled 11361 . . . . 5 (πœ‘ β†’ 𝐢 ≀ 𝐡)
52 iccss 13393 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) ∧ (𝐴 ≀ 𝐴 ∧ 𝐢 ≀ 𝐡)) β†’ (𝐴[,]𝐢) βŠ† (𝐴[,]𝐡))
531, 10, 35, 51, 52syl22anc 836 . . . 4 (πœ‘ β†’ (𝐴[,]𝐢) βŠ† (𝐴[,]𝐡))
54 dvcvx.f . . . 4 (πœ‘ β†’ 𝐹 ∈ ((𝐴[,]𝐡)–cn→ℝ))
55 rescncf 24761 . . . 4 ((𝐴[,]𝐢) βŠ† (𝐴[,]𝐡) β†’ (𝐹 ∈ ((𝐴[,]𝐡)–cn→ℝ) β†’ (𝐹 β†Ύ (𝐴[,]𝐢)) ∈ ((𝐴[,]𝐢)–cn→ℝ)))
5653, 54, 55sylc 65 . . 3 (πœ‘ β†’ (𝐹 β†Ύ (𝐴[,]𝐢)) ∈ ((𝐴[,]𝐢)–cn→ℝ))
57 ax-resscn 11164 . . . . . . . 8 ℝ βŠ† β„‚
5857a1i 11 . . . . . . 7 (πœ‘ β†’ ℝ βŠ† β„‚)
59 cncff 24757 . . . . . . . . 9 (𝐹 ∈ ((𝐴[,]𝐡)–cn→ℝ) β†’ 𝐹:(𝐴[,]𝐡)βŸΆβ„)
6054, 59syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐹:(𝐴[,]𝐡)βŸΆβ„)
61 fss 6725 . . . . . . . 8 ((𝐹:(𝐴[,]𝐡)βŸΆβ„ ∧ ℝ βŠ† β„‚) β†’ 𝐹:(𝐴[,]𝐡)βŸΆβ„‚)
6260, 57, 61sylancl 585 . . . . . . 7 (πœ‘ β†’ 𝐹:(𝐴[,]𝐡)βŸΆβ„‚)
63 iccssre 13407 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴[,]𝐡) βŠ† ℝ)
641, 10, 63syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† ℝ)
65 iccssre 13407 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ (𝐴[,]𝐢) βŠ† ℝ)
661, 13, 65syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝐴[,]𝐢) βŠ† ℝ)
67 eqid 2724 . . . . . . . 8 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
6867tgioo2 24663 . . . . . . . 8 (topGenβ€˜ran (,)) = ((TopOpenβ€˜β„‚fld) β†Ύt ℝ)
6967, 68dvres 25784 . . . . . . 7 (((ℝ βŠ† β„‚ ∧ 𝐹:(𝐴[,]𝐡)βŸΆβ„‚) ∧ ((𝐴[,]𝐡) βŠ† ℝ ∧ (𝐴[,]𝐢) βŠ† ℝ)) β†’ (ℝ D (𝐹 β†Ύ (𝐴[,]𝐢))) = ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴[,]𝐢))))
7058, 62, 64, 66, 69syl22anc 836 . . . . . 6 (πœ‘ β†’ (ℝ D (𝐹 β†Ύ (𝐴[,]𝐢))) = ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴[,]𝐢))))
71 iccntr 24681 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴[,]𝐢)) = (𝐴(,)𝐢))
721, 13, 71syl2anc 583 . . . . . . 7 (πœ‘ β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴[,]𝐢)) = (𝐴(,)𝐢))
7372reseq2d 5972 . . . . . 6 (πœ‘ β†’ ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴[,]𝐢))) = ((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢)))
7470, 73eqtrd 2764 . . . . 5 (πœ‘ β†’ (ℝ D (𝐹 β†Ύ (𝐴[,]𝐢))) = ((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢)))
7574dmeqd 5896 . . . 4 (πœ‘ β†’ dom (ℝ D (𝐹 β†Ύ (𝐴[,]𝐢))) = dom ((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢)))
76 dmres 5994 . . . . 5 dom ((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢)) = ((𝐴(,)𝐢) ∩ dom (ℝ D 𝐹))
7710rexrd 11263 . . . . . . . 8 (πœ‘ β†’ 𝐡 ∈ ℝ*)
78 iooss2 13361 . . . . . . . 8 ((𝐡 ∈ ℝ* ∧ 𝐢 ≀ 𝐡) β†’ (𝐴(,)𝐢) βŠ† (𝐴(,)𝐡))
7977, 51, 78syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝐴(,)𝐢) βŠ† (𝐴(,)𝐡))
80 dvcvx.d . . . . . . . 8 (πœ‘ β†’ (ℝ D 𝐹) Isom < , < ((𝐴(,)𝐡), π‘Š))
81 isof1o 7313 . . . . . . . 8 ((ℝ D 𝐹) Isom < , < ((𝐴(,)𝐡), π‘Š) β†’ (ℝ D 𝐹):(𝐴(,)𝐡)–1-1-ontoβ†’π‘Š)
82 f1odm 6828 . . . . . . . 8 ((ℝ D 𝐹):(𝐴(,)𝐡)–1-1-ontoβ†’π‘Š β†’ dom (ℝ D 𝐹) = (𝐴(,)𝐡))
8380, 81, 823syl 18 . . . . . . 7 (πœ‘ β†’ dom (ℝ D 𝐹) = (𝐴(,)𝐡))
8479, 83sseqtrrd 4016 . . . . . 6 (πœ‘ β†’ (𝐴(,)𝐢) βŠ† dom (ℝ D 𝐹))
85 df-ss 3958 . . . . . 6 ((𝐴(,)𝐢) βŠ† dom (ℝ D 𝐹) ↔ ((𝐴(,)𝐢) ∩ dom (ℝ D 𝐹)) = (𝐴(,)𝐢))
8684, 85sylib 217 . . . . 5 (πœ‘ β†’ ((𝐴(,)𝐢) ∩ dom (ℝ D 𝐹)) = (𝐴(,)𝐢))
8776, 86eqtrid 2776 . . . 4 (πœ‘ β†’ dom ((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢)) = (𝐴(,)𝐢))
8875, 87eqtrd 2764 . . 3 (πœ‘ β†’ dom (ℝ D (𝐹 β†Ύ (𝐴[,]𝐢))) = (𝐴(,)𝐢))
891, 13, 34, 56, 88mvth 25869 . 2 (πœ‘ β†’ βˆƒπ‘₯ ∈ (𝐴(,)𝐢)((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)))
901, 13, 34ltled 11361 . . . . 5 (πœ‘ β†’ 𝐴 ≀ 𝐢)
9110leidd 11779 . . . . 5 (πœ‘ β†’ 𝐡 ≀ 𝐡)
92 iccss 13393 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) ∧ (𝐴 ≀ 𝐢 ∧ 𝐡 ≀ 𝐡)) β†’ (𝐢[,]𝐡) βŠ† (𝐴[,]𝐡))
931, 10, 90, 91, 92syl22anc 836 . . . 4 (πœ‘ β†’ (𝐢[,]𝐡) βŠ† (𝐴[,]𝐡))
94 rescncf 24761 . . . 4 ((𝐢[,]𝐡) βŠ† (𝐴[,]𝐡) β†’ (𝐹 ∈ ((𝐴[,]𝐡)–cn→ℝ) β†’ (𝐹 β†Ύ (𝐢[,]𝐡)) ∈ ((𝐢[,]𝐡)–cn→ℝ)))
9593, 54, 94sylc 65 . . 3 (πœ‘ β†’ (𝐹 β†Ύ (𝐢[,]𝐡)) ∈ ((𝐢[,]𝐡)–cn→ℝ))
96 iccssre 13407 . . . . . . . 8 ((𝐢 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐢[,]𝐡) βŠ† ℝ)
9713, 10, 96syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝐢[,]𝐡) βŠ† ℝ)
9867, 68dvres 25784 . . . . . . 7 (((ℝ βŠ† β„‚ ∧ 𝐹:(𝐴[,]𝐡)βŸΆβ„‚) ∧ ((𝐴[,]𝐡) βŠ† ℝ ∧ (𝐢[,]𝐡) βŠ† ℝ)) β†’ (ℝ D (𝐹 β†Ύ (𝐢[,]𝐡))) = ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐢[,]𝐡))))
9958, 62, 64, 97, 98syl22anc 836 . . . . . 6 (πœ‘ β†’ (ℝ D (𝐹 β†Ύ (𝐢[,]𝐡))) = ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐢[,]𝐡))))
100 iccntr 24681 . . . . . . . 8 ((𝐢 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐢[,]𝐡)) = (𝐢(,)𝐡))
10113, 10, 100syl2anc 583 . . . . . . 7 (πœ‘ β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐢[,]𝐡)) = (𝐢(,)𝐡))
102101reseq2d 5972 . . . . . 6 (πœ‘ β†’ ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐢[,]𝐡))) = ((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡)))
10399, 102eqtrd 2764 . . . . 5 (πœ‘ β†’ (ℝ D (𝐹 β†Ύ (𝐢[,]𝐡))) = ((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡)))
104103dmeqd 5896 . . . 4 (πœ‘ β†’ dom (ℝ D (𝐹 β†Ύ (𝐢[,]𝐡))) = dom ((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡)))
105 dmres 5994 . . . . 5 dom ((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡)) = ((𝐢(,)𝐡) ∩ dom (ℝ D 𝐹))
1061rexrd 11263 . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ ℝ*)
107 iooss1 13360 . . . . . . . 8 ((𝐴 ∈ ℝ* ∧ 𝐴 ≀ 𝐢) β†’ (𝐢(,)𝐡) βŠ† (𝐴(,)𝐡))
108106, 90, 107syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝐢(,)𝐡) βŠ† (𝐴(,)𝐡))
109108, 83sseqtrrd 4016 . . . . . 6 (πœ‘ β†’ (𝐢(,)𝐡) βŠ† dom (ℝ D 𝐹))
110 df-ss 3958 . . . . . 6 ((𝐢(,)𝐡) βŠ† dom (ℝ D 𝐹) ↔ ((𝐢(,)𝐡) ∩ dom (ℝ D 𝐹)) = (𝐢(,)𝐡))
111109, 110sylib 217 . . . . 5 (πœ‘ β†’ ((𝐢(,)𝐡) ∩ dom (ℝ D 𝐹)) = (𝐢(,)𝐡))
112105, 111eqtrid 2776 . . . 4 (πœ‘ β†’ dom ((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡)) = (𝐢(,)𝐡))
113104, 112eqtrd 2764 . . 3 (πœ‘ β†’ dom (ℝ D (𝐹 β†Ύ (𝐢[,]𝐡))) = (𝐢(,)𝐡))
11413, 10, 50, 95, 113mvth 25869 . 2 (πœ‘ β†’ βˆƒπ‘¦ ∈ (𝐢(,)𝐡)((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢)))
115 reeanv 3218 . . 3 (βˆƒπ‘₯ ∈ (𝐴(,)𝐢)βˆƒπ‘¦ ∈ (𝐢(,)𝐡)(((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ ((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢))) ↔ (βˆƒπ‘₯ ∈ (𝐴(,)𝐢)((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ βˆƒπ‘¦ ∈ (𝐢(,)𝐡)((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢))))
11674fveq1d 6884 . . . . . . . 8 (πœ‘ β†’ ((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = (((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢))β€˜π‘₯))
117 fvres 6901 . . . . . . . . 9 (π‘₯ ∈ (𝐴(,)𝐢) β†’ (((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢))β€˜π‘₯) = ((ℝ D 𝐹)β€˜π‘₯))
118117adantr 480 . . . . . . . 8 ((π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡)) β†’ (((ℝ D 𝐹) β†Ύ (𝐴(,)𝐢))β€˜π‘₯) = ((ℝ D 𝐹)β€˜π‘₯))
119116, 118sylan9eq 2784 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((ℝ D 𝐹)β€˜π‘₯))
12013rexrd 11263 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐢 ∈ ℝ*)
121 ubicc2 13443 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ* ∧ 𝐢 ∈ ℝ* ∧ 𝐴 ≀ 𝐢) β†’ 𝐢 ∈ (𝐴[,]𝐢))
122106, 120, 90, 121syl3anc 1368 . . . . . . . . . . 11 (πœ‘ β†’ 𝐢 ∈ (𝐴[,]𝐢))
123122fvresd 6902 . . . . . . . . . 10 (πœ‘ β†’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) = (πΉβ€˜πΆ))
124 lbicc2 13442 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ* ∧ 𝐢 ∈ ℝ* ∧ 𝐴 ≀ 𝐢) β†’ 𝐴 ∈ (𝐴[,]𝐢))
125106, 120, 90, 124syl3anc 1368 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ (𝐴[,]𝐢))
126125fvresd 6902 . . . . . . . . . 10 (πœ‘ β†’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄) = (πΉβ€˜π΄))
127123, 126oveq12d 7420 . . . . . . . . 9 (πœ‘ β†’ (((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) = ((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)))
128127oveq1d 7417 . . . . . . . 8 (πœ‘ β†’ ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)))
129128adantr 480 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)))
130119, 129eqeq12d 2740 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ (((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) ↔ ((ℝ D 𝐹)β€˜π‘₯) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴))))
131103fveq1d 6884 . . . . . . . 8 (πœ‘ β†’ ((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = (((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡))β€˜π‘¦))
132 fvres 6901 . . . . . . . . 9 (𝑦 ∈ (𝐢(,)𝐡) β†’ (((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡))β€˜π‘¦) = ((ℝ D 𝐹)β€˜π‘¦))
133132adantl 481 . . . . . . . 8 ((π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡)) β†’ (((ℝ D 𝐹) β†Ύ (𝐢(,)𝐡))β€˜π‘¦) = ((ℝ D 𝐹)β€˜π‘¦))
134131, 133sylan9eq 2784 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((ℝ D 𝐹)β€˜π‘¦))
135 ubicc2 13443 . . . . . . . . . . . 12 ((𝐢 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝐢 ≀ 𝐡) β†’ 𝐡 ∈ (𝐢[,]𝐡))
136120, 77, 51, 135syl3anc 1368 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ∈ (𝐢[,]𝐡))
137136fvresd 6902 . . . . . . . . . 10 (πœ‘ β†’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) = (πΉβ€˜π΅))
138 lbicc2 13442 . . . . . . . . . . . 12 ((𝐢 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝐢 ≀ 𝐡) β†’ 𝐢 ∈ (𝐢[,]𝐡))
139120, 77, 51, 138syl3anc 1368 . . . . . . . . . . 11 (πœ‘ β†’ 𝐢 ∈ (𝐢[,]𝐡))
140139fvresd 6902 . . . . . . . . . 10 (πœ‘ β†’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ) = (πΉβ€˜πΆ))
141137, 140oveq12d 7420 . . . . . . . . 9 (πœ‘ β†’ (((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) = ((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)))
142141oveq1d 7417 . . . . . . . 8 (πœ‘ β†’ ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢)) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢)))
143142adantr 480 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢)) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢)))
144134, 143eqeq12d 2740 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ (((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢)) ↔ ((ℝ D 𝐹)β€˜π‘¦) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢))))
145130, 144anbi12d 630 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ ((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢))) ↔ (((ℝ D 𝐹)β€˜π‘₯) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ ((ℝ D 𝐹)β€˜π‘¦) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢)))))
146 elioore 13355 . . . . . . . . . 10 (π‘₯ ∈ (𝐴(,)𝐢) β†’ π‘₯ ∈ ℝ)
147146ad2antrl 725 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ π‘₯ ∈ ℝ)
14813adantr 480 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ 𝐢 ∈ ℝ)
149 elioore 13355 . . . . . . . . . 10 (𝑦 ∈ (𝐢(,)𝐡) β†’ 𝑦 ∈ ℝ)
150149ad2antll 726 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ 𝑦 ∈ ℝ)
151 eliooord 13384 . . . . . . . . . . 11 (π‘₯ ∈ (𝐴(,)𝐢) β†’ (𝐴 < π‘₯ ∧ π‘₯ < 𝐢))
152151ad2antrl 725 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ (𝐴 < π‘₯ ∧ π‘₯ < 𝐢))
153152simprd 495 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ π‘₯ < 𝐢)
154 eliooord 13384 . . . . . . . . . . 11 (𝑦 ∈ (𝐢(,)𝐡) β†’ (𝐢 < 𝑦 ∧ 𝑦 < 𝐡))
155154ad2antll 726 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ (𝐢 < 𝑦 ∧ 𝑦 < 𝐡))
156155simpld 494 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ 𝐢 < 𝑦)
157147, 148, 150, 153, 156lttrd 11374 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ π‘₯ < 𝑦)
15880adantr 480 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ (ℝ D 𝐹) Isom < , < ((𝐴(,)𝐡), π‘Š))
15979sselda 3975 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐢)) β†’ π‘₯ ∈ (𝐴(,)𝐡))
160159adantrr 714 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ π‘₯ ∈ (𝐴(,)𝐡))
161108sselda 3975 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ (𝐢(,)𝐡)) β†’ 𝑦 ∈ (𝐴(,)𝐡))
162161adantrl 713 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ 𝑦 ∈ (𝐴(,)𝐡))
163 isorel 7316 . . . . . . . . 9 (((ℝ D 𝐹) Isom < , < ((𝐴(,)𝐡), π‘Š) ∧ (π‘₯ ∈ (𝐴(,)𝐡) ∧ 𝑦 ∈ (𝐴(,)𝐡))) β†’ (π‘₯ < 𝑦 ↔ ((ℝ D 𝐹)β€˜π‘₯) < ((ℝ D 𝐹)β€˜π‘¦)))
164158, 160, 162, 163syl12anc 834 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ (π‘₯ < 𝑦 ↔ ((ℝ D 𝐹)β€˜π‘₯) < ((ℝ D 𝐹)β€˜π‘¦)))
165157, 164mpbid 231 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((ℝ D 𝐹)β€˜π‘₯) < ((ℝ D 𝐹)β€˜π‘¦))
166 breq12 5144 . . . . . . 7 ((((ℝ D 𝐹)β€˜π‘₯) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ ((ℝ D 𝐹)β€˜π‘¦) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢))) β†’ (((ℝ D 𝐹)β€˜π‘₯) < ((ℝ D 𝐹)β€˜π‘¦) ↔ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢))))
167165, 166syl5ibcom 244 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (𝐴(,)𝐢) ∧ 𝑦 ∈ (𝐢(,)𝐡))) β†’ ((((ℝ D 𝐹)β€˜π‘₯) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ ((ℝ D 𝐹)β€˜π‘¦) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢))) β†’ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢))))
16853, 122sseldd 3976 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐢 ∈ (𝐴[,]𝐡))
16960, 168ffvelcdmd 7078 . . . . . . . . . . 11 (πœ‘ β†’ (πΉβ€˜πΆ) ∈ ℝ)
17053, 125sseldd 3976 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 ∈ (𝐴[,]𝐡))
17160, 170ffvelcdmd 7078 . . . . . . . . . . 11 (πœ‘ β†’ (πΉβ€˜π΄) ∈ ℝ)
172169, 171resubcld 11641 . . . . . . . . . 10 (πœ‘ β†’ ((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) ∈ ℝ)
17327gt0ne0d 11777 . . . . . . . . . 10 (πœ‘ β†’ (1 βˆ’ 𝑇) β‰  0)
174172, 9, 173redivcld 12041 . . . . . . . . 9 (πœ‘ β†’ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) ∈ ℝ)
17593, 136sseldd 3976 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ (𝐴[,]𝐡))
17660, 175ffvelcdmd 7078 . . . . . . . . . . 11 (πœ‘ β†’ (πΉβ€˜π΅) ∈ ℝ)
177176, 169resubcld 11641 . . . . . . . . . 10 (πœ‘ β†’ ((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) ∈ ℝ)
17842gt0ne0d 11777 . . . . . . . . . 10 (πœ‘ β†’ 𝑇 β‰  0)
179177, 5, 178redivcld 12041 . . . . . . . . 9 (πœ‘ β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) ∈ ℝ)
18010, 1resubcld 11641 . . . . . . . . 9 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ∈ ℝ)
1811, 10posdifd 11800 . . . . . . . . . 10 (πœ‘ β†’ (𝐴 < 𝐡 ↔ 0 < (𝐡 βˆ’ 𝐴)))
18221, 181mpbid 231 . . . . . . . . 9 (πœ‘ β†’ 0 < (𝐡 βˆ’ 𝐴))
183 ltdiv1 12077 . . . . . . . . 9 (((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) ∈ ℝ ∧ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) ∈ ℝ ∧ ((𝐡 βˆ’ 𝐴) ∈ ℝ ∧ 0 < (𝐡 βˆ’ 𝐴))) β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) ↔ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) / (𝐡 βˆ’ 𝐴)) < ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) / (𝐡 βˆ’ 𝐴))))
184174, 179, 180, 182, 183syl112anc 1371 . . . . . . . 8 (πœ‘ β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) ↔ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) / (𝐡 βˆ’ 𝐴)) < ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) / (𝐡 βˆ’ 𝐴))))
185172recnd 11241 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) ∈ β„‚)
186185, 15mulcomd 11234 . . . . . . . . . . 11 (πœ‘ β†’ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) Β· 𝑇) = (𝑇 Β· ((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄))))
187169recnd 11241 . . . . . . . . . . . 12 (πœ‘ β†’ (πΉβ€˜πΆ) ∈ β„‚)
188171recnd 11241 . . . . . . . . . . . 12 (πœ‘ β†’ (πΉβ€˜π΄) ∈ β„‚)
18915, 187, 188subdid 11669 . . . . . . . . . . 11 (πœ‘ β†’ (𝑇 Β· ((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄))) = ((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))))
190186, 189eqtrd 2764 . . . . . . . . . 10 (πœ‘ β†’ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) Β· 𝑇) = ((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))))
191177recnd 11241 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) ∈ β„‚)
1929recnd 11241 . . . . . . . . . . . 12 (πœ‘ β†’ (1 βˆ’ 𝑇) ∈ β„‚)
193191, 192mulcomd 11234 . . . . . . . . . . 11 (πœ‘ β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) Β· (1 βˆ’ 𝑇)) = ((1 βˆ’ 𝑇) Β· ((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ))))
194176recnd 11241 . . . . . . . . . . . 12 (πœ‘ β†’ (πΉβ€˜π΅) ∈ β„‚)
195192, 194, 187subdid 11669 . . . . . . . . . . 11 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· ((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ))) = (((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) βˆ’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))))
196193, 195eqtrd 2764 . . . . . . . . . 10 (πœ‘ β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) Β· (1 βˆ’ 𝑇)) = (((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) βˆ’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))))
197190, 196breq12d 5152 . . . . . . . . 9 (πœ‘ β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) Β· 𝑇) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) Β· (1 βˆ’ 𝑇)) ↔ ((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) < (((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) βˆ’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ)))))
1985, 42jca 511 . . . . . . . . . 10 (πœ‘ β†’ (𝑇 ∈ ℝ ∧ 0 < 𝑇))
1999, 27jca 511 . . . . . . . . . 10 (πœ‘ β†’ ((1 βˆ’ 𝑇) ∈ ℝ ∧ 0 < (1 βˆ’ 𝑇)))
200 lt2mul2div 12091 . . . . . . . . . 10 (((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) ∈ ℝ ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇)) ∧ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) ∈ ℝ ∧ ((1 βˆ’ 𝑇) ∈ ℝ ∧ 0 < (1 βˆ’ 𝑇)))) β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) Β· 𝑇) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) Β· (1 βˆ’ 𝑇)) ↔ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇)))
201172, 198, 177, 199, 200syl22anc 836 . . . . . . . . 9 (πœ‘ β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) Β· 𝑇) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) Β· (1 βˆ’ 𝑇)) ↔ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇)))
2025, 169remulcld 11243 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑇 Β· (πΉβ€˜πΆ)) ∈ ℝ)
203202recnd 11241 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑇 Β· (πΉβ€˜πΆ)) ∈ β„‚)
2049, 169remulcld 11243 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ)) ∈ ℝ)
205204recnd 11241 . . . . . . . . . . . . 13 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ)) ∈ β„‚)
2065, 171remulcld 11243 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑇 Β· (πΉβ€˜π΄)) ∈ ℝ)
207206recnd 11241 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑇 Β· (πΉβ€˜π΄)) ∈ β„‚)
208203, 205, 207addsubd 11591 . . . . . . . . . . . 12 (πœ‘ β†’ (((𝑇 Β· (πΉβ€˜πΆ)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) = (((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))))
209 ax-1cn 11165 . . . . . . . . . . . . . . . 16 1 ∈ β„‚
210 pncan3 11467 . . . . . . . . . . . . . . . 16 ((𝑇 ∈ β„‚ ∧ 1 ∈ β„‚) β†’ (𝑇 + (1 βˆ’ 𝑇)) = 1)
21115, 209, 210sylancl 585 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑇 + (1 βˆ’ 𝑇)) = 1)
212211oveq1d 7417 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑇 + (1 βˆ’ 𝑇)) Β· (πΉβ€˜πΆ)) = (1 Β· (πΉβ€˜πΆ)))
21315, 192, 187adddird 11238 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑇 + (1 βˆ’ 𝑇)) Β· (πΉβ€˜πΆ)) = ((𝑇 Β· (πΉβ€˜πΆ)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))))
214187mullidd 11231 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1 Β· (πΉβ€˜πΆ)) = (πΉβ€˜πΆ))
215212, 213, 2143eqtr3d 2772 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝑇 Β· (πΉβ€˜πΆ)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))) = (πΉβ€˜πΆ))
216215oveq1d 7417 . . . . . . . . . . . 12 (πœ‘ β†’ (((𝑇 Β· (πΉβ€˜πΆ)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) = ((πΉβ€˜πΆ) βˆ’ (𝑇 Β· (πΉβ€˜π΄))))
217208, 216eqtr3d 2766 . . . . . . . . . . 11 (πœ‘ β†’ (((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))) = ((πΉβ€˜πΆ) βˆ’ (𝑇 Β· (πΉβ€˜π΄))))
218217breq1d 5149 . . . . . . . . . 10 (πœ‘ β†’ ((((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))) < ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) ↔ ((πΉβ€˜πΆ) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) < ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅))))
219202, 206resubcld 11641 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) ∈ ℝ)
2209, 176remulcld 11243 . . . . . . . . . . 11 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) ∈ ℝ)
221219, 204, 220ltaddsubd 11813 . . . . . . . . . 10 (πœ‘ β†’ ((((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))) < ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) ↔ ((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) < (((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) βˆ’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ)))))
222169, 206, 220ltsubadd2d 11811 . . . . . . . . . 10 (πœ‘ β†’ (((πΉβ€˜πΆ) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) < ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) ↔ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)))))
223218, 221, 2223bitr3d 309 . . . . . . . . 9 (πœ‘ β†’ (((𝑇 Β· (πΉβ€˜πΆ)) βˆ’ (𝑇 Β· (πΉβ€˜π΄))) < (((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)) βˆ’ ((1 βˆ’ 𝑇) Β· (πΉβ€˜πΆ))) ↔ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)))))
224197, 201, 2233bitr3d 309 . . . . . . . 8 (πœ‘ β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) < (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) ↔ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)))))
225180recnd 11241 . . . . . . . . . . 11 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ∈ β„‚)
226182gt0ne0d 11777 . . . . . . . . . . 11 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) β‰  0)
227185, 192, 225, 173, 226divdiv1d 12020 . . . . . . . . . 10 (πœ‘ β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) / (𝐡 βˆ’ 𝐴)) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / ((1 βˆ’ 𝑇) Β· (𝐡 βˆ’ 𝐴))))
22820oveq2d 7418 . . . . . . . . . . . . 13 (πœ‘ β†’ (((1 βˆ’ 𝑇) Β· 𝐡) βˆ’ ((1 βˆ’ 𝑇) Β· 𝐴)) = (((1 βˆ’ 𝑇) Β· 𝐡) βˆ’ (𝐴 βˆ’ (𝑇 Β· 𝐴))))
22911recnd 11241 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· 𝐡) ∈ β„‚)
2306recnd 11241 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑇 Β· 𝐴) ∈ β„‚)
231229, 16, 230subsub3d 11600 . . . . . . . . . . . . 13 (πœ‘ β†’ (((1 βˆ’ 𝑇) Β· 𝐡) βˆ’ (𝐴 βˆ’ (𝑇 Β· 𝐴))) = ((((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴)) βˆ’ 𝐴))
232228, 231eqtrd 2764 . . . . . . . . . . . 12 (πœ‘ β†’ (((1 βˆ’ 𝑇) Β· 𝐡) βˆ’ ((1 βˆ’ 𝑇) Β· 𝐴)) = ((((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴)) βˆ’ 𝐴))
233192, 36, 16subdid 11669 . . . . . . . . . . . 12 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· (𝐡 βˆ’ 𝐴)) = (((1 βˆ’ 𝑇) Β· 𝐡) βˆ’ ((1 βˆ’ 𝑇) Β· 𝐴)))
234230, 229addcomd 11415 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑇 Β· 𝐴) + ((1 βˆ’ 𝑇) Β· 𝐡)) = (((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴)))
2352, 234eqtrid 2776 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐢 = (((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴)))
236235oveq1d 7417 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐢 βˆ’ 𝐴) = ((((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴)) βˆ’ 𝐴))
237232, 233, 2363eqtr4d 2774 . . . . . . . . . . 11 (πœ‘ β†’ ((1 βˆ’ 𝑇) Β· (𝐡 βˆ’ 𝐴)) = (𝐢 βˆ’ 𝐴))
238237oveq2d 7418 . . . . . . . . . 10 (πœ‘ β†’ (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / ((1 βˆ’ 𝑇) Β· (𝐡 βˆ’ 𝐴))) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)))
239227, 238eqtrd 2764 . . . . . . . . 9 (πœ‘ β†’ ((((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (1 βˆ’ 𝑇)) / (𝐡 βˆ’ 𝐴)) = (((πΉβ€˜πΆ) βˆ’ (πΉβ€˜π΄)) / (𝐢 βˆ’ 𝐴)))
240191, 15, 225, 178, 226divdiv1d 12020 . . . . . . . . . 10 (πœ‘ β†’ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) / (𝐡 βˆ’ 𝐴)) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝑇 Β· (𝐡 βˆ’ 𝐴))))
24136, 229, 230subsub4d 11601 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐡 βˆ’ ((1 βˆ’ 𝑇) Β· 𝐡)) βˆ’ (𝑇 Β· 𝐴)) = (𝐡 βˆ’ (((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴))))
24240oveq2d 7418 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐡 βˆ’ ((1 βˆ’ 𝑇) Β· 𝐡)) = (𝐡 βˆ’ (𝐡 βˆ’ (𝑇 Β· 𝐡))))
24341recnd 11241 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑇 Β· 𝐡) ∈ β„‚)
24436, 243nncand 11575 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐡 βˆ’ (𝐡 βˆ’ (𝑇 Β· 𝐡))) = (𝑇 Β· 𝐡))
245242, 244eqtrd 2764 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐡 βˆ’ ((1 βˆ’ 𝑇) Β· 𝐡)) = (𝑇 Β· 𝐡))
246245oveq1d 7417 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐡 βˆ’ ((1 βˆ’ 𝑇) Β· 𝐡)) βˆ’ (𝑇 Β· 𝐴)) = ((𝑇 Β· 𝐡) βˆ’ (𝑇 Β· 𝐴)))
247241, 246eqtr3d 2766 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐡 βˆ’ (((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴))) = ((𝑇 Β· 𝐡) βˆ’ (𝑇 Β· 𝐴)))
248235oveq2d 7418 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐡 βˆ’ 𝐢) = (𝐡 βˆ’ (((1 βˆ’ 𝑇) Β· 𝐡) + (𝑇 Β· 𝐴))))
24915, 36, 16subdid 11669 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑇 Β· (𝐡 βˆ’ 𝐴)) = ((𝑇 Β· 𝐡) βˆ’ (𝑇 Β· 𝐴)))
250247, 248, 2493eqtr4d 2774 . . . . . . . . . . 11 (πœ‘ β†’ (𝐡 βˆ’ 𝐢) = (𝑇 Β· (𝐡 βˆ’ 𝐴)))
251250oveq2d 7418 . . . . . . . . . 10 (πœ‘ β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢)) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝑇 Β· (𝐡 βˆ’ 𝐴))))
252240, 251eqtr4d 2767 . . . . . . . . 9 (πœ‘ β†’ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / 𝑇) / (𝐡 βˆ’ 𝐴)) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜πΆ)) / (𝐡 βˆ’ 𝐢)))
253239, 252breq12d 5152 . . . . . . . 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 3203 . . 3 (πœ‘ β†’ (βˆƒπ‘₯ ∈ (𝐴(,)𝐢)βˆƒπ‘¦ ∈ (𝐢(,)𝐡)(((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ ((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢))) β†’ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)))))
259115, 258biimtrrid 242 . 2 (πœ‘ β†’ ((βˆƒπ‘₯ ∈ (𝐴(,)𝐢)((ℝ D (𝐹 β†Ύ (𝐴[,]𝐢)))β€˜π‘₯) = ((((𝐹 β†Ύ (𝐴[,]𝐢))β€˜πΆ) βˆ’ ((𝐹 β†Ύ (𝐴[,]𝐢))β€˜π΄)) / (𝐢 βˆ’ 𝐴)) ∧ βˆƒπ‘¦ ∈ (𝐢(,)𝐡)((ℝ D (𝐹 β†Ύ (𝐢[,]𝐡)))β€˜π‘¦) = ((((𝐹 β†Ύ (𝐢[,]𝐡))β€˜π΅) βˆ’ ((𝐹 β†Ύ (𝐢[,]𝐡))β€˜πΆ)) / (𝐡 βˆ’ 𝐢))) β†’ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅)))))
26089, 114, 259mp2and 696 1 (πœ‘ β†’ (πΉβ€˜πΆ) < ((𝑇 Β· (πΉβ€˜π΄)) + ((1 βˆ’ 𝑇) Β· (πΉβ€˜π΅))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098  βˆƒwrex 3062   ∩ cin 3940   βŠ† wss 3941   class class class wbr 5139  dom cdm 5667  ran crn 5668   β†Ύ cres 5669  βŸΆwf 6530  β€“1-1-ontoβ†’wf1o 6533  β€˜cfv 6534   Isom wiso 6535  (class class class)co 7402  β„‚cc 11105  β„cr 11106  0cc0 11107  1c1 11108   + caddc 11110   Β· cmul 11112  β„*cxr 11246   < clt 11247   ≀ cle 11248   βˆ’ cmin 11443   / cdiv 11870  (,)cioo 13325  [,]cicc 13328  TopOpenctopn 17372  topGenctg 17388  β„‚fldccnfld 21234  intcnt 22865  β€“cnβ†’ccncf 24740   D cdv 25736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185  ax-addf 11186
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-tp 4626  df-op 4628  df-uni 4901  df-int 4942  df-iun 4990  df-iin 4991  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-se 5623  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-isom 6543  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-of 7664  df-om 7850  df-1st 7969  df-2nd 7970  df-supp 8142  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-er 8700  df-map 8819  df-pm 8820  df-ixp 8889  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9502  df-card 9931  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-div 11871  df-nn 12212  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280  df-9 12281  df-n0 12472  df-z 12558  df-dec 12677  df-uz 12822  df-q 12932  df-rp 12976  df-xneg 13093  df-xadd 13094  df-xmul 13095  df-ioo 13329  df-ico 13331  df-icc 13332  df-fz 13486  df-fzo 13629  df-seq 13968  df-exp 14029  df-hash 14292  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-struct 17085  df-sets 17102  df-slot 17120  df-ndx 17132  df-base 17150  df-ress 17179  df-plusg 17215  df-mulr 17216  df-starv 17217  df-sca 17218  df-vsca 17219  df-ip 17220  df-tset 17221  df-ple 17222  df-ds 17224  df-unif 17225  df-hom 17226  df-cco 17227  df-rest 17373  df-topn 17374  df-0g 17392  df-gsum 17393  df-topgen 17394  df-pt 17395  df-prds 17398  df-xrs 17453  df-qtop 17458  df-imas 17459  df-xps 17461  df-mre 17535  df-mrc 17536  df-acs 17538  df-mgm 18569  df-sgrp 18648  df-mnd 18664  df-submnd 18710  df-mulg 18992  df-cntz 19229  df-cmn 19698  df-psmet 21226  df-xmet 21227  df-met 21228  df-bl 21229  df-mopn 21230  df-fbas 21231  df-fg 21232  df-cnfld 21235  df-top 22740  df-topon 22757  df-topsp 22779  df-bases 22793  df-cld 22867  df-ntr 22868  df-cls 22869  df-nei 22946  df-lp 22984  df-perf 22985  df-cn 23075  df-cnp 23076  df-haus 23163  df-cmp 23235  df-tx 23410  df-hmeo 23603  df-fil 23694  df-fm 23786  df-flim 23787  df-flf 23788  df-xms 24170  df-ms 24171  df-tms 24172  df-cncf 24742  df-limc 25739  df-dv 25740
This theorem is referenced by:  efcvx  26327  logccv  26538
  Copyright terms: Public domain W3C validator