# Metamath Proof Explorer

## Theorem axcontlem8

Description: Lemma for axcont . A point in D is between two others if its function value falls in the middle. (Contributed by Scott Fenton, 18-Jun-2013)

Ref Expression
Hypotheses axcontlem8.1 ${⊢}{D}=\left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}$
axcontlem8.2 ${⊢}{F}=\left\{⟨{x},{t}⟩|\left({x}\in {D}\wedge \left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)\right\}$
Assertion axcontlem8 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({P}\in {D}\wedge {Q}\in {D}\wedge {R}\in {D}\right)\right)\to \left(\left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\to {Q}\mathrm{Btwn}⟨{P},{R}⟩\right)$

### Proof

Step Hyp Ref Expression
1 axcontlem8.1 ${⊢}{D}=\left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}$
2 axcontlem8.2 ${⊢}{F}=\left\{⟨{x},{t}⟩|\left({x}\in {D}\wedge \left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)\right\}$
3 1 2 axcontlem6 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {P}\in {D}\right)\to \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)$
4 3 ex ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\to \left({P}\in {D}\to \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)\right)$
5 1 2 axcontlem6 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {Q}\in {D}\right)\to \left({F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\right)$
6 5 ex ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\to \left({Q}\in {D}\to \left({F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\right)\right)$
7 1 2 axcontlem6 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {R}\in {D}\right)\to \left({F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
8 7 ex ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\to \left({R}\in {D}\to \left({F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
9 4 6 8 3anim123d ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\to \left(\left({P}\in {D}\wedge {Q}\in {D}\wedge {R}\in {D}\right)\to \left(\left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)\wedge \left({F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\right)\wedge \left({F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)\right)$
10 9 imp ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({P}\in {D}\wedge {Q}\in {D}\wedge {R}\in {D}\right)\right)\to \left(\left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)\wedge \left({F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\right)\wedge \left({F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
11 10 adantr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({P}\in {D}\wedge {Q}\in {D}\wedge {R}\in {D}\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\to \left(\left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)\wedge \left({F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\right)\wedge \left({F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
12 3an6 ${⊢}\left(\left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)\wedge \left({F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\right)\wedge \left({F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)↔\left(\left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
13 0elunit ${⊢}0\in \left[0,1\right]$
14 simplr1 ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\to {F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)$
15 14 ad2antlr ${⊢}\left(\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)$
16 elrege0 ${⊢}{F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)↔\left({F}\left({P}\right)\in ℝ\wedge 0\le {F}\left({P}\right)\right)$
17 16 simplbi ${⊢}{F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\to {F}\left({P}\right)\in ℝ$
18 15 17 syl ${⊢}\left(\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({P}\right)\in ℝ$
19 18 recnd ${⊢}\left(\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({P}\right)\in ℂ$
20 simprrl ${⊢}\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({P}\right)\le {F}\left({Q}\right)$
21 20 adantr ${⊢}\left(\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({P}\right)\le {F}\left({Q}\right)$
22 simprrr ${⊢}\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({Q}\right)\le {F}\left({R}\right)$
23 simpl ${⊢}\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({P}\right)={F}\left({R}\right)$
24 22 23 breqtrrd ${⊢}\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({Q}\right)\le {F}\left({P}\right)$
25 24 adantr ${⊢}\left(\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({Q}\right)\le {F}\left({P}\right)$
26 simplr2 ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\to {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)$
27 26 ad2antlr ${⊢}\left(\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)$
28 elrege0 ${⊢}{F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)↔\left({F}\left({Q}\right)\in ℝ\wedge 0\le {F}\left({Q}\right)\right)$
29 28 simplbi ${⊢}{F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\to {F}\left({Q}\right)\in ℝ$
30 27 29 syl ${⊢}\left(\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({Q}\right)\in ℝ$
31 18 30 letri3d ${⊢}\left(\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left({F}\left({P}\right)={F}\left({Q}\right)↔\left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({P}\right)\right)\right)$
32 21 25 31 mpbir2and ${⊢}\left(\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({P}\right)={F}\left({Q}\right)$
33 simpll ${⊢}\left(\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({P}\right)={F}\left({R}\right)$
34 simpll2 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\to {Z}\in 𝔼\left({N}\right)$
35 34 adantr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\to {Z}\in 𝔼\left({N}\right)$
36 35 ad2antlr ${⊢}\left(\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\in 𝔼\left({N}\right)$
37 fveecn ${⊢}\left({Z}\in 𝔼\left({N}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\left({i}\right)\in ℂ$
38 36 37 sylancom ${⊢}\left(\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\left({i}\right)\in ℂ$
39 simpll3 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\to {U}\in 𝔼\left({N}\right)$
40 39 adantr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\to {U}\in 𝔼\left({N}\right)$
41 40 ad2antlr ${⊢}\left(\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {U}\in 𝔼\left({N}\right)$
42 fveecn ${⊢}\left({U}\in 𝔼\left({N}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {U}\left({i}\right)\in ℂ$
43 41 42 sylancom ${⊢}\left(\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {U}\left({i}\right)\in ℂ$
44 ax-1cn ${⊢}1\in ℂ$
45 simpl ${⊢}\left({F}\left({P}\right)\in ℂ\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({P}\right)\in ℂ$
46 subcl ${⊢}\left(1\in ℂ\wedge {F}\left({P}\right)\in ℂ\right)\to 1-{F}\left({P}\right)\in ℂ$
47 44 45 46 sylancr ${⊢}\left({F}\left({P}\right)\in ℂ\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 1-{F}\left({P}\right)\in ℂ$
48 simprl ${⊢}\left({F}\left({P}\right)\in ℂ\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {Z}\left({i}\right)\in ℂ$
49 47 48 mulcld ${⊢}\left({F}\left({P}\right)\in ℂ\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{F}\left({P}\right)\right){Z}\left({i}\right)\in ℂ$
50 mulcl ${⊢}\left({F}\left({P}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\to {F}\left({P}\right){U}\left({i}\right)\in ℂ$
51 50 adantrl ${⊢}\left({F}\left({P}\right)\in ℂ\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({P}\right){U}\left({i}\right)\in ℂ$
52 49 51 addcld ${⊢}\left({F}\left({P}\right)\in ℂ\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\in ℂ$
53 52 mulid2d ${⊢}\left({F}\left({P}\right)\in ℂ\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)$
54 52 mul02d ${⊢}\left({F}\left({P}\right)\in ℂ\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 0\cdot \left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)=0$
55 53 54 oveq12d ${⊢}\left({F}\left({P}\right)\in ℂ\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)+0$
56 52 addid1d ${⊢}\left({F}\left({P}\right)\in ℂ\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)+0=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)$
57 55 56 eqtr2d ${⊢}\left({F}\left({P}\right)\in ℂ\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)=1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)$
58 57 3adant2 ${⊢}\left({F}\left({P}\right)\in ℂ\wedge \left({F}\left({P}\right)={F}\left({Q}\right)\wedge {F}\left({P}\right)={F}\left({R}\right)\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)=1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)$
59 oveq2 ${⊢}{F}\left({P}\right)={F}\left({Q}\right)\to 1-{F}\left({P}\right)=1-{F}\left({Q}\right)$
60 59 oveq1d ${⊢}{F}\left({P}\right)={F}\left({Q}\right)\to \left(1-{F}\left({P}\right)\right){Z}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)$
61 oveq1 ${⊢}{F}\left({P}\right)={F}\left({Q}\right)\to {F}\left({P}\right){U}\left({i}\right)={F}\left({Q}\right){U}\left({i}\right)$
62 60 61 oveq12d ${⊢}{F}\left({P}\right)={F}\left({Q}\right)\to \left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)$
63 oveq2 ${⊢}{F}\left({P}\right)={F}\left({R}\right)\to 1-{F}\left({P}\right)=1-{F}\left({R}\right)$
64 63 oveq1d ${⊢}{F}\left({P}\right)={F}\left({R}\right)\to \left(1-{F}\left({P}\right)\right){Z}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)$
65 oveq1 ${⊢}{F}\left({P}\right)={F}\left({R}\right)\to {F}\left({P}\right){U}\left({i}\right)={F}\left({R}\right){U}\left({i}\right)$
66 64 65 oveq12d ${⊢}{F}\left({P}\right)={F}\left({R}\right)\to \left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)$
67 66 oveq2d ${⊢}{F}\left({P}\right)={F}\left({R}\right)\to 0\cdot \left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)=0\cdot \left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
68 67 oveq2d ${⊢}{F}\left({P}\right)={F}\left({R}\right)\to 1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)=1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
69 62 68 eqeqan12d ${⊢}\left({F}\left({P}\right)={F}\left({Q}\right)\wedge {F}\left({P}\right)={F}\left({R}\right)\right)\to \left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)=1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)↔\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
70 69 3ad2ant2 ${⊢}\left({F}\left({P}\right)\in ℂ\wedge \left({F}\left({P}\right)={F}\left({Q}\right)\wedge {F}\left({P}\right)={F}\left({R}\right)\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)=1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)↔\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
71 58 70 mpbid ${⊢}\left({F}\left({P}\right)\in ℂ\wedge \left({F}\left({P}\right)={F}\left({Q}\right)\wedge {F}\left({P}\right)={F}\left({R}\right)\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
72 19 32 33 38 43 71 syl122anc ${⊢}\left(\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
73 72 ralrimiva ${⊢}\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
74 oveq2 ${⊢}{t}=0\to 1-{t}=1-0$
75 1m0e1 ${⊢}1-0=1$
76 74 75 syl6eq ${⊢}{t}=0\to 1-{t}=1$
77 76 oveq1d ${⊢}{t}=0\to \left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)=1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)$
78 oveq1 ${⊢}{t}=0\to {t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)=0\cdot \left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
79 77 78 oveq12d ${⊢}{t}=0\to \left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)=1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
80 79 eqeq2d ${⊢}{t}=0\to \left(\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)↔\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
81 80 ralbidv ${⊢}{t}=0\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
82 81 rspcev ${⊢}\left(0\in \left[0,1\right]\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=1\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+0\cdot \left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
83 13 73 82 sylancr ${⊢}\left({F}\left({P}\right)={F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
84 83 ex ${⊢}{F}\left({P}\right)={F}\left({R}\right)\to \left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
85 26 adantl ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)$
86 85 29 syl ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({Q}\right)\in ℝ$
87 simplr3 ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\to {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)$
88 87 adantl ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)$
89 elrege0 ${⊢}{F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)↔\left({F}\left({R}\right)\in ℝ\wedge 0\le {F}\left({R}\right)\right)$
90 89 simplbi ${⊢}{F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\to {F}\left({R}\right)\in ℝ$
91 88 90 syl ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({R}\right)\in ℝ$
92 14 adantl ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)$
93 92 17 syl ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({P}\right)\in ℝ$
94 simprrr ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({Q}\right)\le {F}\left({R}\right)$
95 86 91 93 94 lesub1dd ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({Q}\right)-{F}\left({P}\right)\le {F}\left({R}\right)-{F}\left({P}\right)$
96 86 93 resubcld ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({Q}\right)-{F}\left({P}\right)\in ℝ$
97 simprrl ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({P}\right)\le {F}\left({Q}\right)$
98 86 93 subge0d ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to \left(0\le {F}\left({Q}\right)-{F}\left({P}\right)↔{F}\left({P}\right)\le {F}\left({Q}\right)\right)$
99 97 98 mpbird ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to 0\le {F}\left({Q}\right)-{F}\left({P}\right)$
100 91 93 resubcld ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({R}\right)-{F}\left({P}\right)\in ℝ$
101 93 86 91 97 94 letrd ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({P}\right)\le {F}\left({R}\right)$
102 simpl ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({P}\right)\ne {F}\left({R}\right)$
103 102 necomd ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({R}\right)\ne {F}\left({P}\right)$
104 93 91 101 103 leneltd ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {F}\left({P}\right)<{F}\left({R}\right)$
105 93 91 posdifd ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to \left({F}\left({P}\right)<{F}\left({R}\right)↔0<{F}\left({R}\right)-{F}\left({P}\right)\right)$
106 104 105 mpbid ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to 0<{F}\left({R}\right)-{F}\left({P}\right)$
107 divelunit ${⊢}\left(\left({F}\left({Q}\right)-{F}\left({P}\right)\in ℝ\wedge 0\le {F}\left({Q}\right)-{F}\left({P}\right)\right)\wedge \left({F}\left({R}\right)-{F}\left({P}\right)\in ℝ\wedge 0<{F}\left({R}\right)-{F}\left({P}\right)\right)\right)\to \left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\in \left[0,1\right]↔{F}\left({Q}\right)-{F}\left({P}\right)\le {F}\left({R}\right)-{F}\left({P}\right)\right)$
108 96 99 100 106 107 syl22anc ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to \left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\in \left[0,1\right]↔{F}\left({Q}\right)-{F}\left({P}\right)\le {F}\left({R}\right)-{F}\left({P}\right)\right)$
109 95 108 mpbird ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to \frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\in \left[0,1\right]$
110 14 ad2antlr ${⊢}\left(\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)$
111 17 recnd ${⊢}{F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\to {F}\left({P}\right)\in ℂ$
112 110 111 syl ${⊢}\left(\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({P}\right)\in ℂ$
113 simpll ${⊢}\left(\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({P}\right)\ne {F}\left({R}\right)$
114 26 ad2antlr ${⊢}\left(\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)$
115 29 recnd ${⊢}{F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\to {F}\left({Q}\right)\in ℂ$
116 114 115 syl ${⊢}\left(\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({Q}\right)\in ℂ$
117 87 ad2antlr ${⊢}\left(\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)$
118 90 recnd ${⊢}{F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\to {F}\left({R}\right)\in ℂ$
119 117 118 syl ${⊢}\left(\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {F}\left({R}\right)\in ℂ$
120 34 ad2antrl ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {Z}\in 𝔼\left({N}\right)$
121 120 37 sylan ${⊢}\left(\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\left({i}\right)\in ℂ$
122 39 ad2antrl ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to {U}\in 𝔼\left({N}\right)$
123 122 42 sylan ${⊢}\left(\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {U}\left({i}\right)\in ℂ$
124 simp2r ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({R}\right)\in ℂ$
125 simp2l ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({Q}\right)\in ℂ$
126 124 125 subcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({R}\right)-{F}\left({Q}\right)\in ℂ$
127 simp1l ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({P}\right)\in ℂ$
128 44 127 46 sylancr ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 1-{F}\left({P}\right)\in ℂ$
129 126 128 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)\in ℂ$
130 125 127 subcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({Q}\right)-{F}\left({P}\right)\in ℂ$
131 subcl ${⊢}\left(1\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\to 1-{F}\left({R}\right)\in ℂ$
132 44 124 131 sylancr ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 1-{F}\left({R}\right)\in ℂ$
133 130 132 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)\in ℂ$
134 124 127 subcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({R}\right)-{F}\left({P}\right)\in ℂ$
135 simp1r ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({P}\right)\ne {F}\left({R}\right)$
136 135 necomd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({R}\right)\ne {F}\left({P}\right)$
137 124 127 136 subne0d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({R}\right)-{F}\left({P}\right)\ne 0$
138 129 133 134 137 divdird ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{\left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)}{{F}\left({R}\right)-{F}\left({P}\right)}=\left(\frac{\left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)+\left(\frac{\left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)$
139 134 mulid1d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({P}\right)\right)\cdot 1={F}\left({R}\right)-{F}\left({P}\right)$
140 134 125 mulcomd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({P}\right)\right){F}\left({Q}\right)={F}\left({Q}\right)\left({F}\left({R}\right)-{F}\left({P}\right)\right)$
141 125 124 127 subdid ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({Q}\right)\left({F}\left({R}\right)-{F}\left({P}\right)\right)={F}\left({Q}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)$
142 140 141 eqtrd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({P}\right)\right){F}\left({Q}\right)={F}\left({Q}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)$
143 139 142 oveq12d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({P}\right)\right)\cdot 1-\left({F}\left({R}\right)-{F}\left({P}\right)\right){F}\left({Q}\right)={F}\left({R}\right)-{F}\left({P}\right)-\left({F}\left({Q}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)\right)$
144 subdi ${⊢}\left({F}\left({R}\right)-{F}\left({P}\right)\in ℂ\wedge 1\in ℂ\wedge {F}\left({Q}\right)\in ℂ\right)\to \left({F}\left({R}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({Q}\right)\right)=\left({F}\left({R}\right)-{F}\left({P}\right)\right)\cdot 1-\left({F}\left({R}\right)-{F}\left({P}\right)\right){F}\left({Q}\right)$
145 44 144 mp3an2 ${⊢}\left({F}\left({R}\right)-{F}\left({P}\right)\in ℂ\wedge {F}\left({Q}\right)\in ℂ\right)\to \left({F}\left({R}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({Q}\right)\right)=\left({F}\left({R}\right)-{F}\left({P}\right)\right)\cdot 1-\left({F}\left({R}\right)-{F}\left({P}\right)\right){F}\left({Q}\right)$
146 134 125 145 syl2anc ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({Q}\right)\right)=\left({F}\left({R}\right)-{F}\left({P}\right)\right)\cdot 1-\left({F}\left({R}\right)-{F}\left({P}\right)\right){F}\left({Q}\right)$
147 subdi ${⊢}\left({F}\left({R}\right)-{F}\left({Q}\right)\in ℂ\wedge 1\in ℂ\wedge {F}\left({P}\right)\in ℂ\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)=\left({F}\left({R}\right)-{F}\left({Q}\right)\right)\cdot 1-\left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)$
148 44 147 mp3an2 ${⊢}\left({F}\left({R}\right)-{F}\left({Q}\right)\in ℂ\wedge {F}\left({P}\right)\in ℂ\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)=\left({F}\left({R}\right)-{F}\left({Q}\right)\right)\cdot 1-\left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)$
149 126 127 148 syl2anc ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)=\left({F}\left({R}\right)-{F}\left({Q}\right)\right)\cdot 1-\left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)$
150 126 mulid1d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right)\cdot 1={F}\left({R}\right)-{F}\left({Q}\right)$
151 124 125 127 subdird ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)={F}\left({R}\right){F}\left({P}\right)-{F}\left({Q}\right){F}\left({P}\right)$
152 124 127 mulcomd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({R}\right){F}\left({P}\right)={F}\left({P}\right){F}\left({R}\right)$
153 152 oveq1d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({R}\right){F}\left({P}\right)-{F}\left({Q}\right){F}\left({P}\right)={F}\left({P}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)$
154 151 153 eqtrd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)={F}\left({P}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)$
155 150 154 oveq12d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right)\cdot 1-\left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)={F}\left({R}\right)-{F}\left({Q}\right)-\left({F}\left({P}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)\right)$
156 149 155 eqtrd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)={F}\left({R}\right)-{F}\left({Q}\right)-\left({F}\left({P}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)\right)$
157 subdi ${⊢}\left({F}\left({Q}\right)-{F}\left({P}\right)\in ℂ\wedge 1\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\to \left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)=\left({F}\left({Q}\right)-{F}\left({P}\right)\right)\cdot 1-\left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)$
158 44 157 mp3an2 ${⊢}\left({F}\left({Q}\right)-{F}\left({P}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\to \left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)=\left({F}\left({Q}\right)-{F}\left({P}\right)\right)\cdot 1-\left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)$
159 130 124 158 syl2anc ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)=\left({F}\left({Q}\right)-{F}\left({P}\right)\right)\cdot 1-\left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)$
160 130 mulid1d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({Q}\right)-{F}\left({P}\right)\right)\cdot 1={F}\left({Q}\right)-{F}\left({P}\right)$
161 125 127 124 subdird ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)={F}\left({Q}\right){F}\left({R}\right)-{F}\left({P}\right){F}\left({R}\right)$
162 160 161 oveq12d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({Q}\right)-{F}\left({P}\right)\right)\cdot 1-\left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)={F}\left({Q}\right)-{F}\left({P}\right)-\left({F}\left({Q}\right){F}\left({R}\right)-{F}\left({P}\right){F}\left({R}\right)\right)$
163 159 162 eqtrd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)={F}\left({Q}\right)-{F}\left({P}\right)-\left({F}\left({Q}\right){F}\left({R}\right)-{F}\left({P}\right){F}\left({R}\right)\right)$
164 156 163 oveq12d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)=\left({F}\left({R}\right)-{F}\left({Q}\right)-\left({F}\left({P}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)\right)\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right)-\left({F}\left({Q}\right){F}\left({R}\right)-{F}\left({P}\right){F}\left({R}\right)\right)$
165 127 124 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({P}\right){F}\left({R}\right)\in ℂ$
166 125 127 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({Q}\right){F}\left({P}\right)\in ℂ$
167 165 166 subcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({P}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)\in ℂ$
168 mulcl ${⊢}\left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\to {F}\left({Q}\right){F}\left({R}\right)\in ℂ$
169 168 3ad2ant2 ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({Q}\right){F}\left({R}\right)\in ℂ$
170 169 165 subcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({Q}\right){F}\left({R}\right)-{F}\left({P}\right){F}\left({R}\right)\in ℂ$
171 126 130 167 170 addsub4d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right)-\left(\left({F}\left({P}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)\right)+{F}\left({Q}\right){F}\left({R}\right)-{F}\left({P}\right){F}\left({R}\right)\right)=\left({F}\left({R}\right)-{F}\left({Q}\right)-\left({F}\left({P}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)\right)\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right)-\left({F}\left({Q}\right){F}\left({R}\right)-{F}\left({P}\right){F}\left({R}\right)\right)$
172 124 125 127 npncand ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right)+{F}\left({Q}\right)-{F}\left({P}\right)={F}\left({R}\right)-{F}\left({P}\right)$
173 165 166 169 npncan3d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({P}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)\right)+{F}\left({Q}\right){F}\left({R}\right)-{F}\left({P}\right){F}\left({R}\right)={F}\left({Q}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)$
174 172 173 oveq12d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right)-\left(\left({F}\left({P}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)\right)+{F}\left({Q}\right){F}\left({R}\right)-{F}\left({P}\right){F}\left({R}\right)\right)={F}\left({R}\right)-{F}\left({P}\right)-\left({F}\left({Q}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)\right)$
175 164 171 174 3eqtr2d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)={F}\left({R}\right)-{F}\left({P}\right)-\left({F}\left({Q}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)\right)$
176 143 146 175 3eqtr4d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({Q}\right)\right)=\left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)$
177 129 133 addcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)\in ℂ$
178 subcl ${⊢}\left(1\in ℂ\wedge {F}\left({Q}\right)\in ℂ\right)\to 1-{F}\left({Q}\right)\in ℂ$
179 44 125 178 sylancr ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 1-{F}\left({Q}\right)\in ℂ$
180 177 134 179 137 divmuld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{\left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)}{{F}\left({R}\right)-{F}\left({P}\right)}=1-{F}\left({Q}\right)↔\left({F}\left({R}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({Q}\right)\right)=\left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)\right)$
181 176 180 mpbird ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{\left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)}{{F}\left({R}\right)-{F}\left({P}\right)}=1-{F}\left({Q}\right)$
182 126 128 134 137 div23d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{\left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)}{{F}\left({R}\right)-{F}\left({P}\right)}=\left(\frac{{F}\left({R}\right)-{F}\left({Q}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({P}\right)\right)$
183 134 130 134 137 divsubdird ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{{F}\left({R}\right)-{F}\left({P}\right)-\left({F}\left({Q}\right)-{F}\left({P}\right)\right)}{{F}\left({R}\right)-{F}\left({P}\right)}=\left(\frac{{F}\left({R}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)$
184 124 125 127 nnncan2d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({R}\right)-{F}\left({P}\right)-\left({F}\left({Q}\right)-{F}\left({P}\right)\right)={F}\left({R}\right)-{F}\left({Q}\right)$
185 184 oveq1d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{{F}\left({R}\right)-{F}\left({P}\right)-\left({F}\left({Q}\right)-{F}\left({P}\right)\right)}{{F}\left({R}\right)-{F}\left({P}\right)}=\frac{{F}\left({R}\right)-{F}\left({Q}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}$
186 134 137 dividd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{{F}\left({R}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}=1$
187 186 oveq1d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{{F}\left({R}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)=1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)$
188 183 185 187 3eqtr3d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{{F}\left({R}\right)-{F}\left({Q}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}=1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)$
189 188 oveq1d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{{F}\left({R}\right)-{F}\left({Q}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({P}\right)\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right)$
190 182 189 eqtrd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{\left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)}{{F}\left({R}\right)-{F}\left({P}\right)}=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right)$
191 130 132 134 137 div23d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{\left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)}{{F}\left({R}\right)-{F}\left({P}\right)}=\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right)$
192 190 191 oveq12d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{\left({F}\left({R}\right)-{F}\left({Q}\right)\right)\left(1-{F}\left({P}\right)\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)+\left(\frac{\left({F}\left({Q}\right)-{F}\left({P}\right)\right)\left(1-{F}\left({R}\right)\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right)$
193 138 181 192 3eqtr3d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 1-{F}\left({Q}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right)$
194 193 oveq1d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)=\left(\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right)\right){Z}\left({i}\right)$
195 126 127 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)\in ℂ$
196 130 124 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)\in ℂ$
197 195 196 134 137 divdird ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{\left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}=\left(\frac{\left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)+\left(\frac{\left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)$
198 154 161 oveq12d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)=\left({F}\left({P}\right){F}\left({R}\right)-{F}\left({Q}\right){F}\left({P}\right)\right)+{F}\left({Q}\right){F}\left({R}\right)-{F}\left({P}\right){F}\left({R}\right)$
199 173 198 142 3eqtr4rd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({P}\right)\right){F}\left({Q}\right)=\left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)$
200 195 196 addcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)\in ℂ$
201 200 134 125 137 divmuld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{\left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}={F}\left({Q}\right)↔\left({F}\left({R}\right)-{F}\left({P}\right)\right){F}\left({Q}\right)=\left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)\right)$
202 199 201 mpbird ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{\left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)+\left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}={F}\left({Q}\right)$
203 126 127 134 137 div23d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{\left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}=\left(\frac{{F}\left({R}\right)-{F}\left({Q}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({P}\right)$
204 188 oveq1d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{{F}\left({R}\right)-{F}\left({Q}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({P}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right)$
205 203 204 eqtrd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{\left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right)$
206 130 124 134 137 div23d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{\left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}=\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right)$
207 205 206 oveq12d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{\left({F}\left({R}\right)-{F}\left({Q}\right)\right){F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)+\left(\frac{\left({F}\left({Q}\right)-{F}\left({P}\right)\right){F}\left({R}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right)$
208 197 202 207 3eqtr3d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({Q}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right)$
209 208 oveq1d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({Q}\right){U}\left({i}\right)=\left(\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right)\right){U}\left({i}\right)$
210 194 209 oveq12d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right)\right){Z}\left({i}\right)+\left(\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right)\right){U}\left({i}\right)$
211 130 134 137 divcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\in ℂ$
212 subcl ${⊢}\left(1\in ℂ\wedge \frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\in ℂ\right)\to 1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\in ℂ$
213 44 211 212 sylancr ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\in ℂ$
214 simp3l ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {Z}\left({i}\right)\in ℂ$
215 128 214 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{F}\left({P}\right)\right){Z}\left({i}\right)\in ℂ$
216 213 215 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)\in ℂ$
217 132 214 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{F}\left({R}\right)\right){Z}\left({i}\right)\in ℂ$
218 211 217 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)\in ℂ$
219 simp3r ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {U}\left({i}\right)\in ℂ$
220 127 219 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({P}\right){U}\left({i}\right)\in ℂ$
221 213 220 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right){U}\left({i}\right)\in ℂ$
222 124 219 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {F}\left({R}\right){U}\left({i}\right)\in ℂ$
223 211 222 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right){U}\left({i}\right)\in ℂ$
224 216 218 221 223 add4d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right){U}\left({i}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right){U}\left({i}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right){U}\left({i}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right){U}\left({i}\right)$
225 213 128 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right)\in ℂ$
226 211 132 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right)\in ℂ$
227 213 128 214 mulassd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)$
228 211 132 214 mulassd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)=\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)$
229 227 228 oveq12d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)$
230 225 214 226 229 joinlmuladdmuld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right)\right){Z}\left({i}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)$
231 213 127 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right)\in ℂ$
232 211 124 mulcld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right)\in ℂ$
233 213 127 219 mulassd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right){U}\left({i}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right){U}\left({i}\right)$
234 211 124 219 mulassd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right){U}\left({i}\right)=\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right){U}\left({i}\right)$
235 233 234 oveq12d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right){U}\left({i}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right){U}\left({i}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right){U}\left({i}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right){U}\left({i}\right)$
236 231 219 232 235 joinlmuladdmuld ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right)\right){U}\left({i}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right){U}\left({i}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right){U}\left({i}\right)$
237 230 236 oveq12d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right)\right){Z}\left({i}\right)+\left(\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right)\right){U}\left({i}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right){U}\left({i}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right){U}\left({i}\right)$
238 213 215 220 adddid ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right){U}\left({i}\right)$
239 211 217 222 adddid ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)=\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right){U}\left({i}\right)$
240 238 239 oveq12d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right){U}\left({i}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right){U}\left({i}\right)$
241 224 237 240 3eqtr4rd ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)=\left(\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(1-{F}\left({P}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(1-{F}\left({R}\right)\right)\right){Z}\left({i}\right)+\left(\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right){F}\left({P}\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right){F}\left({R}\right)\right){U}\left({i}\right)$
242 210 241 eqtr4d ${⊢}\left(\left({F}\left({P}\right)\in ℂ\wedge {F}\left({P}\right)\ne {F}\left({R}\right)\right)\wedge \left({F}\left({Q}\right)\in ℂ\wedge {F}\left({R}\right)\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
243 112 113 116 119 121 123 242 syl222anc ${⊢}\left(\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
244 243 ralrimiva ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
245 oveq2 ${⊢}{t}=\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\to 1-{t}=1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)$
246 245 oveq1d ${⊢}{t}=\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\to \left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)$
247 oveq1 ${⊢}{t}=\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\to {t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)=\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
248 246 247 oveq12d ${⊢}{t}=\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\to \left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
249 248 eqeq2d ${⊢}{t}=\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\to \left(\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)↔\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
250 249 ralbidv ${⊢}{t}=\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
251 250 rspcev ${⊢}\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\in \left[0,1\right]\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+\left(\frac{{F}\left({Q}\right)-{F}\left({P}\right)}{{F}\left({R}\right)-{F}\left({P}\right)}\right)\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
252 109 244 251 syl2anc ${⊢}\left({F}\left({P}\right)\ne {F}\left({R}\right)\wedge \left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
253 252 ex ${⊢}{F}\left({P}\right)\ne {F}\left({R}\right)\to \left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
254 84 253 pm2.61ine ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
255 r19.26-3 ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge {Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\wedge {R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)↔\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
256 simp2 ${⊢}\left({P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge {Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\wedge {R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\to {Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)$
257 oveq2 ${⊢}{P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\to \left(1-{t}\right){P}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)$
258 oveq2 ${⊢}{R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\to {t}{R}\left({i}\right)={t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
259 257 258 oveqan12d ${⊢}\left({P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge {R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\to \left(1-{t}\right){P}\left({i}\right)+{t}{R}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
260 259 3adant2 ${⊢}\left({P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge {Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\wedge {R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\to \left(1-{t}\right){P}\left({i}\right)+{t}{R}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)$
261 256 260 eqeq12d ${⊢}\left({P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge {Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\wedge {R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\to \left({Q}\left({i}\right)=\left(1-{t}\right){P}\left({i}\right)+{t}{R}\left({i}\right)↔\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
262 261 ralimi ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge {Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\wedge {R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({Q}\left({i}\right)=\left(1-{t}\right){P}\left({i}\right)+{t}{R}\left({i}\right)↔\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
263 ralbi ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({Q}\left({i}\right)=\left(1-{t}\right){P}\left({i}\right)+{t}{R}\left({i}\right)↔\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{t}\right){P}\left({i}\right)+{t}{R}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
264 262 263 syl ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge {Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\wedge {R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{t}\right){P}\left({i}\right)+{t}{R}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
265 264 rexbidv ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge {Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\wedge {R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\to \left(\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{t}\right){P}\left({i}\right)+{t}{R}\left({i}\right)↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)$
266 265 biimprcd ${⊢}\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge {Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\wedge {R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{t}\right){P}\left({i}\right)+{t}{R}\left({i}\right)\right)$
267 255 266 syl5bir ${⊢}\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)=\left(1-{t}\right)\left(\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\right)+{t}\left(\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\to \left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{t}\right){P}\left({i}\right)+{t}{R}\left({i}\right)\right)$
268 254 267 syl ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\to \left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{t}\right){P}\left({i}\right)+{t}{R}\left({i}\right)\right)$
269 268 an32s ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\wedge \left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)\to \left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{t}\right){P}\left({i}\right)+{t}{R}\left({i}\right)\right)$
270 269 expimpd ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\to \left(\left(\left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{t}\right){P}\left({i}\right)+{t}{R}\left({i}\right)\right)$
271 270 adantlr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({P}\in {D}\wedge {Q}\in {D}\wedge {R}\in {D}\right)\right)\wedge \left({F}\left({P}\right)\le {F}\left({Q}\right)\wedge {F}\left({Q}\right)\le {F}\left({R}\right)\right)\right)\to \left(\left(\left({F}\left({P}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({Q}\right)\in \left[0,\mathrm{+\infty }\right)\wedge {F}\left({R}\right)\in \left[0,\mathrm{+\infty }\right)\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)=\left(1-{F}\left({P}\right)\right){Z}\left({i}\right)+{F}\left({P}\right){U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{F}\left({Q}\right)\right){Z}\left({i}\right)+{F}\left({Q}\right){U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{R}\left({i}\right)=\left(1-{F}\left({R}\right)\right){Z}\left({i}\right)+{F}\left({R}\right){U}\left({i}\right)\right)\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)=\left(1-{t}\right){P}\left({i}\right)+{t}{R}\left({i}\right)\right)$
272 12 271 syl5bi ${⊢}\left(\right)$