Metamath Proof Explorer

Theorem constrcccllem

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

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

Proof

Step Hyp Ref Expression
1 constr0.1 ⊢ 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
2 constrcccllem.a ⊢ ( 𝜑 → 𝐴 ∈ Constr )
3 constrcccllem.b ⊢ ( 𝜑 → 𝐵 ∈ Constr )
4 constrcccllem.c ⊢ ( 𝜑 → 𝐺 ∈ Constr )
5 constrcccllem.d ⊢ ( 𝜑 → 𝐷 ∈ Constr )
6 constrcccllem.e ⊢ ( 𝜑 → 𝐸 ∈ Constr )
7 constrcccllem.f ⊢ ( 𝜑 → 𝐹 ∈ Constr )
8 constrcccllem.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
9 constrcccllem.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐷 )
10 constrcccllem.2 ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐺 ) ) )
11 constrcccllem.3 ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) )
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 neeq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ≠ 𝑑 ↔ 𝐴 ≠ 𝑑 ) )
20 oveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑋 − 𝑎 ) = ( 𝑋 − 𝐴 ) )
21 20 fveq2d ⊢ ( 𝑎 = 𝐴 → ( abs ‘ ( 𝑋 − 𝑎 ) ) = ( abs ‘ ( 𝑋 − 𝐴 ) ) )
22 21 eqeq1d ⊢ ( 𝑎 = 𝐴 → ( ( abs ‘ ( 𝑋 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ↔ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ) )
23 19 22 3anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
24 23 rexbidv ⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
25 24 2rexbidv ⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
26 oveq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 − 𝑐 ) = ( 𝐵 − 𝑐 ) )
27 26 fveq2d ⊢ ( 𝑏 = 𝐵 → ( abs ‘ ( 𝑏 − 𝑐 ) ) = ( abs ‘ ( 𝐵 − 𝑐 ) ) )
28 27 eqeq2d ⊢ ( 𝑏 = 𝐵 → ( ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ↔ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝑐 ) ) ) )
29 28 3anbi2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
30 29 rexbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
31 30 2rexbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
32 oveq2 ⊢ ( 𝑐 = 𝐺 → ( 𝐵 − 𝑐 ) = ( 𝐵 − 𝐺 ) )
33 32 fveq2d ⊢ ( 𝑐 = 𝐺 → ( abs ‘ ( 𝐵 − 𝑐 ) ) = ( abs ‘ ( 𝐵 − 𝐺 ) ) )
34 33 eqeq2d ⊢ ( 𝑐 = 𝐺 → ( ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝑐 ) ) ↔ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐺 ) ) ) )
35 34 3anbi2d ⊢ ( 𝑐 = 𝐺 → ( ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐺 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
36 35 rexbidv ⊢ ( 𝑐 = 𝐺 → ( ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐺 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
37 36 2rexbidv ⊢ ( 𝑐 = 𝐺 → ( ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐺 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
38 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐴 ∈ Constr )
39 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) )
40 39 unssad ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → { 𝐴 , 𝐵 , 𝐺 } ⊆ ( 𝐶 ‘ 𝑛 ) )
41 38 40 tpssad ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐴 ∈ ( 𝐶 ‘ 𝑛 ) )
42 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐵 ∈ Constr )
43 42 40 tpssbd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐵 ∈ ( 𝐶 ‘ 𝑛 ) )
44 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐺 ∈ Constr )
45 44 40 tpsscd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐺 ∈ ( 𝐶 ‘ 𝑛 ) )
46 neeq2 ⊢ ( 𝑑 = 𝐷 → ( 𝐴 ≠ 𝑑 ↔ 𝐴 ≠ 𝐷 ) )
47 oveq2 ⊢ ( 𝑑 = 𝐷 → ( 𝑋 − 𝑑 ) = ( 𝑋 − 𝐷 ) )
48 47 fveq2d ⊢ ( 𝑑 = 𝐷 → ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑋 − 𝐷 ) ) )
49 48 eqeq1d ⊢ ( 𝑑 = 𝐷 → ( ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ↔ ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) )
50 46 49 3anbi13d ⊢ ( 𝑑 = 𝐷 → ( ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐺 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ( 𝐴 ≠ 𝐷 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐺 ) ) ∧ ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
51 oveq1 ⊢ ( 𝑒 = 𝐸 → ( 𝑒 − 𝑓 ) = ( 𝐸 − 𝑓 ) )
52 51 fveq2d ⊢ ( 𝑒 = 𝐸 → ( abs ‘ ( 𝑒 − 𝑓 ) ) = ( abs ‘ ( 𝐸 − 𝑓 ) ) )
53 52 eqeq2d ⊢ ( 𝑒 = 𝐸 → ( ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ↔ ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝑓 ) ) ) )
54 53 3anbi3d ⊢ ( 𝑒 = 𝐸 → ( ( 𝐴 ≠ 𝐷 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐺 ) ) ∧ ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ↔ ( 𝐴 ≠ 𝐷 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐺 ) ) ∧ ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝑓 ) ) ) ) )
55 oveq2 ⊢ ( 𝑓 = 𝐹 → ( 𝐸 − 𝑓 ) = ( 𝐸 − 𝐹 ) )
56 55 fveq2d ⊢ ( 𝑓 = 𝐹 → ( abs ‘ ( 𝐸 − 𝑓 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) )
57 56 eqeq2d ⊢ ( 𝑓 = 𝐹 → ( ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝑓 ) ) ↔ ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) ) )
58 57 3anbi3d ⊢ ( 𝑓 = 𝐹 → ( ( 𝐴 ≠ 𝐷 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐺 ) ) ∧ ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝑓 ) ) ) ↔ ( 𝐴 ≠ 𝐷 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐺 ) ) ∧ ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) ) ) )
59 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐷 ∈ Constr )
60 39 unssbd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → { 𝐷 , 𝐸 , 𝐹 } ⊆ ( 𝐶 ‘ 𝑛 ) )
61 59 60 tpssad ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐷 ∈ ( 𝐶 ‘ 𝑛 ) )
62 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐸 ∈ Constr )
63 62 60 tpssbd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐸 ∈ ( 𝐶 ‘ 𝑛 ) )
64 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐹 ∈ Constr )
65 64 60 tpsscd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐹 ∈ ( 𝐶 ‘ 𝑛 ) )
66 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐴 ≠ 𝐷 )
67 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐺 ) ) )
68 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) )
69 66 67 68 3jca ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ( 𝐴 ≠ 𝐷 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐺 ) ) ∧ ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) ) )
70 50 54 58 61 63 65 69 3rspcedvdw ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝐴 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐺 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) )
71 25 31 37 41 43 45 70 3rspcedvdw ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) )
72 71 3mix3d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ( ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) )
73 nnon ⊢ ( 𝑛 ∈ ω → 𝑛 ∈ On )
74 73 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝑛 ∈ On )
75 eqid ⊢ ( 𝐶 ‘ 𝑛 ) = ( 𝐶 ‘ 𝑛 )
76 1 74 75 constrsuc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ( 𝑋 ∈ ( 𝐶 ‘ suc 𝑛 ) ↔ ( 𝑋 ∈ ℂ ∧ ( ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑋 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑡 ∈ ℝ ( 𝑋 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑋 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝐶 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝐶 ‘ 𝑛 ) ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑋 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑋 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) ) ) )
77 18 72 76 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝑋 ∈ ( 𝐶 ‘ suc 𝑛 ) )
78 14 17 77 rspcedvd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ∃ 𝑚 ∈ ω 𝑋 ∈ ( 𝐶 ‘ 𝑚 ) )
79 1 isconstr ⊢ ( 𝑋 ∈ Constr ↔ ∃ 𝑚 ∈ ω 𝑋 ∈ ( 𝐶 ‘ 𝑚 ) )
80 78 79 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝑋 ∈ Constr )
81 2 3 4 tpssd ⊢ ( 𝜑 → { 𝐴 , 𝐵 , 𝐺 } ⊆ Constr )
82 5 6 7 tpssd ⊢ ( 𝜑 → { 𝐷 , 𝐸 , 𝐹 } ⊆ Constr )
83 81 82 unssd ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ Constr )
84 tpfi ⊢ { 𝐴 , 𝐵 , 𝐺 } ∈ Fin
85 84 a1i ⊢ ( 𝜑 → { 𝐴 , 𝐵 , 𝐺 } ∈ Fin )
86 tpfi ⊢ { 𝐷 , 𝐸 , 𝐹 } ∈ Fin
87 86 a1i ⊢ ( 𝜑 → { 𝐷 , 𝐸 , 𝐹 } ∈ Fin )
88 85 87 unfid ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ∈ Fin )
89 1 83 88 constrfiss ⊢ ( 𝜑 → ∃ 𝑛 ∈ ω ( { 𝐴 , 𝐵 , 𝐺 } ∪ { 𝐷 , 𝐸 , 𝐹 } ) ⊆ ( 𝐶 ‘ 𝑛 ) )
90 80 89 r19.29a ⊢ ( 𝜑 → 𝑋 ∈ Constr )