Metamath Proof Explorer


Theorem constrelextdg2

Description: If the N -th step ( CN ) of the construction of constuctible numbers is included in a subfield F of the complex numbers, then any element X of the next step ( Csuc N ) is either in F or in a quadratic extension of F . (Contributed by Thierry Arnoux, 6-Jul-2025)

Ref Expression
Hypotheses constr0.1 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } )
constrelextdg2.k 𝐾 = ( ℂflds 𝐹 )
constrelextdg2.l 𝐿 = ( ℂflds ( ℂfld fldGen ( 𝐹 ∪ { 𝑋 } ) ) )
constrelextdg2.f ( 𝜑𝐹 ∈ ( SubDRing ‘ ℂfld ) )
constrelextdg2.n ( 𝜑𝑁 ∈ On )
constrelextdg2.1 ( 𝜑 → ( 𝐶𝑁 ) ⊆ 𝐹 )
constrelextdg2.x ( 𝜑𝑋 ∈ ( 𝐶 ‘ suc 𝑁 ) )
Assertion constrelextdg2 ( 𝜑 → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )

Proof

Step Hyp Ref Expression
1 constr0.1 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } )
2 constrelextdg2.k 𝐾 = ( ℂflds 𝐹 )
3 constrelextdg2.l 𝐿 = ( ℂflds ( ℂfld fldGen ( 𝐹 ∪ { 𝑋 } ) ) )
4 constrelextdg2.f ( 𝜑𝐹 ∈ ( SubDRing ‘ ℂfld ) )
5 constrelextdg2.n ( 𝜑𝑁 ∈ On )
6 constrelextdg2.1 ( 𝜑 → ( 𝐶𝑁 ) ⊆ 𝐹 )
7 constrelextdg2.x ( 𝜑𝑋 ∈ ( 𝐶 ‘ suc 𝑁 ) )
8 cnfldbas ℂ = ( Base ‘ ℂfld )
9 8 sdrgss ( 𝐹 ∈ ( SubDRing ‘ ℂfld ) → 𝐹 ⊆ ℂ )
10 4 9 syl ( 𝜑𝐹 ⊆ ℂ )
11 10 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝐹 ⊆ ℂ )
12 6 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 𝐶𝑁 ) ⊆ 𝐹 )
13 simp-7r ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑎 ∈ ( 𝐶𝑁 ) )
14 12 13 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑎𝐹 )
15 simp-6r ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑏 ∈ ( 𝐶𝑁 ) )
16 12 15 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑏𝐹 )
17 simp-5r ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑐 ∈ ( 𝐶𝑁 ) )
18 12 17 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑐𝐹 )
19 simp-4r ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑑 ∈ ( 𝐶𝑁 ) )
20 12 19 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑑𝐹 )
21 simpllr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑡 ∈ ℝ )
22 simplr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑟 ∈ ℝ )
23 simpr1 ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) )
24 simpr2 ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) )
25 simpr3 ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 )
26 eqid ( 𝑎 + ( ( ( ( ( 𝑎𝑐 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) − ( ( ( ∗ ‘ 𝑎 ) − ( ∗ ‘ 𝑐 ) ) · ( 𝑑𝑐 ) ) ) / ( ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ( 𝑏𝑎 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) ) ) · ( 𝑏𝑎 ) ) ) = ( 𝑎 + ( ( ( ( ( 𝑎𝑐 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) − ( ( ( ∗ ‘ 𝑎 ) − ( ∗ ‘ 𝑐 ) ) · ( 𝑑𝑐 ) ) ) / ( ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ( 𝑏𝑎 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) ) ) · ( 𝑏𝑎 ) ) )
27 11 14 16 18 20 21 22 23 24 25 26 constrrtll ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑋 = ( 𝑎 + ( ( ( ( ( 𝑎𝑐 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) − ( ( ( ∗ ‘ 𝑎 ) − ( ∗ ‘ 𝑐 ) ) · ( 𝑑𝑐 ) ) ) / ( ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ( 𝑏𝑎 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) ) ) · ( 𝑏𝑎 ) ) ) )
28 cnfldadd + = ( +g ‘ ℂfld )
29 sdrgsubrg ( 𝐹 ∈ ( SubDRing ‘ ℂfld ) → 𝐹 ∈ ( SubRing ‘ ℂfld ) )
30 subrgsubg ( 𝐹 ∈ ( SubRing ‘ ℂfld ) → 𝐹 ∈ ( SubGrp ‘ ℂfld ) )
31 4 29 30 3syl ( 𝜑𝐹 ∈ ( SubGrp ‘ ℂfld ) )
32 31 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝐹 ∈ ( SubGrp ‘ ℂfld ) )
33 cnfldmul · = ( .r ‘ ℂfld )
34 4 29 syl ( 𝜑𝐹 ∈ ( SubRing ‘ ℂfld ) )
35 34 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝐹 ∈ ( SubRing ‘ ℂfld ) )
36 cnflddiv / = ( /r ‘ ℂfld )
37 cnfld0 0 = ( 0g ‘ ℂfld )
38 4 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝐹 ∈ ( SubDRing ‘ ℂfld ) )
39 cnfldsub − = ( -g ‘ ℂfld )
40 39 32 14 18 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 𝑎𝑐 ) ∈ 𝐹 )
41 5 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑁 ∈ On )
42 1 41 19 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ∗ ‘ 𝑑 ) ∈ ( 𝐶𝑁 ) )
43 12 42 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ∗ ‘ 𝑑 ) ∈ 𝐹 )
44 1 41 17 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ∗ ‘ 𝑐 ) ∈ ( 𝐶𝑁 ) )
45 12 44 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ∗ ‘ 𝑐 ) ∈ 𝐹 )
46 39 32 43 45 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ∈ 𝐹 )
47 33 35 40 46 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( 𝑎𝑐 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) ∈ 𝐹 )
48 1 41 13 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ∗ ‘ 𝑎 ) ∈ ( 𝐶𝑁 ) )
49 12 48 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ∗ ‘ 𝑎 ) ∈ 𝐹 )
50 39 32 49 45 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ∗ ‘ 𝑎 ) − ( ∗ ‘ 𝑐 ) ) ∈ 𝐹 )
51 39 32 20 18 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 𝑑𝑐 ) ∈ 𝐹 )
52 33 35 50 51 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ( ∗ ‘ 𝑎 ) − ( ∗ ‘ 𝑐 ) ) · ( 𝑑𝑐 ) ) ∈ 𝐹 )
53 39 32 47 52 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ( 𝑎𝑐 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) − ( ( ( ∗ ‘ 𝑎 ) − ( ∗ ‘ 𝑐 ) ) · ( 𝑑𝑐 ) ) ) ∈ 𝐹 )
54 1 41 15 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ∗ ‘ 𝑏 ) ∈ ( 𝐶𝑁 ) )
55 12 54 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ∗ ‘ 𝑏 ) ∈ 𝐹 )
56 39 32 55 49 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) ∈ 𝐹 )
57 33 35 56 51 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) · ( 𝑑𝑐 ) ) ∈ 𝐹 )
58 39 32 16 14 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 𝑏𝑎 ) ∈ 𝐹 )
59 33 35 58 46 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( 𝑏𝑎 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) ∈ 𝐹 )
60 39 32 57 59 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ( 𝑏𝑎 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) ) ∈ 𝐹 )
61 11 16 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑏 ∈ ℂ )
62 11 14 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑎 ∈ ℂ )
63 61 62 cjsubd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ∗ ‘ ( 𝑏𝑎 ) ) = ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) )
64 63 oveq1d ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) = ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) · ( 𝑑𝑐 ) ) )
65 11 58 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 𝑏𝑎 ) ∈ ℂ )
66 65 cjcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ∗ ‘ ( 𝑏𝑎 ) ) ∈ ℂ )
67 11 51 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 𝑑𝑐 ) ∈ ℂ )
68 66 67 cjmuld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ∗ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) = ( ( ∗ ‘ ( ∗ ‘ ( 𝑏𝑎 ) ) ) · ( ∗ ‘ ( 𝑑𝑐 ) ) ) )
69 65 cjcjd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ∗ ‘ ( ∗ ‘ ( 𝑏𝑎 ) ) ) = ( 𝑏𝑎 ) )
70 11 20 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑑 ∈ ℂ )
71 11 18 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑐 ∈ ℂ )
72 70 71 cjsubd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ∗ ‘ ( 𝑑𝑐 ) ) = ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) )
73 69 72 oveq12d ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ∗ ‘ ( ∗ ‘ ( 𝑏𝑎 ) ) ) · ( ∗ ‘ ( 𝑑𝑐 ) ) ) = ( ( 𝑏𝑎 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) )
74 68 73 eqtrd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ∗ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) = ( ( 𝑏𝑎 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) )
75 64 74 oveq12d ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ∗ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ) = ( ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ( 𝑏𝑎 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) ) )
76 66 67 mulcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ∈ ℂ )
77 imval2 ( ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ∈ ℂ → ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) = ( ( ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ∗ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ) / ( 2 · i ) ) )
78 76 77 syl ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) = ( ( ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ∗ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ) / ( 2 · i ) ) )
79 78 neeq1d ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ↔ ( ( ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ∗ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ) / ( 2 · i ) ) ≠ 0 ) )
80 25 79 mpbid ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ∗ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ) / ( 2 · i ) ) ≠ 0 )
81 76 cjcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ∗ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ∈ ℂ )
82 76 81 subcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ∗ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ) ∈ ℂ )
83 2cnd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 2 ∈ ℂ )
84 ax-icn i ∈ ℂ
85 84 a1i ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → i ∈ ℂ )
86 83 85 mulcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 2 · i ) ∈ ℂ )
87 2cn 2 ∈ ℂ
88 2ne0 2 ≠ 0
89 ine0 i ≠ 0
90 87 84 88 89 mulne0i ( 2 · i ) ≠ 0
91 90 a1i ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 2 · i ) ≠ 0 )
92 82 86 91 divne0bd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ∗ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ) ≠ 0 ↔ ( ( ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ∗ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ) / ( 2 · i ) ) ≠ 0 ) )
93 80 92 mpbird ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ∗ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ) ≠ 0 )
94 75 93 eqnetrrd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ( 𝑏𝑎 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) ) ≠ 0 )
95 36 37 38 53 60 94 sdrgdvcl ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ( ( 𝑎𝑐 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) − ( ( ( ∗ ‘ 𝑎 ) − ( ∗ ‘ 𝑐 ) ) · ( 𝑑𝑐 ) ) ) / ( ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ( 𝑏𝑎 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) ) ) ∈ 𝐹 )
96 33 35 95 58 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( ( ( ( ( 𝑎𝑐 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) − ( ( ( ∗ ‘ 𝑎 ) − ( ∗ ‘ 𝑐 ) ) · ( 𝑑𝑐 ) ) ) / ( ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ( 𝑏𝑎 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) ) ) · ( 𝑏𝑎 ) ) ∈ 𝐹 )
97 28 32 14 96 subgcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 𝑎 + ( ( ( ( ( 𝑎𝑐 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) − ( ( ( ∗ ‘ 𝑎 ) − ( ∗ ‘ 𝑐 ) ) · ( 𝑑𝑐 ) ) ) / ( ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) · ( 𝑑𝑐 ) ) − ( ( 𝑏𝑎 ) · ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑐 ) ) ) ) ) · ( 𝑏𝑎 ) ) ) ∈ 𝐹 )
98 27 97 eqeltrd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → 𝑋𝐹 )
99 98 orcd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
100 99 r19.29an ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
101 100 r19.29an ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
102 101 r19.29an ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
103 102 r19.29an ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
104 103 r19.29an ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
105 104 r19.29an ( ( 𝜑 ∧ ∃ 𝑎 ∈ ( 𝐶𝑁 ) ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
106 1 5 constrsscn ( 𝜑 → ( 𝐶𝑁 ) ⊆ ℂ )
107 106 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎 = 𝑏 ) → ( 𝐶𝑁 ) ⊆ ℂ )
108 simp-8r ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎 = 𝑏 ) → 𝑎 ∈ ( 𝐶𝑁 ) )
109 simp-7r ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎 = 𝑏 ) → 𝑏 ∈ ( 𝐶𝑁 ) )
110 simp-6r ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎 = 𝑏 ) → 𝑐 ∈ ( 𝐶𝑁 ) )
111 simp-5r ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎 = 𝑏 ) → 𝑒 ∈ ( 𝐶𝑁 ) )
112 simp-4r ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎 = 𝑏 ) → 𝑓 ∈ ( 𝐶𝑁 ) )
113 simpllr ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎 = 𝑏 ) → 𝑡 ∈ ℝ )
114 simplrl ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎 = 𝑏 ) → 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) )
115 simplrr ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎 = 𝑏 ) → ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
116 simpr ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎 = 𝑏 ) → 𝑎 = 𝑏 )
117 107 108 109 110 111 112 113 114 115 116 constrrtlc2 ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎 = 𝑏 ) → 𝑋 = 𝑎 )
118 6 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎 = 𝑏 ) → ( 𝐶𝑁 ) ⊆ 𝐹 )
119 118 108 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎 = 𝑏 ) → 𝑎𝐹 )
120 117 119 eqeltrd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎 = 𝑏 ) → 𝑋𝐹 )
121 120 orcd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎 = 𝑏 ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
122 eqid ( Poly1𝐾 ) = ( Poly1𝐾 )
123 eqid ( .g ‘ ( mulGrp ‘ ℂfld ) ) = ( .g ‘ ( mulGrp ‘ ℂfld ) )
124 cnfldfld fld ∈ Field
125 124 a1i ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ℂfld ∈ Field )
126 4 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝐹 ∈ ( SubDRing ‘ ℂfld ) )
127 eqid ( 𝐶𝑁 ) = ( 𝐶𝑁 )
128 1 5 127 constrsuc ( 𝜑 → ( 𝑋 ∈ ( 𝐶 ‘ suc 𝑁 ) ↔ ( 𝑋 ∈ ℂ ∧ ( ∃ 𝑎 ∈ ( 𝐶𝑁 ) ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ ( 𝐶𝑁 ) ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎 ∈ ( 𝐶𝑁 ) ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ) ) )
129 7 128 mpbid ( 𝜑 → ( 𝑋 ∈ ℂ ∧ ( ∃ 𝑎 ∈ ( 𝐶𝑁 ) ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ ( 𝐶𝑁 ) ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎 ∈ ( 𝐶𝑁 ) ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ) )
130 129 simpld ( 𝜑𝑋 ∈ ℂ )
131 130 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑋 ∈ ℂ )
132 31 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝐹 ∈ ( SubGrp ‘ ℂfld ) )
133 6 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 𝐶𝑁 ) ⊆ 𝐹 )
134 5 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑁 ∈ On )
135 simp-8r ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑎 ∈ ( 𝐶𝑁 ) )
136 1 134 135 constrconj ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ∗ ‘ 𝑎 ) ∈ ( 𝐶𝑁 ) )
137 133 136 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ∗ ‘ 𝑎 ) ∈ 𝐹 )
138 126 29 syl ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝐹 ∈ ( SubRing ‘ ℂfld ) )
139 133 135 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑎𝐹 )
140 simp-7r ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑏 ∈ ( 𝐶𝑁 ) )
141 1 134 140 constrconj ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ∗ ‘ 𝑏 ) ∈ ( 𝐶𝑁 ) )
142 133 141 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ∗ ‘ 𝑏 ) ∈ 𝐹 )
143 39 132 142 137 subgsubcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) ∈ 𝐹 )
144 133 140 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑏𝐹 )
145 39 132 144 139 subgsubcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 𝑏𝑎 ) ∈ 𝐹 )
146 106 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 𝐶𝑁 ) ⊆ ℂ )
147 146 140 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑏 ∈ ℂ )
148 146 135 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑎 ∈ ℂ )
149 simpr ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑎𝑏 )
150 149 necomd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑏𝑎 )
151 147 148 150 subne0d ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 𝑏𝑎 ) ≠ 0 )
152 36 37 126 143 145 151 sdrgdvcl ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ∈ 𝐹 )
153 33 138 139 152 subrgmcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ∈ 𝐹 )
154 39 132 137 153 subgsubcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) ∈ 𝐹 )
155 simp-6r ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑐 ∈ ( 𝐶𝑁 ) )
156 1 134 155 constrconj ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ∗ ‘ 𝑐 ) ∈ ( 𝐶𝑁 ) )
157 133 156 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ∗ ‘ 𝑐 ) ∈ 𝐹 )
158 39 132 154 157 subgsubcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ∈ 𝐹 )
159 133 155 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑐𝐹 )
160 33 138 159 152 subrgmcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 𝑐 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ∈ 𝐹 )
161 39 132 158 160 subgsubcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) − ( 𝑐 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) ∈ 𝐹 )
162 simp-5r ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑒 ∈ ( 𝐶𝑁 ) )
163 simp-4r ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑓 ∈ ( 𝐶𝑁 ) )
164 simpllr ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑡 ∈ ℝ )
165 simplrl ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) )
166 simplrr ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
167 eqid ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) = ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) )
168 eqid ( ( ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) − ( 𝑐 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) = ( ( ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) − ( 𝑐 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) )
169 eqid ( - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) = ( - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) )
170 146 135 140 155 162 163 164 165 166 167 168 169 149 constrrtlc1 ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( ( 𝑋 ↑ 2 ) + ( ( ( ( ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) − ( 𝑐 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) · 𝑋 ) + ( - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) ) = 0 ∧ ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ≠ 0 ) )
171 170 simprd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ≠ 0 )
172 36 37 126 161 152 171 sdrgdvcl ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) − ( 𝑐 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ∈ 𝐹 )
173 df-neg - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) = ( 0 − ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) )
174 1 134 constr01 ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → { 0 , 1 } ⊆ ( 𝐶𝑁 ) )
175 37 fvexi 0 ∈ V
176 175 prid1 0 ∈ { 0 , 1 }
177 176 a1i ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 0 ∈ { 0 , 1 } )
178 174 177 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 0 ∈ ( 𝐶𝑁 ) )
179 133 178 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 0 ∈ 𝐹 )
180 33 138 159 158 subrgmcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) ∈ 𝐹 )
181 133 162 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑒𝐹 )
182 133 163 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑓𝐹 )
183 39 132 181 182 subgsubcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 𝑒𝑓 ) ∈ 𝐹 )
184 1 134 162 constrconj ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ∗ ‘ 𝑒 ) ∈ ( 𝐶𝑁 ) )
185 133 184 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ∗ ‘ 𝑒 ) ∈ 𝐹 )
186 1 134 163 constrconj ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ∗ ‘ 𝑓 ) ∈ ( 𝐶𝑁 ) )
187 133 186 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ∗ ‘ 𝑓 ) ∈ 𝐹 )
188 39 132 185 187 subgsubcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ∈ 𝐹 )
189 33 138 183 188 subrgmcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ∈ 𝐹 )
190 28 132 180 189 subgcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) ∈ 𝐹 )
191 39 132 179 190 subgsubcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 0 − ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) ) ∈ 𝐹 )
192 173 191 eqeltrid ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) ∈ 𝐹 )
193 36 37 126 192 152 171 sdrgdvcl ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ∈ 𝐹 )
194 2nn0 2 ∈ ℕ0
195 194 a1i ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 2 ∈ ℕ0 )
196 cnfldexp ( ( 𝑋 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( 2 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑋 ) = ( 𝑋 ↑ 2 ) )
197 131 195 196 syl2anc ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 2 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑋 ) = ( 𝑋 ↑ 2 ) )
198 197 oveq1d ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( 2 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑋 ) + ( ( ( ( ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) − ( 𝑐 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) · 𝑋 ) + ( - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) ) = ( ( 𝑋 ↑ 2 ) + ( ( ( ( ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) − ( 𝑐 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) · 𝑋 ) + ( - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) ) )
199 170 simpld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( 𝑋 ↑ 2 ) + ( ( ( ( ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) − ( 𝑐 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) · 𝑋 ) + ( - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) ) = 0 )
200 198 199 eqtrd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( 2 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑋 ) + ( ( ( ( ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) − ( 𝑐 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) · 𝑋 ) + ( - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) ) = 0 )
201 2 3 37 122 8 33 28 123 125 126 131 172 193 200 rtelextdg2 ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
202 exmidne ( 𝑎 = 𝑏𝑎𝑏 )
203 202 a1i ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑎 = 𝑏𝑎𝑏 ) )
204 121 201 203 mpjaodan ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
205 204 r19.29an ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
206 205 r19.29an ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑓 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
207 206 r19.29an ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
208 207 r19.29an ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
209 208 r19.29an ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
210 209 r19.29an ( ( 𝜑 ∧ ∃ 𝑎 ∈ ( 𝐶𝑁 ) ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
211 124 a1i ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ℂfld ∈ Field )
212 4 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝐹 ∈ ( SubDRing ‘ ℂfld ) )
213 130 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑋 ∈ ℂ )
214 212 29 30 3syl ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝐹 ∈ ( SubGrp ‘ ℂfld ) )
215 212 29 syl ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝐹 ∈ ( SubRing ‘ ℂfld ) )
216 6 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝐶𝑁 ) ⊆ 𝐹 )
217 simpllr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑒 ∈ ( 𝐶𝑁 ) )
218 216 217 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑒𝐹 )
219 simplr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑓 ∈ ( 𝐶𝑁 ) )
220 216 219 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑓𝐹 )
221 39 214 218 220 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑒𝑓 ) ∈ 𝐹 )
222 106 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝐶𝑁 ) ⊆ ℂ )
223 222 217 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑒 ∈ ℂ )
224 222 219 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑓 ∈ ℂ )
225 223 224 cjsubd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ ( 𝑒𝑓 ) ) = ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) )
226 5 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑁 ∈ On )
227 1 226 217 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑒 ) ∈ ( 𝐶𝑁 ) )
228 216 227 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑒 ) ∈ 𝐹 )
229 1 226 219 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑓 ) ∈ ( 𝐶𝑁 ) )
230 216 229 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑓 ) ∈ 𝐹 )
231 39 214 228 230 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ∈ 𝐹 )
232 225 231 eqeltrd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ ( 𝑒𝑓 ) ) ∈ 𝐹 )
233 33 215 221 232 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) ∈ 𝐹 )
234 simp-4r ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑑 ∈ ( 𝐶𝑁 ) )
235 1 226 234 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑑 ) ∈ ( 𝐶𝑁 ) )
236 216 235 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑑 ) ∈ 𝐹 )
237 216 234 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑑𝐹 )
238 simp-7r ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑎 ∈ ( 𝐶𝑁 ) )
239 216 238 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑎𝐹 )
240 28 214 237 239 subgcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑑 + 𝑎 ) ∈ 𝐹 )
241 33 215 236 240 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ∈ 𝐹 )
242 39 214 233 241 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) ∈ 𝐹 )
243 simp-6r ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑏 ∈ ( 𝐶𝑁 ) )
244 216 243 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑏𝐹 )
245 simp-5r ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑐 ∈ ( 𝐶𝑁 ) )
246 216 245 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑐𝐹 )
247 39 214 244 246 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑏𝑐 ) ∈ 𝐹 )
248 222 243 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑏 ∈ ℂ )
249 222 245 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑐 ∈ ℂ )
250 248 249 cjsubd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ ( 𝑏𝑐 ) ) = ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑐 ) ) )
251 1 226 243 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑏 ) ∈ ( 𝐶𝑁 ) )
252 216 251 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑏 ) ∈ 𝐹 )
253 1 226 245 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑐 ) ∈ ( 𝐶𝑁 ) )
254 216 253 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑐 ) ∈ 𝐹 )
255 39 214 252 254 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑐 ) ) ∈ 𝐹 )
256 250 255 eqeltrd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ ( 𝑏𝑐 ) ) ∈ 𝐹 )
257 33 215 247 256 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) ∈ 𝐹 )
258 1 226 238 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑎 ) ∈ ( 𝐶𝑁 ) )
259 216 258 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑎 ) ∈ 𝐹 )
260 33 215 259 240 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ∈ 𝐹 )
261 39 214 257 260 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ∈ 𝐹 )
262 39 214 242 261 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) ∈ 𝐹 )
263 39 214 236 259 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ∈ 𝐹 )
264 222 234 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑑 ∈ ℂ )
265 222 238 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑎 ∈ ℂ )
266 264 265 cjsubd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ ( 𝑑𝑎 ) ) = ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) )
267 264 265 subcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑑𝑎 ) ∈ ℂ )
268 simpr1 ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑎𝑑 )
269 268 necomd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑑𝑎 )
270 264 265 269 subne0d ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑑𝑎 ) ≠ 0 )
271 267 270 cjne0d ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ ( 𝑑𝑎 ) ) ≠ 0 )
272 266 271 eqnetrrd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ≠ 0 )
273 36 37 212 262 263 272 sdrgdvcl ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ∈ 𝐹 )
274 df-neg - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) = ( 0 − ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) )
275 1 226 constr01 ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → { 0 , 1 } ⊆ ( 𝐶𝑁 ) )
276 176 a1i ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 0 ∈ { 0 , 1 } )
277 275 276 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 0 ∈ ( 𝐶𝑁 ) )
278 216 277 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 0 ∈ 𝐹 )
279 33 215 237 239 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑑 · 𝑎 ) ∈ 𝐹 )
280 33 215 259 279 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) ∈ 𝐹 )
281 33 215 257 237 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ∈ 𝐹 )
282 39 214 280 281 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) ∈ 𝐹 )
283 33 215 236 279 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) ∈ 𝐹 )
284 33 215 233 239 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ∈ 𝐹 )
285 39 214 283 284 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ∈ 𝐹 )
286 39 214 282 285 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) ∈ 𝐹 )
287 36 37 212 286 263 272 sdrgdvcl ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ∈ 𝐹 )
288 39 214 278 287 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 0 − ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ) ∈ 𝐹 )
289 274 288 eqeltrid ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ∈ 𝐹 )
290 213 194 196 sylancl ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 2 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑋 ) = ( 𝑋 ↑ 2 ) )
291 290 oveq1d ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( 2 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑋 ) + ( ( ( ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) · 𝑋 ) + - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ) ) = ( ( 𝑋 ↑ 2 ) + ( ( ( ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) · 𝑋 ) + - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ) ) )
292 simpr2 ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) )
293 simpr3 ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
294 eqid ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) = ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) )
295 eqid ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) = ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) )
296 eqid ( ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) = ( ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) )
297 eqid - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) = - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) )
298 222 238 243 245 234 217 219 213 268 292 293 294 295 296 297 constrrtcc ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( 𝑋 ↑ 2 ) + ( ( ( ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) · 𝑋 ) + - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ) ) = 0 )
299 291 298 eqtrd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( 2 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑋 ) + ( ( ( ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) · 𝑋 ) + - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ) ) = 0 )
300 2 3 37 122 8 33 28 123 211 212 213 273 289 299 rtelextdg2 ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
301 300 r19.29an ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑓 ∈ ( 𝐶𝑁 ) ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
302 301 r19.29an ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
303 302 r19.29an ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
304 303 r19.29an ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
305 304 r19.29an ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
306 305 r19.29an ( ( 𝜑 ∧ ∃ 𝑎 ∈ ( 𝐶𝑁 ) ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
307 129 simprd ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝐶𝑁 ) ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ ( 𝐶𝑁 ) ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎 ∈ ( 𝐶𝑁 ) ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
308 105 210 306 307 mpjao3dan ( 𝜑 → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )