Metamath Proof Explorer

Theorem constrllcllem

Description: Constructible numbers are closed under line-line intersections. (Contributed by Thierry Arnoux, 2-Nov-2025)

Ref Expression
Hypotheses constr0.1 ⊢ 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
constrllcllem.a ⊢ ( 𝜑 → 𝐴 ∈ Constr )
constrllcllem.b ⊢ ( 𝜑 → 𝐵 ∈ Constr )
constrllcllem.c ⊢ ( 𝜑 → 𝐺 ∈ Constr )
constrllcllem.e ⊢ ( 𝜑 → 𝐷 ∈ Constr )
constrllcllem.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
constrllcllem.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
constrllcllem.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
constrllcllem.1 ⊢ ( 𝜑 → 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) )
constrllcllem.2 ⊢ ( 𝜑 → 𝑋 = ( 𝐺 + ( 𝑅 · ( 𝐷 − 𝐺 ) ) ) )
constrllcllem.3 ⊢ ( 𝜑 → ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐺 ) ) ) ≠ 0 )
Assertion constrllcllem ( 𝜑 → 𝑋 ∈ Constr )

Proof

Step Hyp Ref Expression
1 constr0.1 ⊢ 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
2 constrllcllem.a ⊢ ( 𝜑 → 𝐴 ∈ Constr )
3 constrllcllem.b ⊢ ( 𝜑 → 𝐵 ∈ Constr )
4 constrllcllem.c ⊢ ( 𝜑 → 𝐺 ∈ Constr )
5 constrllcllem.e ⊢ ( 𝜑 → 𝐷 ∈ Constr )
6 constrllcllem.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
7 constrllcllem.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
8 constrllcllem.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
9 constrllcllem.1 ⊢ ( 𝜑 → 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) )
10 constrllcllem.2 ⊢ ( 𝜑 → 𝑋 = ( 𝐺 + ( 𝑅 · ( 𝐷 − 𝐺 ) ) ) )
11 constrllcllem.3 ⊢ ( 𝜑 → ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐺 ) ) ) ≠ 0 )
12 peano2b ⊢ ( 𝑛 ∈ ω ↔ suc 𝑛 ∈ ω )
13 12 biimpi ⊢ ( 𝑛 ∈ ω → suc 𝑛 ∈ ω )
14 13 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → suc 𝑛 ∈ ω )
15 fveq2 ⊢ ( 𝑚 = suc 𝑛 → ( 𝐶 ‘ 𝑚 ) = ( 𝐶 ‘ suc 𝑛 ) )
16 15 eleq2d ⊢ ( 𝑚 = suc 𝑛 → ( 𝑋 ∈ ( 𝐶 ‘ 𝑚 ) ↔ 𝑋 ∈ ( 𝐶 ‘ suc 𝑛 ) ) )
17 16 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑚 = suc 𝑛 ) → ( 𝑋 ∈ ( 𝐶 ‘ 𝑚 ) ↔ 𝑋 ∈ ( 𝐶 ‘ suc 𝑛 ) ) )
18 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝑋 ∈ ℂ )
19 id ⊢ ( 𝑎 = 𝐴 → 𝑎 = 𝐴 )
20 oveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑏 − 𝑎 ) = ( 𝑏 − 𝐴 ) )
21 20 oveq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑡 · ( 𝑏 − 𝑎 ) ) = ( 𝑡 · ( 𝑏 − 𝐴 ) ) )
22 19 21 oveq12d ⊢ ( 𝑎 = 𝐴 → ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) = ( 𝐴 + ( 𝑡 · ( 𝑏 − 𝐴 ) ) ) )
23 22 eqeq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ↔ 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝑏 − 𝐴 ) ) ) ) )
24 20 fveq2d ⊢ ( 𝑎 = 𝐴 → ( ∗ ‘ ( 𝑏 − 𝑎 ) ) = ( ∗ ‘ ( 𝑏 − 𝐴 ) ) )
25 24 oveq1d ⊢ ( 𝑎 = 𝐴 → ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) = ( ( ∗ ‘ ( 𝑏 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) )
26 25 fveq2d ⊢ ( 𝑎 = 𝐴 → ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) )
27 26 neeq1d ⊢ ( 𝑎 = 𝐴 → ( ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ↔ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) )
28 23 27 3anbi13d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ↔ ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝑏 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ) )
29 28 rexbidv ⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝑏 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ) )
30 29 2rexbidv ⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝑏 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ) )
31 oveq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 − 𝐴 ) = ( 𝐵 − 𝐴 ) )
32 31 oveq2d ⊢ ( 𝑏 = 𝐵 → ( 𝑡 · ( 𝑏 − 𝐴 ) ) = ( 𝑡 · ( 𝐵 − 𝐴 ) ) )
33 32 oveq2d ⊢ ( 𝑏 = 𝐵 → ( 𝐴 + ( 𝑡 · ( 𝑏 − 𝐴 ) ) ) = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) )
34 33 eqeq2d ⊢ ( 𝑏 = 𝐵 → ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝑏 − 𝐴 ) ) ) ↔ 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) ) )
35 31 fveq2d ⊢ ( 𝑏 = 𝐵 → ( ∗ ‘ ( 𝑏 − 𝐴 ) ) = ( ∗ ‘ ( 𝐵 − 𝐴 ) ) )
36 35 oveq1d ⊢ ( 𝑏 = 𝐵 → ( ( ∗ ‘ ( 𝑏 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) = ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) )
37 36 fveq2d ⊢ ( 𝑏 = 𝐵 → ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) )
38 37 neeq1d ⊢ ( 𝑏 = 𝐵 → ( ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ↔ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) )
39 34 38 3anbi13d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝑏 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ↔ ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ) )
40 39 rexbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝑏 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ) )
41 40 2rexbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝑏 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ) )
42 id ⊢ ( 𝑐 = 𝐺 → 𝑐 = 𝐺 )
43 oveq2 ⊢ ( 𝑐 = 𝐺 → ( 𝑑 − 𝑐 ) = ( 𝑑 − 𝐺 ) )
44 43 oveq2d ⊢ ( 𝑐 = 𝐺 → ( 𝑟 · ( 𝑑 − 𝑐 ) ) = ( 𝑟 · ( 𝑑 − 𝐺 ) ) )
45 42 44 oveq12d ⊢ ( 𝑐 = 𝐺 → ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) = ( 𝐺 + ( 𝑟 · ( 𝑑 − 𝐺 ) ) ) )
46 45 eqeq2d ⊢ ( 𝑐 = 𝐺 → ( 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ↔ 𝑋 = ( 𝐺 + ( 𝑟 · ( 𝑑 − 𝐺 ) ) ) ) )
47 43 oveq2d ⊢ ( 𝑐 = 𝐺 → ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) = ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝐺 ) ) )
48 47 fveq2d ⊢ ( 𝑐 = 𝐺 → ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝐺 ) ) ) )
49 48 neeq1d ⊢ ( 𝑐 = 𝐺 → ( ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ↔ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝐺 ) ) ) ≠ 0 ) )
50 46 49 3anbi23d ⊢ ( 𝑐 = 𝐺 → ( ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ↔ ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝐺 + ( 𝑟 · ( 𝑑 − 𝐺 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝐺 ) ) ) ≠ 0 ) ) )
51 50 rexbidv ⊢ ( 𝑐 = 𝐺 → ( ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝐺 + ( 𝑟 · ( 𝑑 − 𝐺 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝐺 ) ) ) ≠ 0 ) ) )
52 51 2rexbidv ⊢ ( 𝑐 = 𝐺 → ( ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ↔ ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝐺 + ( 𝑟 · ( 𝑑 − 𝐺 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝐺 ) ) ) ≠ 0 ) ) )
53 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐴 ∈ Constr )
54 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) )
55 54 unssad ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → { 𝐴 , 𝐵 } ⊆ ( 𝐶 ‘ 𝑛 ) )
56 53 55 prssad ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐴 ∈ ( 𝐶 ‘ 𝑛 ) )
57 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐵 ∈ Constr )
58 57 55 prssbd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐵 ∈ ( 𝐶 ‘ 𝑛 ) )
59 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐺 ∈ Constr )
60 54 unssbd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → { 𝐺 , 𝐷 } ⊆ ( 𝐶 ‘ 𝑛 ) )
61 59 60 prssad ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐺 ∈ ( 𝐶 ‘ 𝑛 ) )
62 oveq1 ⊢ ( 𝑑 = 𝐷 → ( 𝑑 − 𝐺 ) = ( 𝐷 − 𝐺 ) )
63 62 oveq2d ⊢ ( 𝑑 = 𝐷 → ( 𝑟 · ( 𝑑 − 𝐺 ) ) = ( 𝑟 · ( 𝐷 − 𝐺 ) ) )
64 63 oveq2d ⊢ ( 𝑑 = 𝐷 → ( 𝐺 + ( 𝑟 · ( 𝑑 − 𝐺 ) ) ) = ( 𝐺 + ( 𝑟 · ( 𝐷 − 𝐺 ) ) ) )
65 64 eqeq2d ⊢ ( 𝑑 = 𝐷 → ( 𝑋 = ( 𝐺 + ( 𝑟 · ( 𝑑 − 𝐺 ) ) ) ↔ 𝑋 = ( 𝐺 + ( 𝑟 · ( 𝐷 − 𝐺 ) ) ) ) )
66 62 oveq2d ⊢ ( 𝑑 = 𝐷 → ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝐺 ) ) = ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐺 ) ) )
67 66 fveq2d ⊢ ( 𝑑 = 𝐷 → ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝐺 ) ) ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐺 ) ) ) )
68 67 neeq1d ⊢ ( 𝑑 = 𝐷 → ( ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝐺 ) ) ) ≠ 0 ↔ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐺 ) ) ) ≠ 0 ) )
69 65 68 3anbi23d ⊢ ( 𝑑 = 𝐷 → ( ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝐺 + ( 𝑟 · ( 𝑑 − 𝐺 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝐺 ) ) ) ≠ 0 ) ↔ ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝐺 + ( 𝑟 · ( 𝐷 − 𝐺 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐺 ) ) ) ≠ 0 ) ) )
70 oveq1 ⊢ ( 𝑡 = 𝑇 → ( 𝑡 · ( 𝐵 − 𝐴 ) ) = ( 𝑇 · ( 𝐵 − 𝐴 ) ) )
71 70 oveq2d ⊢ ( 𝑡 = 𝑇 → ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) )
72 71 eqeq2d ⊢ ( 𝑡 = 𝑇 → ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) ↔ 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ) )
73 72 3anbi1d ⊢ ( 𝑡 = 𝑇 → ( ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝐺 + ( 𝑟 · ( 𝐷 − 𝐺 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐺 ) ) ) ≠ 0 ) ↔ ( 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝐺 + ( 𝑟 · ( 𝐷 − 𝐺 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐺 ) ) ) ≠ 0 ) ) )
74 oveq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 · ( 𝐷 − 𝐺 ) ) = ( 𝑅 · ( 𝐷 − 𝐺 ) ) )
75 74 oveq2d ⊢ ( 𝑟 = 𝑅 → ( 𝐺 + ( 𝑟 · ( 𝐷 − 𝐺 ) ) ) = ( 𝐺 + ( 𝑅 · ( 𝐷 − 𝐺 ) ) ) )
76 75 eqeq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑋 = ( 𝐺 + ( 𝑟 · ( 𝐷 − 𝐺 ) ) ) ↔ 𝑋 = ( 𝐺 + ( 𝑅 · ( 𝐷 − 𝐺 ) ) ) ) )
77 76 3anbi2d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝐺 + ( 𝑟 · ( 𝐷 − 𝐺 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐺 ) ) ) ≠ 0 ) ↔ ( 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝐺 + ( 𝑅 · ( 𝐷 − 𝐺 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐺 ) ) ) ≠ 0 ) ) )
78 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐷 ∈ Constr )
79 78 60 prssbd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐷 ∈ ( 𝐶 ‘ 𝑛 ) )
80 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝑇 ∈ ℝ )
81 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝑅 ∈ ℝ )
82 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) )
83 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝑋 = ( 𝐺 + ( 𝑅 · ( 𝐷 − 𝐺 ) ) ) )
84 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐺 ) ) ) ≠ 0 )
85 82 83 84 3jca ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ( 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝐺 + ( 𝑅 · ( 𝐷 − 𝐺 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐺 ) ) ) ≠ 0 ) )
86 69 73 77 79 80 81 85 3rspcedvdw ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝐴 + ( 𝑡 · ( 𝐵 − 𝐴 ) ) ) ∧ 𝑋 = ( 𝐺 + ( 𝑟 · ( 𝑑 − 𝐺 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝑑 − 𝐺 ) ) ) ≠ 0 ) )
87 30 41 52 56 58 61 86 3rspcedvdw ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) )
88 87 3mix1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ( ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
89 nnon ⊢ ( 𝑛 ∈ ω → 𝑛 ∈ On )
90 89 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝑛 ∈ On )
91 eqid ⊢ ( 𝐶 ‘ 𝑛 ) = ( 𝐶 ‘ 𝑛 )
92 1 90 91 constrsuc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ( 𝑋 ∈ ( 𝐶 ‘ suc 𝑛 ) ↔ ( 𝑋 ∈ ℂ ∧ ( ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) ) ) )
93 18 88 92 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝑋 ∈ ( 𝐶 ‘ suc 𝑛 ) )
94 14 17 93 rspcedvd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ∃ 𝑚 ∈ ω 𝑋 ∈ ( 𝐶 ‘ 𝑚 ) )
95 1 isconstr ⊢ ( 𝑋 ∈ Constr ↔ ∃ 𝑚 ∈ ω 𝑋 ∈ ( 𝐶 ‘ 𝑚 ) )
96 94 95 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝑋 ∈ Constr )
97 2 3 prssd ⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ Constr )
98 4 5 prssd ⊢ ( 𝜑 → { 𝐺 , 𝐷 } ⊆ Constr )
99 97 98 unssd ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ Constr )
100 prfi ⊢ { 𝐴 , 𝐵 } ∈ Fin
101 100 a1i ⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ Fin )
102 prfi ⊢ { 𝐺 , 𝐷 } ∈ Fin
103 102 a1i ⊢ ( 𝜑 → { 𝐺 , 𝐷 } ∈ Fin )
104 101 103 unfid ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ∈ Fin )
105 1 99 104 constrfiss ⊢ ( 𝜑 → ∃ 𝑛 ∈ ω ( { 𝐴 , 𝐵 } ∪ { 𝐺 , 𝐷 } ) ⊆ ( 𝐶 ‘ 𝑛 ) )
106 96 105 r19.29a ⊢ ( 𝜑 → 𝑋 ∈ Constr )