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 F = x 0 1 x B + 1 x A
Assertion iccf1o A B A < B F : 0 1 1-1 onto A B F -1 = y A B y A B A

Proof

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