iccf1o - Metamath Proof Explorer

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

Theorem iccf1o 12697

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**
Step	Hyp	Ref	Expression
1		iccf1o.1	. 2 ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)))
2		elicc01 12669	. . . . . . . 8 ⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))
3	2	simp1bi 1126	. . . . . . 7 ⊢ (𝑥 ∈ (0[,]1) → 𝑥 ∈ ℝ)
4	3	adantl 474	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → 𝑥 ∈ ℝ)
5	4	recnd 10467	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → 𝑥 ∈ ℂ)
6		simpl2 1173	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → 𝐵 ∈ ℝ)
7	6	recnd 10467	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → 𝐵 ∈ ℂ)
8	5, 7	mulcld 10459	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (𝑥 · 𝐵) ∈ ℂ)
9		ax-1cn 10392	. . . . . 6 ⊢ 1 ∈ ℂ
10		subcl 10684	. . . . . 6 ⊢ ((1 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (1 − 𝑥) ∈ ℂ)
11	9, 5, 10	sylancr 579	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (1 − 𝑥) ∈ ℂ)
12		simpl1 1172	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → 𝐴 ∈ ℝ)
13	12	recnd 10467	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → 𝐴 ∈ ℂ)
14	11, 13	mulcld 10459	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((1 − 𝑥) · 𝐴) ∈ ℂ)
15	8, 14	addcomd 10641	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)) = (((1 − 𝑥) · 𝐴) + (𝑥 · 𝐵)))
16		lincmb01cmp 12696	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (((1 − 𝑥) · 𝐴) + (𝑥 · 𝐵)) ∈ (𝐴[,]𝐵))
17	15, 16	eqeltrd 2861	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)) ∈ (𝐴[,]𝐵))
18		simpr 477	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ (𝐴[,]𝐵))
19		simpl1 1172	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
20		simpl2 1173	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
21		elicc2 12616	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)))
22	21	3adant3 1113	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)))
23	22	biimpa 469	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))
24	23	simp1d 1123	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ)
25		eqid 2773	. . . . . . 7 ⊢ (𝐴 − 𝐴) = (𝐴 − 𝐴)
26		eqid 2773	. . . . . . 7 ⊢ (𝐵 − 𝐴) = (𝐵 − 𝐴)
27	25, 26	iccshftl 12689	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℝ ∧ 𝐴 ∈ ℝ)) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 − 𝐴) ∈ ((𝐴 − 𝐴)[,](𝐵 − 𝐴))))
28	19, 20, 24, 19, 27	syl22anc 827	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 − 𝐴) ∈ ((𝐴 − 𝐴)[,](𝐵 − 𝐴))))
29	18, 28	mpbid 224	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 − 𝐴) ∈ ((𝐴 − 𝐴)[,](𝐵 − 𝐴)))
30	24, 19	resubcld 10868	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 − 𝐴) ∈ ℝ)
31	30	recnd 10467	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 − 𝐴) ∈ ℂ)
32		difrp 12243	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℝ⁺))
33	32	biimp3a 1449	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐵 − 𝐴) ∈ ℝ⁺)
34	33	adantr 473	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐵 − 𝐴) ∈ ℝ⁺)
35	34	rpcnd 12249	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐵 − 𝐴) ∈ ℂ)
36	34	rpne0d 12252	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐵 − 𝐴) ≠ 0)
37	31, 35, 36	divcan1d 11217	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝑦 − 𝐴) / (𝐵 − 𝐴)) · (𝐵 − 𝐴)) = (𝑦 − 𝐴))
38	35	mul02d 10637	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (0 · (𝐵 − 𝐴)) = 0)
39	19	recnd 10467	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℂ)
40	39	subidd 10785	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐴 − 𝐴) = 0)
41	38, 40	eqtr4d 2812	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (0 · (𝐵 − 𝐴)) = (𝐴 − 𝐴))
42	35	mulid2d 10457	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (1 · (𝐵 − 𝐴)) = (𝐵 − 𝐴))
43	41, 42	oveq12d 6993	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((0 · (𝐵 − 𝐴))[,](1 · (𝐵 − 𝐴))) = ((𝐴 − 𝐴)[,](𝐵 − 𝐴)))
44	29, 37, 43	3eltr4d 2876	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝑦 − 𝐴) / (𝐵 − 𝐴)) · (𝐵 − 𝐴)) ∈ ((0 · (𝐵 − 𝐴))[,](1 · (𝐵 − 𝐴))))
45		0red 10442	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 0 ∈ ℝ)
46		1red 10439	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 1 ∈ ℝ)
47	30, 34	rerpdivcld 12278	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝑦 − 𝐴) / (𝐵 − 𝐴)) ∈ ℝ)
48		eqid 2773	. . . . 5 ⊢ (0 · (𝐵 − 𝐴)) = (0 · (𝐵 − 𝐴))
49		eqid 2773	. . . . 5 ⊢ (1 · (𝐵 − 𝐴)) = (1 · (𝐵 − 𝐴))
50	48, 49	iccdil 12691	. . . 4 ⊢ (((0 ∈ ℝ ∧ 1 ∈ ℝ) ∧ (((𝑦 − 𝐴) / (𝐵 − 𝐴)) ∈ ℝ ∧ (𝐵 − 𝐴) ∈ ℝ⁺)) → (((𝑦 − 𝐴) / (𝐵 − 𝐴)) ∈ (0[,]1) ↔ (((𝑦 − 𝐴) / (𝐵 − 𝐴)) · (𝐵 − 𝐴)) ∈ ((0 · (𝐵 − 𝐴))[,](1 · (𝐵 − 𝐴)))))
51	45, 46, 47, 34, 50	syl22anc 827	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝑦 − 𝐴) / (𝐵 − 𝐴)) ∈ (0[,]1) ↔ (((𝑦 − 𝐴) / (𝐵 − 𝐴)) · (𝐵 − 𝐴)) ∈ ((0 · (𝐵 − 𝐴))[,](1 · (𝐵 − 𝐴)))))
52	44, 51	mpbird 249	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝑦 − 𝐴) / (𝐵 − 𝐴)) ∈ (0[,]1))
53		eqcom 2780	. . . 4 ⊢ (𝑥 = ((𝑦 − 𝐴) / (𝐵 − 𝐴)) ↔ ((𝑦 − 𝐴) / (𝐵 − 𝐴)) = 𝑥)
54	31	adantrl 704	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝑦 − 𝐴) ∈ ℂ)
55	5	adantrr 705	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → 𝑥 ∈ ℂ)
56	35	adantrl 704	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝐵 − 𝐴) ∈ ℂ)
57	36	adantrl 704	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝐵 − 𝐴) ≠ 0)
58	54, 55, 56, 57	divmul3d 11250	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (((𝑦 − 𝐴) / (𝐵 − 𝐴)) = 𝑥 ↔ (𝑦 − 𝐴) = (𝑥 · (𝐵 − 𝐴))))
59	53, 58	syl5bb 275	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝑥 = ((𝑦 − 𝐴) / (𝐵 − 𝐴)) ↔ (𝑦 − 𝐴) = (𝑥 · (𝐵 − 𝐴))))
60	24	adantrl 704	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ ℝ)
61	60	recnd 10467	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ ℂ)
62	39	adantrl 704	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → 𝐴 ∈ ℂ)
63	6, 12	resubcld 10868	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (𝐵 − 𝐴) ∈ ℝ)
64	4, 63	remulcld 10469	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (𝑥 · (𝐵 − 𝐴)) ∈ ℝ)
65	64	adantrr 705	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝑥 · (𝐵 − 𝐴)) ∈ ℝ)
66	65	recnd 10467	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝑥 · (𝐵 − 𝐴)) ∈ ℂ)
67	61, 62, 66	subadd2d 10816	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → ((𝑦 − 𝐴) = (𝑥 · (𝐵 − 𝐴)) ↔ ((𝑥 · (𝐵 − 𝐴)) + 𝐴) = 𝑦))
68		eqcom 2780	. . . 4 ⊢ (((𝑥 · (𝐵 − 𝐴)) + 𝐴) = 𝑦 ↔ 𝑦 = ((𝑥 · (𝐵 − 𝐴)) + 𝐴))
69	67, 68	syl6bb 279	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → ((𝑦 − 𝐴) = (𝑥 · (𝐵 − 𝐴)) ↔ 𝑦 = ((𝑥 · (𝐵 − 𝐴)) + 𝐴)))
70	5, 13	mulcld 10459	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (𝑥 · 𝐴) ∈ ℂ)
71	8, 70, 13	subadd23d 10819	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (((𝑥 · 𝐵) − (𝑥 · 𝐴)) + 𝐴) = ((𝑥 · 𝐵) + (𝐴 − (𝑥 · 𝐴))))
72	5, 7, 13	subdid 10896	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (𝑥 · (𝐵 − 𝐴)) = ((𝑥 · 𝐵) − (𝑥 · 𝐴)))
73	72	oveq1d 6990	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((𝑥 · (𝐵 − 𝐴)) + 𝐴) = (((𝑥 · 𝐵) − (𝑥 · 𝐴)) + 𝐴))
74		1cnd 10433	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → 1 ∈ ℂ)
75	74, 5, 13	subdird 10897	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((1 − 𝑥) · 𝐴) = ((1 · 𝐴) − (𝑥 · 𝐴)))
76	13	mulid2d 10457	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → (1 · 𝐴) = 𝐴)
77	76	oveq1d 6990	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((1 · 𝐴) − (𝑥 · 𝐴)) = (𝐴 − (𝑥 · 𝐴)))
78	75, 77	eqtrd 2809	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((1 − 𝑥) · 𝐴) = (𝐴 − (𝑥 · 𝐴)))
79	78	oveq2d 6991	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)) = ((𝑥 · 𝐵) + (𝐴 − (𝑥 · 𝐴))))
80	71, 73, 79	3eqtr4d 2819	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑥 ∈ (0[,]1)) → ((𝑥 · (𝐵 − 𝐴)) + 𝐴) = ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)))
81	80	adantrr 705	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → ((𝑥 · (𝐵 − 𝐴)) + 𝐴) = ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)))
82	81	eqeq2d 2783	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝑦 = ((𝑥 · (𝐵 − 𝐴)) + 𝐴) ↔ 𝑦 = ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴))))
83	59, 69, 82	3bitrd 297	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝑥 = ((𝑦 − 𝐴) / (𝐵 − 𝐴)) ↔ 𝑦 = ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴))))
84	1, 17, 52, 83	f1ocnv2d 7215	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵) ∧ ^◡𝐹 = (𝑦 ∈ (𝐴[,]𝐵) ↦ ((𝑦 − 𝐴) / (𝐵 − 𝐴)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1069 = wceq 1508 ∈ wcel 2051 ≠ wne 2962 class class class wbr 4926 ↦ cmpt 5005 ^◡ccnv 5403 –1-1-onto→wf1o 6185 (class class class)co 6975 ℂcc 10332 ℝcr 10333 0cc0 10334 1c1 10335 + caddc 10337 · cmul 10339 < clt 10473 ≤ cle 10474 − cmin 10669 / cdiv 11097 ℝ⁺crp 12203 [,]cicc 12556

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2745 ax-sep 5057 ax-nul 5064 ax-pow 5116 ax-pr 5183 ax-un 7278 ax-cnex 10390 ax-resscn 10391 ax-1cn 10392 ax-icn 10393 ax-addcl 10394 ax-addrcl 10395 ax-mulcl 10396 ax-mulrcl 10397 ax-mulcom 10398 ax-addass 10399 ax-mulass 10400 ax-distr 10401 ax-i2m1 10402 ax-1ne0 10403 ax-1rid 10404 ax-rnegex 10405 ax-rrecex 10406 ax-cnre 10407 ax-pre-lttri 10408 ax-pre-lttrn 10409 ax-pre-ltadd 10410 ax-pre-mulgt0 10411

This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ne 2963 df-nel 3069 df-ral 3088 df-rex 3089 df-reu 3090 df-rmo 3091 df-rab 3092 df-v 3412 df-sbc 3677 df-csb 3782 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-nul 4174 df-if 4346 df-pw 4419 df-sn 4437 df-pr 4439 df-op 4443 df-uni 4710 df-br 4927 df-opab 4989 df-mpt 5006 df-id 5309 df-po 5323 df-so 5324 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-res 5416 df-ima 5417 df-iota 6150 df-fun 6188 df-fn 6189 df-f 6190 df-f1 6191 df-fo 6192 df-f1o 6193 df-fv 6194 df-riota 6936 df-ov 6978 df-oprab 6979 df-mpo 6980 df-er 8088 df-en 8306 df-dom 8307 df-sdom 8308 df-pnf 10475 df-mnf 10476 df-xr 10477 df-ltxr 10478 df-le 10479 df-sub 10671 df-neg 10672 df-div 11098 df-rp 12204 df-icc 12560

This theorem is referenced by: iccen 12698 icchmeo 23264

W3C validator