Metamath Proof Explorer


Theorem constrsuc

Description: Membership in the successor step of the construction of constructible numbers. (Contributed by Thierry Arnoux, 25-Jun-2025)

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

Proof

Step Hyp Ref Expression
1 constr0.1 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } )
2 constrsuc.1 ( 𝜑𝑁 ∈ On )
3 constrsuc.2 𝑆 = ( 𝐶𝑁 )
4 1 fveq1i ( 𝐶 ‘ suc 𝑁 ) = ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ suc 𝑁 )
5 rdgsuc ( 𝑁 ∈ On → ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ suc 𝑁 ) = ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) ‘ ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑁 ) ) )
6 2 5 syl ( 𝜑 → ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ suc 𝑁 ) = ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) ‘ ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑁 ) ) )
7 4 6 eqtrid ( 𝜑 → ( 𝐶 ‘ suc 𝑁 ) = ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) ‘ ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑁 ) ) )
8 1 fveq1i ( 𝐶𝑁 ) = ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑁 )
9 3 8 eqtri 𝑆 = ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑁 )
10 9 fveq2i ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) ‘ 𝑆 ) = ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) ‘ ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑁 ) )
11 7 10 eqtr4di ( 𝜑 → ( 𝐶 ‘ suc 𝑁 ) = ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) ‘ 𝑆 ) )
12 11 eleq2d ( 𝜑 → ( 𝑋 ∈ ( 𝐶 ‘ suc 𝑁 ) ↔ 𝑋 ∈ ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) ‘ 𝑆 ) ) )
13 eqid ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) = ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } )
14 id ( 𝑠 = 𝑆𝑠 = 𝑆 )
15 rexeq ( 𝑠 = 𝑆 → ( ∃ 𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) )
16 14 15 rexeqbidv ( 𝑠 = 𝑆 → ( ∃ 𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) )
17 14 16 rexeqbidv ( 𝑠 = 𝑆 → ( ∃ 𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) )
18 14 17 rexeqbidv ( 𝑠 = 𝑆 → ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) )
19 rexeq ( 𝑠 = 𝑆 → ( ∃ 𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
20 14 19 rexeqbidv ( 𝑠 = 𝑆 → ( ∃ 𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
21 14 20 rexeqbidv ( 𝑠 = 𝑆 → ( ∃ 𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
22 14 21 rexeqbidv ( 𝑠 = 𝑆 → ( ∃ 𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
23 14 22 rexeqbidvv ( 𝑠 = 𝑆 → ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
24 rexeq ( 𝑠 = 𝑆 → ( ∃ 𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
25 14 24 rexeqbidv ( 𝑠 = 𝑆 → ( ∃ 𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
26 14 25 rexeqbidv ( 𝑠 = 𝑆 → ( ∃ 𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
27 14 26 rexeqbidv ( 𝑠 = 𝑆 → ( ∃ 𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
28 14 27 rexeqbidv ( 𝑠 = 𝑆 → ( ∃ 𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
29 14 28 rexeqbidvv ( 𝑠 = 𝑆 → ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
30 18 23 29 3orbi123d ( 𝑠 = 𝑆 → ( ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ↔ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ) )
31 30 rabbidv ( 𝑠 = 𝑆 → { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } = { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } )
32 31 adantl ( ( 𝜑𝑠 = 𝑆 ) → { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } = { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } )
33 3 fvexi 𝑆 ∈ V
34 33 a1i ( 𝜑𝑆 ∈ V )
35 cnex ℂ ∈ V
36 ssrab2 { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ⊆ ℂ
37 35 36 ssexi { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ∈ V
38 37 a1i ( 𝜑 → { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ∈ V )
39 13 32 34 38 fvmptd2 ( 𝜑 → ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) ‘ 𝑆 ) = { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } )
40 39 eleq2d ( 𝜑 → ( 𝑋 ∈ ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) ‘ 𝑆 ) ↔ 𝑋 ∈ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) )
41 eqeq1 ( 𝑥 = 𝑦 → ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ↔ 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ) )
42 eqeq1 ( 𝑥 = 𝑦 → ( 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ↔ 𝑦 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ) )
43 41 42 3anbi12d ( 𝑥 = 𝑦 → ( ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ↔ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑦 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) )
44 43 2rexbidv ( 𝑥 = 𝑦 → ( ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑦 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) )
45 44 2rexbidv ( 𝑥 = 𝑦 → ( ∃ 𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑦 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) )
46 45 2rexbidv ( 𝑥 = 𝑦 → ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑦 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) )
47 fvoveq1 ( 𝑥 = 𝑦 → ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑦𝑐 ) ) )
48 47 eqeq1d ( 𝑥 = 𝑦 → ( ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ↔ ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) )
49 41 48 anbi12d ( 𝑥 = 𝑦 → ( ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
50 49 2rexbidv ( 𝑥 = 𝑦 → ( ∃ 𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑓𝑆𝑡 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
51 50 2rexbidv ( 𝑥 = 𝑦 → ( ∃ 𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
52 51 2rexbidv ( 𝑥 = 𝑦 → ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
53 fvoveq1 ( 𝑥 = 𝑦 → ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑦𝑎 ) ) )
54 53 eqeq1d ( 𝑥 = 𝑦 → ( ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ↔ ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ) )
55 fvoveq1 ( 𝑥 = 𝑦 → ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑦𝑑 ) ) )
56 55 eqeq1d ( 𝑥 = 𝑦 → ( ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ↔ ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) )
57 54 56 3anbi23d ( 𝑥 = 𝑦 → ( ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
58 57 2rexbidv ( 𝑥 = 𝑦 → ( ∃ 𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
59 58 2rexbidv ( 𝑥 = 𝑦 → ( ∃ 𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
60 59 2rexbidv ( 𝑥 = 𝑦 → ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
61 46 52 60 3orbi123d ( 𝑥 = 𝑦 → ( ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ↔ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑦 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ) )
62 61 cbvrabv { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } = { 𝑦 ∈ ℂ ∣ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑦 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) }
63 62 eleq2i ( 𝑋 ∈ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ↔ 𝑋 ∈ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑦 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } )
64 eqeq1 ( 𝑦 = 𝑋 → ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ↔ 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ) )
65 eqeq1 ( 𝑦 = 𝑋 → ( 𝑦 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ↔ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ) )
66 64 65 3anbi12d ( 𝑦 = 𝑋 → ( ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑦 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ↔ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) )
67 66 2rexbidv ( 𝑦 = 𝑋 → ( ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑦 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) )
68 67 2rexbidv ( 𝑦 = 𝑋 → ( ∃ 𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑦 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) )
69 68 2rexbidv ( 𝑦 = 𝑋 → ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑦 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) )
70 fvoveq1 ( 𝑦 = 𝑋 → ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑋𝑐 ) ) )
71 70 eqeq1d ( 𝑦 = 𝑋 → ( ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ↔ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) )
72 64 71 anbi12d ( 𝑦 = 𝑋 → ( ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
73 72 2rexbidv ( 𝑦 = 𝑋 → ( ∃ 𝑓𝑆𝑡 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑓𝑆𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
74 73 2rexbidv ( 𝑦 = 𝑋 → ( ∃ 𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
75 74 2rexbidv ( 𝑦 = 𝑋 → ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
76 fvoveq1 ( 𝑦 = 𝑋 → ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑋𝑎 ) ) )
77 76 eqeq1d ( 𝑦 = 𝑋 → ( ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ↔ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ) )
78 fvoveq1 ( 𝑦 = 𝑋 → ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑋𝑑 ) ) )
79 78 eqeq1d ( 𝑦 = 𝑋 → ( ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ↔ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) )
80 77 79 3anbi23d ( 𝑦 = 𝑋 → ( ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
81 80 2rexbidv ( 𝑦 = 𝑋 → ( ∃ 𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
82 81 2rexbidv ( 𝑦 = 𝑋 → ( ∃ 𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
83 82 2rexbidv ( 𝑦 = 𝑋 → ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ↔ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
84 69 75 83 3orbi123d ( 𝑦 = 𝑋 → ( ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑦 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ↔ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ) )
85 84 elrab ( 𝑋 ∈ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑦 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑦 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑦𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑦𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑦𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ↔ ( 𝑋 ∈ ℂ ∧ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ) )
86 63 85 bitri ( 𝑋 ∈ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ↔ ( 𝑋 ∈ ℂ ∧ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ) )
87 86 a1i ( 𝜑 → ( 𝑋 ∈ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ↔ ( 𝑋 ∈ ℂ ∧ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ) ) )
88 12 40 87 3bitrd ( 𝜑 → ( 𝑋 ∈ ( 𝐶 ‘ suc 𝑁 ) ↔ ( 𝑋 ∈ ℂ ∧ ( ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ) ) )