Metamath Proof Explorer

Theorem iccf1o

Description: Describe a bijection from [ 0 , 1 ] to an arbitrary nontrivial closed interval [ A , B ] . (Contributed by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypothesis iccf1o.1 ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) )
Assertion iccf1o ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 𝐴 [,] 𝐵 ) ∧ ◡ 𝐹 = ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 iccf1o.1 ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) )
2 elicc01 ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) )
3 2 simp1bi ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → 𝑥 ∈ ℝ )
4 3 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → 𝑥 ∈ ℝ )
5 4 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → 𝑥 ∈ ℂ )
6 simpl2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → 𝐵 ∈ ℝ )
7 6 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → 𝐵 ∈ ℂ )
8 5 7 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 𝑥 · 𝐵 ) ∈ ℂ )
9 ax-1cn ⊢ 1 ∈ ℂ
10 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 1 − 𝑥 ) ∈ ℂ )
11 9 5 10 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 1 − 𝑥 ) ∈ ℂ )
12 simpl1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → 𝐴 ∈ ℝ )
13 12 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → 𝐴 ∈ ℂ )
14 11 13 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑥 ) · 𝐴 ) ∈ ℂ )
15 8 14 addcomd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) = ( ( ( 1 − 𝑥 ) · 𝐴 ) + ( 𝑥 · 𝐵 ) ) )
16 lincmb01cmp ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑥 ) · 𝐴 ) + ( 𝑥 · 𝐵 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
17 15 16 eqeltrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
18 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
19 simpl1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℝ )
20 simpl2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ )
21 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) )
22 21 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) )
23 22 biimpa ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) )
24 23 simp1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑦 ∈ ℝ )
25 eqid ⊢ ( 𝐴 − 𝐴 ) = ( 𝐴 − 𝐴 )
26 eqid ⊢ ( 𝐵 − 𝐴 ) = ( 𝐵 − 𝐴 )
27 25 26 iccshftl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 − 𝐴 ) ∈ ( ( 𝐴 − 𝐴 ) [,] ( 𝐵 − 𝐴 ) ) ) )
28 19 20 24 19 27 syl22anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 − 𝐴 ) ∈ ( ( 𝐴 − 𝐴 ) [,] ( 𝐵 − 𝐴 ) ) ) )
29 18 28 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 − 𝐴 ) ∈ ( ( 𝐴 − 𝐴 ) [,] ( 𝐵 − 𝐴 ) ) )
30 24 19 resubcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 − 𝐴 ) ∈ ℝ )
31 30 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 − 𝐴 ) ∈ ℂ )
32 difrp ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( 𝐵 − 𝐴 ) ∈ ℝ+ ) )
33 32 biimp3a ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐵 − 𝐴 ) ∈ ℝ+ )
34 33 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐵 − 𝐴 ) ∈ ℝ+ )
35 34 rpcnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐵 − 𝐴 ) ∈ ℂ )
36 34 rpne0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐵 − 𝐴 ) ≠ 0 )
37 31 35 36 divcan1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · ( 𝐵 − 𝐴 ) ) = ( 𝑦 − 𝐴 ) )
38 35 mul02d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 0 · ( 𝐵 − 𝐴 ) ) = 0 )
39 19 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℂ )
40 39 subidd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 − 𝐴 ) = 0 )
41 38 40 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 0 · ( 𝐵 − 𝐴 ) ) = ( 𝐴 − 𝐴 ) )
42 35 mulid2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 1 · ( 𝐵 − 𝐴 ) ) = ( 𝐵 − 𝐴 ) )
43 41 42 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 0 · ( 𝐵 − 𝐴 ) ) [,] ( 1 · ( 𝐵 − 𝐴 ) ) ) = ( ( 𝐴 − 𝐴 ) [,] ( 𝐵 − 𝐴 ) ) )
44 29 37 43 3eltr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · ( 𝐵 − 𝐴 ) ) ∈ ( ( 0 · ( 𝐵 − 𝐴 ) ) [,] ( 1 · ( 𝐵 − 𝐴 ) ) ) )
45 0red ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 0 ∈ ℝ )
46 1red ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 1 ∈ ℝ )
47 30 34 rerpdivcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ∈ ℝ )
48 eqid ⊢ ( 0 · ( 𝐵 − 𝐴 ) ) = ( 0 · ( 𝐵 − 𝐴 ) )
49 eqid ⊢ ( 1 · ( 𝐵 − 𝐴 ) ) = ( 1 · ( 𝐵 − 𝐴 ) )
50 48 49 iccdil ⊢ ( ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ∈ ℝ ∧ ( 𝐵 − 𝐴 ) ∈ ℝ+ ) ) → ( ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ∈ ( 0 [,] 1 ) ↔ ( ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · ( 𝐵 − 𝐴 ) ) ∈ ( ( 0 · ( 𝐵 − 𝐴 ) ) [,] ( 1 · ( 𝐵 − 𝐴 ) ) ) ) )
51 45 46 47 34 50 syl22anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ∈ ( 0 [,] 1 ) ↔ ( ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · ( 𝐵 − 𝐴 ) ) ∈ ( ( 0 · ( 𝐵 − 𝐴 ) ) [,] ( 1 · ( 𝐵 − 𝐴 ) ) ) ) )
52 44 51 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ∈ ( 0 [,] 1 ) )
53 eqcom ⊢ ( 𝑥 = ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ↔ ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) = 𝑥 )
54 31 adantrl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑦 − 𝐴 ) ∈ ℂ )
55 5 adantrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑥 ∈ ℂ )
56 35 adantrl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐵 − 𝐴 ) ∈ ℂ )
57 36 adantrl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐵 − 𝐴 ) ≠ 0 )
58 54 55 56 57 divmul3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) = 𝑥 ↔ ( 𝑦 − 𝐴 ) = ( 𝑥 · ( 𝐵 − 𝐴 ) ) ) )
59 53 58 syl5bb ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 = ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ↔ ( 𝑦 − 𝐴 ) = ( 𝑥 · ( 𝐵 − 𝐴 ) ) ) )
60 24 adantrl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑦 ∈ ℝ )
61 60 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑦 ∈ ℂ )
62 39 adantrl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝐴 ∈ ℂ )
63 6 12 resubcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
64 4 63 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 𝑥 · ( 𝐵 − 𝐴 ) ) ∈ ℝ )
65 64 adantrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 · ( 𝐵 − 𝐴 ) ) ∈ ℝ )
66 65 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 · ( 𝐵 − 𝐴 ) ) ∈ ℂ )
67 61 62 66 subadd2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝑦 − 𝐴 ) = ( 𝑥 · ( 𝐵 − 𝐴 ) ) ↔ ( ( 𝑥 · ( 𝐵 − 𝐴 ) ) + 𝐴 ) = 𝑦 ) )
68 eqcom ⊢ ( ( ( 𝑥 · ( 𝐵 − 𝐴 ) ) + 𝐴 ) = 𝑦 ↔ 𝑦 = ( ( 𝑥 · ( 𝐵 − 𝐴 ) ) + 𝐴 ) )
69 67 68 bitrdi ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝑦 − 𝐴 ) = ( 𝑥 · ( 𝐵 − 𝐴 ) ) ↔ 𝑦 = ( ( 𝑥 · ( 𝐵 − 𝐴 ) ) + 𝐴 ) ) )
70 5 13 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 𝑥 · 𝐴 ) ∈ ℂ )
71 8 70 13 subadd23d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( ( 𝑥 · 𝐵 ) − ( 𝑥 · 𝐴 ) ) + 𝐴 ) = ( ( 𝑥 · 𝐵 ) + ( 𝐴 − ( 𝑥 · 𝐴 ) ) ) )
72 5 7 13 subdid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 𝑥 · ( 𝐵 − 𝐴 ) ) = ( ( 𝑥 · 𝐵 ) − ( 𝑥 · 𝐴 ) ) )
73 72 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑥 · ( 𝐵 − 𝐴 ) ) + 𝐴 ) = ( ( ( 𝑥 · 𝐵 ) − ( 𝑥 · 𝐴 ) ) + 𝐴 ) )
74 1cnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → 1 ∈ ℂ )
75 74 5 13 subdird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑥 ) · 𝐴 ) = ( ( 1 · 𝐴 ) − ( 𝑥 · 𝐴 ) ) )
76 13 mulid2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 1 · 𝐴 ) = 𝐴 )
77 76 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 1 · 𝐴 ) − ( 𝑥 · 𝐴 ) ) = ( 𝐴 − ( 𝑥 · 𝐴 ) ) )
78 75 77 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑥 ) · 𝐴 ) = ( 𝐴 − ( 𝑥 · 𝐴 ) ) )
79 78 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) = ( ( 𝑥 · 𝐵 ) + ( 𝐴 − ( 𝑥 · 𝐴 ) ) ) )
80 71 73 79 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑥 · ( 𝐵 − 𝐴 ) ) + 𝐴 ) = ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) )
81 80 adantrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝑥 · ( 𝐵 − 𝐴 ) ) + 𝐴 ) = ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) )
82 81 eqeq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑦 = ( ( 𝑥 · ( 𝐵 − 𝐴 ) ) + 𝐴 ) ↔ 𝑦 = ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) ) )
83 59 69 82 3bitrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 = ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ↔ 𝑦 = ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) ) )
84 1 17 52 83 f1ocnv2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 𝐴 [,] 𝐵 ) ∧ ◡ 𝐹 = ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) ) )