constrsslem

Description: Lemma for constrss . This lemma requires the additional condition that 0 is the constructible number; that condition is removed in constrss . (Proposed by Saveliy Skresanov, 23-JUn-2025.) (Contributed by Thierry Arnoux, 25-Jun-2025)

	Ref	Expression
Hypotheses	constr0.1	$⊢ C = rec ((s \in V ⟼ \{x \in ℂ \| (\exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in s \exists b \in s \exists c \in s \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}), \{0, 1\})$
	constrsscn.1	$⊢ φ \to N \in On$
	constrsslem.1	$⊢ φ \to 0 \in C (N)$
Assertion	constrsslem	$⊢ φ \to C (N) \subseteq C (suc N)$

Proof

Step	Hyp	Ref	Expression
1		constr0.1	$⊢ C = rec ((s \in V ⟼ \{x \in ℂ \| (\exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in s \exists b \in s \exists c \in s \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}), \{0, 1\})$
2		constrsscn.1	$⊢ φ \to N \in On$
3		constrsslem.1	$⊢ φ \to 0 \in C (N)$
4	1 2	constrsscn	$⊢ φ \to C (N) \subseteq ℂ$
5	4	sselda	$⊢ (φ \land x \in C (N)) \to x \in ℂ$
6		simpr	$⊢ (φ \land x \in C (N)) \to x \in C (N)$
7		id	$⊢ a = x \to a = x$
8		oveq2	$⊢ a = x \to b - a = b - x$
9	8	oveq2d	$⊢ a = x \to t (b - a) = t (b - x)$
10	7 9	oveq12d	$⊢ a = x \to a + t (b - a) = x + t (b - x)$
11	10	eqeq2d	$⊢ a = x \to (x = a + t (b - a) \leftrightarrow x = x + t (b - x))$
12	11	anbi1d	$⊢ a = x \to ((x = a + t (b - a) \land \|x - c\| = \|e - f\|) \leftrightarrow (x = x + t (b - x) \land \|x - c\| = \|e - f\|))$
13	12	rexbidv	$⊢ a = x \to (\exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \leftrightarrow \exists t \in ℝ (x = x + t (b - x) \land \|x - c\| = \|e - f\|))$
14	13	2rexbidv	$⊢ a = x \to (\exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \leftrightarrow \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = x + t (b - x) \land \|x - c\| = \|e - f\|))$
15	14	2rexbidv	$⊢ a = x \to (\exists b \in C (N) \exists c \in C (N) \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \leftrightarrow \exists b \in C (N) \exists c \in C (N) \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = x + t (b - x) \land \|x - c\| = \|e - f\|))$
16	15	adantl	$⊢ ((φ \land x \in C (N)) \land a = x) \to (\exists b \in C (N) \exists c \in C (N) \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \leftrightarrow \exists b \in C (N) \exists c \in C (N) \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = x + t (b - x) \land \|x - c\| = \|e - f\|))$
17	3	adantr	$⊢ (φ \land x \in C (N)) \to 0 \in C (N)$
18		oveq1	$⊢ b = 0 \to b - x = 0 - x$
19	18	oveq2d	$⊢ b = 0 \to t (b - x) = t (0 - x)$
20	19	oveq2d	$⊢ b = 0 \to x + t (b - x) = x + t (0 - x)$
21	20	eqeq2d	$⊢ b = 0 \to (x = x + t (b - x) \leftrightarrow x = x + t (0 - x))$
22	21	anbi1d	$⊢ b = 0 \to ((x = x + t (b - x) \land \|x - c\| = \|e - f\|) \leftrightarrow (x = x + t (0 - x) \land \|x - c\| = \|e - f\|))$
23	22	2rexbidv	$⊢ b = 0 \to (\exists f \in C (N) \exists t \in ℝ (x = x + t (b - x) \land \|x - c\| = \|e - f\|) \leftrightarrow \exists f \in C (N) \exists t \in ℝ (x = x + t (0 - x) \land \|x - c\| = \|e - f\|))$
24	23	2rexbidv	$⊢ b = 0 \to (\exists c \in C (N) \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = x + t (b - x) \land \|x - c\| = \|e - f\|) \leftrightarrow \exists c \in C (N) \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = x + t (0 - x) \land \|x - c\| = \|e - f\|))$
25	24	adantl	$⊢ ((φ \land x \in C (N)) \land b = 0) \to (\exists c \in C (N) \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = x + t (b - x) \land \|x - c\| = \|e - f\|) \leftrightarrow \exists c \in C (N) \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = x + t (0 - x) \land \|x - c\| = \|e - f\|))$
26		oveq2	$⊢ c = 0 \to x - c = x - 0$
27	26	fveq2d	$⊢ c = 0 \to \|x - c\| = \|x - 0\|$
28	27	eqeq1d	$⊢ c = 0 \to (\|x - c\| = \|e - f\| \leftrightarrow \|x - 0\| = \|e - f\|)$
29	28	anbi2d	$⊢ c = 0 \to ((x = x + t (0 - x) \land \|x - c\| = \|e - f\|) \leftrightarrow (x = x + t (0 - x) \land \|x - 0\| = \|e - f\|))$
30	29	rexbidv	$⊢ c = 0 \to (\exists t \in ℝ (x = x + t (0 - x) \land \|x - c\| = \|e - f\|) \leftrightarrow \exists t \in ℝ (x = x + t (0 - x) \land \|x - 0\| = \|e - f\|))$
31	30	2rexbidv	$⊢ c = 0 \to (\exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = x + t (0 - x) \land \|x - c\| = \|e - f\|) \leftrightarrow \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = x + t (0 - x) \land \|x - 0\| = \|e - f\|))$
32	31	adantl	$⊢ ((φ \land x \in C (N)) \land c = 0) \to (\exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = x + t (0 - x) \land \|x - c\| = \|e - f\|) \leftrightarrow \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = x + t (0 - x) \land \|x - 0\| = \|e - f\|))$
33		oveq1	$⊢ e = x \to e - f = x - f$
34	33	fveq2d	$⊢ e = x \to \|e - f\| = \|x - f\|$
35	34	eqeq2d	$⊢ e = x \to (\|x - 0\| = \|e - f\| \leftrightarrow \|x - 0\| = \|x - f\|)$
36	35	anbi2d	$⊢ e = x \to ((x = x + t (0 - x) \land \|x - 0\| = \|e - f\|) \leftrightarrow (x = x + t (0 - x) \land \|x - 0\| = \|x - f\|))$
37	36	2rexbidv	$⊢ e = x \to (\exists f \in C (N) \exists t \in ℝ (x = x + t (0 - x) \land \|x - 0\| = \|e - f\|) \leftrightarrow \exists f \in C (N) \exists t \in ℝ (x = x + t (0 - x) \land \|x - 0\| = \|x - f\|))$
38	37	adantl	$⊢ ((φ \land x \in C (N)) \land e = x) \to (\exists f \in C (N) \exists t \in ℝ (x = x + t (0 - x) \land \|x - 0\| = \|e - f\|) \leftrightarrow \exists f \in C (N) \exists t \in ℝ (x = x + t (0 - x) \land \|x - 0\| = \|x - f\|))$
39		oveq2	$⊢ f = 0 \to x - f = x - 0$
40	39	fveq2d	$⊢ f = 0 \to \|x - f\| = \|x - 0\|$
41	40	eqeq2d	$⊢ f = 0 \to (\|x - 0\| = \|x - f\| \leftrightarrow \|x - 0\| = \|x - 0\|)$
42	41	anbi2d	$⊢ f = 0 \to ((x = x + t (0 - x) \land \|x - 0\| = \|x - f\|) \leftrightarrow (x = x + t (0 - x) \land \|x - 0\| = \|x - 0\|))$
43	42	rexbidv	$⊢ f = 0 \to (\exists t \in ℝ (x = x + t (0 - x) \land \|x - 0\| = \|x - f\|) \leftrightarrow \exists t \in ℝ (x = x + t (0 - x) \land \|x - 0\| = \|x - 0\|))$
44	43	adantl	$⊢ ((φ \land x \in C (N)) \land f = 0) \to (\exists t \in ℝ (x = x + t (0 - x) \land \|x - 0\| = \|x - f\|) \leftrightarrow \exists t \in ℝ (x = x + t (0 - x) \land \|x - 0\| = \|x - 0\|))$
45		0red	$⊢ (φ \land x \in C (N)) \to 0 \in ℝ$
46		oveq1	$⊢ t = 0 \to t (0 - x) = 0 \cdot (0 - x)$
47	46	oveq2d	$⊢ t = 0 \to x + t (0 - x) = x + 0 \cdot (0 - x)$
48	47	eqeq2d	$⊢ t = 0 \to (x = x + t (0 - x) \leftrightarrow x = x + 0 \cdot (0 - x))$
49	48	anbi1d	$⊢ t = 0 \to ((x = x + t (0 - x) \land \|x - 0\| = \|x - 0\|) \leftrightarrow (x = x + 0 \cdot (0 - x) \land \|x - 0\| = \|x - 0\|))$
50	49	adantl	$⊢ ((φ \land x \in C (N)) \land t = 0) \to ((x = x + t (0 - x) \land \|x - 0\| = \|x - 0\|) \leftrightarrow (x = x + 0 \cdot (0 - x) \land \|x - 0\| = \|x - 0\|))$
51		0cnd	$⊢ (φ \land x \in C (N)) \to 0 \in ℂ$
52	51 5	subcld	$⊢ (φ \land x \in C (N)) \to 0 - x \in ℂ$
53	52	mul02d	$⊢ (φ \land x \in C (N)) \to 0 \cdot (0 - x) = 0$
54	53	oveq2d	$⊢ (φ \land x \in C (N)) \to x + 0 \cdot (0 - x) = x + 0$
55	5	addridd	$⊢ (φ \land x \in C (N)) \to x + 0 = x$
56	54 55	eqtr2d	$⊢ (φ \land x \in C (N)) \to x = x + 0 \cdot (0 - x)$
57		eqidd	$⊢ (φ \land x \in C (N)) \to \|x - 0\| = \|x - 0\|$
58	56 57	jca	$⊢ (φ \land x \in C (N)) \to (x = x + 0 \cdot (0 - x) \land \|x - 0\| = \|x - 0\|)$
59	45 50 58	rspcedvd	$⊢ (φ \land x \in C (N)) \to \exists t \in ℝ (x = x + t (0 - x) \land \|x - 0\| = \|x - 0\|)$
60	17 44 59	rspcedvd	$⊢ (φ \land x \in C (N)) \to \exists f \in C (N) \exists t \in ℝ (x = x + t (0 - x) \land \|x - 0\| = \|x - f\|)$
61	6 38 60	rspcedvd	$⊢ (φ \land x \in C (N)) \to \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = x + t (0 - x) \land \|x - 0\| = \|e - f\|)$
62	17 32 61	rspcedvd	$⊢ (φ \land x \in C (N)) \to \exists c \in C (N) \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = x + t (0 - x) \land \|x - c\| = \|e - f\|)$
63	17 25 62	rspcedvd	$⊢ (φ \land x \in C (N)) \to \exists b \in C (N) \exists c \in C (N) \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = x + t (b - x) \land \|x - c\| = \|e - f\|)$
64	6 16 63	rspcedvd	$⊢ (φ \land x \in C (N)) \to \exists a \in C (N) \exists b \in C (N) \exists c \in C (N) \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)$
65	64	3mix2d	$⊢ (φ \land x \in C (N)) \to (\exists a \in C (N) \exists b \in C (N) \exists c \in C (N) \exists d \in C (N) \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in C (N) \exists b \in C (N) \exists c \in C (N) \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in C (N) \exists b \in C (N) \exists c \in C (N) \exists d \in C (N) \exists e \in C (N) \exists f \in C (N) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))$
66		eqid	$⊢ C (N) = C (N)$
67	1 2 66	constrsuc	$⊢ φ \to (x \in C (suc N) \leftrightarrow (x \in ℂ \land (\exists a \in C (N) \exists b \in C (N) \exists c \in C (N) \exists d \in C (N) \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in C (N) \exists b \in C (N) \exists c \in C (N) \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in C (N) \exists b \in C (N) \exists c \in C (N) \exists d \in C (N) \exists e \in C (N) \exists f \in C (N) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))))$
68	67	adantr	$⊢ (φ \land x \in C (N)) \to (x \in C (suc N) \leftrightarrow (x \in ℂ \land (\exists a \in C (N) \exists b \in C (N) \exists c \in C (N) \exists d \in C (N) \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in C (N) \exists b \in C (N) \exists c \in C (N) \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in C (N) \exists b \in C (N) \exists c \in C (N) \exists d \in C (N) \exists e \in C (N) \exists f \in C (N) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))))$
69	5 65 68	mpbir2and	$⊢ (φ \land x \in C (N)) \to x \in C (suc N)$
70	69	ex	$⊢ φ \to (x \in C (N) \to x \in C (suc N))$
71	70	ssrdv	$⊢ φ \to C (N) \subseteq C (suc N)$

Metamath Proof Explorer

Theorem constrsslem

Proof