Metamath Proof Explorer

Theorem constrsscn

Description: Closure of the constructible points in the complex numbers. (Contributed by Thierry Arnoux, 25-Jun-2025)

Ref Expression
Hypotheses constr0.1 ⊢ 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
constrsscn.1 ⊢ ( 𝜑 → 𝑁 ∈ On )
Assertion constrsscn ( 𝜑 → ( 𝐶 ‘ 𝑁 ) ⊆ ℂ )

Proof

Step Hyp Ref Expression
1 constr0.1 ⊢ 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
2 constrsscn.1 ⊢ ( 𝜑 → 𝑁 ∈ On )
3 fveq2 ⊢ ( 𝑚 = ∅ → ( 𝐶 ‘ 𝑚 ) = ( 𝐶 ‘ ∅ ) )
4 3 sseq1d ⊢ ( 𝑚 = ∅ → ( ( 𝐶 ‘ 𝑚 ) ⊆ ℂ ↔ ( 𝐶 ‘ ∅ ) ⊆ ℂ ) )
5 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐶 ‘ 𝑚 ) = ( 𝐶 ‘ 𝑛 ) )
6 5 sseq1d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐶 ‘ 𝑚 ) ⊆ ℂ ↔ ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ) )
7 fveq2 ⊢ ( 𝑚 = suc 𝑛 → ( 𝐶 ‘ 𝑚 ) = ( 𝐶 ‘ suc 𝑛 ) )
8 7 sseq1d ⊢ ( 𝑚 = suc 𝑛 → ( ( 𝐶 ‘ 𝑚 ) ⊆ ℂ ↔ ( 𝐶 ‘ suc 𝑛 ) ⊆ ℂ ) )
9 fveq2 ⊢ ( 𝑚 = 𝑁 → ( 𝐶 ‘ 𝑚 ) = ( 𝐶 ‘ 𝑁 ) )
10 9 sseq1d ⊢ ( 𝑚 = 𝑁 → ( ( 𝐶 ‘ 𝑚 ) ⊆ ℂ ↔ ( 𝐶 ‘ 𝑁 ) ⊆ ℂ ) )
11 1 constr0 ⊢ ( 𝐶 ‘ ∅ ) = { 0 , 1 }
12 0cn ⊢ 0 ∈ ℂ
13 ax-1cn ⊢ 1 ∈ ℂ
14 prssi ⊢ ( ( 0 ∈ ℂ ∧ 1 ∈ ℂ ) → { 0 , 1 } ⊆ ℂ )
15 12 13 14 mp2an ⊢ { 0 , 1 } ⊆ ℂ
16 11 15 eqsstri ⊢ ( 𝐶 ‘ ∅ ) ⊆ ℂ
17 simpl ⊢ ( ( 𝑛 ∈ On ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ) → 𝑛 ∈ On )
18 eqid ⊢ ( 𝐶 ‘ 𝑛 ) = ( 𝐶 ‘ 𝑛 )
19 1 17 18 constrsuc ⊢ ( ( 𝑛 ∈ On ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ) → ( 𝑥 ∈ ( 𝐶 ‘ suc 𝑛 ) ↔ ( 𝑥 ∈ ℂ ∧ ( ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) ) ) )
20 19 biimpa ⊢ ( ( ( 𝑛 ∈ On ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ) ∧ 𝑥 ∈ ( 𝐶 ‘ suc 𝑛 ) ) → ( 𝑥 ∈ ℂ ∧ ( ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) ) )
21 20 simpld ⊢ ( ( ( 𝑛 ∈ On ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ) ∧ 𝑥 ∈ ( 𝐶 ‘ suc 𝑛 ) ) → 𝑥 ∈ ℂ )
22 21 ex ⊢ ( ( 𝑛 ∈ On ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ) → ( 𝑥 ∈ ( 𝐶 ‘ suc 𝑛 ) → 𝑥 ∈ ℂ ) )
23 22 ssrdv ⊢ ( ( 𝑛 ∈ On ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ) → ( 𝐶 ‘ suc 𝑛 ) ⊆ ℂ )
24 23 ex ⊢ ( 𝑛 ∈ On → ( ( 𝐶 ‘ 𝑛 ) ⊆ ℂ → ( 𝐶 ‘ suc 𝑛 ) ⊆ ℂ ) )
25 vex ⊢ 𝑚 ∈ V
26 25 a1i ⊢ ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ) → 𝑚 ∈ V )
27 simpl ⊢ ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ) → Lim 𝑚 )
28 1 26 27 constrlim ⊢ ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ) → ( 𝐶 ‘ 𝑚 ) = ∪ 𝑜 ∈ 𝑚 ( 𝐶 ‘ 𝑜 ) )
29 fveq2 ⊢ ( 𝑛 = 𝑜 → ( 𝐶 ‘ 𝑛 ) = ( 𝐶 ‘ 𝑜 ) )
30 29 sseq1d ⊢ ( 𝑛 = 𝑜 → ( ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ↔ ( 𝐶 ‘ 𝑜 ) ⊆ ℂ ) )
31 simplr ⊢ ( ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ) ∧ 𝑜 ∈ 𝑚 ) → ∀ 𝑛 ∈ 𝑚 ( 𝐶 ‘ 𝑛 ) ⊆ ℂ )
32 simpr ⊢ ( ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ) ∧ 𝑜 ∈ 𝑚 ) → 𝑜 ∈ 𝑚 )
33 30 31 32 rspcdva ⊢ ( ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ) ∧ 𝑜 ∈ 𝑚 ) → ( 𝐶 ‘ 𝑜 ) ⊆ ℂ )
34 33 iunssd ⊢ ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ) → ∪ 𝑜 ∈ 𝑚 ( 𝐶 ‘ 𝑜 ) ⊆ ℂ )
35 28 34 eqsstrd ⊢ ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝐶 ‘ 𝑛 ) ⊆ ℂ ) → ( 𝐶 ‘ 𝑚 ) ⊆ ℂ )
36 35 ex ⊢ ( Lim 𝑚 → ( ∀ 𝑛 ∈ 𝑚 ( 𝐶 ‘ 𝑛 ) ⊆ ℂ → ( 𝐶 ‘ 𝑚 ) ⊆ ℂ ) )
37 4 6 8 10 16 24 36 tfinds ⊢ ( 𝑁 ∈ On → ( 𝐶 ‘ 𝑁 ) ⊆ ℂ )
38 2 37 syl ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑁 ) ⊆ ℂ )