Proof of Theorem iccf1o
Step | Hyp | Ref
| Expression |
1 | | iccf1o.1 |
. 2
⊢ 𝐹 = (x ∈ (0[,]1)
↦ ((x · B) + ((1 − x) · A))) |
2 | | 0re 6825 |
. . . . . . . . 9
⊢ 0 ∈ ℝ |
3 | | 1re 6824 |
. . . . . . . . 9
⊢ 1 ∈ ℝ |
4 | 2, 3 | elicc2i 8578 |
. . . . . . . 8
⊢ (x ∈ (0[,]1) ↔
(x ∈
ℝ ∧ 0 ≤ x ∧ x ≤ 1)) |
5 | 4 | simp1bi 918 |
. . . . . . 7
⊢ (x ∈ (0[,]1) →
x ∈
ℝ) |
6 | 5 | adantl 262 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → x ∈
ℝ) |
7 | 6 | recnd 6851 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → x ∈
ℂ) |
8 | | simpl2 907 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → B ∈
ℝ) |
9 | 8 | recnd 6851 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → B ∈
ℂ) |
10 | 7, 9 | mulcld 6845 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → (x · B)
∈ ℂ) |
11 | | ax-1cn 6776 |
. . . . . 6
⊢ 1 ∈ ℂ |
12 | | subcl 7007 |
. . . . . 6
⊢ ((1 ∈ ℂ ∧
x ∈
ℂ) → (1 − x) ∈ ℂ) |
13 | 11, 7, 12 | sylancr 393 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → (1 − x) ∈
ℂ) |
14 | | simpl1 906 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → A ∈
ℝ) |
15 | 14 | recnd 6851 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → A ∈
ℂ) |
16 | 13, 15 | mulcld 6845 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → ((1 − x) · A)
∈ ℂ) |
17 | 10, 16 | addcomd 6961 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → ((x · B) +
((1 − x) · A)) = (((1 − x) · A) +
(x · B))) |
18 | | lincmb01cmp 8641 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → (((1 − x) · A) +
(x · B)) ∈ (A[,]B)) |
19 | 17, 18 | eqeltrd 2111 |
. 2
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → ((x · B) +
((1 − x) · A)) ∈ (A[,]B)) |
20 | | simpr 103 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → y
∈ (A[,]B)) |
21 | | simpl1 906 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → A
∈ ℝ) |
22 | | simpl2 907 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → B
∈ ℝ) |
23 | | elicc2 8577 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧
B ∈
ℝ) → (y ∈ (A[,]B) ↔ (y
∈ ℝ ∧
A ≤ y ∧ y ≤ B))) |
24 | 23 | 3adant3 923 |
. . . . . . . 8
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) →
(y ∈
(A[,]B)
↔ (y ∈ ℝ ∧
A ≤ y ∧ y ≤ B))) |
25 | 24 | biimpa 280 |
. . . . . . 7
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → (y
∈ ℝ ∧
A ≤ y ∧ y ≤ B)) |
26 | 25 | simp1d 915 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → y
∈ ℝ) |
27 | | eqid 2037 |
. . . . . . 7
⊢ (A − A) =
(A − A) |
28 | | eqid 2037 |
. . . . . . 7
⊢ (B − A) =
(B − A) |
29 | 27, 28 | iccshftl 8634 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (y ∈ ℝ ∧ A ∈ ℝ)) → (y ∈ (A[,]B) ↔
(y − A) ∈ ((A − A)[,](B −
A)))) |
30 | 21, 22, 26, 21, 29 | syl22anc 1135 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → (y
∈ (A[,]B) ↔
(y − A) ∈ ((A − A)[,](B −
A)))) |
31 | 20, 30 | mpbid 135 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → (y
− A) ∈ ((A −
A)[,](B
− A))) |
32 | 26, 21 | resubcld 7175 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → (y
− A) ∈ ℝ) |
33 | 32 | recnd 6851 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → (y
− A) ∈ ℂ) |
34 | | difrp 8394 |
. . . . . . . 8
⊢
((A ∈ ℝ ∧
B ∈
ℝ) → (A < B ↔ (B
− A) ∈ ℝ+)) |
35 | 34 | biimp3a 1234 |
. . . . . . 7
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) →
(B − A) ∈
ℝ+) |
36 | 35 | adantr 261 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → (B
− A) ∈ ℝ+) |
37 | 36 | rpcnd 8399 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → (B
− A) ∈ ℂ) |
38 | | rpap0 8374 |
. . . . . 6
⊢
((B − A) ∈
ℝ+ → (B −
A) # 0) |
39 | 36, 38 | syl 14 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → (B
− A) # 0) |
40 | 33, 37, 39 | divcanap1d 7548 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → (((y
− A) / (B − A))
· (B − A)) = (y −
A)) |
41 | 37 | mul02d 7185 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → (0 · (B − A)) =
0) |
42 | 21 | recnd 6851 |
. . . . . . 7
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → A
∈ ℂ) |
43 | 42 | subidd 7106 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → (A
− A) = 0) |
44 | 41, 43 | eqtr4d 2072 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → (0 · (B − A)) =
(A − A)) |
45 | 37 | mulid2d 6843 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → (1 · (B − A)) =
(B − A)) |
46 | 44, 45 | oveq12d 5473 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → ((0 · (B − A))[,](1 · (B − A))) =
((A − A)[,](B −
A))) |
47 | 31, 40, 46 | 3eltr4d 2118 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → (((y
− A) / (B − A))
· (B − A)) ∈ ((0 ·
(B − A))[,](1 · (B − A)))) |
48 | | 0red 6826 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → 0 ∈
ℝ) |
49 | | 1red 6840 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → 1 ∈
ℝ) |
50 | 32, 36 | rerpdivcld 8424 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → ((y
− A) / (B − A))
∈ ℝ) |
51 | | eqid 2037 |
. . . . 5
⊢ (0
· (B − A)) = (0 · (B − A)) |
52 | | eqid 2037 |
. . . . 5
⊢ (1
· (B − A)) = (1 · (B − A)) |
53 | 51, 52 | iccdil 8636 |
. . . 4
⊢ (((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))))) |
54 | 48, 49, 50, 36, 53 | syl22anc 1135 |
. . 3
⊢
(((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))))) |
55 | 47, 54 | mpbird 156 |
. 2
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ y ∈ (A[,]B)) → ((y
− A) / (B − A))
∈ (0[,]1)) |
56 | | eqcom 2039 |
. . . 4
⊢ (x = ((y −
A) / (B
− A)) ↔ ((y − A) /
(B − A)) = x) |
57 | 33 | adantrl 447 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → (y
− A) ∈ ℂ) |
58 | 7 | adantrr 448 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → x
∈ ℂ) |
59 | 37 | adantrl 447 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → (B
− A) ∈ ℂ) |
60 | 39 | adantrl 447 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → (B
− A) # 0) |
61 | 57, 58, 59, 60 | divmulap3d 7581 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → (((y
− A) / (B − A)) =
x ↔ (y − A) =
(x · (B − A)))) |
62 | 56, 61 | syl5bb 181 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → (x =
((y − A) / (B −
A)) ↔ (y − A) =
(x · (B − A)))) |
63 | 26 | adantrl 447 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → y
∈ ℝ) |
64 | 63 | recnd 6851 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → y
∈ ℂ) |
65 | 42 | adantrl 447 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → A
∈ ℂ) |
66 | 8, 14 | resubcld 7175 |
. . . . . . . 8
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → (B − A)
∈ ℝ) |
67 | 6, 66 | remulcld 6853 |
. . . . . . 7
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → (x · (B
− A)) ∈ ℝ) |
68 | 67 | adantrr 448 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → (x
· (B − A)) ∈
ℝ) |
69 | 68 | recnd 6851 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → (x
· (B − A)) ∈
ℂ) |
70 | 64, 65, 69 | subadd2d 7137 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → ((y
− A) = (x · (B
− A)) ↔ ((x · (B
− A)) + A) = y)) |
71 | | eqcom 2039 |
. . . 4
⊢
(((x · (B − A)) +
A) = y
↔ y = ((x · (B
− A)) + A)) |
72 | 70, 71 | syl6bb 185 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → ((y
− A) = (x · (B
− A)) ↔ y = ((x ·
(B − A)) + A))) |
73 | 7, 15 | mulcld 6845 |
. . . . . . 7
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → (x · A)
∈ ℂ) |
74 | 10, 73, 15 | subadd23d 7140 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → (((x · B)
− (x · A)) + A) =
((x · B) + (A −
(x · A)))) |
75 | 7, 9, 15 | subdid 7207 |
. . . . . . 7
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → (x · (B
− A)) = ((x · B)
− (x · A))) |
76 | 75 | oveq1d 5470 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → ((x · (B
− A)) + A) = (((x
· B) − (x · A)) +
A)) |
77 | | 1cnd 6841 |
. . . . . . . . 9
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → 1 ∈ ℂ) |
78 | 77, 7, 15 | subdird 7208 |
. . . . . . . 8
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → ((1 − x) · A) =
((1 · A) − (x · A))) |
79 | 15 | mulid2d 6843 |
. . . . . . . . 9
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → (1 · A) = A) |
80 | 79 | oveq1d 5470 |
. . . . . . . 8
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → ((1 · A) − (x
· A)) = (A − (x
· A))) |
81 | 78, 80 | eqtrd 2069 |
. . . . . . 7
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → ((1 − x) · A) =
(A − (x · A))) |
82 | 81 | oveq2d 5471 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → ((x · B) +
((1 − x) · A)) = ((x
· B) + (A − (x
· A)))) |
83 | 74, 76, 82 | 3eqtr4d 2079 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ x ∈ (0[,]1)) → ((x · (B
− A)) + A) = ((x
· B) + ((1 − x) · A))) |
84 | 83 | adantrr 448 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → ((x
· (B − A)) + A) =
((x · B) + ((1 − x) · A))) |
85 | 84 | eqeq2d 2048 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → (y =
((x · (B − A)) +
A) ↔ y = ((x ·
B) + ((1 − x) · A)))) |
86 | 62, 72, 85 | 3bitrd 203 |
. 2
⊢
(((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) ∧ (x ∈ (0[,]1) ∧
y ∈
(A[,]B))) → (x =
((y − A) / (B −
A)) ↔ y = ((x ·
B) + ((1 − x) · A)))) |
87 | 1, 19, 55, 86 | f1ocnv2d 5646 |
1
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ A < B) →
(𝐹:(0[,]1)–1-1-onto→(A[,]B) ∧ ◡𝐹 = (y ∈ (A[,]B) ↦
((y − A) / (B −
A))))) |