Step | Hyp | Ref
| Expression |
1 | | icoshft 8628 |
. . 3
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (x ∈ (A[,)B) → (x +
𝐶) ∈ ((A + 𝐶)[,)(B + 𝐶)))) |
2 | 1 | ralrimiv 2385 |
. 2
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ∀x ∈ (A[,)B)(x + 𝐶) ∈
((A + 𝐶)[,)(B +
𝐶))) |
3 | | readdcl 6805 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧ 𝐶 ∈ ℝ) → (A + 𝐶) ∈
ℝ) |
4 | 3 | 3adant2 922 |
. . . . . . . 8
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (A + 𝐶) ∈
ℝ) |
5 | | readdcl 6805 |
. . . . . . . . 9
⊢
((B ∈ ℝ ∧ 𝐶 ∈ ℝ) → (B + 𝐶) ∈
ℝ) |
6 | 5 | 3adant1 921 |
. . . . . . . 8
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (B + 𝐶) ∈
ℝ) |
7 | | renegcl 7068 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ → -𝐶 ∈
ℝ) |
8 | 7 | 3ad2ant3 926 |
. . . . . . . 8
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → -𝐶 ∈ ℝ) |
9 | | icoshft 8628 |
. . . . . . . 8
⊢
(((A + 𝐶) ∈
ℝ ∧ (B + 𝐶) ∈
ℝ ∧ -𝐶 ∈
ℝ) → (y ∈ ((A + 𝐶)[,)(B + 𝐶)) → (y + -𝐶) ∈
(((A + 𝐶) + -𝐶)[,)((B
+ 𝐶) + -𝐶)))) |
10 | 4, 6, 8, 9 | syl3anc 1134 |
. . . . . . 7
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (y ∈ ((A + 𝐶)[,)(B + 𝐶)) → (y + -𝐶) ∈
(((A + 𝐶) + -𝐶)[,)((B
+ 𝐶) + -𝐶)))) |
11 | 10 | imp 115 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) → (y + -𝐶) ∈
(((A + 𝐶) + -𝐶)[,)((B
+ 𝐶) + -𝐶))) |
12 | 6 | rexrd 6872 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (B + 𝐶) ∈
ℝ*) |
13 | | icossre 8593 |
. . . . . . . . . 10
⊢
(((A + 𝐶) ∈
ℝ ∧ (B + 𝐶) ∈
ℝ*) → ((A + 𝐶)[,)(B + 𝐶)) ⊆ ℝ) |
14 | 4, 12, 13 | syl2anc 391 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ((A + 𝐶)[,)(B +
𝐶)) ⊆
ℝ) |
15 | 14 | sselda 2939 |
. . . . . . . 8
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) → y ∈
ℝ) |
16 | 15 | recnd 6851 |
. . . . . . 7
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) → y ∈
ℂ) |
17 | | simpl3 908 |
. . . . . . . 8
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) → 𝐶 ∈ ℝ) |
18 | 17 | recnd 6851 |
. . . . . . 7
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) → 𝐶 ∈ ℂ) |
19 | 16, 18 | negsubd 7124 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) → (y + -𝐶) = (y
− 𝐶)) |
20 | 4 | recnd 6851 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (A + 𝐶) ∈
ℂ) |
21 | | simp3 905 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → 𝐶 ∈ ℝ) |
22 | 21 | recnd 6851 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → 𝐶 ∈ ℂ) |
23 | 20, 22 | negsubd 7124 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ((A + 𝐶) + -𝐶) = ((A
+ 𝐶) − 𝐶)) |
24 | | simp1 903 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → A ∈ ℝ) |
25 | 24 | recnd 6851 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → A ∈ ℂ) |
26 | 25, 22 | pncand 7119 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ((A + 𝐶) − 𝐶) = A) |
27 | 23, 26 | eqtrd 2069 |
. . . . . . . 8
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ((A + 𝐶) + -𝐶) = A) |
28 | 6 | recnd 6851 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (B + 𝐶) ∈
ℂ) |
29 | 28, 22 | negsubd 7124 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ((B + 𝐶) + -𝐶) = ((B
+ 𝐶) − 𝐶)) |
30 | | simp2 904 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → B ∈ ℝ) |
31 | 30 | recnd 6851 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → B ∈ ℂ) |
32 | 31, 22 | pncand 7119 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ((B + 𝐶) − 𝐶) = B) |
33 | 29, 32 | eqtrd 2069 |
. . . . . . . 8
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ((B + 𝐶) + -𝐶) = B) |
34 | 27, 33 | oveq12d 5473 |
. . . . . . 7
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → (((A + 𝐶) + -𝐶)[,)((B
+ 𝐶) + -𝐶)) = (A[,)B)) |
35 | 34 | adantr 261 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) → (((A + 𝐶) + -𝐶)[,)((B
+ 𝐶) + -𝐶)) = (A[,)B)) |
36 | 11, 19, 35 | 3eltr3d 2117 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) → (y − 𝐶) ∈
(A[,)B)) |
37 | | reueq 2732 |
. . . . 5
⊢
((y − 𝐶) ∈
(A[,)B)
↔ ∃!x ∈ (A[,)B)x = (y −
𝐶)) |
38 | 36, 37 | sylib 127 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) → ∃!x ∈ (A[,)B)x = (y − 𝐶)) |
39 | 15 | adantr 261 |
. . . . . . . 8
⊢
((((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) ∧ x ∈ (A[,)B)) → y
∈ ℝ) |
40 | 39 | recnd 6851 |
. . . . . . 7
⊢
((((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) ∧ x ∈ (A[,)B)) → y
∈ ℂ) |
41 | | simpll3 944 |
. . . . . . . 8
⊢
((((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) ∧ x ∈ (A[,)B)) → 𝐶 ∈
ℝ) |
42 | 41 | recnd 6851 |
. . . . . . 7
⊢
((((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) ∧ x ∈ (A[,)B)) → 𝐶 ∈
ℂ) |
43 | | simpl1 906 |
. . . . . . . . . 10
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) → A ∈
ℝ) |
44 | | simpl2 907 |
. . . . . . . . . . 11
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) → B ∈
ℝ) |
45 | 44 | rexrd 6872 |
. . . . . . . . . 10
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) → B ∈
ℝ*) |
46 | | icossre 8593 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧
B ∈
ℝ*) → (A[,)B) ⊆ ℝ) |
47 | 43, 45, 46 | syl2anc 391 |
. . . . . . . . 9
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) → (A[,)B) ⊆
ℝ) |
48 | 47 | sselda 2939 |
. . . . . . . 8
⊢
((((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) ∧ x ∈ (A[,)B)) → x
∈ ℝ) |
49 | 48 | recnd 6851 |
. . . . . . 7
⊢
((((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) ∧ x ∈ (A[,)B)) → x
∈ ℂ) |
50 | 40, 42, 49 | subadd2d 7137 |
. . . . . 6
⊢
((((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) ∧ x ∈ (A[,)B)) → ((y
− 𝐶) = x ↔ (x +
𝐶) = y)) |
51 | | eqcom 2039 |
. . . . . 6
⊢ (x = (y −
𝐶) ↔ (y − 𝐶) = x) |
52 | | eqcom 2039 |
. . . . . 6
⊢ (y = (x + 𝐶) ↔ (x + 𝐶) = y) |
53 | 50, 51, 52 | 3bitr4g 212 |
. . . . 5
⊢
((((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) ∧ x ∈ (A[,)B)) → (x =
(y − 𝐶) ↔ y = (x + 𝐶))) |
54 | 53 | reubidva 2486 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) → (∃!x ∈ (A[,)B)x = (y − 𝐶) ↔ ∃!x ∈ (A[,)B)y = (x + 𝐶))) |
55 | 38, 54 | mpbid 135 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ y ∈ ((A + 𝐶)[,)(B +
𝐶))) → ∃!x ∈ (A[,)B)y = (x + 𝐶)) |
56 | 55 | ralrimiva 2386 |
. 2
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ∀y ∈ ((A + 𝐶)[,)(B +
𝐶))∃!x ∈ (A[,)B)y = (x + 𝐶)) |
57 | | icoshftf1o.1 |
. . 3
⊢ 𝐹 = (x ∈ (A[,)B) ↦
(x + 𝐶)) |
58 | 57 | f1ompt 5263 |
. 2
⊢ (𝐹:(A[,)B)–1-1-onto→((A +
𝐶)[,)(B + 𝐶)) ↔ (∀x ∈ (A[,)B)(x + 𝐶) ∈ ((A + 𝐶)[,)(B + 𝐶)) ∧ ∀y ∈ ((A + 𝐶)[,)(B + 𝐶))∃!x ∈ (A[,)B)y = (x + 𝐶))) |
59 | 2, 56, 58 | sylanbrc 394 |
1
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → 𝐹:(A[,)B)–1-1-onto→((A +
𝐶)[,)(B + 𝐶))) |