ttgcontlem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ttgcontlem1		Structured version Visualization version GIF version

Theorem ttgcontlem1 28142

Description: Lemma for % ttgcont . (Contributed by Thierry Arnoux, 24-May-2019.)

**Hypotheses**
Ref	Expression
ttgval.n	⊢ 𝐺 = (toTG‘𝐻)
ttgitvval.i	⊢ 𝐼 = (Itv‘𝐺)
ttgitvval.b	⊢ 𝑃 = (Base‘𝐻)
ttgitvval.m	⊢ − = (-_g‘𝐻)
ttgitvval.s	⊢ · = ( ·_𝑠 ‘𝐻)
ttgelitv.x	⊢ (𝜑 → 𝑋 ∈ 𝑃)
ttgelitv.y	⊢ (𝜑 → 𝑌 ∈ 𝑃)
ttgbtwnid.r	⊢ 𝑅 = (Base‘(Scalar‘𝐻))
ttgbtwnid.2	⊢ (𝜑 → (0[,]1) ⊆ 𝑅)
ttgitvval.p	⊢ + = (+_g‘𝐻)
ttgcontlem1.h	⊢ (𝜑 → 𝐻 ∈ ℂVec)
ttgcontlem1.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
ttgcontlem1.n	⊢ (𝜑 → 𝑁 ∈ 𝑃)
ttgcontlem1.o	⊢ (𝜑 → 𝑀 ≠ 0)
ttgcontlem1.p	⊢ (𝜑 → 𝐾 ≠ 0)
ttgcontlem1.q	⊢ (𝜑 → 𝐾 ≠ 1)
ttgcontlem1.r	⊢ (𝜑 → 𝐿 ≠ 𝑀)
ttgcontlem1.s	⊢ (𝜑 → 𝐿 ≤ (𝑀 / 𝐾))
ttgcontlem1.l	⊢ (𝜑 → 𝐿 ∈ (0[,]1))
ttgcontlem1.k	⊢ (𝜑 → 𝐾 ∈ (0[,]1))
ttgcontlem1.m	⊢ (𝜑 → 𝑀 ∈ (0[,]𝐿))
ttgcontlem1.y	⊢ (𝜑 → (𝑋 − 𝐴) = (𝐾 · (𝑌 − 𝐴)))
ttgcontlem1.x	⊢ (𝜑 → (𝑋 − 𝐴) = (𝑀 · (𝑁 − 𝐴)))
ttgcontlem1.b	⊢ (𝜑 → 𝐵 = (𝐴 + (𝐿 · (𝑁 − 𝐴))))

**Assertion**
Ref	Expression
ttgcontlem1	⊢ (𝜑 → 𝐵 ∈ (𝑋𝐼𝑌))

Proof of Theorem ttgcontlem1 Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		unitssre 13476	. . . . . . . 8 ⊢ (0[,]1) ⊆ ℝ
2		ttgcontlem1.l	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ (0[,]1))
3	1, 2	sselid 3981	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℝ)
4		ttgcontlem1.k	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (0[,]1))
5	1, 4	sselid 3981	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℝ)
6	3, 5	remulcld 11244	. . . . . 6 ⊢ (𝜑 → (𝐿 · 𝐾) ∈ ℝ)
7		0re 11216	. . . . . . . . 9 ⊢ 0 ∈ ℝ
8		iccssre 13406	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (0[,]𝐿) ⊆ ℝ)
9	7, 3, 8	sylancr 588	. . . . . . . 8 ⊢ (𝜑 → (0[,]𝐿) ⊆ ℝ)
10		ttgcontlem1.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0[,]𝐿))
11	9, 10	sseldd 3984	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℝ)
12	11, 5	remulcld 11244	. . . . . 6 ⊢ (𝜑 → (𝑀 · 𝐾) ∈ ℝ)
13	6, 12	resubcld 11642	. . . . 5 ⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ∈ ℝ)
14		1red 11215	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℝ)
15	11, 14	remulcld 11244	. . . . . 6 ⊢ (𝜑 → (𝑀 · 1) ∈ ℝ)
16	15, 12	resubcld 11642	. . . . 5 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℝ)
17	11	recnd 11242	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
18		1cnd 11209	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℂ)
19	5	recnd 11242	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℂ)
20	17, 18, 19	subdid 11670	. . . . . 6 ⊢ (𝜑 → (𝑀 · (1 − 𝐾)) = ((𝑀 · 1) − (𝑀 · 𝐾)))
21	18, 19	subcld 11571	. . . . . . 7 ⊢ (𝜑 → (1 − 𝐾) ∈ ℂ)
22		ttgcontlem1.o	. . . . . . 7 ⊢ (𝜑 → 𝑀 ≠ 0)
23		ttgcontlem1.q	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≠ 1)
24	23	necomd 2997	. . . . . . . 8 ⊢ (𝜑 → 1 ≠ 𝐾)
25	18, 19, 24	subne0d 11580	. . . . . . 7 ⊢ (𝜑 → (1 − 𝐾) ≠ 0)
26	17, 21, 22, 25	mulne0d 11866	. . . . . 6 ⊢ (𝜑 → (𝑀 · (1 − 𝐾)) ≠ 0)
27	20, 26	eqnetrrd 3010	. . . . 5 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ≠ 0)
28	13, 16, 27	redivcld 12042	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ ℝ)
29		0xr 11261	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
30	3	rexrd 11264	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ ℝ^*)
31		iccgelb 13380	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ 𝐿 ∈ ℝ^* ∧ 𝑀 ∈ (0[,]𝐿)) → 0 ≤ 𝑀)
32	29, 30, 10, 31	mp3an2i 1467	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑀)
33	11, 32, 22	ne0gt0d 11351	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
34	11, 33	elrpd 13013	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℝ⁺)
35	14	rexrd 11264	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℝ^*)
36		iccleub 13379	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ 𝐾 ∈ (0[,]1)) → 𝐾 ≤ 1)
37	29, 35, 4, 36	mp3an2i 1467	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≤ 1)
38	5, 14, 37, 24	leneltd 11368	. . . . . . . 8 ⊢ (𝜑 → 𝐾 < 1)
39		difrp 13012	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐾 < 1 ↔ (1 − 𝐾) ∈ ℝ⁺))
40	5, 14, 39	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → (𝐾 < 1 ↔ (1 − 𝐾) ∈ ℝ⁺))
41	38, 40	mpbid 231	. . . . . . 7 ⊢ (𝜑 → (1 − 𝐾) ∈ ℝ⁺)
42	34, 41	rpmulcld 13032	. . . . . 6 ⊢ (𝜑 → (𝑀 · (1 − 𝐾)) ∈ ℝ⁺)
43	20, 42	eqeltrrd 2835	. . . . 5 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℝ⁺)
44	3, 11	resubcld 11642	. . . . . . 7 ⊢ (𝜑 → (𝐿 − 𝑀) ∈ ℝ)
45		iccleub 13379	. . . . . . . . 9 ⊢ ((0 ∈ ℝ^* ∧ 𝐿 ∈ ℝ^* ∧ 𝑀 ∈ (0[,]𝐿)) → 𝑀 ≤ 𝐿)
46	29, 30, 10, 45	mp3an2i 1467	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ≤ 𝐿)
47	3, 11	subge0d 11804	. . . . . . . 8 ⊢ (𝜑 → (0 ≤ (𝐿 − 𝑀) ↔ 𝑀 ≤ 𝐿))
48	46, 47	mpbird 257	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (𝐿 − 𝑀))
49		iccgelb 13380	. . . . . . . 8 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ 𝐾 ∈ (0[,]1)) → 0 ≤ 𝐾)
50	29, 35, 4, 49	mp3an2i 1467	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 𝐾)
51	44, 5, 48, 50	mulge0d 11791	. . . . . 6 ⊢ (𝜑 → 0 ≤ ((𝐿 − 𝑀) · 𝐾))
52	3	recnd 11242	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℂ)
53	52, 17, 19	subdird 11671	. . . . . 6 ⊢ (𝜑 → ((𝐿 − 𝑀) · 𝐾) = ((𝐿 · 𝐾) − (𝑀 · 𝐾)))
54	51, 53	breqtrd 5175	. . . . 5 ⊢ (𝜑 → 0 ≤ ((𝐿 · 𝐾) − (𝑀 · 𝐾)))
55	13, 43, 54	divge0d 13056	. . . 4 ⊢ (𝜑 → 0 ≤ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))))
56		ttgcontlem1.s	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ≤ (𝑀 / 𝐾))
57		ttgcontlem1.p	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ≠ 0)
58	5, 50, 57	ne0gt0d 11351	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < 𝐾)
59	5, 58	elrpd 13013	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℝ⁺)
60	3, 11, 59	lemuldivd 13065	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 · 𝐾) ≤ 𝑀 ↔ 𝐿 ≤ (𝑀 / 𝐾)))
61	56, 60	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → (𝐿 · 𝐾) ≤ 𝑀)
62	17	mulridd 11231	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 1) = 𝑀)
63	61, 62	breqtrrd 5177	. . . . . . 7 ⊢ (𝜑 → (𝐿 · 𝐾) ≤ (𝑀 · 1))
64	6, 15, 12, 63	lesub1dd 11830	. . . . . 6 ⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ ((𝑀 · 1) − (𝑀 · 𝐾)))
65	17, 18	mulcld 11234	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 1) ∈ ℂ)
66	17, 19	mulcld 11234	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 𝐾) ∈ ℂ)
67	65, 66	subcld 11571	. . . . . . 7 ⊢ (𝜑 → ((𝑀 · 1) − (𝑀 · 𝐾)) ∈ ℂ)
68	67	mulridd 11231	. . . . . 6 ⊢ (𝜑 → (((𝑀 · 1) − (𝑀 · 𝐾)) · 1) = ((𝑀 · 1) − (𝑀 · 𝐾)))
69	64, 68	breqtrrd 5177	. . . . 5 ⊢ (𝜑 → ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ (((𝑀 · 1) − (𝑀 · 𝐾)) · 1))
70	13, 14, 43	ledivmuld 13069	. . . . 5 ⊢ (𝜑 → ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1 ↔ ((𝐿 · 𝐾) − (𝑀 · 𝐾)) ≤ (((𝑀 · 1) − (𝑀 · 𝐾)) · 1)))
71	69, 70	mpbird 257	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1)
72		elicc01 13443	. . . 4 ⊢ ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1) ↔ ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ ℝ ∧ 0 ≤ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∧ (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ≤ 1))
73	28, 55, 71, 72	syl3anbrc 1344	. . 3 ⊢ (𝜑 → (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1))
74		ttgcontlem1.h	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ ℂVec)
75	74	cvsclm 24642	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ ℂMod)
76		ttgbtwnid.2	. . . . . . . 8 ⊢ (𝜑 → (0[,]1) ⊆ 𝑅)
77	76, 2	sseldd 3984	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ 𝑅)
78		0elunit 13446	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]1)
79		iccss2 13395	. . . . . . . . . 10 ⊢ ((0 ∈ (0[,]1) ∧ 𝐿 ∈ (0[,]1)) → (0[,]𝐿) ⊆ (0[,]1))
80	78, 2, 79	sylancr 588	. . . . . . . . 9 ⊢ (𝜑 → (0[,]𝐿) ⊆ (0[,]1))
81	80, 76	sstrd 3993	. . . . . . . 8 ⊢ (𝜑 → (0[,]𝐿) ⊆ 𝑅)
82	81, 10	sseldd 3984	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ 𝑅)
83		eqid 2733	. . . . . . . 8 ⊢ (Scalar‘𝐻) = (Scalar‘𝐻)
84		ttgbtwnid.r	. . . . . . . 8 ⊢ 𝑅 = (Base‘(Scalar‘𝐻))
85	83, 84	clmsubcl 24602	. . . . . . 7 ⊢ ((𝐻 ∈ ℂMod ∧ 𝐿 ∈ 𝑅 ∧ 𝑀 ∈ 𝑅) → (𝐿 − 𝑀) ∈ 𝑅)
86	75, 77, 82, 85	syl3anc 1372	. . . . . 6 ⊢ (𝜑 → (𝐿 − 𝑀) ∈ 𝑅)
87	83, 84	cvsdivcl 24649	. . . . . 6 ⊢ ((𝐻 ∈ ℂVec ∧ ((𝐿 − 𝑀) ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ∧ 𝑀 ≠ 0)) → ((𝐿 − 𝑀) / 𝑀) ∈ 𝑅)
88	74, 86, 82, 22, 87	syl13anc 1373	. . . . 5 ⊢ (𝜑 → ((𝐿 − 𝑀) / 𝑀) ∈ 𝑅)
89	76, 4	sseldd 3984	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ 𝑅)
90		1elunit 13447	. . . . . . . . 9 ⊢ 1 ∈ (0[,]1)
91	90	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ (0[,]1))
92	76, 91	sseldd 3984	. . . . . . 7 ⊢ (𝜑 → 1 ∈ 𝑅)
93	83, 84	clmsubcl 24602	. . . . . . 7 ⊢ ((𝐻 ∈ ℂMod ∧ 1 ∈ 𝑅 ∧ 𝐾 ∈ 𝑅) → (1 − 𝐾) ∈ 𝑅)
94	75, 92, 89, 93	syl3anc 1372	. . . . . 6 ⊢ (𝜑 → (1 − 𝐾) ∈ 𝑅)
95	83, 84	cvsdivcl 24649	. . . . . 6 ⊢ ((𝐻 ∈ ℂVec ∧ (𝐾 ∈ 𝑅 ∧ (1 − 𝐾) ∈ 𝑅 ∧ (1 − 𝐾) ≠ 0)) → (𝐾 / (1 − 𝐾)) ∈ 𝑅)
96	74, 89, 94, 25, 95	syl13anc 1373	. . . . 5 ⊢ (𝜑 → (𝐾 / (1 − 𝐾)) ∈ 𝑅)
97		clmgrp 24584	. . . . . . 7 ⊢ (𝐻 ∈ ℂMod → 𝐻 ∈ Grp)
98	75, 97	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ Grp)
99		ttgelitv.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
100		ttgelitv.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
101		ttgitvval.b	. . . . . . 7 ⊢ 𝑃 = (Base‘𝐻)
102		ttgitvval.m	. . . . . . 7 ⊢ − = (-_g‘𝐻)
103	101, 102	grpsubcl 18903	. . . . . 6 ⊢ ((𝐻 ∈ Grp ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃) → (𝑌 − 𝑋) ∈ 𝑃)
104	98, 99, 100, 103	syl3anc 1372	. . . . 5 ⊢ (𝜑 → (𝑌 − 𝑋) ∈ 𝑃)
105		ttgitvval.s	. . . . . 6 ⊢ · = ( ·_𝑠 ‘𝐻)
106	101, 83, 105, 84	clmvsass 24605	. . . . 5 ⊢ ((𝐻 ∈ ℂMod ∧ (((𝐿 − 𝑀) / 𝑀) ∈ 𝑅 ∧ (𝐾 / (1 − 𝐾)) ∈ 𝑅 ∧ (𝑌 − 𝑋) ∈ 𝑃)) → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))))
107	75, 88, 96, 104, 106	syl13anc 1373	. . . 4 ⊢ (𝜑 → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))))
108	44	recnd 11242	. . . . . . 7 ⊢ (𝜑 → (𝐿 − 𝑀) ∈ ℂ)
109	108, 17, 19, 21, 22, 25	divmuldivd 12031	. . . . . 6 ⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) = (((𝐿 − 𝑀) · 𝐾) / (𝑀 · (1 − 𝐾))))
110	53, 20	oveq12d 7427	. . . . . 6 ⊢ (𝜑 → (((𝐿 − 𝑀) · 𝐾) / (𝑀 · (1 − 𝐾))) = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))))
111	109, 110	eqtrd 2773	. . . . 5 ⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))))
112	111	oveq1d 7424	. . . 4 ⊢ (𝜑 → ((((𝐿 − 𝑀) / 𝑀) · (𝐾 / (1 − 𝐾))) · (𝑌 − 𝑋)) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))
113		ttgcontlem1.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
114	101, 102	grpsubcl 18903	. . . . . . . 8 ⊢ ((𝐻 ∈ Grp ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑋 − 𝐴) ∈ 𝑃)
115	98, 100, 113, 114	syl3anc 1372	. . . . . . 7 ⊢ (𝜑 → (𝑋 − 𝐴) ∈ 𝑃)
116		ttgcontlem1.y	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 − 𝐴) = (𝐾 · (𝑌 − 𝐴)))
117	116	oveq2d 7425	. . . . . . . . 9 ⊢ (𝜑 → ((1 − 𝐾) · (𝑋 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
118	19, 21	mulcomd 11235	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 · (1 − 𝐾)) = ((1 − 𝐾) · 𝐾))
119	118	oveq1d 7424	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)))
120	101, 102	grpsubcl 18903	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ 𝑌 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑌 − 𝐴) ∈ 𝑃)
121	98, 99, 113, 120	syl3anc 1372	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 − 𝐴) ∈ 𝑃)
122	101, 83, 105, 84	clmvsass 24605	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ (𝐾 ∈ 𝑅 ∧ (1 − 𝐾) ∈ 𝑅 ∧ (𝑌 − 𝐴) ∈ 𝑃)) → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))))
123	75, 89, 94, 121, 122	syl13anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾 · (1 − 𝐾)) · (𝑌 − 𝐴)) = (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))))
124	101, 83, 105, 84	clmvsass 24605	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ ((1 − 𝐾) ∈ 𝑅 ∧ 𝐾 ∈ 𝑅 ∧ (𝑌 − 𝐴) ∈ 𝑃)) → (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
125	75, 94, 89, 121, 124	syl13anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → (((1 − 𝐾) · 𝐾) · (𝑌 − 𝐴)) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
126	119, 123, 125	3eqtr3d 2781	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))) = ((1 − 𝐾) · (𝐾 · (𝑌 − 𝐴))))
127		eqid 2733	. . . . . . . . . . . . 13 ⊢ (-_g‘(Scalar‘𝐻)) = (-_g‘(Scalar‘𝐻))
128		clmlmod 24583	. . . . . . . . . . . . . 14 ⊢ (𝐻 ∈ ℂMod → 𝐻 ∈ LMod)
129	75, 128	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ∈ LMod)
130	101, 105, 83, 84, 102, 127, 129, 92, 89, 121	lmodsubdir 20530	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1(-_g‘(Scalar‘𝐻))𝐾) · (𝑌 − 𝐴)) = ((1 · (𝑌 − 𝐴)) − (𝐾 · (𝑌 − 𝐴))))
131	83, 84	clmsub 24596	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ ℂMod ∧ 1 ∈ 𝑅 ∧ 𝐾 ∈ 𝑅) → (1 − 𝐾) = (1(-_g‘(Scalar‘𝐻))𝐾))
132	75, 92, 89, 131	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 − 𝐾) = (1(-_g‘(Scalar‘𝐻))𝐾))
133	132	oveq1d 7424	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = ((1(-_g‘(Scalar‘𝐻))𝐾) · (𝑌 − 𝐴)))
134	101, 105	clmvs1 24609	. . . . . . . . . . . . . . 15 ⊢ ((𝐻 ∈ ℂMod ∧ (𝑌 − 𝐴) ∈ 𝑃) → (1 · (𝑌 − 𝐴)) = (𝑌 − 𝐴))
135	75, 121, 134	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 · (𝑌 − 𝐴)) = (𝑌 − 𝐴))
136	135	eqcomd 2739	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 − 𝐴) = (1 · (𝑌 − 𝐴)))
137	136, 116	oveq12d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = ((1 · (𝑌 − 𝐴)) − (𝐾 · (𝑌 − 𝐴))))
138	130, 133, 137	3eqtr4d 2783	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = ((𝑌 − 𝐴) − (𝑋 − 𝐴)))
139	101, 102	grpnnncan2 18920	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ (𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃)) → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = (𝑌 − 𝑋))
140	98, 99, 100, 113, 139	syl13anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 − 𝐴) − (𝑋 − 𝐴)) = (𝑌 − 𝑋))
141	138, 140	eqtrd 2773	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − 𝐾) · (𝑌 − 𝐴)) = (𝑌 − 𝑋))
142	141	oveq2d 7425	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 · ((1 − 𝐾) · (𝑌 − 𝐴))) = (𝐾 · (𝑌 − 𝑋)))
143	117, 126, 142	3eqtr2rd 2780	. . . . . . . 8 ⊢ (𝜑 → (𝐾 · (𝑌 − 𝑋)) = ((1 − 𝐾) · (𝑋 − 𝐴)))
144	101, 105, 83, 84, 74, 89, 94, 104, 115, 57, 143	cvsmuleqdivd 24650	. . . . . . 7 ⊢ (𝜑 → (𝑌 − 𝑋) = (((1 − 𝐾) / 𝐾) · (𝑋 − 𝐴)))
145	101, 105, 83, 84, 74, 94, 89, 104, 115, 25, 57, 144	cvsdiveqd 24651	. . . . . 6 ⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) = (𝑋 − 𝐴))
146	145, 115	eqeltrd 2834	. . . . 5 ⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) ∈ 𝑃)
147		ttgcontlem1.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 = (𝐴 + (𝐿 · (𝑁 − 𝐴))))
148		ttgcontlem1.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ 𝑃)
149	101, 102	grpsubcl 18903	. . . . . . . . . 10 ⊢ ((𝐻 ∈ Grp ∧ 𝑁 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃) → (𝑁 − 𝐴) ∈ 𝑃)
150	98, 148, 113, 149	syl3anc 1372	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 − 𝐴) ∈ 𝑃)
151	101, 83, 105, 84	lmodvscl 20489	. . . . . . . . 9 ⊢ ((𝐻 ∈ LMod ∧ 𝐿 ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃) → (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃)
152	129, 77, 150, 151	syl3anc 1372	. . . . . . . 8 ⊢ (𝜑 → (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃)
153		ttgitvval.p	. . . . . . . . 9 ⊢ + = (+_g‘𝐻)
154	101, 153	grpcl 18827	. . . . . . . 8 ⊢ ((𝐻 ∈ Grp ∧ 𝐴 ∈ 𝑃 ∧ (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃) → (𝐴 + (𝐿 · (𝑁 − 𝐴))) ∈ 𝑃)
155	98, 113, 152, 154	syl3anc 1372	. . . . . . 7 ⊢ (𝜑 → (𝐴 + (𝐿 · (𝑁 − 𝐴))) ∈ 𝑃)
156	147, 155	eqeltrd 2834	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
157	101, 102	grpsubcl 18903	. . . . . 6 ⊢ ((𝐻 ∈ Grp ∧ 𝐵 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃) → (𝐵 − 𝑋) ∈ 𝑃)
158	98, 156, 100, 157	syl3anc 1372	. . . . 5 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ 𝑃)
159		ttgcontlem1.r	. . . . . 6 ⊢ (𝜑 → 𝐿 ≠ 𝑀)
160	52, 17, 159	subne0d 11580	. . . . 5 ⊢ (𝜑 → (𝐿 − 𝑀) ≠ 0)
161		ttgcontlem1.x	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 − 𝐴) = (𝑀 · (𝑁 − 𝐴)))
162	161	oveq2d 7425	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑋 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
163	17, 108	mulcomd 11235	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 · (𝐿 − 𝑀)) = ((𝐿 − 𝑀) · 𝑀))
164	163	oveq1d 7424	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)))
165	101, 83, 105, 84	clmvsass 24605	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ (𝑀 ∈ 𝑅 ∧ (𝐿 − 𝑀) ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃)) → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))))
166	75, 82, 86, 150, 165	syl13anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · (𝐿 − 𝑀)) · (𝑁 − 𝐴)) = (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))))
167	101, 83, 105, 84	clmvsass 24605	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ ℂMod ∧ ((𝐿 − 𝑀) ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ∧ (𝑁 − 𝐴) ∈ 𝑃)) → (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
168	75, 86, 82, 150, 167	syl13anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐿 − 𝑀) · 𝑀) · (𝑁 − 𝐴)) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
169	164, 166, 168	3eqtr3d 2781	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))) = ((𝐿 − 𝑀) · (𝑀 · (𝑁 − 𝐴))))
170	101, 105, 83, 84, 102, 127, 129, 77, 82, 150	lmodsubdir 20530	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿(-_g‘(Scalar‘𝐻))𝑀) · (𝑁 − 𝐴)) = ((𝐿 · (𝑁 − 𝐴)) − (𝑀 · (𝑁 − 𝐴))))
171	83, 84	clmsub 24596	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ ℂMod ∧ 𝐿 ∈ 𝑅 ∧ 𝑀 ∈ 𝑅) → (𝐿 − 𝑀) = (𝐿(-_g‘(Scalar‘𝐻))𝑀))
172	75, 77, 82, 171	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 𝑀) = (𝐿(-_g‘(Scalar‘𝐻))𝑀))
173	172	oveq1d 7424	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = ((𝐿(-_g‘(Scalar‘𝐻))𝑀) · (𝑁 − 𝐴)))
174	147	oveq1d 7424	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 − 𝐴) = ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴))
175		lmodabl 20519	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ LMod → 𝐻 ∈ Abel)
176	129, 175	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻 ∈ Abel)
177	101, 153, 102	ablpncan2 19683	. . . . . . . . . . . . . . 15 ⊢ ((𝐻 ∈ Abel ∧ 𝐴 ∈ 𝑃 ∧ (𝐿 · (𝑁 − 𝐴)) ∈ 𝑃) → ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴) = (𝐿 · (𝑁 − 𝐴)))
178	176, 113, 152, 177	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 + (𝐿 · (𝑁 − 𝐴))) − 𝐴) = (𝐿 · (𝑁 − 𝐴)))
179	174, 178	eqtrd 2773	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐿 · (𝑁 − 𝐴)))
180	179, 161	oveq12d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = ((𝐿 · (𝑁 − 𝐴)) − (𝑀 · (𝑁 − 𝐴))))
181	170, 173, 180	3eqtr4d 2783	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = ((𝐵 − 𝐴) − (𝑋 − 𝐴)))
182	101, 102	grpnnncan2 18920	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ (𝐵 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃)) → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = (𝐵 − 𝑋))
183	98, 156, 100, 113, 182	syl13anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 − 𝐴) − (𝑋 − 𝐴)) = (𝐵 − 𝑋))
184	181, 183	eqtrd 2773	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 𝑀) · (𝑁 − 𝐴)) = (𝐵 − 𝑋))
185	184	oveq2d 7425	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 · ((𝐿 − 𝑀) · (𝑁 − 𝐴))) = (𝑀 · (𝐵 − 𝑋)))
186	162, 169, 185	3eqtr2rd 2780	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · (𝐵 − 𝑋)) = ((𝐿 − 𝑀) · (𝑋 − 𝐴)))
187	101, 105, 83, 84, 74, 82, 86, 158, 115, 22, 186	cvsmuleqdivd 24650	. . . . . . 7 ⊢ (𝜑 → (𝐵 − 𝑋) = (((𝐿 − 𝑀) / 𝑀) · (𝑋 − 𝐴)))
188	101, 105, 83, 84, 74, 86, 82, 158, 115, 160, 22, 187	cvsdiveqd 24651	. . . . . 6 ⊢ (𝜑 → ((𝑀 / (𝐿 − 𝑀)) · (𝐵 − 𝑋)) = (𝑋 − 𝐴))
189	145, 188	eqtr4d 2776	. . . . 5 ⊢ (𝜑 → ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋)) = ((𝑀 / (𝐿 − 𝑀)) · (𝐵 − 𝑋)))
190	101, 105, 83, 84, 74, 82, 86, 146, 158, 22, 160, 189	cvsdiveqd 24651	. . . 4 ⊢ (𝜑 → (((𝐿 − 𝑀) / 𝑀) · ((𝐾 / (1 − 𝐾)) · (𝑌 − 𝑋))) = (𝐵 − 𝑋))
191	107, 112, 190	3eqtr3rd 2782	. . 3 ⊢ (𝜑 → (𝐵 − 𝑋) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))
192		oveq1 7416	. . . 4 ⊢ (𝑘 = (((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) → (𝑘 · (𝑌 − 𝑋)) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋)))
193	192	rspceeqv 3634	. . 3 ⊢ (((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) ∈ (0[,]1) ∧ (𝐵 − 𝑋) = ((((𝐿 · 𝐾) − (𝑀 · 𝐾)) / ((𝑀 · 1) − (𝑀 · 𝐾))) · (𝑌 − 𝑋))) → ∃𝑘 ∈ (0[,]1)(𝐵 − 𝑋) = (𝑘 · (𝑌 − 𝑋)))
194	73, 191, 193	syl2anc 585	. 2 ⊢ (𝜑 → ∃𝑘 ∈ (0[,]1)(𝐵 − 𝑋) = (𝑘 · (𝑌 − 𝑋)))
195		ttgval.n	. . 3 ⊢ 𝐺 = (toTG‘𝐻)
196		ttgitvval.i	. . 3 ⊢ 𝐼 = (Itv‘𝐺)
197	195, 196, 101, 102, 105, 100, 99, 74, 156	ttgelitv 28140	. 2 ⊢ (𝜑 → (𝐵 ∈ (𝑋𝐼𝑌) ↔ ∃𝑘 ∈ (0[,]1)(𝐵 − 𝑋) = (𝑘 · (𝑌 − 𝑋))))
198	194, 197	mpbird 257	1 ⊢ (𝜑 → 𝐵 ∈ (𝑋𝐼𝑌))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 ∃wrex 3071 ⊆ wss 3949 class class class wbr 5149 ‘cfv 6544 (class class class)co 7409 ℝcr 11109 0cc0 11110 1c1 11111 · cmul 11115 ℝ^*cxr 11247 < clt 11248 ≤ cle 11249 − cmin 11444 / cdiv 11871 ℝ⁺crp 12974 [,]cicc 13327 Basecbs 17144 +_gcplusg 17197 Scalarcsca 17200 ·_𝑠 cvsca 17201 Grpcgrp 18819 -_gcsg 18821 Abelcabl 19649 LModclmod 20471 ℂModcclm 24578 ℂVecccvs 24639 Itvcitv 27684 toTGcttg 28124

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187 ax-addf 11189 ax-mulf 11190

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-1st 7975 df-2nd 7976 df-tpos 8211 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-div 11872 df-nn 12213 df-2 12275 df-3 12276 df-4 12277 df-5 12278 df-6 12279 df-7 12280 df-8 12281 df-9 12282 df-n0 12473 df-z 12559 df-dec 12678 df-uz 12823 df-rp 12975 df-icc 13331 df-fz 13485 df-struct 17080 df-sets 17097 df-slot 17115 df-ndx 17127 df-base 17145 df-ress 17174 df-plusg 17210 df-mulr 17211 df-starv 17212 df-tset 17216 df-ple 17217 df-ds 17219 df-unif 17220 df-0g 17387 df-mgm 18561 df-sgrp 18610 df-mnd 18626 df-grp 18822 df-minusg 18823 df-sbg 18824 df-subg 19003 df-cmn 19650 df-abl 19651 df-mgp 19988 df-ur 20005 df-ring 20058 df-cring 20059 df-oppr 20150 df-dvdsr 20171 df-unit 20172 df-invr 20202 df-dvr 20215 df-subrg 20317 df-drng 20359 df-lmod 20473 df-lvec 20714 df-cnfld 20945 df-clm 24579 df-cvs 24640 df-itv 27686 df-lng 27687 df-ttg 28125

This theorem is referenced by: (None)

W3C validator