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∈01⟼x⁢B+1−x⁢A
Assertion iccf1o ⊢A∈ℝ∧B∈ℝ∧A<B→F:01⟶1-1 ontoAB∧F-1=y∈AB⟼y−AB−A

Proof

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