Step | Hyp | Ref
| Expression |
1 | | unitssre 12319 |
. . . . . . . 8
⊢ (0[,]1)
⊆ ℝ |
2 | | ttgcontlem1.l |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (0[,]1)) |
3 | 1, 2 | sseldi 3601 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ ℝ) |
4 | | ttgcontlem1.k |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ (0[,]1)) |
5 | 1, 4 | sseldi 3601 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℝ) |
6 | 3, 5 | remulcld 10070 |
. . . . . 6
⊢ (𝜑 → (𝐿 · 𝐾) ∈ ℝ) |
7 | | 0re 10040 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
8 | | iccssre 12255 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝐿
∈ ℝ) → (0[,]𝐿) ⊆ ℝ) |
9 | 7, 3, 8 | sylancr 695 |
. . . . . . . 8
⊢ (𝜑 → (0[,]𝐿) ⊆ ℝ) |
10 | | ttgcontlem1.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (0[,]𝐿)) |
11 | 9, 10 | sseldd 3604 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℝ) |
12 | 11, 5 | remulcld 10070 |
. . . . . 6
⊢ (𝜑 → (𝑀 · 𝐾) ∈ ℝ) |
13 | 6, 12 | resubcld 10458 |
. . . . 5
⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ∈ ℝ) |
14 | | 1red 10055 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℝ) |
15 | 11, 14 | remulcld 10070 |
. . . . . 6
⊢ (𝜑 → (𝑀 · 1) ∈
ℝ) |
16 | 15, 12 | resubcld 10458 |
. . . . 5
⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℝ) |
17 | 11 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
18 | | 1cnd 10056 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) |
19 | 5 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℂ) |
20 | 17, 18, 19 | subdid 10486 |
. . . . . 6
⊢ (𝜑 → (𝑀 · (1 − 𝐾)) = ((𝑀 · 1) − (𝑀 · 𝐾))) |
21 | 18, 19 | subcld 10392 |
. . . . . . 7
⊢ (𝜑 → (1 − 𝐾) ∈
ℂ) |
22 | | ttgcontlem1.o |
. . . . . . 7
⊢ (𝜑 → 𝑀 ≠ 0) |
23 | | ttgcontlem1.q |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ≠ 1) |
24 | 23 | necomd 2849 |
. . . . . . . 8
⊢ (𝜑 → 1 ≠ 𝐾) |
25 | 18, 19, 24 | subne0d 10401 |
. . . . . . 7
⊢ (𝜑 → (1 − 𝐾) ≠ 0) |
26 | 17, 21, 22, 25 | mulne0d 10679 |
. . . . . 6
⊢ (𝜑 → (𝑀 · (1 − 𝐾)) ≠ 0) |
27 | 20, 26 | eqnetrrd 2862 |
. . . . 5
⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ≠ 0) |
28 | 13, 16, 27 | redivcld 10853 |
. . . 4
⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ ℝ) |
29 | | 0xr 10086 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
30 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ*) |
31 | 3 | rexrd 10089 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈
ℝ*) |
32 | | iccgelb 12230 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 𝐿 ∈ ℝ* ∧ 𝑀 ∈ (0[,]𝐿)) → 0 ≤ 𝑀) |
33 | 30, 31, 10, 32 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝑀) |
34 | 11, 33, 22 | ne0gt0d 10174 |
. . . . . . . 8
⊢ (𝜑 → 0 < 𝑀) |
35 | 11, 34 | elrpd 11869 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
ℝ+) |
36 | 14 | rexrd 10089 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ*) |
37 | | iccleub 12229 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝐾 ∈ (0[,]1)) → 𝐾 ≤ 1) |
38 | 30, 36, 4, 37 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ≤ 1) |
39 | 5, 14 | ltlend 10182 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 < 1 ↔ (𝐾 ≤ 1 ∧ 1 ≠ 𝐾))) |
40 | 38, 24, 39 | mpbir2and 957 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 < 1) |
41 | | difrp 11868 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐾 < 1
↔ (1 − 𝐾) ∈
ℝ+)) |
42 | 5, 14, 41 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 < 1 ↔ (1 − 𝐾) ∈
ℝ+)) |
43 | 40, 42 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → (1 − 𝐾) ∈
ℝ+) |
44 | 35, 43 | rpmulcld 11888 |
. . . . . 6
⊢ (𝜑 → (𝑀 · (1 − 𝐾)) ∈
ℝ+) |
45 | 20, 44 | eqeltrrd 2702 |
. . . . 5
⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈
ℝ+) |
46 | 3, 11 | resubcld 10458 |
. . . . . . 7
⊢ (𝜑 → (𝐿 − 𝑀) ∈ ℝ) |
47 | | iccleub 12229 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 𝐿 ∈ ℝ* ∧ 𝑀 ∈ (0[,]𝐿)) → 𝑀 ≤ 𝐿) |
48 | 30, 31, 10, 47 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ≤ 𝐿) |
49 | 3, 11 | subge0d 10617 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ (𝐿 − 𝑀) ↔ 𝑀 ≤ 𝐿)) |
50 | 48, 49 | mpbird 247 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (𝐿 − 𝑀)) |
51 | | iccgelb 12230 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝐾 ∈ (0[,]1)) → 0 ≤
𝐾) |
52 | 30, 36, 4, 51 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝐾) |
53 | 46, 5, 50, 52 | mulge0d 10604 |
. . . . . 6
⊢ (𝜑 → 0 ≤ ((𝐿 − 𝑀) · 𝐾)) |
54 | 3 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ ℂ) |
55 | 54, 17, 19 | subdird 10487 |
. . . . . 6
⊢ (𝜑 → ((𝐿 − 𝑀) · 𝐾) = ((𝐿 · 𝐾) − (𝑀 · 𝐾))) |
56 | 53, 55 | breqtrd 4679 |
. . . . 5
⊢ (𝜑 → 0 ≤ ((𝐿 · 𝐾) − (𝑀 · 𝐾))) |
57 | 13, 45, 56 | divge0d 11912 |
. . . 4
⊢ (𝜑 → 0 ≤ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾)))) |
58 | | ttgcontlem1.s |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ≤ (𝑀 / 𝐾)) |
59 | | ttgcontlem1.p |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ≠ 0) |
60 | 5, 52, 59 | ne0gt0d 10174 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 𝐾) |
61 | 5, 60 | elrpd 11869 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈
ℝ+) |
62 | 3, 11, 61 | lemuldivd 11921 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐿 · 𝐾) ≤ 𝑀 ↔ 𝐿 ≤ (𝑀 / 𝐾))) |
63 | 58, 62 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → (𝐿 · 𝐾) ≤ 𝑀) |
64 | 17 | mulid1d 10057 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 · 1) = 𝑀) |
65 | 63, 64 | breqtrrd 4681 |
. . . . . . 7
⊢ (𝜑 → (𝐿 · 𝐾) ≤ (𝑀 · 1)) |
66 | 6, 15, 12, 65 | lesub1dd 10643 |
. . . . . 6
⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ ((𝑀 · 1) − (𝑀 · 𝐾))) |
67 | 17, 18 | mulcld 10060 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 · 1) ∈
ℂ) |
68 | 17, 19 | mulcld 10060 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 · 𝐾) ∈ ℂ) |
69 | 67, 68 | subcld 10392 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℂ) |
70 | 69 | mulid1d 10057 |
. . . . . 6
⊢ (𝜑 → (((𝑀 · 1) − (𝑀 · 𝐾)) · 1) = ((𝑀 · 1) − (𝑀 · 𝐾))) |
71 | 66, 70 | breqtrrd 4681 |
. . . . 5
⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ (((𝑀 · 1) − (𝑀 · 𝐾)) · 1)) |
72 | 13, 14, 45 | ledivmuld 11925 |
. . . . 5
⊢ (𝜑 → ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1 ↔ ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ (((𝑀 · 1) − (𝑀 · 𝐾)) · 1))) |
73 | 71, 72 | mpbird 247 |
. . . 4
⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1) |
74 | | 1re 10039 |
. . . . 5
⊢ 1 ∈
ℝ |
75 | 7, 74 | elicc2i 12239 |
. . . 4
⊢ ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1) ↔ ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ ℝ ∧ 0 ≤ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∧ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1)) |
76 | 28, 57, 73, 75 | syl3anbrc 1246 |
. . 3
⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1)) |
77 | | ttgcontlem1.h |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ ℂVec) |
78 | 77 | cvsclm 22926 |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ ℂMod) |
79 | | ttgbtwnid.2 |
. . . . . . . 8
⊢ (𝜑 → (0[,]1) ⊆ 𝑅) |
80 | 79, 2 | sseldd 3604 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ 𝑅) |
81 | | 0elunit 12290 |
. . . . . . . . . 10
⊢ 0 ∈
(0[,]1) |
82 | | iccss2 12244 |
. . . . . . . . . 10
⊢ ((0
∈ (0[,]1) ∧ 𝐿
∈ (0[,]1)) → (0[,]𝐿) ⊆ (0[,]1)) |
83 | 81, 2, 82 | sylancr 695 |
. . . . . . . . 9
⊢ (𝜑 → (0[,]𝐿) ⊆ (0[,]1)) |
84 | 83, 79 | sstrd 3613 |
. . . . . . . 8
⊢ (𝜑 → (0[,]𝐿) ⊆ 𝑅) |
85 | 84, 10 | sseldd 3604 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ 𝑅) |
86 | | eqid 2622 |
. . . . . . . 8
⊢
(Scalar‘𝐻) =
(Scalar‘𝐻) |
87 | | ttgbtwnid.r |
. . . . . . . 8
⊢ 𝑅 =
(Base‘(Scalar‘𝐻)) |
88 | 86, 87 | clmsubcl 22886 |
. . . . . . 7
⊢ ((𝐻 ∈ ℂMod ∧ 𝐿 ∈ 𝑅 ∧ 𝑀 ∈ 𝑅) → (𝐿 − 𝑀) ∈ 𝑅) |
89 | 78, 80, 85, 88 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → (𝐿 − 𝑀) ∈ 𝑅) |
90 | 86, 87 | cvsdivcl 22933 |
. . . . . 6
⊢ ((𝐻 ∈ ℂVec ∧ ((𝐿 − 𝑀) ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ∧ 𝑀 ≠ 0)) → ((𝐿 − 𝑀) / 𝑀) ∈ 𝑅) |
91 | 77, 89, 85, 22, 90 | syl13anc 1328 |
. . . . 5
⊢ (𝜑 → ((𝐿 − 𝑀) / 𝑀) ∈ 𝑅) |
92 | 79, 4 | sseldd 3604 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ 𝑅) |
93 | | 1elunit 12291 |
. . . . . . . . 9
⊢ 1 ∈
(0[,]1) |
94 | 93 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
(0[,]1)) |
95 | 79, 94 | sseldd 3604 |
. . . . . . 7
⊢ (𝜑 → 1 ∈ 𝑅) |
96 | 86, 87 | clmsubcl 22886 |
. . . . . . 7
⊢ ((𝐻 ∈ ℂMod ∧ 1
∈ 𝑅 ∧ 𝐾 ∈ 𝑅) → (1 − 𝐾) ∈ 𝑅) |
97 | 78, 95, 92, 96 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → (1 − 𝐾) ∈ 𝑅) |
98 | 86, 87 | cvsdivcl 22933 |
. . . . . 6
⊢ ((𝐻 ∈ ℂVec ∧ (𝐾 ∈ 𝑅 ∧ (1 − 𝐾) ∈ 𝑅 ∧ (1 − 𝐾) ≠ 0)) → (𝐾 / (1 − 𝐾)) ∈ 𝑅) |
99 | 77, 92, 97, 25, 98 | syl13anc 1328 |
. . . . 5
⊢ (𝜑 → (𝐾 / (1 − 𝐾)) ∈ 𝑅) |
100 | | clmgrp 22868 |
. . . . . . 7
⊢ (𝐻 ∈ ℂMod → 𝐻 ∈ Grp) |
101 | 78, 100 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ Grp) |
102 | | ttgelitv.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
103 | | ttgelitv.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
104 | | ttgitvval.b |
. . . . . . 7
⊢ 𝑃 = (Base‘𝐻) |
105 | | ttgitvval.m |
. . . . . . 7
⊢ − =
(-g‘𝐻) |
106 | 104, 105 | grpsubcl 17495 |
. . . . . 6
⊢ ((𝐻 ∈ Grp ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃) → (𝑌 − 𝑋) ∈ 𝑃) |
107 | 101, 102,
103, 106 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (𝑌 − 𝑋) ∈ 𝑃) |
108 | | ttgitvval.s |
. . . . . 6
⊢ · = (
·𝑠 ‘𝐻) |
109 | 104, 86, 108, 87 | clmvsass 22889 |
. . . . 5
⊢ ((𝐻 ∈ ℂMod ∧
(((𝐿 − 𝑀) / 𝑀) ∈ 𝑅 ∧ (𝐾 / (1 − 𝐾)) ∈ 𝑅 ∧ (𝑌 − 𝑋) ∈ 𝑃)) → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)))) |
110 | 78, 91, 99, 107, 109 | syl13anc 1328 |
. . . 4
⊢ (𝜑 → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)))) |
111 | 46 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → (𝐿 − 𝑀) ∈ ℂ) |
112 | 111, 17, 19, 21, 22, 25 | divmuldivd 10842 |
. . . . . 6
⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) = (((𝐿 − 𝑀) · 𝐾) / (𝑀 · (1 − 𝐾)))) |
113 | 55, 20 | oveq12d 6668 |
. . . . . 6
⊢ (𝜑 → (((𝐿 − 𝑀) · 𝐾) / (𝑀 · (1 − 𝐾))) = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾)))) |
114 | 112, 113 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾)))) |
115 | 114 | oveq1d 6665 |
. . . 4
⊢ (𝜑 → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋))) |
116 | | ttgcontlem1.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
117 | 104, 105 | grpsubcl 17495 |
. . . . . . . 8
⊢ ((𝐻 ∈ Grp ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑋 − 𝐴) ∈ 𝑃) |
118 | 101, 103,
116, 117 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (𝑋 − 𝐴) ∈ 𝑃) |
119 | | ttgcontlem1.y |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 − 𝐴) = (𝐾 · (𝑌 − 𝐴))) |
120 | 119 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝜑 → ((1 − 𝐾) · (𝑋 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴)))) |
121 | 19, 21 | mulcomd 10061 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾 · (1 − 𝐾)) = ((1 − 𝐾) · 𝐾)) |
122 | 121 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴))) |
123 | 104, 105 | grpsubcl 17495 |
. . . . . . . . . . . 12
⊢ ((𝐻 ∈ Grp ∧ 𝑌 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑌 − 𝐴) ∈ 𝑃) |
124 | 101, 102,
116, 123 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 − 𝐴) ∈ 𝑃) |
125 | 104, 86, 108, 87 | clmvsass 22889 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ ℂMod ∧ (𝐾 ∈ 𝑅 ∧ (1 − 𝐾) ∈ 𝑅 ∧ (𝑌 − 𝐴) ∈ 𝑃)) → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴)))) |
126 | 78, 92, 97, 124, 125 | syl13anc 1328 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴)))) |
127 | 104, 86, 108, 87 | clmvsass 22889 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ ℂMod ∧ ((1
− 𝐾) ∈ 𝑅 ∧ 𝐾 ∈ 𝑅 ∧ (𝑌 − 𝐴) ∈ 𝑃)) → (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴)))) |
128 | 78, 97, 92, 124, 127 | syl13anc 1328 |
. . . . . . . . . 10
⊢ (𝜑 → (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴)))) |
129 | 122, 126,
128 | 3eqtr3d 2664 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴)))) |
130 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(-g‘(Scalar‘𝐻)) =
(-g‘(Scalar‘𝐻)) |
131 | | clmlmod 22867 |
. . . . . . . . . . . . . 14
⊢ (𝐻 ∈ ℂMod → 𝐻 ∈ LMod) |
132 | 78, 131 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻 ∈ LMod) |
133 | 104, 108,
86, 87, 105, 130, 132, 95, 92, 124 | lmodsubdir 18921 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((1(-g‘(Scalar‘𝐻))𝐾) · (𝑌 − 𝐴)) = ((1 · (𝑌 − 𝐴)) − (𝐾 · (𝑌 − 𝐴)))) |
134 | 86, 87 | clmsub 22880 |
. . . . . . . . . . . . . 14
⊢ ((𝐻 ∈ ℂMod ∧ 1
∈ 𝑅 ∧ 𝐾 ∈ 𝑅) → (1 − 𝐾) =
(1(-g‘(Scalar‘𝐻))𝐾)) |
135 | 78, 95, 92, 134 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 − 𝐾) =
(1(-g‘(Scalar‘𝐻))𝐾)) |
136 | 135 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) =
((1(-g‘(Scalar‘𝐻))𝐾) · (𝑌 − 𝐴))) |
137 | 104, 108 | clmvs1 22893 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻 ∈ ℂMod ∧ (𝑌 − 𝐴) ∈ 𝑃) → (1 · (𝑌 − 𝐴)) = (𝑌 − 𝐴)) |
138 | 78, 124, 137 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 · (𝑌 − 𝐴)) = (𝑌 − 𝐴)) |
139 | 138 | eqcomd 2628 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 − 𝐴) = (1 · (𝑌 − 𝐴))) |
140 | 139, 119 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = ((1 · (𝑌 − 𝐴)) − (𝐾 · (𝑌 − 𝐴)))) |
141 | 133, 136,
140 | 3eqtr4d 2666 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = ((𝑌 − 𝐴) − (𝑋 − 𝐴))) |
142 | 104, 105 | grpnnncan2 17512 |
. . . . . . . . . . . 12
⊢ ((𝐻 ∈ Grp ∧ (𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃)) → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = (𝑌 − 𝑋)) |
143 | 101, 102,
103, 116, 142 | syl13anc 1328 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = (𝑌 − 𝑋)) |
144 | 141, 143 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = (𝑌 − 𝑋)) |
145 | 144 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))) = (𝐾 · (𝑌 − 𝑋))) |
146 | 120, 129,
145 | 3eqtr2rd 2663 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 · (𝑌 − 𝑋)) = ((1 − 𝐾) · (𝑋 − 𝐴))) |
147 | 104, 108,
86, 87, 77, 92, 97, 107, 118, 59, 146 | cvsmuleqdivd 22934 |
. . . . . . 7
⊢ (𝜑 → (𝑌 − 𝑋) = (((1 − 𝐾) / 𝐾) · (𝑋 − 𝐴))) |
148 | 104, 108,
86, 87, 77, 97, 92, 107, 118, 25, 59, 147 | cvsdiveqd 22935 |
. . . . . 6
⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) = (𝑋 − 𝐴)) |
149 | 148, 118 | eqeltrd 2701 |
. . . . 5
⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) ∈ 𝑃) |
150 | | ttgcontlem1.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (𝐴 + (𝐿 · (𝑁 − 𝐴)))) |
151 | | ttgcontlem1.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ 𝑃) |
152 | 104, 105 | grpsubcl 17495 |
. . . . . . . . . 10
⊢ ((𝐻 ∈ Grp ∧ 𝑁 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑁 − 𝐴) ∈ 𝑃) |
153 | 101, 151,
116, 152 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 − 𝐴) ∈ 𝑃) |
154 | 104, 86, 108, 87 | lmodvscl 18880 |
. . . . . . . . 9
⊢ ((𝐻 ∈ LMod ∧ 𝐿 ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃) → (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃) |
155 | 132, 80, 153, 154 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃) |
156 | | ttgitvval.p |
. . . . . . . . 9
⊢ + =
(+g‘𝐻) |
157 | 104, 156 | grpcl 17430 |
. . . . . . . 8
⊢ ((𝐻 ∈ Grp ∧ 𝐴 ∈ 𝑃 ∧ (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃) → (𝐴 + (𝐿 · (𝑁 − 𝐴))) ∈ 𝑃) |
158 | 101, 116,
155, 157 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (𝐴 + (𝐿 · (𝑁 − 𝐴))) ∈ 𝑃) |
159 | 150, 158 | eqeltrd 2701 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
160 | 104, 105 | grpsubcl 17495 |
. . . . . 6
⊢ ((𝐻 ∈ Grp ∧ 𝐵 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃) → (𝐵 − 𝑋) ∈ 𝑃) |
161 | 101, 159,
103, 160 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (𝐵 − 𝑋) ∈ 𝑃) |
162 | | ttgcontlem1.r |
. . . . . 6
⊢ (𝜑 → 𝐿 ≠ 𝑀) |
163 | 54, 17, 162 | subne0d 10401 |
. . . . 5
⊢ (𝜑 → (𝐿 − 𝑀) ≠ 0) |
164 | | ttgcontlem1.x |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 − 𝐴) = (𝑀 · (𝑁 − 𝐴))) |
165 | 164 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑋 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴)))) |
166 | 17, 111 | mulcomd 10061 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 · (𝐿 − 𝑀)) = ((𝐿 − 𝑀) · 𝑀)) |
167 | 166 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴))) |
168 | 104, 86, 108, 87 | clmvsass 22889 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ ℂMod ∧ (𝑀 ∈ 𝑅 ∧ (𝐿 − 𝑀) ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃)) → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴)))) |
169 | 78, 85, 89, 153, 168 | syl13anc 1328 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴)))) |
170 | 104, 86, 108, 87 | clmvsass 22889 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ ℂMod ∧ ((𝐿 − 𝑀) ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃)) → (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴)))) |
171 | 78, 89, 85, 153, 170 | syl13anc 1328 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴)))) |
172 | 167, 169,
171 | 3eqtr3d 2664 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴)))) |
173 | 104, 108,
86, 87, 105, 130, 132, 80, 85, 153 | lmodsubdir 18921 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐿(-g‘(Scalar‘𝐻))𝑀) · (𝑁 − 𝐴)) = ((𝐿 · (𝑁 − 𝐴)) − (𝑀 · (𝑁 − 𝐴)))) |
174 | 86, 87 | clmsub 22880 |
. . . . . . . . . . . . . 14
⊢ ((𝐻 ∈ ℂMod ∧ 𝐿 ∈ 𝑅 ∧ 𝑀 ∈ 𝑅) → (𝐿 − 𝑀) = (𝐿(-g‘(Scalar‘𝐻))𝑀)) |
175 | 78, 80, 85, 174 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 − 𝑀) = (𝐿(-g‘(Scalar‘𝐻))𝑀)) |
176 | 175 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = ((𝐿(-g‘(Scalar‘𝐻))𝑀) · (𝑁 − 𝐴))) |
177 | 150 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 − 𝐴) = ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴)) |
178 | | lmodabl 18910 |
. . . . . . . . . . . . . . . 16
⊢ (𝐻 ∈ LMod → 𝐻 ∈ Abel) |
179 | 132, 178 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻 ∈ Abel) |
180 | 104, 156,
105 | ablpncan2 18221 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻 ∈ Abel ∧ 𝐴 ∈ 𝑃 ∧ (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃) → ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴) = (𝐿 · (𝑁 − 𝐴))) |
181 | 179, 116,
155, 180 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴) = (𝐿 · (𝑁 − 𝐴))) |
182 | 177, 181 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 − 𝐴) = (𝐿 · (𝑁 − 𝐴))) |
183 | 182, 164 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = ((𝐿 · (𝑁 − 𝐴)) − (𝑀 · (𝑁 − 𝐴)))) |
184 | 173, 176,
183 | 3eqtr4d 2666 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = ((𝐵 − 𝐴) − (𝑋 − 𝐴))) |
185 | 104, 105 | grpnnncan2 17512 |
. . . . . . . . . . . 12
⊢ ((𝐻 ∈ Grp ∧ (𝐵 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃)) → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = (𝐵 − 𝑋)) |
186 | 101, 159,
103, 116, 185 | syl13anc 1328 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = (𝐵 − 𝑋)) |
187 | 184, 186 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = (𝐵 − 𝑋)) |
188 | 187 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))) = (𝑀 · (𝐵 − 𝑋))) |
189 | 165, 172,
188 | 3eqtr2rd 2663 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 · (𝐵 − 𝑋)) = ((𝐿 − 𝑀) · (𝑋 − 𝐴))) |
190 | 104, 108,
86, 87, 77, 85, 89, 161, 118, 22, 189 | cvsmuleqdivd 22934 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − 𝑋) = (((𝐿 − 𝑀) / 𝑀) · (𝑋 − 𝐴))) |
191 | 104, 108,
86, 87, 77, 89, 85, 161, 118, 163, 22, 190 | cvsdiveqd 22935 |
. . . . . 6
⊢ (𝜑 → ((𝑀 / (𝐿 − 𝑀)) · (𝐵 − 𝑋)) = (𝑋 − 𝐴)) |
192 | 148, 191 | eqtr4d 2659 |
. . . . 5
⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) = ((𝑀 / (𝐿 − 𝑀)) · (𝐵 − 𝑋))) |
193 | 104, 108,
86, 87, 77, 85, 89, 149, 161, 22, 163, 192 | cvsdiveqd 22935 |
. . . 4
⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))) = (𝐵 − 𝑋)) |
194 | 110, 115,
193 | 3eqtr3rd 2665 |
. . 3
⊢ (𝜑 → (𝐵 − 𝑋) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋))) |
195 | | oveq1 6657 |
. . . . 5
⊢ (𝑘 = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) → (𝑘 · (𝑌 − 𝑋)) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋))) |
196 | 195 | eqeq2d 2632 |
. . . 4
⊢ (𝑘 = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) → ((𝐵 − 𝑋) = (𝑘 · (𝑌 − 𝑋)) ↔ (𝐵 − 𝑋) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))) |
197 | 196 | rspcev 3309 |
. . 3
⊢
(((((𝐿 ·
𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1) ∧ (𝐵 − 𝑋) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋))) → ∃𝑘 ∈ (0[,]1)(𝐵 − 𝑋) = (𝑘 · (𝑌 − 𝑋))) |
198 | 76, 194, 197 | syl2anc 693 |
. 2
⊢ (𝜑 → ∃𝑘 ∈ (0[,]1)(𝐵 − 𝑋) = (𝑘 · (𝑌 − 𝑋))) |
199 | | ttgval.n |
. . 3
⊢ 𝐺 = (toTG‘𝐻) |
200 | | ttgitvval.i |
. . 3
⊢ 𝐼 = (Itv‘𝐺) |
201 | 199, 200,
104, 105, 108, 103, 102, 77, 159 | ttgelitv 25763 |
. 2
⊢ (𝜑 → (𝐵 ∈ (𝑋𝐼𝑌) ↔ ∃𝑘 ∈ (0[,]1)(𝐵 − 𝑋) = (𝑘 · (𝑌 − 𝑋)))) |
202 | 198, 201 | mpbird 247 |
1
⊢ (𝜑 → 𝐵 ∈ (𝑋𝐼𝑌)) |