ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  iccf1o GIF version

Theorem iccf1o 9316
Description: Describe a bijection from [0, 1] to an arbitrary nontrivial closed interval [𝐴, 𝐵]. (Contributed by Mario Carneiro, 8-Sep-2015.)
Hypothesis
Ref Expression
iccf1o.1 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)))
Assertion
Ref Expression
iccf1o ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵) ∧ 𝐹 = (𝑦 ∈ (𝐴[,]𝐵) ↦ ((𝑦𝐴) / (𝐵𝐴)))))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦
Allowed substitution hints:   𝐹(𝑥,𝑦)

Proof of Theorem iccf1o
StepHypRef Expression
1 iccf1o.1 . 2 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)))
2 0re 7391 . . . . . . . . 9 0 ∈ ℝ
3 1re 7390 . . . . . . . . 9 1 ∈ ℝ
42, 3elicc2i 9252 . . . . . . . 8 (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ 1))
54simp1bi 954 . . . . . . 7 (𝑥 ∈ (0[,]1) → 𝑥 ∈ ℝ)
65adantl 271 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → 𝑥 ∈ ℝ)
76recnd 7419 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → 𝑥 ∈ ℂ)
8 simpl2 943 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → 𝐵 ∈ ℝ)
98recnd 7419 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → 𝐵 ∈ ℂ)
107, 9mulcld 7411 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (𝑥 · 𝐵) ∈ ℂ)
11 ax-1cn 7341 . . . . . 6 1 ∈ ℂ
12 subcl 7584 . . . . . 6 ((1 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (1 − 𝑥) ∈ ℂ)
1311, 7, 12sylancr 405 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (1 − 𝑥) ∈ ℂ)
14 simpl1 942 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → 𝐴 ∈ ℝ)
1514recnd 7419 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → 𝐴 ∈ ℂ)
1613, 15mulcld 7411 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((1 − 𝑥) · 𝐴) ∈ ℂ)
1710, 16addcomd 7536 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)) = (((1 − 𝑥) · 𝐴) + (𝑥 · 𝐵)))
18 lincmb01cmp 9315 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (((1 − 𝑥) · 𝐴) + (𝑥 · 𝐵)) ∈ (𝐴[,]𝐵))
1917, 18eqeltrd 2159 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)) ∈ (𝐴[,]𝐵))
20 simpr 108 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ (𝐴[,]𝐵))
21 simpl1 942 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
22 simpl2 943 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
23 elicc2 9251 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴𝑦𝑦𝐵)))
24233adant3 959 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴𝑦𝑦𝐵)))
2524biimpa 290 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ ℝ ∧ 𝐴𝑦𝑦𝐵))
2625simp1d 951 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ)
27 eqid 2083 . . . . . . 7 (𝐴𝐴) = (𝐴𝐴)
28 eqid 2083 . . . . . . 7 (𝐵𝐴) = (𝐵𝐴)
2927, 28iccshftl 9308 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℝ ∧ 𝐴 ∈ ℝ)) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦𝐴) ∈ ((𝐴𝐴)[,](𝐵𝐴))))
3021, 22, 26, 21, 29syl22anc 1171 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦𝐴) ∈ ((𝐴𝐴)[,](𝐵𝐴))))
3120, 30mpbid 145 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦𝐴) ∈ ((𝐴𝐴)[,](𝐵𝐴)))
3226, 21resubcld 7762 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦𝐴) ∈ ℝ)
3332recnd 7419 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦𝐴) ∈ ℂ)
34 difrp 9065 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐵𝐴) ∈ ℝ+))
3534biimp3a 1277 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐵𝐴) ∈ ℝ+)
3635adantr 270 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐵𝐴) ∈ ℝ+)
3736rpcnd 9070 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐵𝐴) ∈ ℂ)
38 rpap0 9045 . . . . . 6 ((𝐵𝐴) ∈ ℝ+ → (𝐵𝐴) # 0)
3936, 38syl 14 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐵𝐴) # 0)
4033, 37, 39divcanap1d 8155 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝑦𝐴) / (𝐵𝐴)) · (𝐵𝐴)) = (𝑦𝐴))
4137mul02d 7773 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (0 · (𝐵𝐴)) = 0)
4221recnd 7419 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℂ)
4342subidd 7684 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐴𝐴) = 0)
4441, 43eqtr4d 2118 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (0 · (𝐵𝐴)) = (𝐴𝐴))
4537mulid2d 7409 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (1 · (𝐵𝐴)) = (𝐵𝐴))
4644, 45oveq12d 5609 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((0 · (𝐵𝐴))[,](1 · (𝐵𝐴))) = ((𝐴𝐴)[,](𝐵𝐴)))
4731, 40, 463eltr4d 2166 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝑦𝐴) / (𝐵𝐴)) · (𝐵𝐴)) ∈ ((0 · (𝐵𝐴))[,](1 · (𝐵𝐴))))
48 0red 7392 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 0 ∈ ℝ)
49 1red 7406 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 1 ∈ ℝ)
5032, 36rerpdivcld 9100 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝑦𝐴) / (𝐵𝐴)) ∈ ℝ)
51 eqid 2083 . . . . 5 (0 · (𝐵𝐴)) = (0 · (𝐵𝐴))
52 eqid 2083 . . . . 5 (1 · (𝐵𝐴)) = (1 · (𝐵𝐴))
5351, 52iccdil 9310 . . . 4 (((0 ∈ ℝ ∧ 1 ∈ ℝ) ∧ (((𝑦𝐴) / (𝐵𝐴)) ∈ ℝ ∧ (𝐵𝐴) ∈ ℝ+)) → (((𝑦𝐴) / (𝐵𝐴)) ∈ (0[,]1) ↔ (((𝑦𝐴) / (𝐵𝐴)) · (𝐵𝐴)) ∈ ((0 · (𝐵𝐴))[,](1 · (𝐵𝐴)))))
5448, 49, 50, 36, 53syl22anc 1171 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝑦𝐴) / (𝐵𝐴)) ∈ (0[,]1) ↔ (((𝑦𝐴) / (𝐵𝐴)) · (𝐵𝐴)) ∈ ((0 · (𝐵𝐴))[,](1 · (𝐵𝐴)))))
5547, 54mpbird 165 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝑦𝐴) / (𝐵𝐴)) ∈ (0[,]1))
56 eqcom 2085 . . . 4 (𝑥 = ((𝑦𝐴) / (𝐵𝐴)) ↔ ((𝑦𝐴) / (𝐵𝐴)) = 𝑥)
5733adantrl 462 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝑦𝐴) ∈ ℂ)
587adantrr 463 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → 𝑥 ∈ ℂ)
5937adantrl 462 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝐵𝐴) ∈ ℂ)
6039adantrl 462 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝐵𝐴) # 0)
6157, 58, 59, 60divmulap3d 8188 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (((𝑦𝐴) / (𝐵𝐴)) = 𝑥 ↔ (𝑦𝐴) = (𝑥 · (𝐵𝐴))))
6256, 61syl5bb 190 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝑥 = ((𝑦𝐴) / (𝐵𝐴)) ↔ (𝑦𝐴) = (𝑥 · (𝐵𝐴))))
6326adantrl 462 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ ℝ)
6463recnd 7419 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ ℂ)
6542adantrl 462 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → 𝐴 ∈ ℂ)
668, 14resubcld 7762 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (𝐵𝐴) ∈ ℝ)
676, 66remulcld 7421 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (𝑥 · (𝐵𝐴)) ∈ ℝ)
6867adantrr 463 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝑥 · (𝐵𝐴)) ∈ ℝ)
6968recnd 7419 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝑥 · (𝐵𝐴)) ∈ ℂ)
7064, 65, 69subadd2d 7715 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → ((𝑦𝐴) = (𝑥 · (𝐵𝐴)) ↔ ((𝑥 · (𝐵𝐴)) + 𝐴) = 𝑦))
71 eqcom 2085 . . . 4 (((𝑥 · (𝐵𝐴)) + 𝐴) = 𝑦𝑦 = ((𝑥 · (𝐵𝐴)) + 𝐴))
7270, 71syl6bb 194 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → ((𝑦𝐴) = (𝑥 · (𝐵𝐴)) ↔ 𝑦 = ((𝑥 · (𝐵𝐴)) + 𝐴)))
737, 15mulcld 7411 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (𝑥 · 𝐴) ∈ ℂ)
7410, 73, 15subadd23d 7718 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (((𝑥 · 𝐵) − (𝑥 · 𝐴)) + 𝐴) = ((𝑥 · 𝐵) + (𝐴 − (𝑥 · 𝐴))))
757, 9, 15subdid 7795 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (𝑥 · (𝐵𝐴)) = ((𝑥 · 𝐵) − (𝑥 · 𝐴)))
7675oveq1d 5606 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((𝑥 · (𝐵𝐴)) + 𝐴) = (((𝑥 · 𝐵) − (𝑥 · 𝐴)) + 𝐴))
77 1cnd 7407 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → 1 ∈ ℂ)
7877, 7, 15subdird 7796 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((1 − 𝑥) · 𝐴) = ((1 · 𝐴) − (𝑥 · 𝐴)))
7915mulid2d 7409 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (1 · 𝐴) = 𝐴)
8079oveq1d 5606 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((1 · 𝐴) − (𝑥 · 𝐴)) = (𝐴 − (𝑥 · 𝐴)))
8178, 80eqtrd 2115 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((1 − 𝑥) · 𝐴) = (𝐴 − (𝑥 · 𝐴)))
8281oveq2d 5607 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)) = ((𝑥 · 𝐵) + (𝐴 − (𝑥 · 𝐴))))
8374, 76, 823eqtr4d 2125 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((𝑥 · (𝐵𝐴)) + 𝐴) = ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)))
8483adantrr 463 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → ((𝑥 · (𝐵𝐴)) + 𝐴) = ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)))
8584eqeq2d 2094 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝑦 = ((𝑥 · (𝐵𝐴)) + 𝐴) ↔ 𝑦 = ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴))))
8662, 72, 853bitrd 212 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝑥 = ((𝑦𝐴) / (𝐵𝐴)) ↔ 𝑦 = ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴))))
871, 19, 55, 86f1ocnv2d 5783 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵) ∧ 𝐹 = (𝑦 ∈ (𝐴[,]𝐵) ↦ ((𝑦𝐴) / (𝐵𝐴)))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  w3a 920   = wceq 1285  wcel 1434   class class class wbr 3811  cmpt 3865  ccnv 4400  1-1-ontowf1o 4968  (class class class)co 5591  cc 7251  cr 7252  0cc0 7253  1c1 7254   + caddc 7256   · cmul 7258   < clt 7425  cle 7426  cmin 7556   # cap 7958   / cdiv 8037  +crp 9029  [,]cicc 9204
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-pow 3974  ax-pr 4000  ax-un 4224  ax-setind 4316  ax-cnex 7339  ax-resscn 7340  ax-1cn 7341  ax-1re 7342  ax-icn 7343  ax-addcl 7344  ax-addrcl 7345  ax-mulcl 7346  ax-mulrcl 7347  ax-addcom 7348  ax-mulcom 7349  ax-addass 7350  ax-mulass 7351  ax-distr 7352  ax-i2m1 7353  ax-0lt1 7354  ax-1rid 7355  ax-0id 7356  ax-rnegex 7357  ax-precex 7358  ax-cnre 7359  ax-pre-ltirr 7360  ax-pre-ltwlin 7361  ax-pre-lttrn 7362  ax-pre-apti 7363  ax-pre-ltadd 7364  ax-pre-mulgt0 7365  ax-pre-mulext 7366
This theorem depends on definitions:  df-bi 115  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-nel 2345  df-ral 2358  df-rex 2359  df-reu 2360  df-rmo 2361  df-rab 2362  df-v 2614  df-sbc 2827  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-br 3812  df-opab 3866  df-mpt 3867  df-id 4084  df-po 4087  df-iso 4088  df-xp 4407  df-rel 4408  df-cnv 4409  df-co 4410  df-dm 4411  df-rn 4412  df-iota 4934  df-fun 4971  df-fn 4972  df-f 4973  df-f1 4974  df-fo 4975  df-f1o 4976  df-fv 4977  df-riota 5547  df-ov 5594  df-oprab 5595  df-mpt2 5596  df-pnf 7427  df-mnf 7428  df-xr 7429  df-ltxr 7430  df-le 7431  df-sub 7558  df-neg 7559  df-reap 7952  df-ap 7959  df-div 8038  df-rp 9030  df-icc 9208
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator