Metamath Proof Explorer

Theorem axlowdimlem16

Description: Lemma for axlowdim . Set up a summation that will help establish distance. (Contributed by Scott Fenton, 21-Apr-2013)

Ref Expression
Hypotheses axlowdimlem16.1 ⊢ 𝑃 = ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) )
axlowdimlem16.2 ⊢ 𝑄 = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) )
Assertion axlowdimlem16 ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) )

Proof

Step Hyp Ref Expression
1 axlowdimlem16.1 ⊢ 𝑃 = ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) )
2 axlowdimlem16.2 ⊢ 𝑄 = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) )
3 elfz1eq ⊢ ( 𝐼 ∈ ( 2 ... 2 ) → 𝐼 = 2 )
4 3z ⊢ 3 ∈ ℤ
5 ax-1cn ⊢ 1 ∈ ℂ
6 5 sqcli ⊢ ( 1 ↑ 2 ) ∈ ℂ
7 fveq2 ⊢ ( 𝑖 = 3 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 3 ) )
8 1 axlowdimlem8 ⊢ ( 𝑃 ‘ 3 ) = - 1
9 7 8 eqtrdi ⊢ ( 𝑖 = 3 → ( 𝑃 ‘ 𝑖 ) = - 1 )
10 9 oveq1d ⊢ ( 𝑖 = 3 → ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = ( - 1 ↑ 2 ) )
11 sqneg ⊢ ( 1 ∈ ℂ → ( - 1 ↑ 2 ) = ( 1 ↑ 2 ) )
12 5 11 ax-mp ⊢ ( - 1 ↑ 2 ) = ( 1 ↑ 2 )
13 10 12 eqtrdi ⊢ ( 𝑖 = 3 → ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = ( 1 ↑ 2 ) )
14 13 fsum1 ⊢ ( ( 3 ∈ ℤ ∧ ( 1 ↑ 2 ) ∈ ℂ ) → Σ 𝑖 ∈ ( 3 ... 3 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = ( 1 ↑ 2 ) )
15 4 6 14 mp2an ⊢ Σ 𝑖 ∈ ( 3 ... 3 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = ( 1 ↑ 2 )
16 df-3 ⊢ 3 = ( 2 + 1 )
17 oveq1 ⊢ ( 𝐼 = 2 → ( 𝐼 + 1 ) = ( 2 + 1 ) )
18 16 17 eqtr4id ⊢ ( 𝐼 = 2 → 3 = ( 𝐼 + 1 ) )
19 18 18 oveq12d ⊢ ( 𝐼 = 2 → ( 3 ... 3 ) = ( ( 𝐼 + 1 ) ... ( 𝐼 + 1 ) ) )
20 19 sumeq1d ⊢ ( 𝐼 = 2 → Σ 𝑖 ∈ ( 3 ... 3 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... ( 𝐼 + 1 ) ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) )
21 17 16 eqtr4di ⊢ ( 𝐼 = 2 → ( 𝐼 + 1 ) = 3 )
22 21 4 eqeltrdi ⊢ ( 𝐼 = 2 → ( 𝐼 + 1 ) ∈ ℤ )
23 fveq2 ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
24 2 axlowdimlem11 ⊢ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 1
25 23 24 eqtrdi ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( 𝑄 ‘ 𝑖 ) = 1 )
26 25 oveq1d ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = ( 1 ↑ 2 ) )
27 26 fsum1 ⊢ ( ( ( 𝐼 + 1 ) ∈ ℤ ∧ ( 1 ↑ 2 ) ∈ ℂ ) → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... ( 𝐼 + 1 ) ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = ( 1 ↑ 2 ) )
28 22 6 27 sylancl ⊢ ( 𝐼 = 2 → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... ( 𝐼 + 1 ) ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = ( 1 ↑ 2 ) )
29 20 28 eqtrd ⊢ ( 𝐼 = 2 → Σ 𝑖 ∈ ( 3 ... 3 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = ( 1 ↑ 2 ) )
30 15 29 eqtr4id ⊢ ( 𝐼 = 2 → Σ 𝑖 ∈ ( 3 ... 3 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 3 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) )
31 3 30 syl ⊢ ( 𝐼 ∈ ( 2 ... 2 ) → Σ 𝑖 ∈ ( 3 ... 3 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 3 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) )
32 31 a1i ⊢ ( 𝑁 = 3 → ( 𝐼 ∈ ( 2 ... 2 ) → Σ 𝑖 ∈ ( 3 ... 3 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 3 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) )
33 oveq1 ⊢ ( 𝑁 = 3 → ( 𝑁 − 1 ) = ( 3 − 1 ) )
34 3m1e2 ⊢ ( 3 − 1 ) = 2
35 33 34 eqtrdi ⊢ ( 𝑁 = 3 → ( 𝑁 − 1 ) = 2 )
36 35 oveq2d ⊢ ( 𝑁 = 3 → ( 2 ... ( 𝑁 − 1 ) ) = ( 2 ... 2 ) )
37 36 eleq2d ⊢ ( 𝑁 = 3 → ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ↔ 𝐼 ∈ ( 2 ... 2 ) ) )
38 oveq2 ⊢ ( 𝑁 = 3 → ( 3 ... 𝑁 ) = ( 3 ... 3 ) )
39 38 sumeq1d ⊢ ( 𝑁 = 3 → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 3 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) )
40 38 sumeq1d ⊢ ( 𝑁 = 3 → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 3 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) )
41 39 40 eqeq12d ⊢ ( 𝑁 = 3 → ( Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ↔ Σ 𝑖 ∈ ( 3 ... 3 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 3 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) )
42 32 37 41 3imtr4d ⊢ ( 𝑁 = 3 → ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) )
43 42 adantld ⊢ ( 𝑁 = 3 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) )
44 simprl ⊢ ( ( 𝑁 ≠ 3 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
45 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
46 45 adantl ⊢ ( ( 𝑁 ≠ 3 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 3 ≤ 𝑁 )
47 simpl ⊢ ( ( 𝑁 ≠ 3 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑁 ≠ 3 )
48 3re ⊢ 3 ∈ ℝ
49 eluzelre ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℝ )
50 49 adantl ⊢ ( ( 𝑁 ≠ 3 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑁 ∈ ℝ )
51 ltlen ⊢ ( ( 3 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 3 < 𝑁 ↔ ( 3 ≤ 𝑁 ∧ 𝑁 ≠ 3 ) ) )
52 48 50 51 sylancr ⊢ ( ( 𝑁 ≠ 3 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 3 < 𝑁 ↔ ( 3 ≤ 𝑁 ∧ 𝑁 ≠ 3 ) ) )
53 46 47 52 mpbir2and ⊢ ( ( 𝑁 ≠ 3 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 3 < 𝑁 )
54 53 adantrr ⊢ ( ( 𝑁 ≠ 3 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 3 < 𝑁 )
55 simprr ⊢ ( ( 𝑁 ≠ 3 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) )
56 fzssp1 ⊢ ( 2 ... ( 𝑁 − 1 ) ) ⊆ ( 2 ... ( ( 𝑁 − 1 ) + 1 ) )
57 simp3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) )
58 56 57 sselid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝐼 ∈ ( 2 ... ( ( 𝑁 − 1 ) + 1 ) ) )
59 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
60 59 3ad2ant1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℤ )
61 60 zcnd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℂ )
62 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
63 61 5 62 sylancl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
64 63 oveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 2 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 2 ... 𝑁 ) )
65 58 64 eleqtrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝐼 ∈ ( 2 ... 𝑁 ) )
66 elfzelz ⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ℤ )
67 65 66 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝐼 ∈ ℤ )
68 67 zred ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝐼 ∈ ℝ )
69 68 ltp1d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝐼 < ( 𝐼 + 1 ) )
70 fzdisj ⊢ ( 𝐼 < ( 𝐼 + 1 ) → ( ( 2 ... 𝐼 ) ∩ ( ( 𝐼 + 1 ) ... 𝑁 ) ) = ∅ )
71 69 70 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ( 2 ... 𝐼 ) ∩ ( ( 𝐼 + 1 ) ... 𝑁 ) ) = ∅ )
72 fzsplit ⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → ( 2 ... 𝑁 ) = ( ( 2 ... 𝐼 ) ∪ ( ( 𝐼 + 1 ) ... 𝑁 ) ) )
73 65 72 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 2 ... 𝑁 ) = ( ( 2 ... 𝐼 ) ∪ ( ( 𝐼 + 1 ) ... 𝑁 ) ) )
74 fzfid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 2 ... 𝑁 ) ∈ Fin )
75 eluzge3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
76 2eluzge1 ⊢ 2 ∈ ( ℤ≥ ‘ 1 )
77 fzss1 ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... ( 𝑁 − 1 ) ) )
78 76 77 ax-mp ⊢ ( 2 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... ( 𝑁 − 1 ) )
79 78 sseli ⊢ ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) → 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
80 2 axlowdimlem10 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
81 75 79 80 syl2an ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
82 fzss1 ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
83 76 82 ax-mp ⊢ ( 2 ... 𝑁 ) ⊆ ( 1 ... 𝑁 )
84 83 sseli ⊢ ( 𝑖 ∈ ( 2 ... 𝑁 ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
85 fveecn ⊢ ( ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℂ )
86 81 84 85 syl2an ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 2 ... 𝑁 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℂ )
87 86 sqcld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 2 ... 𝑁 ) ) → ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ∈ ℂ )
88 87 3adantl2 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 2 ... 𝑁 ) ) → ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ∈ ℂ )
89 71 73 74 88 fsumsplit ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 2 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = ( Σ 𝑖 ∈ ( 2 ... 𝐼 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) + Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) )
90 elfzelz ⊢ ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) → 𝐼 ∈ ℤ )
91 90 zred ⊢ ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) → 𝐼 ∈ ℝ )
92 91 3ad2ant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝐼 ∈ ℝ )
93 49 3ad2ant1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℝ )
94 peano2rem ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )
95 93 94 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ℝ )
96 elfzle2 ⊢ ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) → 𝐼 ≤ ( 𝑁 − 1 ) )
97 96 3ad2ant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝐼 ≤ ( 𝑁 − 1 ) )
98 93 ltm1d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) < 𝑁 )
99 92 95 93 97 98 lelttrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝐼 < 𝑁 )
100 92 93 99 ltled ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝐼 ≤ 𝑁 )
101 90 3ad2ant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝐼 ∈ ℤ )
102 eluz ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐼 ) ↔ 𝐼 ≤ 𝑁 ) )
103 101 60 102 syl2anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐼 ) ↔ 𝐼 ≤ 𝑁 ) )
104 100 103 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐼 ) )
105 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐼 ) → ( 1 ... 𝐼 ) ⊆ ( 1 ... 𝑁 ) )
106 104 105 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 1 ... 𝐼 ) ⊆ ( 1 ... 𝑁 ) )
107 106 sseld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 𝑖 ∈ ( 1 ... 𝐼 ) → 𝑖 ∈ ( 1 ... 𝑁 ) ) )
108 fzss1 ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ... 𝐼 ) ⊆ ( 1 ... 𝐼 ) )
109 76 108 ax-mp ⊢ ( 2 ... 𝐼 ) ⊆ ( 1 ... 𝐼 )
110 109 sseli ⊢ ( 𝑖 ∈ ( 2 ... 𝐼 ) → 𝑖 ∈ ( 1 ... 𝐼 ) )
111 107 110 impel ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 2 ... 𝐼 ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
112 elfzelz ⊢ ( 𝑖 ∈ ( 2 ... 𝐼 ) → 𝑖 ∈ ℤ )
113 112 zred ⊢ ( 𝑖 ∈ ( 2 ... 𝐼 ) → 𝑖 ∈ ℝ )
114 113 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 2 ... 𝐼 ) ) → 𝑖 ∈ ℝ )
115 92 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 2 ... 𝐼 ) ) → 𝐼 ∈ ℝ )
116 peano2re ⊢ ( 𝐼 ∈ ℝ → ( 𝐼 + 1 ) ∈ ℝ )
117 91 116 syl ⊢ ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) → ( 𝐼 + 1 ) ∈ ℝ )
118 117 3ad2ant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 𝐼 + 1 ) ∈ ℝ )
119 118 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 2 ... 𝐼 ) ) → ( 𝐼 + 1 ) ∈ ℝ )
120 elfzle2 ⊢ ( 𝑖 ∈ ( 2 ... 𝐼 ) → 𝑖 ≤ 𝐼 )
121 120 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 2 ... 𝐼 ) ) → 𝑖 ≤ 𝐼 )
122 115 ltp1d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 2 ... 𝐼 ) ) → 𝐼 < ( 𝐼 + 1 ) )
123 114 115 119 121 122 lelttrd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 2 ... 𝐼 ) ) → 𝑖 < ( 𝐼 + 1 ) )
124 114 123 ltned ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 2 ... 𝐼 ) ) → 𝑖 ≠ ( 𝐼 + 1 ) )
125 2 axlowdimlem12 ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑖 ≠ ( 𝐼 + 1 ) ) → ( 𝑄 ‘ 𝑖 ) = 0 )
126 111 124 125 syl2anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 2 ... 𝐼 ) ) → ( 𝑄 ‘ 𝑖 ) = 0 )
127 126 sq0id ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 2 ... 𝐼 ) ) → ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = 0 )
128 127 sumeq2dv ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 2 ... 𝐼 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 2 ... 𝐼 ) 0 )
129 fzfi ⊢ ( 2 ... 𝐼 ) ∈ Fin
130 129 olci ⊢ ( ( 2 ... 𝐼 ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 2 ... 𝐼 ) ∈ Fin )
131 sumz ⊢ ( ( ( 2 ... 𝐼 ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 2 ... 𝐼 ) ∈ Fin ) → Σ 𝑖 ∈ ( 2 ... 𝐼 ) 0 = 0 )
132 130 131 ax-mp ⊢ Σ 𝑖 ∈ ( 2 ... 𝐼 ) 0 = 0
133 128 132 eqtrdi ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 2 ... 𝐼 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = 0 )
134 101 peano2zd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 𝐼 + 1 ) ∈ ℤ )
135 sq1 ⊢ ( 1 ↑ 2 ) = 1
136 26 135 eqtrdi ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = 1 )
137 136 fsum1 ⊢ ( ( ( 𝐼 + 1 ) ∈ ℤ ∧ 1 ∈ ℂ ) → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... ( 𝐼 + 1 ) ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = 1 )
138 134 5 137 sylancl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... ( 𝐼 + 1 ) ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = 1 )
139 oveq2 ⊢ ( ( 𝐼 + 1 ) = 𝑁 → ( ( 𝐼 + 1 ) ... ( 𝐼 + 1 ) ) = ( ( 𝐼 + 1 ) ... 𝑁 ) )
140 139 sumeq1d ⊢ ( ( 𝐼 + 1 ) = 𝑁 → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... ( 𝐼 + 1 ) ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) )
141 140 eqeq1d ⊢ ( ( 𝐼 + 1 ) = 𝑁 → ( Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... ( 𝐼 + 1 ) ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = 1 ↔ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = 1 ) )
142 138 141 syl5ib ⊢ ( ( 𝐼 + 1 ) = 𝑁 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = 1 ) )
143 101 adantl ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 𝐼 ∈ ℤ )
144 143 zred ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 𝐼 ∈ ℝ )
145 60 adantl ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 𝑁 ∈ ℤ )
146 145 zred ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 𝑁 ∈ ℝ )
147 146 94 syl ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑁 − 1 ) ∈ ℝ )
148 97 adantl ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 𝐼 ≤ ( 𝑁 − 1 ) )
149 146 ltm1d ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑁 − 1 ) < 𝑁 )
150 144 147 146 148 149 lelttrd ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 𝐼 < 𝑁 )
151 1red ⊢ ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) → 1 ∈ ℝ )
152 2re ⊢ 2 ∈ ℝ
153 152 a1i ⊢ ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) → 2 ∈ ℝ )
154 1le2 ⊢ 1 ≤ 2
155 154 a1i ⊢ ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) → 1 ≤ 2 )
156 elfzle1 ⊢ ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) → 2 ≤ 𝐼 )
157 151 153 91 155 156 letrd ⊢ ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) → 1 ≤ 𝐼 )
158 157 3ad2ant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 1 ≤ 𝐼 )
159 158 adantl ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 1 ≤ 𝐼 )
160 elnnz1 ⊢ ( 𝐼 ∈ ℕ ↔ ( 𝐼 ∈ ℤ ∧ 1 ≤ 𝐼 ) )
161 143 159 160 sylanbrc ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 𝐼 ∈ ℕ )
162 75 3ad2ant1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℕ )
163 162 adantl ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 𝑁 ∈ ℕ )
164 nnltp1le ⊢ ( ( 𝐼 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐼 < 𝑁 ↔ ( 𝐼 + 1 ) ≤ 𝑁 ) )
165 161 163 164 syl2anc ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → ( 𝐼 < 𝑁 ↔ ( 𝐼 + 1 ) ≤ 𝑁 ) )
166 150 165 mpbid ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → ( 𝐼 + 1 ) ≤ 𝑁 )
167 eluz ⊢ ( ( ( 𝐼 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) ↔ ( 𝐼 + 1 ) ≤ 𝑁 ) )
168 134 145 167 syl2an2 ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) ↔ ( 𝐼 + 1 ) ≤ 𝑁 ) )
169 166 168 mpbird ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) )
170 simpr1 ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
171 simpr3 ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) )
172 170 171 81 syl2anc ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
173 172 adantr ⊢ ( ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ... 𝑁 ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
174 161 peano2nnd ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → ( 𝐼 + 1 ) ∈ ℕ )
175 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
176 174 175 eleqtrdi ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
177 fzss1 ⊢ ( ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( ( 𝐼 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
178 176 177 syl ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → ( ( 𝐼 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
179 178 sselda ⊢ ( ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ... 𝑁 ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
180 173 179 85 syl2anc ⊢ ( ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ... 𝑁 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℂ )
181 180 sqcld ⊢ ( ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ... 𝑁 ) ) → ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ∈ ℂ )
182 23 oveq1d ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) ↑ 2 ) )
183 24 oveq1i ⊢ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) ↑ 2 ) = ( 1 ↑ 2 )
184 183 135 eqtri ⊢ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) ↑ 2 ) = 1
185 182 184 eqtrdi ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = 1 )
186 169 181 185 fsum1p ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = ( 1 + Σ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) )
187 174 peano2nnd ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → ( ( 𝐼 + 1 ) + 1 ) ∈ ℕ )
188 187 175 eleqtrdi ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → ( ( 𝐼 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
189 fzss1 ⊢ ( ( ( 𝐼 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
190 188 189 syl ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
191 190 sselda ⊢ ( ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
192 144 116 syl ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → ( 𝐼 + 1 ) ∈ ℝ )
193 192 adantr ⊢ ( ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ) → ( 𝐼 + 1 ) ∈ ℝ )
194 peano2re ⊢ ( ( 𝐼 + 1 ) ∈ ℝ → ( ( 𝐼 + 1 ) + 1 ) ∈ ℝ )
195 193 194 syl ⊢ ( ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ) → ( ( 𝐼 + 1 ) + 1 ) ∈ ℝ )
196 elfzelz ⊢ ( 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) → 𝑖 ∈ ℤ )
197 196 zred ⊢ ( 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) → 𝑖 ∈ ℝ )
198 197 adantl ⊢ ( ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ) → 𝑖 ∈ ℝ )
199 193 ltp1d ⊢ ( ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ) → ( 𝐼 + 1 ) < ( ( 𝐼 + 1 ) + 1 ) )
200 elfzle1 ⊢ ( 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) → ( ( 𝐼 + 1 ) + 1 ) ≤ 𝑖 )
201 200 adantl ⊢ ( ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ) → ( ( 𝐼 + 1 ) + 1 ) ≤ 𝑖 )
202 193 195 198 199 201 ltletrd ⊢ ( ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ) → ( 𝐼 + 1 ) < 𝑖 )
203 193 202 gtned ⊢ ( ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ) → 𝑖 ≠ ( 𝐼 + 1 ) )
204 191 203 125 syl2anc ⊢ ( ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ) → ( 𝑄 ‘ 𝑖 ) = 0 )
205 204 sq0id ⊢ ( ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) ∧ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ) → ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = 0 )
206 205 sumeq2dv ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → Σ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) 0 )
207 fzfi ⊢ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ∈ Fin
208 207 olci ⊢ ( ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ∈ Fin )
209 sumz ⊢ ( ( ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ∈ Fin ) → Σ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) 0 = 0 )
210 208 209 ax-mp ⊢ Σ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) 0 = 0
211 206 210 eqtrdi ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → Σ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = 0 )
212 211 oveq2d ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → ( 1 + Σ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) = ( 1 + 0 ) )
213 1p0e1 ⊢ ( 1 + 0 ) = 1
214 212 213 eqtrdi ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → ( 1 + Σ 𝑖 ∈ ( ( ( 𝐼 + 1 ) + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) = 1 )
215 186 214 eqtrd ⊢ ( ( ( 𝐼 + 1 ) ≠ 𝑁 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = 1 )
216 215 ex ⊢ ( ( 𝐼 + 1 ) ≠ 𝑁 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = 1 ) )
217 142 216 pm2.61ine ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = 1 )
218 133 217 oveq12d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( Σ 𝑖 ∈ ( 2 ... 𝐼 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) + Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) = ( 0 + 1 ) )
219 0p1e1 ⊢ ( 0 + 1 ) = 1
220 218 219 eqtrdi ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( Σ 𝑖 ∈ ( 2 ... 𝐼 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) + Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) = 1 )
221 89 220 eqtrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 2 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = 1 )
222 simp1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
223 2lt3 ⊢ 2 < 3
224 152 48 223 ltleii ⊢ 2 ≤ 3
225 2z ⊢ 2 ∈ ℤ
226 225 eluz1i ⊢ ( 3 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 3 ∈ ℤ ∧ 2 ≤ 3 ) )
227 4 224 226 mpbir2an ⊢ 3 ∈ ( ℤ≥ ‘ 2 )
228 uztrn ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
229 222 227 228 sylancl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
230 fveq2 ⊢ ( 𝑖 = 2 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 2 ) )
231 230 oveq1d ⊢ ( 𝑖 = 2 → ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = ( ( 𝑄 ‘ 2 ) ↑ 2 ) )
232 229 88 231 fsum1p ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 2 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = ( ( ( 𝑄 ‘ 2 ) ↑ 2 ) + Σ 𝑖 ∈ ( ( 2 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) )
233 59 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → 𝑁 ∈ ℤ )
234 233 zred ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → 𝑁 ∈ ℝ )
235 lttr ⊢ ( ( 2 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 2 < 3 ∧ 3 < 𝑁 ) → 2 < 𝑁 ) )
236 152 48 235 mp3an12 ⊢ ( 𝑁 ∈ ℝ → ( ( 2 < 3 ∧ 3 < 𝑁 ) → 2 < 𝑁 ) )
237 223 236 mpani ⊢ ( 𝑁 ∈ ℝ → ( 3 < 𝑁 → 2 < 𝑁 ) )
238 49 237 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 3 < 𝑁 → 2 < 𝑁 ) )
239 238 imp ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → 2 < 𝑁 )
240 ltle ⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 2 < 𝑁 → 2 ≤ 𝑁 ) )
241 152 240 mpan ⊢ ( 𝑁 ∈ ℝ → ( 2 < 𝑁 → 2 ≤ 𝑁 ) )
242 234 239 241 sylc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → 2 ≤ 𝑁 )
243 242 154 jctil ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → ( 1 ≤ 2 ∧ 2 ≤ 𝑁 ) )
244 1z ⊢ 1 ∈ ℤ
245 elfz ⊢ ( ( 2 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 2 ∧ 2 ≤ 𝑁 ) ) )
246 225 244 233 245 mp3an12i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → ( 2 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 2 ∧ 2 ≤ 𝑁 ) ) )
247 243 246 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → 2 ∈ ( 1 ... 𝑁 ) )
248 247 3adant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 2 ∈ ( 1 ... 𝑁 ) )
249 91 ltp1d ⊢ ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) → 𝐼 < ( 𝐼 + 1 ) )
250 153 91 117 156 249 lelttrd ⊢ ( 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) → 2 < ( 𝐼 + 1 ) )
251 250 3ad2ant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 2 < ( 𝐼 + 1 ) )
252 ltne ⊢ ( ( 2 ∈ ℝ ∧ 2 < ( 𝐼 + 1 ) ) → ( 𝐼 + 1 ) ≠ 2 )
253 152 251 252 sylancr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 𝐼 + 1 ) ≠ 2 )
254 253 necomd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 2 ≠ ( 𝐼 + 1 ) )
255 2 axlowdimlem12 ⊢ ( ( 2 ∈ ( 1 ... 𝑁 ) ∧ 2 ≠ ( 𝐼 + 1 ) ) → ( 𝑄 ‘ 2 ) = 0 )
256 248 254 255 syl2anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 𝑄 ‘ 2 ) = 0 )
257 256 sq0id ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑄 ‘ 2 ) ↑ 2 ) = 0 )
258 257 oveq1d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑄 ‘ 2 ) ↑ 2 ) + Σ 𝑖 ∈ ( ( 2 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) = ( 0 + Σ 𝑖 ∈ ( ( 2 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) )
259 16 oveq1i ⊢ ( 3 ... 𝑁 ) = ( ( 2 + 1 ) ... 𝑁 )
260 259 sumeq1i ⊢ Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( ( 2 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 )
261 260 oveq2i ⊢ ( 0 + Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) = ( 0 + Σ 𝑖 ∈ ( ( 2 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) )
262 258 261 eqtr4di ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑄 ‘ 2 ) ↑ 2 ) + Σ 𝑖 ∈ ( ( 2 + 1 ) ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) = ( 0 + Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) )
263 fzfid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 3 ... 𝑁 ) ∈ Fin )
264 3nn ⊢ 3 ∈ ℕ
265 264 175 eleqtri ⊢ 3 ∈ ( ℤ≥ ‘ 1 )
266 fzss1 ⊢ ( 3 ∈ ( ℤ≥ ‘ 1 ) → ( 3 ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
267 265 266 ax-mp ⊢ ( 3 ... 𝑁 ) ⊆ ( 1 ... 𝑁 )
268 267 sseli ⊢ ( 𝑖 ∈ ( 3 ... 𝑁 ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
269 81 268 85 syl2an ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℂ )
270 269 sqcld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ∈ ℂ )
271 270 3adantl2 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ∈ ℂ )
272 263 271 fsumcl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ∈ ℂ )
273 272 addid2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 0 + Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) = Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) )
274 232 262 273 3eqtrrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 2 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) )
275 simpl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
276 1 axlowdimlem7 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
277 276 ad2antrr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
278 268 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
279 fveecn ⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℂ )
280 277 278 279 syl2anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℂ )
281 280 sqcld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) ∧ 𝑖 ∈ ( 3 ... 𝑁 ) ) → ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) ∈ ℂ )
282 neg1sqe1 ⊢ ( - 1 ↑ 2 ) = 1
283 10 282 eqtrdi ⊢ ( 𝑖 = 3 → ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = 1 )
284 275 281 283 fsum1p ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = ( 1 + Σ 𝑖 ∈ ( ( 3 + 1 ) ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) ) )
285 1re ⊢ 1 ∈ ℝ
286 zaddcl ⊢ ( ( 3 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 3 + 1 ) ∈ ℤ )
287 4 244 286 mp2an ⊢ ( 3 + 1 ) ∈ ℤ
288 287 zrei ⊢ ( 3 + 1 ) ∈ ℝ
289 1lt3 ⊢ 1 < 3
290 48 ltp1i ⊢ 3 < ( 3 + 1 )
291 285 48 288 lttri ⊢ ( ( 1 < 3 ∧ 3 < ( 3 + 1 ) ) → 1 < ( 3 + 1 ) )
292 289 290 291 mp2an ⊢ 1 < ( 3 + 1 )
293 285 288 292 ltleii ⊢ 1 ≤ ( 3 + 1 )
294 eluz ⊢ ( ( 1 ∈ ℤ ∧ ( 3 + 1 ) ∈ ℤ ) → ( ( 3 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ↔ 1 ≤ ( 3 + 1 ) ) )
295 244 287 294 mp2an ⊢ ( ( 3 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ↔ 1 ≤ ( 3 + 1 ) )
296 293 295 mpbir ⊢ ( 3 + 1 ) ∈ ( ℤ≥ ‘ 1 )
297 fzss1 ⊢ ( ( 3 + 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( ( 3 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
298 296 297 ax-mp ⊢ ( ( 3 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 )
299 298 sseli ⊢ ( 𝑖 ∈ ( ( 3 + 1 ) ... 𝑁 ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
300 48 288 ltnlei ⊢ ( 3 < ( 3 + 1 ) ↔ ¬ ( 3 + 1 ) ≤ 3 )
301 290 300 mpbi ⊢ ¬ ( 3 + 1 ) ≤ 3
302 301 intnanr ⊢ ¬ ( ( 3 + 1 ) ≤ 3 ∧ 3 ≤ 𝑁 )
303 elfz ⊢ ( ( 3 ∈ ℤ ∧ ( 3 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 3 ∈ ( ( 3 + 1 ) ... 𝑁 ) ↔ ( ( 3 + 1 ) ≤ 3 ∧ 3 ≤ 𝑁 ) ) )
304 4 287 233 303 mp3an12i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → ( 3 ∈ ( ( 3 + 1 ) ... 𝑁 ) ↔ ( ( 3 + 1 ) ≤ 3 ∧ 3 ≤ 𝑁 ) ) )
305 302 304 mtbiri ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → ¬ 3 ∈ ( ( 3 + 1 ) ... 𝑁 ) )
306 eleq1 ⊢ ( 𝑖 = 3 → ( 𝑖 ∈ ( ( 3 + 1 ) ... 𝑁 ) ↔ 3 ∈ ( ( 3 + 1 ) ... 𝑁 ) ) )
307 306 notbid ⊢ ( 𝑖 = 3 → ( ¬ 𝑖 ∈ ( ( 3 + 1 ) ... 𝑁 ) ↔ ¬ 3 ∈ ( ( 3 + 1 ) ... 𝑁 ) ) )
308 305 307 syl5ibrcom ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → ( 𝑖 = 3 → ¬ 𝑖 ∈ ( ( 3 + 1 ) ... 𝑁 ) ) )
309 308 necon2ad ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → ( 𝑖 ∈ ( ( 3 + 1 ) ... 𝑁 ) → 𝑖 ≠ 3 ) )
310 309 imp ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) ∧ 𝑖 ∈ ( ( 3 + 1 ) ... 𝑁 ) ) → 𝑖 ≠ 3 )
311 1 axlowdimlem9 ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑖 ≠ 3 ) → ( 𝑃 ‘ 𝑖 ) = 0 )
312 299 310 311 syl2an2 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) ∧ 𝑖 ∈ ( ( 3 + 1 ) ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) = 0 )
313 312 sq0id ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) ∧ 𝑖 ∈ ( ( 3 + 1 ) ... 𝑁 ) ) → ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = 0 )
314 313 sumeq2dv ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → Σ 𝑖 ∈ ( ( 3 + 1 ) ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( ( 3 + 1 ) ... 𝑁 ) 0 )
315 fzfi ⊢ ( ( 3 + 1 ) ... 𝑁 ) ∈ Fin
316 315 olci ⊢ ( ( ( 3 + 1 ) ... 𝑁 ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( ( 3 + 1 ) ... 𝑁 ) ∈ Fin )
317 sumz ⊢ ( ( ( ( 3 + 1 ) ... 𝑁 ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( ( 3 + 1 ) ... 𝑁 ) ∈ Fin ) → Σ 𝑖 ∈ ( ( 3 + 1 ) ... 𝑁 ) 0 = 0 )
318 316 317 ax-mp ⊢ Σ 𝑖 ∈ ( ( 3 + 1 ) ... 𝑁 ) 0 = 0
319 314 318 eqtrdi ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → Σ 𝑖 ∈ ( ( 3 + 1 ) ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = 0 )
320 319 oveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → ( 1 + Σ 𝑖 ∈ ( ( 3 + 1 ) ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) ) = ( 1 + 0 ) )
321 284 320 eqtrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = ( 1 + 0 ) )
322 321 213 eqtrdi ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = 1 )
323 322 3adant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = 1 )
324 221 274 323 3eqtr4rd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 3 < 𝑁 ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) )
325 44 54 55 324 syl3anc ⊢ ( ( 𝑁 ≠ 3 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) )
326 325 ex ⊢ ( 𝑁 ≠ 3 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) ) )
327 43 326 pm2.61ine ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐼 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑃 ‘ 𝑖 ) ↑ 2 ) = Σ 𝑖 ∈ ( 3 ... 𝑁 ) ( ( 𝑄 ‘ 𝑖 ) ↑ 2 ) )