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 
|- P = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
axlowdimlem16.2 
|- Q = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) )
axlowdimlem17.3 
|- A = ( { <. 1 , X >. , <. 2 , Y >. } u. ( ( 3 ... N ) X. { 0 } ) )
axlowdimlem17.4 
|- X e. RR
axlowdimlem17.5 
|- Y e. RR
Assertion axlowdimlem17 
|- ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> <. P , A >. Cgr <. Q , A >. )

Proof

Step Hyp Ref Expression
1 axlowdimlem16.1 
 |-  P = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
2 axlowdimlem16.2 
 |-  Q = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) )
3 axlowdimlem17.3 
 |-  A = ( { <. 1 , X >. , <. 2 , Y >. } u. ( ( 3 ... N ) X. { 0 } ) )
4 axlowdimlem17.4 
 |-  X e. RR
5 axlowdimlem17.5 
 |-  Y e. RR
6 uzuzle23 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
7 6 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> N e. ( ZZ>= ` 2 ) )
8 fzss2 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 ... 2 ) C_ ( 1 ... N ) )
9 7 8 syl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> ( 1 ... 2 ) C_ ( 1 ... N ) )
10 simpr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> i e. ( 1 ... 2 ) )
11 9 10 sseldd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> i e. ( 1 ... N ) )
12 fznuz 
 |-  ( i e. ( 1 ... 2 ) -> -. i e. ( ZZ>= ` ( 2 + 1 ) ) )
13 12 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> -. i e. ( ZZ>= ` ( 2 + 1 ) ) )
14 3z 
 |-  3 e. ZZ
15 uzid 
 |-  ( 3 e. ZZ -> 3 e. ( ZZ>= ` 3 ) )
16 14 15 ax-mp 
 |-  3 e. ( ZZ>= ` 3 )
17 df-3 
 |-  3 = ( 2 + 1 )
18 17 fveq2i 
 |-  ( ZZ>= ` 3 ) = ( ZZ>= ` ( 2 + 1 ) )
19 16 18 eleqtri 
 |-  3 e. ( ZZ>= ` ( 2 + 1 ) )
20 eleq1 
 |-  ( i = 3 -> ( i e. ( ZZ>= ` ( 2 + 1 ) ) <-> 3 e. ( ZZ>= ` ( 2 + 1 ) ) ) )
21 19 20 mpbiri 
 |-  ( i = 3 -> i e. ( ZZ>= ` ( 2 + 1 ) ) )
22 21 necon3bi 
 |-  ( -. i e. ( ZZ>= ` ( 2 + 1 ) ) -> i =/= 3 )
23 13 22 syl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> i =/= 3 )
24 1 axlowdimlem9 
 |-  ( ( i e. ( 1 ... N ) /\ i =/= 3 ) -> ( P ` i ) = 0 )
25 11 23 24 syl2anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> ( P ` i ) = 0 )
26 elfzuz 
 |-  ( I e. ( 2 ... ( N - 1 ) ) -> I e. ( ZZ>= ` 2 ) )
27 26 ad2antlr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> I e. ( ZZ>= ` 2 ) )
28 eluzp1p1 
 |-  ( I e. ( ZZ>= ` 2 ) -> ( I + 1 ) e. ( ZZ>= ` ( 2 + 1 ) ) )
29 27 28 syl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> ( I + 1 ) e. ( ZZ>= ` ( 2 + 1 ) ) )
30 uzss 
 |-  ( ( I + 1 ) e. ( ZZ>= ` ( 2 + 1 ) ) -> ( ZZ>= ` ( I + 1 ) ) C_ ( ZZ>= ` ( 2 + 1 ) ) )
31 29 30 syl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> ( ZZ>= ` ( I + 1 ) ) C_ ( ZZ>= ` ( 2 + 1 ) ) )
32 31 13 ssneldd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> -. i e. ( ZZ>= ` ( I + 1 ) ) )
33 eluzelz 
 |-  ( ( I + 1 ) e. ( ZZ>= ` ( 2 + 1 ) ) -> ( I + 1 ) e. ZZ )
34 29 33 syl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> ( I + 1 ) e. ZZ )
35 uzid 
 |-  ( ( I + 1 ) e. ZZ -> ( I + 1 ) e. ( ZZ>= ` ( I + 1 ) ) )
36 34 35 syl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> ( I + 1 ) e. ( ZZ>= ` ( I + 1 ) ) )
37 eleq1 
 |-  ( i = ( I + 1 ) -> ( i e. ( ZZ>= ` ( I + 1 ) ) <-> ( I + 1 ) e. ( ZZ>= ` ( I + 1 ) ) ) )
38 36 37 syl5ibrcom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> ( i = ( I + 1 ) -> i e. ( ZZ>= ` ( I + 1 ) ) ) )
39 38 necon3bd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> ( -. i e. ( ZZ>= ` ( I + 1 ) ) -> i =/= ( I + 1 ) ) )
40 32 39 mpd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> i =/= ( I + 1 ) )
41 2 axlowdimlem12 
 |-  ( ( i e. ( 1 ... N ) /\ i =/= ( I + 1 ) ) -> ( Q ` i ) = 0 )
42 11 40 41 syl2anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> ( Q ` i ) = 0 )
43 25 42 eqtr4d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> ( P ` i ) = ( Q ` i ) )
44 43 oveq1d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> ( ( P ` i ) - ( A ` i ) ) = ( ( Q ` i ) - ( A ` i ) ) )
45 44 oveq1d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... 2 ) ) -> ( ( ( P ` i ) - ( A ` i ) ) ^ 2 ) = ( ( ( Q ` i ) - ( A ` i ) ) ^ 2 ) )
46 45 sumeq2dv 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> sum_ i e. ( 1 ... 2 ) ( ( ( P ` i ) - ( A ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... 2 ) ( ( ( Q ` i ) - ( A ` i ) ) ^ 2 ) )
47 1 2 axlowdimlem16 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> sum_ i e. ( 3 ... N ) ( ( P ` i ) ^ 2 ) = sum_ i e. ( 3 ... N ) ( ( Q ` i ) ^ 2 ) )
48 3 fveq1i 
 |-  ( A ` i ) = ( ( { <. 1 , X >. , <. 2 , Y >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i )
49 axlowdimlem2 
 |-  ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/)
50 4 5 axlowdimlem4 
 |-  { <. 1 , X >. , <. 2 , Y >. } : ( 1 ... 2 ) --> RR
51 ffn 
 |-  ( { <. 1 , X >. , <. 2 , Y >. } : ( 1 ... 2 ) --> RR -> { <. 1 , X >. , <. 2 , Y >. } Fn ( 1 ... 2 ) )
52 50 51 ax-mp 
 |-  { <. 1 , X >. , <. 2 , Y >. } Fn ( 1 ... 2 )
53 axlowdimlem1 
 |-  ( ( 3 ... N ) X. { 0 } ) : ( 3 ... N ) --> RR
54 ffn 
 |-  ( ( ( 3 ... N ) X. { 0 } ) : ( 3 ... N ) --> RR -> ( ( 3 ... N ) X. { 0 } ) Fn ( 3 ... N ) )
55 53 54 ax-mp 
 |-  ( ( 3 ... N ) X. { 0 } ) Fn ( 3 ... N )
56 fvun2 
 |-  ( ( { <. 1 , X >. , <. 2 , Y >. } Fn ( 1 ... 2 ) /\ ( ( 3 ... N ) X. { 0 } ) Fn ( 3 ... N ) /\ ( ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/) /\ i e. ( 3 ... N ) ) ) -> ( ( { <. 1 , X >. , <. 2 , Y >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) = ( ( ( 3 ... N ) X. { 0 } ) ` i ) )
57 52 55 56 mp3an12 
 |-  ( ( ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/) /\ i e. ( 3 ... N ) ) -> ( ( { <. 1 , X >. , <. 2 , Y >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) = ( ( ( 3 ... N ) X. { 0 } ) ` i ) )
58 49 57 mpan 
 |-  ( i e. ( 3 ... N ) -> ( ( { <. 1 , X >. , <. 2 , Y >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) = ( ( ( 3 ... N ) X. { 0 } ) ` i ) )
59 48 58 syl5eq 
 |-  ( i e. ( 3 ... N ) -> ( A ` i ) = ( ( ( 3 ... N ) X. { 0 } ) ` i ) )
60 c0ex 
 |-  0 e. _V
61 60 fvconst2 
 |-  ( i e. ( 3 ... N ) -> ( ( ( 3 ... N ) X. { 0 } ) ` i ) = 0 )
62 59 61 eqtrd 
 |-  ( i e. ( 3 ... N ) -> ( A ` i ) = 0 )
63 62 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 3 ... N ) ) -> ( A ` i ) = 0 )
64 63 oveq2d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 3 ... N ) ) -> ( ( P ` i ) - ( A ` i ) ) = ( ( P ` i ) - 0 ) )
65 1 axlowdimlem7 
 |-  ( N e. ( ZZ>= ` 3 ) -> P e. ( EE ` N ) )
66 65 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 3 ... N ) ) -> P e. ( EE ` N ) )
67 3nn 
 |-  3 e. NN
68 nnuz 
 |-  NN = ( ZZ>= ` 1 )
69 67 68 eleqtri 
 |-  3 e. ( ZZ>= ` 1 )
70 fzss1 
 |-  ( 3 e. ( ZZ>= ` 1 ) -> ( 3 ... N ) C_ ( 1 ... N ) )
71 69 70 ax-mp 
 |-  ( 3 ... N ) C_ ( 1 ... N )
72 71 sseli 
 |-  ( i e. ( 3 ... N ) -> i e. ( 1 ... N ) )
73 72 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 3 ... N ) ) -> i e. ( 1 ... N ) )
74 fveecn 
 |-  ( ( P e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( P ` i ) e. CC )
75 66 73 74 syl2anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 3 ... N ) ) -> ( P ` i ) e. CC )
76 75 subid1d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 3 ... N ) ) -> ( ( P ` i ) - 0 ) = ( P ` i ) )
77 64 76 eqtrd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 3 ... N ) ) -> ( ( P ` i ) - ( A ` i ) ) = ( P ` i ) )
78 77 oveq1d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 3 ... N ) ) -> ( ( ( P ` i ) - ( A ` i ) ) ^ 2 ) = ( ( P ` i ) ^ 2 ) )
79 78 sumeq2dv 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> sum_ i e. ( 3 ... N ) ( ( ( P ` i ) - ( A ` i ) ) ^ 2 ) = sum_ i e. ( 3 ... N ) ( ( P ` i ) ^ 2 ) )
80 63 oveq2d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 3 ... N ) ) -> ( ( Q ` i ) - ( A ` i ) ) = ( ( Q ` i ) - 0 ) )
81 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
82 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
83 fzss1 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> ( 2 ... ( N - 1 ) ) C_ ( 1 ... ( N - 1 ) ) )
84 82 83 ax-mp 
 |-  ( 2 ... ( N - 1 ) ) C_ ( 1 ... ( N - 1 ) )
85 84 sseli 
 |-  ( I e. ( 2 ... ( N - 1 ) ) -> I e. ( 1 ... ( N - 1 ) ) )
86 2 axlowdimlem10 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> Q e. ( EE ` N ) )
87 81 85 86 syl2an 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> Q e. ( EE ` N ) )
88 fveecn 
 |-  ( ( Q e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( Q ` i ) e. CC )
89 87 72 88 syl2an 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 3 ... N ) ) -> ( Q ` i ) e. CC )
90 89 subid1d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 3 ... N ) ) -> ( ( Q ` i ) - 0 ) = ( Q ` i ) )
91 80 90 eqtrd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 3 ... N ) ) -> ( ( Q ` i ) - ( A ` i ) ) = ( Q ` i ) )
92 91 oveq1d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 3 ... N ) ) -> ( ( ( Q ` i ) - ( A ` i ) ) ^ 2 ) = ( ( Q ` i ) ^ 2 ) )
93 92 sumeq2dv 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> sum_ i e. ( 3 ... N ) ( ( ( Q ` i ) - ( A ` i ) ) ^ 2 ) = sum_ i e. ( 3 ... N ) ( ( Q ` i ) ^ 2 ) )
94 47 79 93 3eqtr4d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> sum_ i e. ( 3 ... N ) ( ( ( P ` i ) - ( A ` i ) ) ^ 2 ) = sum_ i e. ( 3 ... N ) ( ( ( Q ` i ) - ( A ` i ) ) ^ 2 ) )
95 46 94 oveq12d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> ( sum_ i e. ( 1 ... 2 ) ( ( ( P ` i ) - ( A ` i ) ) ^ 2 ) + sum_ i e. ( 3 ... N ) ( ( ( P ` i ) - ( A ` i ) ) ^ 2 ) ) = ( sum_ i e. ( 1 ... 2 ) ( ( ( Q ` i ) - ( A ` i ) ) ^ 2 ) + sum_ i e. ( 3 ... N ) ( ( ( Q ` i ) - ( A ` i ) ) ^ 2 ) ) )
96 49 a1i 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/) )
97 eluzelre 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. RR )
98 eluzle 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
99 2re 
 |-  2 e. RR
100 3re 
 |-  3 e. RR
101 2lt3 
 |-  2 < 3
102 99 100 101 ltleii 
 |-  2 <_ 3
103 letr 
 |-  ( ( 2 e. RR /\ 3 e. RR /\ N e. RR ) -> ( ( 2 <_ 3 /\ 3 <_ N ) -> 2 <_ N ) )
104 99 100 103 mp3an12 
 |-  ( N e. RR -> ( ( 2 <_ 3 /\ 3 <_ N ) -> 2 <_ N ) )
105 102 104 mpani 
 |-  ( N e. RR -> ( 3 <_ N -> 2 <_ N ) )
106 97 98 105 sylc 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 <_ N )
107 1le2 
 |-  1 <_ 2
108 106 107 jctil 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( 1 <_ 2 /\ 2 <_ N ) )
109 108 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> ( 1 <_ 2 /\ 2 <_ N ) )
110 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
111 110 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> N e. ZZ )
112 2z 
 |-  2 e. ZZ
113 1z 
 |-  1 e. ZZ
114 elfz 
 |-  ( ( 2 e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( 2 e. ( 1 ... N ) <-> ( 1 <_ 2 /\ 2 <_ N ) ) )
115 112 113 114 mp3an12 
 |-  ( N e. ZZ -> ( 2 e. ( 1 ... N ) <-> ( 1 <_ 2 /\ 2 <_ N ) ) )
116 111 115 syl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> ( 2 e. ( 1 ... N ) <-> ( 1 <_ 2 /\ 2 <_ N ) ) )
117 109 116 mpbird 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> 2 e. ( 1 ... N ) )
118 fzsplit 
 |-  ( 2 e. ( 1 ... N ) -> ( 1 ... N ) = ( ( 1 ... 2 ) u. ( ( 2 + 1 ) ... N ) ) )
119 117 118 syl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... 2 ) u. ( ( 2 + 1 ) ... N ) ) )
120 17 oveq1i 
 |-  ( 3 ... N ) = ( ( 2 + 1 ) ... N )
121 120 uneq2i 
 |-  ( ( 1 ... 2 ) u. ( 3 ... N ) ) = ( ( 1 ... 2 ) u. ( ( 2 + 1 ) ... N ) )
122 119 121 eqtr4di 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... 2 ) u. ( 3 ... N ) ) )
123 fzfid 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> ( 1 ... N ) e. Fin )
124 65 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... N ) ) -> P e. ( EE ` N ) )
125 124 74 sylancom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( P ` i ) e. CC )
126 4 5 axlowdimlem5 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , X >. , <. 2 , Y >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
127 3 126 eqeltrid 
 |-  ( N e. ( ZZ>= ` 2 ) -> A e. ( EE ` N ) )
128 6 127 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> A e. ( EE ` N ) )
129 128 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... N ) ) -> A e. ( EE ` N ) )
130 fveecn 
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
131 129 130 sylancom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
132 125 131 subcld 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( P ` i ) - ( A ` i ) ) e. CC )
133 132 sqcld 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( P ` i ) - ( A ` i ) ) ^ 2 ) e. CC )
134 96 122 123 133 fsumsplit 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> sum_ i e. ( 1 ... N ) ( ( ( P ` i ) - ( A ` i ) ) ^ 2 ) = ( sum_ i e. ( 1 ... 2 ) ( ( ( P ` i ) - ( A ` i ) ) ^ 2 ) + sum_ i e. ( 3 ... N ) ( ( ( P ` i ) - ( A ` i ) ) ^ 2 ) ) )
135 87 88 sylan 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( Q ` i ) e. CC )
136 135 131 subcld 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( Q ` i ) - ( A ` i ) ) e. CC )
137 136 sqcld 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( Q ` i ) - ( A ` i ) ) ^ 2 ) e. CC )
138 96 122 123 137 fsumsplit 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> sum_ i e. ( 1 ... N ) ( ( ( Q ` i ) - ( A ` i ) ) ^ 2 ) = ( sum_ i e. ( 1 ... 2 ) ( ( ( Q ` i ) - ( A ` i ) ) ^ 2 ) + sum_ i e. ( 3 ... N ) ( ( ( Q ` i ) - ( A ` i ) ) ^ 2 ) ) )
139 95 134 138 3eqtr4d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> sum_ i e. ( 1 ... N ) ( ( ( P ` i ) - ( A ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( Q ` i ) - ( A ` i ) ) ^ 2 ) )
140 65 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> P e. ( EE ` N ) )
141 128 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> A e. ( EE ` N ) )
142 brcgr 
 |-  ( ( ( P e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) ) -> ( <. P , A >. Cgr <. Q , A >. <-> sum_ i e. ( 1 ... N ) ( ( ( P ` i ) - ( A ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( Q ` i ) - ( A ` i ) ) ^ 2 ) ) )
143 140 141 87 141 142 syl22anc 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> ( <. P , A >. Cgr <. Q , A >. <-> sum_ i e. ( 1 ... N ) ( ( ( P ` i ) - ( A ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( Q ` i ) - ( A ` i ) ) ^ 2 ) ) )
144 139 143 mpbird 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> <. P , A >. Cgr <. Q , A >. )