Metamath Proof Explorer

Theorem axlowdimlem17

Description: Lemma for axlowdim . Establish a congruence result. (Contributed by Scott Fenton, 22-Apr-2013) (Proof shortened by Mario Carneiro, 22-May-2014)

Ref Expression
Hypotheses axlowdimlem16.1 ⊢ 𝑃 = ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) )
axlowdimlem16.2 ⊢ 𝑄 = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) )
axlowdimlem17.3 ⊢ 𝐴 = ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) )
axlowdimlem17.4 ⊢ 𝑋 ∈ ℝ
axlowdimlem17.5 ⊢ 𝑌 ∈ ℝ
Assertion axlowdimlem17 ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ⟨ 𝑃 , 𝐴 ⟩ Cgr ⟨ 𝑄 , 𝐴 ⟩ )

Proof

Step Hyp Ref Expression
1 axlowdimlem16.1 ⊢ 𝑃 = ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) )
2 axlowdimlem16.2 ⊢ 𝑄 = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) )
3 axlowdimlem17.3 ⊢ 𝐴 = ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) )
4 axlowdimlem17.4 ⊢ 𝑋 ∈ ℝ
5 axlowdimlem17.5 ⊢ 𝑌 ∈ ℝ
6 uzuzle23 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
7 6 ad2antrr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
8 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 1 ... 2 ) ⊆ ( 1 ... 𝑁 ) )
9 7 8 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → ( 1 ... 2 ) ⊆ ( 1 ... 𝑁 ) )
10 simpr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → 𝑖 ∈ ( 1 ... 2 ) )
11 9 10 sseldd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
12 fznuz ⊢ ( 𝑖 ∈ ( 1 ... 2 ) → ¬ 𝑖 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) )
13 12 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → ¬ 𝑖 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) )
14 3z ⊢ 3 ∈ ℤ
15 uzid ⊢ ( 3 ∈ ℤ → 3 ∈ ( ℤ≥ ‘ 3 ) )
16 14 15 ax-mp ⊢ 3 ∈ ( ℤ≥ ‘ 3 )
17 df-3 ⊢ 3 = ( 2 + 1 )
18 17 fveq2i ⊢ ( ℤ≥ ‘ 3 ) = ( ℤ≥ ‘ ( 2 + 1 ) )
19 16 18 eleqtri ⊢ 3 ∈ ( ℤ≥ ‘ ( 2 + 1 ) )
20 eleq1 ⊢ ( 𝑖 = 3 → ( 𝑖 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) ↔ 3 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) ) )
21 19 20 mpbiri ⊢ ( 𝑖 = 3 → 𝑖 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) )
22 21 necon3bi ⊢ ( ¬ 𝑖 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) → 𝑖 ≠ 3 )
23 13 22 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → 𝑖 ≠ 3 )
24 1 axlowdimlem9 ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑖 ≠ 3 ) → ( 𝑃 ‘ 𝑖 ) = 0 )
25 11 23 24 syl2anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → ( 𝑃 ‘ 𝑖 ) = 0 )
26 elfzuz ⊢ ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) → 𝐼 ∈ ( ℤ≥ ‘ 2 ) )
27 26 ad2antlr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → 𝐼 ∈ ( ℤ≥ ‘ 2 ) )
28 eluzp1p1 ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) )
29 27 28 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) )
30 uzss ⊢ ( ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) → ( ℤ≥ ‘ ( 𝐼 + 1 ) ) ⊆ ( ℤ≥ ‘ ( 2 + 1 ) ) )
31 29 30 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → ( ℤ≥ ‘ ( 𝐼 + 1 ) ) ⊆ ( ℤ≥ ‘ ( 2 + 1 ) ) )
32 31 13 ssneldd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → ¬ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) )
33 eluzelz ⊢ ( ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) → ( 𝐼 + 1 ) ∈ ℤ )
34 29 33 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → ( 𝐼 + 1 ) ∈ ℤ )
35 uzid ⊢ ( ( 𝐼 + 1 ) ∈ ℤ → ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) )
36 34 35 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) )
37 eleq1 ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( 𝑖 ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) ↔ ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) ) )
38 36 37 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → ( 𝑖 = ( 𝐼 + 1 ) → 𝑖 ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) ) )
39 38 necon3bd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → ( ¬ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) → 𝑖 ≠ ( 𝐼 + 1 ) ) )
40 32 39 mpd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → 𝑖 ≠ ( 𝐼 + 1 ) )
41 2 axlowdimlem12 ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑖 ≠ ( 𝐼 + 1 ) ) → ( 𝑄 ‘ 𝑖 ) = 0 )
42 11 40 41 syl2anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → ( 𝑄 ‘ 𝑖 ) = 0 )
43 25 42 eqtr4d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → ( 𝑃 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑖 ) )
44 43 oveq1d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) )
45 44 oveq1d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 2 ) ) → ( ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) )
46 45 sumeq2dv ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 1 ... 2 ) ( ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 2 ) ( ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) )
47 1 2 axlowdimlem16 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) )
48 3 fveq1i ⊢ ( 𝐴 ‘ 𝑖 ) = ( ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 )
49 axlowdimlem2 ⊢ ( ( 1 ... 2 ) ∩ ( 3 ... 𝑁 ) ) = ∅
50 4 5 axlowdimlem4 ⊢ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } : ( 1 ... 2 ) ⟶ ℝ
51 ffn ⊢ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } : ( 1 ... 2 ) ⟶ ℝ → { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } Fn ( 1 ... 2 ) )
52 50 51 ax-mp ⊢ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } Fn ( 1 ... 2 )
53 axlowdimlem1 ⊢ ( ( 3 ... 𝑁 ) × { 0 } ) : ( 3 ... 𝑁 ) ⟶ ℝ
54 ffn ⊢ ( ( ( 3 ... 𝑁 ) × { 0 } ) : ( 3 ... 𝑁 ) ⟶ ℝ → ( ( 3 ... 𝑁 ) × { 0 } ) Fn ( 3 ... 𝑁 ) )
55 53 54 ax-mp ⊢ ( ( 3 ... 𝑁 ) × { 0 } ) Fn ( 3 ... 𝑁 )
56 fvun2 ⊢ ( ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } Fn ( 1 ... 2 ) ∧ ( ( 3 ... 𝑁 ) × { 0 } ) Fn ( 3 ... 𝑁 ) ∧ ( ( ( 1 ... 2 ) ∩ ( 3 ... 𝑁 ) ) = ∅ ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) ) → ( ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) = ( ( ( 3 ... 𝑁 ) × { 0 } ) ‘ 𝑖 ) )
57 52 55 56 mp3an12 ⊢ ( ( ( ( 1 ... 2 ) ∩ ( 3 ... 𝑁 ) ) = ∅ ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) = ( ( ( 3 ... 𝑁 ) × { 0 } ) ‘ 𝑖 ) )
58 49 57 mpan ⊢ ( 𝑖 ∈ ( 3 ... 𝑁 ) → ( ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) = ( ( ( 3 ... 𝑁 ) × { 0 } ) ‘ 𝑖 ) )
59 48 58 eqtrid ⊢ ( 𝑖 ∈ ( 3 ... 𝑁 ) → ( 𝐴 ‘ 𝑖 ) = ( ( ( 3 ... 𝑁 ) × { 0 } ) ‘ 𝑖 ) )
60 c0ex ⊢ 0 ∈ V
61 60 fvconst2 ⊢ ( 𝑖 ∈ ( 3 ... 𝑁 ) → ( ( ( 3 ... 𝑁 ) × { 0 } ) ‘ 𝑖 ) = 0 )
62 59 61 eqtrd ⊢ ( 𝑖 ∈ ( 3 ... 𝑁 ) → ( 𝐴 ‘ 𝑖 ) = 0 )
63 62 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) = 0 )
64 63 oveq2d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( 𝑃 ‘ 𝑖 ) − 0 ) )
65 1 axlowdimlem7 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
66 65 ad2antrr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
67 3nn ⊢ 3 ∈ ℕ
68 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
69 67 68 eleqtri ⊢ 3 ∈ ( ℤ≥ ‘ 1 )
70 fzss1 ⊢ ( 3 ∈ ( ℤ≥ ‘ 1 ) → ( 3 ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
71 69 70 ax-mp ⊢ ( 3 ... 𝑁 ) ⊆ ( 1 ... 𝑁 )
72 71 sseli ⊢ ( 𝑖 ∈ ( 3 ... 𝑁 ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
73 72 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
74 fveecn ⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℂ )
75 66 73 74 syl2anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℂ )
76 75 subid1d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( ( 𝑃 ‘ 𝑖 ) − 0 ) = ( 𝑃 ‘ 𝑖 ) )
77 64 76 eqtrd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( 𝑃 ‘ 𝑖 ) )
78 77 oveq1d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) = ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) )
79 78 sumeq2dv ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) )
80 63 oveq2d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( 𝑄 ‘ 𝑖 ) − 0 ) )
81 eluz3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
82 2eluzge1 ⊢ 2 ∈ ( ℤ≥ ‘ 1 )
83 fzss1 ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... ( 𝑁 − 1 ) ) )
84 82 83 ax-mp ⊢ ( 2 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... ( 𝑁 − 1 ) )
85 84 sseli ⊢ ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) → 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
86 2 axlowdimlem10 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
87 81 85 86 syl2an ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
88 fveecn ⊢ ( ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℂ )
89 87 72 88 syl2an ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℂ )
90 89 subid1d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( ( 𝑄 ‘ 𝑖 ) − 0 ) = ( 𝑄 ‘ 𝑖 ) )
91 80 90 eqtrd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( 𝑄 ‘ 𝑖 ) )
92 91 oveq1d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) = ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) )
93 92 sumeq2dv ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) )
94 47 79 93 3eqtr4d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) )
95 46 94 oveq12d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( Σ 𝑖 ∈ ( 1 ... 2 ) ( ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) + Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) ) = ( Σ 𝑖 ∈ ( 1 ... 2 ) ( ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) + Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) ) )
96 49 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ( 1 ... 2 ) ∩ ( 3 ... 𝑁 ) ) = ∅ )
97 eluzelre ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℝ )
98 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
99 2re ⊢ 2 ∈ ℝ
100 3re ⊢ 3 ∈ ℝ
101 2lt3 ⊢ 2 < 3
102 99 100 101 ltleii ⊢ 2 ≤ 3
103 letr ⊢ ( ( 2 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 2 ≤ 3 ∧ 3 ≤ 𝑁 ) → 2 ≤ 𝑁 ) )
104 99 100 103 mp3an12 ⊢ ( 𝑁 ∈ ℝ → ( ( 2 ≤ 3 ∧ 3 ≤ 𝑁 ) → 2 ≤ 𝑁 ) )
105 102 104 mpani ⊢ ( 𝑁 ∈ ℝ → ( 3 ≤ 𝑁 → 2 ≤ 𝑁 ) )
106 97 98 105 sylc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ≤ 𝑁 )
107 1le2 ⊢ 1 ≤ 2
108 106 107 jctil ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 1 ≤ 2 ∧ 2 ≤ 𝑁 ) )
109 108 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 1 ≤ 2 ∧ 2 ≤ 𝑁 ) )
110 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
111 110 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℤ )
112 2z ⊢ 2 ∈ ℤ
113 1z ⊢ 1 ∈ ℤ
114 elfz ⊢ ( ( 2 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 2 ∧ 2 ≤ 𝑁 ) ) )
115 112 113 114 mp3an12 ⊢ ( 𝑁 ∈ ℤ → ( 2 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 2 ∧ 2 ≤ 𝑁 ) ) )
116 111 115 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 2 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 2 ∧ 2 ≤ 𝑁 ) ) )
117 109 116 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 2 ∈ ( 1 ... 𝑁 ) )
118 fzsplit ⊢ ( 2 ∈ ( 1 ... 𝑁 ) → ( 1 ... 𝑁 ) = ( ( 1 ... 2 ) ∪ ( ( 2 + 1 ) ... 𝑁 ) ) )
119 117 118 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... 2 ) ∪ ( ( 2 + 1 ) ... 𝑁 ) ) )
120 17 oveq1i ⊢ ( 3 ... 𝑁 ) = ( ( 2 + 1 ) ... 𝑁 )
121 120 uneq2i ⊢ ( ( 1 ... 2 ) ∪ ( 3 ... 𝑁 ) ) = ( ( 1 ... 2 ) ∪ ( ( 2 + 1 ) ... 𝑁 ) )
122 119 121 eqtr4di ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... 2 ) ∪ ( 3 ... 𝑁 ) ) )
123 fzfid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 1 ... 𝑁 ) ∈ Fin )
124 65 ad2antrr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
125 124 74 sylancom ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℂ )
126 4 5 axlowdimlem5 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
127 3 126 eqeltrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
128 6 127 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
129 128 ad2antrr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
130 fveecn ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
131 129 130 sylancom ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
132 125 131 subcld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ∈ ℂ )
133 132 sqcld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℂ )
134 96 122 123 133 fsumsplit ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) = ( Σ 𝑖 ∈ ( 1 ... 2 ) ( ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) + Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) ) )
135 87 88 sylan ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℂ )
136 135 131 subcld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ∈ ℂ )
137 136 sqcld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℂ )
138 96 122 123 137 fsumsplit ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) = ( Σ 𝑖 ∈ ( 1 ... 2 ) ( ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) + Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) ) )
139 95 134 138 3eqtr4d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) )
140 65 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
141 128 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
142 brcgr ⊢ ( ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑃 , 𝐴 ⟩ Cgr ⟨ 𝑄 , 𝐴 ⟩ ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) ) )
143 140 141 87 141 142 syl22anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ⟨ 𝑃 , 𝐴 ⟩ Cgr ⟨ 𝑄 , 𝐴 ⟩ ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑃 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑄 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) ) )
144 139 143 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ⟨ 𝑃 , 𝐴 ⟩ Cgr ⟨ 𝑄 , 𝐴 ⟩ )