Metamath Proof Explorer

Theorem 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 ⊢ 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
constrsscn.1 ⊢ ( 𝜑 → 𝑁 ∈ On )
constrsslem.1 ⊢ ( 𝜑 → 0 ∈ ( 𝐶 ‘ 𝑁 ) )
Assertion constrsslem ( 𝜑 → ( 𝐶 ‘ 𝑁 ) ⊆ ( 𝐶 ‘ suc 𝑁 ) )

Proof

Step Hyp Ref Expression
1 constr0.1 ⊢ 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
2 constrsscn.1 ⊢ ( 𝜑 → 𝑁 ∈ On )
3 constrsslem.1 ⊢ ( 𝜑 → 0 ∈ ( 𝐶 ‘ 𝑁 ) )
4 1 2 constrsscn ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑁 ) ⊆ ℂ )
5 4 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑥 ∈ ℂ )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) )
7 id ⊢ ( 𝑎 = 𝑥 → 𝑎 = 𝑥 )
8 oveq2 ⊢ ( 𝑎 = 𝑥 → ( 𝑏 − 𝑎 ) = ( 𝑏 − 𝑥 ) )
9 8 oveq2d ⊢ ( 𝑎 = 𝑥 → ( 𝑡 · ( 𝑏 − 𝑎 ) ) = ( 𝑡 · ( 𝑏 − 𝑥 ) ) )
10 7 9 oveq12d ⊢ ( 𝑎 = 𝑥 → ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) = ( 𝑥 + ( 𝑡 · ( 𝑏 − 𝑥 ) ) ) )
11 10 eqeq2d ⊢ ( 𝑎 = 𝑥 → ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ↔ 𝑥 = ( 𝑥 + ( 𝑡 · ( 𝑏 − 𝑥 ) ) ) ) )
12 11 anbi1d ⊢ ( 𝑎 = 𝑥 → ( ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 𝑏 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
13 12 rexbidv ⊢ ( 𝑎 = 𝑥 → ( ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 𝑏 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
14 13 2rexbidv ⊢ ( 𝑎 = 𝑥 → ( ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 𝑏 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
15 14 2rexbidv ⊢ ( 𝑎 = 𝑥 → ( ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 𝑏 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
16 15 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑎 = 𝑥 ) → ( ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 𝑏 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
17 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → 0 ∈ ( 𝐶 ‘ 𝑁 ) )
18 oveq1 ⊢ ( 𝑏 = 0 → ( 𝑏 − 𝑥 ) = ( 0 − 𝑥 ) )
19 18 oveq2d ⊢ ( 𝑏 = 0 → ( 𝑡 · ( 𝑏 − 𝑥 ) ) = ( 𝑡 · ( 0 − 𝑥 ) ) )
20 19 oveq2d ⊢ ( 𝑏 = 0 → ( 𝑥 + ( 𝑡 · ( 𝑏 − 𝑥 ) ) ) = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) )
21 20 eqeq2d ⊢ ( 𝑏 = 0 → ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 𝑏 − 𝑥 ) ) ) ↔ 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ) )
22 21 anbi1d ⊢ ( 𝑏 = 0 → ( ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 𝑏 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
23 22 2rexbidv ⊢ ( 𝑏 = 0 → ( ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 𝑏 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
24 23 2rexbidv ⊢ ( 𝑏 = 0 → ( ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 𝑏 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
25 24 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑏 = 0 ) → ( ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 𝑏 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
26 oveq2 ⊢ ( 𝑐 = 0 → ( 𝑥 − 𝑐 ) = ( 𝑥 − 0 ) )
27 26 fveq2d ⊢ ( 𝑐 = 0 → ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑥 − 0 ) ) )
28 27 eqeq1d ⊢ ( 𝑐 = 0 → ( ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ↔ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) )
29 28 anbi2d ⊢ ( 𝑐 = 0 → ( ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
30 29 rexbidv ⊢ ( 𝑐 = 0 → ( ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
31 30 2rexbidv ⊢ ( 𝑐 = 0 → ( ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
32 31 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑐 = 0 ) → ( ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
33 oveq1 ⊢ ( 𝑒 = 𝑥 → ( 𝑒 − 𝑓 ) = ( 𝑥 − 𝑓 ) )
34 33 fveq2d ⊢ ( 𝑒 = 𝑥 → ( abs ‘ ( 𝑒 − 𝑓 ) ) = ( abs ‘ ( 𝑥 − 𝑓 ) ) )
35 34 eqeq2d ⊢ ( 𝑒 = 𝑥 → ( ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ↔ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 𝑓 ) ) ) )
36 35 anbi2d ⊢ ( 𝑒 = 𝑥 → ( ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 𝑓 ) ) ) ) )
37 36 2rexbidv ⊢ ( 𝑒 = 𝑥 → ( ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 𝑓 ) ) ) ) )
38 37 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑒 = 𝑥 ) → ( ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 𝑓 ) ) ) ) )
39 oveq2 ⊢ ( 𝑓 = 0 → ( 𝑥 − 𝑓 ) = ( 𝑥 − 0 ) )
40 39 fveq2d ⊢ ( 𝑓 = 0 → ( abs ‘ ( 𝑥 − 𝑓 ) ) = ( abs ‘ ( 𝑥 − 0 ) ) )
41 40 eqeq2d ⊢ ( 𝑓 = 0 → ( ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 𝑓 ) ) ↔ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 0 ) ) ) )
42 41 anbi2d ⊢ ( 𝑓 = 0 → ( ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 𝑓 ) ) ) ↔ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 0 ) ) ) ) )
43 42 rexbidv ⊢ ( 𝑓 = 0 → ( ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 𝑓 ) ) ) ↔ ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 0 ) ) ) ) )
44 43 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑓 = 0 ) → ( ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 𝑓 ) ) ) ↔ ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 0 ) ) ) ) )
45 0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → 0 ∈ ℝ )
46 oveq1 ⊢ ( 𝑡 = 0 → ( 𝑡 · ( 0 − 𝑥 ) ) = ( 0 · ( 0 − 𝑥 ) ) )
47 46 oveq2d ⊢ ( 𝑡 = 0 → ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) = ( 𝑥 + ( 0 · ( 0 − 𝑥 ) ) ) )
48 47 eqeq2d ⊢ ( 𝑡 = 0 → ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ↔ 𝑥 = ( 𝑥 + ( 0 · ( 0 − 𝑥 ) ) ) ) )
49 48 anbi1d ⊢ ( 𝑡 = 0 → ( ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 0 ) ) ) ↔ ( 𝑥 = ( 𝑥 + ( 0 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 0 ) ) ) ) )
50 49 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑡 = 0 ) → ( ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 0 ) ) ) ↔ ( 𝑥 = ( 𝑥 + ( 0 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 0 ) ) ) ) )
51 0cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → 0 ∈ ℂ )
52 51 5 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 0 − 𝑥 ) ∈ ℂ )
53 52 mul02d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 0 · ( 0 − 𝑥 ) ) = 0 )
54 53 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 𝑥 + ( 0 · ( 0 − 𝑥 ) ) ) = ( 𝑥 + 0 ) )
55 5 addridd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 𝑥 + 0 ) = 𝑥 )
56 54 55 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑥 = ( 𝑥 + ( 0 · ( 0 − 𝑥 ) ) ) )
57 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 0 ) ) )
58 56 57 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 𝑥 = ( 𝑥 + ( 0 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 0 ) ) ) )
59 45 50 58 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 0 ) ) ) )
60 17 44 59 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑥 − 𝑓 ) ) ) )
61 6 38 60 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) )
62 17 32 61 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 0 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) )
63 17 25 62 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑥 + ( 𝑡 · ( 𝑏 − 𝑥 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) )
64 6 16 63 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) )
65 64 3mix2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
66 eqid ⊢ ( 𝐶 ‘ 𝑁 ) = ( 𝐶 ‘ 𝑁 )
67 1 2 66 constrsuc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐶 ‘ suc 𝑁 ) ↔ ( 𝑥 ∈ ℂ ∧ ( ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) ) ) )
68 67 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 𝑥 ∈ ( 𝐶 ‘ suc 𝑁 ) ↔ ( 𝑥 ∈ ℂ ∧ ( ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑁 ) ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) ) ) )
69 5 65 68 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝐶 ‘ suc 𝑁 ) )
70 69 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐶 ‘ 𝑁 ) → 𝑥 ∈ ( 𝐶 ‘ suc 𝑁 ) ) )
71 70 ssrdv ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑁 ) ⊆ ( 𝐶 ‘ suc 𝑁 ) )