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 0elpr01 0 ∈ { 0 , 1 }
176 175 a1i ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 0 ∈ { 0 , 1 } )
177 174 176 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 0 ∈ ( 𝐶𝑁 ) )
178 133 177 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 0 ∈ 𝐹 )
179 33 138 159 158 subrgmcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) ∈ 𝐹 )
180 133 162 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑒𝐹 )
181 133 163 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 𝑓𝐹 )
182 39 132 180 181 subgsubcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 𝑒𝑓 ) ∈ 𝐹 )
183 1 134 162 constrconj ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ∗ ‘ 𝑒 ) ∈ ( 𝐶𝑁 ) )
184 133 183 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ∗ ‘ 𝑒 ) ∈ 𝐹 )
185 1 134 163 constrconj ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ∗ ‘ 𝑓 ) ∈ ( 𝐶𝑁 ) )
186 133 185 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ∗ ‘ 𝑓 ) ∈ 𝐹 )
187 39 132 184 186 subgsubcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ∈ 𝐹 )
188 33 138 182 187 subrgmcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ∈ 𝐹 )
189 28 132 179 188 subgcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) ∈ 𝐹 )
190 39 132 178 189 subgsubcld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 0 − ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) ) ∈ 𝐹 )
191 173 190 eqeltrid ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) ∈ 𝐹 )
192 36 37 126 191 152 171 sdrgdvcl ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ∈ 𝐹 )
193 2nn0 2 ∈ ℕ0
194 193 a1i ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → 2 ∈ ℕ0 )
195 cnfldexp ( ( 𝑋 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( 2 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑋 ) = ( 𝑋 ↑ 2 ) )
196 131 194 195 syl2anc ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 2 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑋 ) = ( 𝑋 ↑ 2 ) )
197 196 oveq1d ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( 2 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑋 ) + ( ( ( ( ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) − ( 𝑐 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) · 𝑋 ) + ( - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) ) = ( ( 𝑋 ↑ 2 ) + ( ( ( ( ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) − ( 𝑐 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) · 𝑋 ) + ( - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) ) )
198 170 simpld ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( 𝑋 ↑ 2 ) + ( ( ( ( ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) − ( 𝑐 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) · 𝑋 ) + ( - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) ) = 0 )
199 197 198 eqtrd ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( ( 2 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑋 ) + ( ( ( ( ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) − ( 𝑐 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) · 𝑋 ) + ( - ( ( 𝑐 · ( ( ( ∗ ‘ 𝑎 ) − ( 𝑎 · ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) − ( ∗ ‘ 𝑐 ) ) ) + ( ( 𝑒𝑓 ) · ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ) ) / ( ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑎 ) ) / ( 𝑏𝑎 ) ) ) ) ) = 0 )
200 2 3 37 122 8 33 28 123 125 126 131 172 192 199 rtelextdg2 ( ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) ∧ 𝑎𝑏 ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
201 exmidne ( 𝑎 = 𝑏𝑎𝑏 )
202 201 a1i ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑎 = 𝑏𝑎𝑏 ) )
203 121 200 202 mpjaodan ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
204 203 r19.29an ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( 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 124 a1i ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ℂfld ∈ Field )
211 4 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝐹 ∈ ( SubDRing ‘ ℂfld ) )
212 130 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑋 ∈ ℂ )
213 211 29 30 3syl ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝐹 ∈ ( SubGrp ‘ ℂfld ) )
214 211 29 syl ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝐹 ∈ ( SubRing ‘ ℂfld ) )
215 6 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝐶𝑁 ) ⊆ 𝐹 )
216 simpllr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑒 ∈ ( 𝐶𝑁 ) )
217 215 216 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑒𝐹 )
218 simplr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑓 ∈ ( 𝐶𝑁 ) )
219 215 218 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑓𝐹 )
220 39 213 217 219 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑒𝑓 ) ∈ 𝐹 )
221 106 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝐶𝑁 ) ⊆ ℂ )
222 221 216 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑒 ∈ ℂ )
223 221 218 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑓 ∈ ℂ )
224 222 223 cjsubd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ ( 𝑒𝑓 ) ) = ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) )
225 5 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑁 ∈ On )
226 1 225 216 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑒 ) ∈ ( 𝐶𝑁 ) )
227 215 226 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑒 ) ∈ 𝐹 )
228 1 225 218 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑓 ) ∈ ( 𝐶𝑁 ) )
229 215 228 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑓 ) ∈ 𝐹 )
230 39 213 227 229 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑒 ) − ( ∗ ‘ 𝑓 ) ) ∈ 𝐹 )
231 224 230 eqeltrd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ ( 𝑒𝑓 ) ) ∈ 𝐹 )
232 33 214 220 231 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) ∈ 𝐹 )
233 simp-4r ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑑 ∈ ( 𝐶𝑁 ) )
234 1 225 233 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑑 ) ∈ ( 𝐶𝑁 ) )
235 215 234 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑑 ) ∈ 𝐹 )
236 215 233 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑑𝐹 )
237 simp-7r ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑎 ∈ ( 𝐶𝑁 ) )
238 215 237 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑎𝐹 )
239 28 213 236 238 subgcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑑 + 𝑎 ) ∈ 𝐹 )
240 33 214 235 239 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ∈ 𝐹 )
241 39 213 232 240 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) ∈ 𝐹 )
242 simp-6r ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑏 ∈ ( 𝐶𝑁 ) )
243 215 242 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑏𝐹 )
244 simp-5r ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑐 ∈ ( 𝐶𝑁 ) )
245 215 244 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑐𝐹 )
246 39 213 243 245 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑏𝑐 ) ∈ 𝐹 )
247 221 242 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑏 ∈ ℂ )
248 221 244 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑐 ∈ ℂ )
249 247 248 cjsubd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ ( 𝑏𝑐 ) ) = ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑐 ) ) )
250 1 225 242 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑏 ) ∈ ( 𝐶𝑁 ) )
251 215 250 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑏 ) ∈ 𝐹 )
252 1 225 244 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑐 ) ∈ ( 𝐶𝑁 ) )
253 215 252 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑐 ) ∈ 𝐹 )
254 39 213 251 253 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑏 ) − ( ∗ ‘ 𝑐 ) ) ∈ 𝐹 )
255 249 254 eqeltrd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ ( 𝑏𝑐 ) ) ∈ 𝐹 )
256 33 214 246 255 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) ∈ 𝐹 )
257 1 225 237 constrconj ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑎 ) ∈ ( 𝐶𝑁 ) )
258 215 257 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ 𝑎 ) ∈ 𝐹 )
259 33 214 258 239 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ∈ 𝐹 )
260 39 213 256 259 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ∈ 𝐹 )
261 39 213 241 260 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) ∈ 𝐹 )
262 39 213 235 258 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ∈ 𝐹 )
263 221 233 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑑 ∈ ℂ )
264 221 237 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑎 ∈ ℂ )
265 263 264 cjsubd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ ( 𝑑𝑎 ) ) = ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) )
266 263 264 subcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑑𝑎 ) ∈ ℂ )
267 simpr1 ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑎𝑑 )
268 267 necomd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 𝑑𝑎 )
269 263 264 268 subne0d ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑑𝑎 ) ≠ 0 )
270 266 269 cjne0d ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ∗ ‘ ( 𝑑𝑎 ) ) ≠ 0 )
271 265 270 eqnetrrd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ≠ 0 )
272 36 37 211 261 262 271 sdrgdvcl ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ∈ 𝐹 )
273 df-neg - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) = ( 0 − ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) )
274 1 225 constr01 ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → { 0 , 1 } ⊆ ( 𝐶𝑁 ) )
275 175 a1i ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 0 ∈ { 0 , 1 } )
276 274 275 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 0 ∈ ( 𝐶𝑁 ) )
277 215 276 sseldd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → 0 ∈ 𝐹 )
278 33 214 236 238 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑑 · 𝑎 ) ∈ 𝐹 )
279 33 214 258 278 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) ∈ 𝐹 )
280 33 214 256 236 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ∈ 𝐹 )
281 39 213 279 280 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) ∈ 𝐹 )
282 33 214 235 278 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) ∈ 𝐹 )
283 33 214 232 238 subrgmcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ∈ 𝐹 )
284 39 213 282 283 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ∈ 𝐹 )
285 39 213 281 284 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) ∈ 𝐹 )
286 36 37 211 285 262 271 sdrgdvcl ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ∈ 𝐹 )
287 39 213 277 286 subgsubcld ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 0 − ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ) ∈ 𝐹 )
288 273 287 eqeltrid ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ∈ 𝐹 )
289 212 193 195 sylancl ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 2 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑋 ) = ( 𝑋 ↑ 2 ) )
290 289 oveq1d ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( 2 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑋 ) + ( ( ( ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) · 𝑋 ) + - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ) ) = ( ( 𝑋 ↑ 2 ) + ( ( ( ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) · 𝑋 ) + - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ) ) )
291 simpr2 ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) )
292 simpr3 ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
293 eqid ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) = ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) )
294 eqid ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) = ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) )
295 eqid ( ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) = ( ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) )
296 eqid - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) = - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) )
297 221 237 242 244 233 216 218 212 267 291 292 293 294 295 296 constrrtcc ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( 𝑋 ↑ 2 ) + ( ( ( ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) · 𝑋 ) + - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ) ) = 0 )
298 290 297 eqtrd ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( ( 2 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑋 ) + ( ( ( ( ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) − ( ( ∗ ‘ 𝑑 ) · ( 𝑑 + 𝑎 ) ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) − ( ( ∗ ‘ 𝑎 ) · ( 𝑑 + 𝑎 ) ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) · 𝑋 ) + - ( ( ( ( ( ∗ ‘ 𝑎 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑏𝑐 ) · ( ∗ ‘ ( 𝑏𝑐 ) ) ) · 𝑑 ) ) − ( ( ( ∗ ‘ 𝑑 ) · ( 𝑑 · 𝑎 ) ) − ( ( ( 𝑒𝑓 ) · ( ∗ ‘ ( 𝑒𝑓 ) ) ) · 𝑎 ) ) ) / ( ( ∗ ‘ 𝑑 ) − ( ∗ ‘ 𝑎 ) ) ) ) ) = 0 )
299 2 3 37 122 8 33 28 123 210 211 212 272 288 298 rtelextdg2 ( ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ 𝑓 ∈ ( 𝐶𝑁 ) ) ∧ ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
300 299 r19.29an ( ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐶𝑁 ) ) ∧ 𝑏 ∈ ( 𝐶𝑁 ) ) ∧ 𝑐 ∈ ( 𝐶𝑁 ) ) ∧ 𝑑 ∈ ( 𝐶𝑁 ) ) ∧ 𝑒 ∈ ( 𝐶𝑁 ) ) ∧ ∃ 𝑓 ∈ ( 𝐶𝑁 ) ( 𝑎𝑑 ∧ ( 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 129 simprd ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝐶𝑁 ) ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ ( 𝐶𝑁 ) ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ∃ 𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎 ∈ ( 𝐶𝑁 ) ∃ 𝑏 ∈ ( 𝐶𝑁 ) ∃ 𝑐 ∈ ( 𝐶𝑁 ) ∃ 𝑑 ∈ ( 𝐶𝑁 ) ∃ 𝑒 ∈ ( 𝐶𝑁 ) ∃ 𝑓 ∈ ( 𝐶𝑁 ) ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑋𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑋𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) )
307 105 209 305 306 mpjao3dan ( 𝜑 → ( 𝑋𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )