| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | uzuzle23 12932 | . . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) | 
| 2 | 1 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → 𝑁 ∈
(ℤ≥‘2)) | 
| 3 |  | fzss2 13605 | . . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → (1...2) ⊆ (1...𝑁)) | 
| 4 | 2, 3 | syl 17 | . . . . . . . . . 10
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (1...2) ⊆
(1...𝑁)) | 
| 5 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → 𝑖 ∈ (1...2)) | 
| 6 | 4, 5 | sseldd 3983 | . . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → 𝑖 ∈ (1...𝑁)) | 
| 7 |  | fznuz 13650 | . . . . . . . . . . 11
⊢ (𝑖 ∈ (1...2) → ¬
𝑖 ∈
(ℤ≥‘(2 + 1))) | 
| 8 | 7 | adantl 481 | . . . . . . . . . 10
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → ¬ 𝑖 ∈
(ℤ≥‘(2 + 1))) | 
| 9 |  | 3z 12652 | . . . . . . . . . . . . . 14
⊢ 3 ∈
ℤ | 
| 10 |  | uzid 12894 | . . . . . . . . . . . . . 14
⊢ (3 ∈
ℤ → 3 ∈ (ℤ≥‘3)) | 
| 11 | 9, 10 | ax-mp 5 | . . . . . . . . . . . . 13
⊢ 3 ∈
(ℤ≥‘3) | 
| 12 |  | df-3 12331 | . . . . . . . . . . . . . 14
⊢ 3 = (2 +
1) | 
| 13 | 12 | fveq2i 6908 | . . . . . . . . . . . . 13
⊢
(ℤ≥‘3) = (ℤ≥‘(2 +
1)) | 
| 14 | 11, 13 | eleqtri 2838 | . . . . . . . . . . . 12
⊢ 3 ∈
(ℤ≥‘(2 + 1)) | 
| 15 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢ (𝑖 = 3 → (𝑖 ∈ (ℤ≥‘(2 +
1)) ↔ 3 ∈ (ℤ≥‘(2 + 1)))) | 
| 16 | 14, 15 | mpbiri 258 | . . . . . . . . . . 11
⊢ (𝑖 = 3 → 𝑖 ∈ (ℤ≥‘(2 +
1))) | 
| 17 | 16 | necon3bi 2966 | . . . . . . . . . 10
⊢ (¬
𝑖 ∈
(ℤ≥‘(2 + 1)) → 𝑖 ≠ 3) | 
| 18 | 8, 17 | syl 17 | . . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → 𝑖 ≠ 3) | 
| 19 |  | axlowdimlem16.1 | . . . . . . . . . 10
⊢ 𝑃 = ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})) | 
| 20 | 19 | axlowdimlem9 28966 | . . . . . . . . 9
⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑖 ≠ 3) → (𝑃‘𝑖) = 0) | 
| 21 | 6, 18, 20 | syl2anc 584 | . . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (𝑃‘𝑖) = 0) | 
| 22 |  | elfzuz 13561 | . . . . . . . . . . . . . 14
⊢ (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ∈
(ℤ≥‘2)) | 
| 23 | 22 | ad2antlr 727 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → 𝐼 ∈
(ℤ≥‘2)) | 
| 24 |  | eluzp1p1 12907 | . . . . . . . . . . . . 13
⊢ (𝐼 ∈
(ℤ≥‘2) → (𝐼 + 1) ∈
(ℤ≥‘(2 + 1))) | 
| 25 | 23, 24 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (𝐼 + 1) ∈
(ℤ≥‘(2 + 1))) | 
| 26 |  | uzss 12902 | . . . . . . . . . . . 12
⊢ ((𝐼 + 1) ∈
(ℤ≥‘(2 + 1)) →
(ℤ≥‘(𝐼 + 1)) ⊆
(ℤ≥‘(2 + 1))) | 
| 27 | 25, 26 | syl 17 | . . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) →
(ℤ≥‘(𝐼 + 1)) ⊆
(ℤ≥‘(2 + 1))) | 
| 28 | 27, 8 | ssneldd 3985 | . . . . . . . . . 10
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → ¬ 𝑖 ∈
(ℤ≥‘(𝐼 + 1))) | 
| 29 |  | eluzelz 12889 | . . . . . . . . . . . . . 14
⊢ ((𝐼 + 1) ∈
(ℤ≥‘(2 + 1)) → (𝐼 + 1) ∈ ℤ) | 
| 30 | 25, 29 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (𝐼 + 1) ∈ ℤ) | 
| 31 |  | uzid 12894 | . . . . . . . . . . . . 13
⊢ ((𝐼 + 1) ∈ ℤ →
(𝐼 + 1) ∈
(ℤ≥‘(𝐼 + 1))) | 
| 32 | 30, 31 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (𝐼 + 1) ∈
(ℤ≥‘(𝐼 + 1))) | 
| 33 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢ (𝑖 = (𝐼 + 1) → (𝑖 ∈ (ℤ≥‘(𝐼 + 1)) ↔ (𝐼 + 1) ∈
(ℤ≥‘(𝐼 + 1)))) | 
| 34 | 32, 33 | syl5ibrcom 247 | . . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (𝑖 = (𝐼 + 1) → 𝑖 ∈ (ℤ≥‘(𝐼 + 1)))) | 
| 35 | 34 | necon3bd 2953 | . . . . . . . . . 10
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (¬ 𝑖 ∈
(ℤ≥‘(𝐼 + 1)) → 𝑖 ≠ (𝐼 + 1))) | 
| 36 | 28, 35 | mpd 15 | . . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → 𝑖 ≠ (𝐼 + 1)) | 
| 37 |  | axlowdimlem16.2 | . . . . . . . . . 10
⊢ 𝑄 = ({〈(𝐼 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0})) | 
| 38 | 37 | axlowdimlem12 28969 | . . . . . . . . 9
⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑖 ≠ (𝐼 + 1)) → (𝑄‘𝑖) = 0) | 
| 39 | 6, 36, 38 | syl2anc 584 | . . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (𝑄‘𝑖) = 0) | 
| 40 | 21, 39 | eqtr4d 2779 | . . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (𝑃‘𝑖) = (𝑄‘𝑖)) | 
| 41 | 40 | oveq1d 7447 | . . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → ((𝑃‘𝑖) − (𝐴‘𝑖)) = ((𝑄‘𝑖) − (𝐴‘𝑖))) | 
| 42 | 41 | oveq1d 7447 | . . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = (((𝑄‘𝑖) − (𝐴‘𝑖))↑2)) | 
| 43 | 42 | sumeq2dv 15739 | . . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (1...2)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = Σ𝑖 ∈ (1...2)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2)) | 
| 44 | 19, 37 | axlowdimlem16 28973 | . . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2)) | 
| 45 |  | axlowdimlem17.3 | . . . . . . . . . . . . 13
⊢ 𝐴 = ({〈1, 𝑋〉, 〈2, 𝑌〉} ∪ ((3...𝑁) × {0})) | 
| 46 | 45 | fveq1i 6906 | . . . . . . . . . . . 12
⊢ (𝐴‘𝑖) = (({〈1, 𝑋〉, 〈2, 𝑌〉} ∪ ((3...𝑁) × {0}))‘𝑖) | 
| 47 |  | axlowdimlem2 28959 | . . . . . . . . . . . . 13
⊢ ((1...2)
∩ (3...𝑁)) =
∅ | 
| 48 |  | axlowdimlem17.4 | . . . . . . . . . . . . . . . 16
⊢ 𝑋 ∈ ℝ | 
| 49 |  | axlowdimlem17.5 | . . . . . . . . . . . . . . . 16
⊢ 𝑌 ∈ ℝ | 
| 50 | 48, 49 | axlowdimlem4 28961 | . . . . . . . . . . . . . . 15
⊢ {〈1,
𝑋〉, 〈2, 𝑌〉}:(1...2)⟶ℝ | 
| 51 |  | ffn 6735 | . . . . . . . . . . . . . . 15
⊢
({〈1, 𝑋〉,
〈2, 𝑌〉}:(1...2)⟶ℝ →
{〈1, 𝑋〉, 〈2,
𝑌〉} Fn
(1...2)) | 
| 52 | 50, 51 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢ {〈1,
𝑋〉, 〈2, 𝑌〉} Fn
(1...2) | 
| 53 |  | axlowdimlem1 28958 | . . . . . . . . . . . . . . 15
⊢
((3...𝑁) ×
{0}):(3...𝑁)⟶ℝ | 
| 54 |  | ffn 6735 | . . . . . . . . . . . . . . 15
⊢
(((3...𝑁) ×
{0}):(3...𝑁)⟶ℝ
→ ((3...𝑁) ×
{0}) Fn (3...𝑁)) | 
| 55 | 53, 54 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢
((3...𝑁) ×
{0}) Fn (3...𝑁) | 
| 56 |  | fvun2 7000 | . . . . . . . . . . . . . 14
⊢
(({〈1, 𝑋〉,
〈2, 𝑌〉} Fn
(1...2) ∧ ((3...𝑁)
× {0}) Fn (3...𝑁)
∧ (((1...2) ∩ (3...𝑁)) = ∅ ∧ 𝑖 ∈ (3...𝑁))) → (({〈1, 𝑋〉, 〈2, 𝑌〉} ∪ ((3...𝑁) × {0}))‘𝑖) = (((3...𝑁) × {0})‘𝑖)) | 
| 57 | 52, 55, 56 | mp3an12 1452 | . . . . . . . . . . . . 13
⊢
((((1...2) ∩ (3...𝑁)) = ∅ ∧ 𝑖 ∈ (3...𝑁)) → (({〈1, 𝑋〉, 〈2, 𝑌〉} ∪ ((3...𝑁) × {0}))‘𝑖) = (((3...𝑁) × {0})‘𝑖)) | 
| 58 | 47, 57 | mpan 690 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ (3...𝑁) → (({〈1, 𝑋〉, 〈2, 𝑌〉} ∪ ((3...𝑁) × {0}))‘𝑖) = (((3...𝑁) × {0})‘𝑖)) | 
| 59 | 46, 58 | eqtrid 2788 | . . . . . . . . . . 11
⊢ (𝑖 ∈ (3...𝑁) → (𝐴‘𝑖) = (((3...𝑁) × {0})‘𝑖)) | 
| 60 |  | c0ex 11256 | . . . . . . . . . . . 12
⊢ 0 ∈
V | 
| 61 | 60 | fvconst2 7225 | . . . . . . . . . . 11
⊢ (𝑖 ∈ (3...𝑁) → (((3...𝑁) × {0})‘𝑖) = 0) | 
| 62 | 59, 61 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝑖 ∈ (3...𝑁) → (𝐴‘𝑖) = 0) | 
| 63 | 62 | adantl 481 | . . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → (𝐴‘𝑖) = 0) | 
| 64 | 63 | oveq2d 7448 | . . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑃‘𝑖) − (𝐴‘𝑖)) = ((𝑃‘𝑖) − 0)) | 
| 65 | 19 | axlowdimlem7 28964 | . . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑃 ∈ (𝔼‘𝑁)) | 
| 66 | 65 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → 𝑃 ∈ (𝔼‘𝑁)) | 
| 67 |  | 3nn 12346 | . . . . . . . . . . . . . 14
⊢ 3 ∈
ℕ | 
| 68 |  | nnuz 12922 | . . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) | 
| 69 | 67, 68 | eleqtri 2838 | . . . . . . . . . . . . 13
⊢ 3 ∈
(ℤ≥‘1) | 
| 70 |  | fzss1 13604 | . . . . . . . . . . . . 13
⊢ (3 ∈
(ℤ≥‘1) → (3...𝑁) ⊆ (1...𝑁)) | 
| 71 | 69, 70 | ax-mp 5 | . . . . . . . . . . . 12
⊢
(3...𝑁) ⊆
(1...𝑁) | 
| 72 | 71 | sseli 3978 | . . . . . . . . . . 11
⊢ (𝑖 ∈ (3...𝑁) → 𝑖 ∈ (1...𝑁)) | 
| 73 | 72 | adantl 481 | . . . . . . . . . 10
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → 𝑖 ∈ (1...𝑁)) | 
| 74 |  | fveecn 28918 | . . . . . . . . . 10
⊢ ((𝑃 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑃‘𝑖) ∈ ℂ) | 
| 75 | 66, 73, 74 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → (𝑃‘𝑖) ∈ ℂ) | 
| 76 | 75 | subid1d 11610 | . . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑃‘𝑖) − 0) = (𝑃‘𝑖)) | 
| 77 | 64, 76 | eqtrd 2776 | . . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑃‘𝑖) − (𝐴‘𝑖)) = (𝑃‘𝑖)) | 
| 78 | 77 | oveq1d 7447 | . . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → (((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = ((𝑃‘𝑖)↑2)) | 
| 79 | 78 | sumeq2dv 15739 | . . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2)) | 
| 80 | 63 | oveq2d 7448 | . . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑄‘𝑖) − (𝐴‘𝑖)) = ((𝑄‘𝑖) − 0)) | 
| 81 |  | eluzge3nn 12933 | . . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℕ) | 
| 82 |  | 2eluzge1 12937 | . . . . . . . . . . . . 13
⊢ 2 ∈
(ℤ≥‘1) | 
| 83 |  | fzss1 13604 | . . . . . . . . . . . . 13
⊢ (2 ∈
(ℤ≥‘1) → (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1))) | 
| 84 | 82, 83 | ax-mp 5 | . . . . . . . . . . . 12
⊢
(2...(𝑁 − 1))
⊆ (1...(𝑁 −
1)) | 
| 85 | 84 | sseli 3978 | . . . . . . . . . . 11
⊢ (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ∈ (1...(𝑁 − 1))) | 
| 86 | 37 | axlowdimlem10 28967 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 𝑄 ∈ (𝔼‘𝑁)) | 
| 87 | 81, 85, 86 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑄 ∈ (𝔼‘𝑁)) | 
| 88 |  | fveecn 28918 | . . . . . . . . . 10
⊢ ((𝑄 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑄‘𝑖) ∈ ℂ) | 
| 89 | 87, 72, 88 | syl2an 596 | . . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → (𝑄‘𝑖) ∈ ℂ) | 
| 90 | 89 | subid1d 11610 | . . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑄‘𝑖) − 0) = (𝑄‘𝑖)) | 
| 91 | 80, 90 | eqtrd 2776 | . . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑄‘𝑖) − (𝐴‘𝑖)) = (𝑄‘𝑖)) | 
| 92 | 91 | oveq1d 7447 | . . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → (((𝑄‘𝑖) − (𝐴‘𝑖))↑2) = ((𝑄‘𝑖)↑2)) | 
| 93 | 92 | sumeq2dv 15739 | . . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2)) | 
| 94 | 44, 79, 93 | 3eqtr4d 2786 | . . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = Σ𝑖 ∈ (3...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2)) | 
| 95 | 43, 94 | oveq12d 7450 | . . 3
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (Σ𝑖 ∈ (1...2)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) + Σ𝑖 ∈ (3...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2)) = (Σ𝑖 ∈ (1...2)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2) + Σ𝑖 ∈ (3...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2))) | 
| 96 | 47 | a1i 11 | . . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → ((1...2) ∩
(3...𝑁)) =
∅) | 
| 97 |  | eluzelre 12890 | . . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℝ) | 
| 98 |  | eluzle 12892 | . . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ≤ 𝑁) | 
| 99 |  | 2re 12341 | . . . . . . . . . . . 12
⊢ 2 ∈
ℝ | 
| 100 |  | 3re 12347 | . . . . . . . . . . . 12
⊢ 3 ∈
ℝ | 
| 101 |  | 2lt3 12439 | . . . . . . . . . . . 12
⊢ 2 <
3 | 
| 102 | 99, 100, 101 | ltleii 11385 | . . . . . . . . . . 11
⊢ 2 ≤
3 | 
| 103 |  | letr 11356 | . . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((2 ≤ 3 ∧ 3
≤ 𝑁) → 2 ≤ 𝑁)) | 
| 104 | 99, 100, 103 | mp3an12 1452 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ → ((2 ≤
3 ∧ 3 ≤ 𝑁) → 2
≤ 𝑁)) | 
| 105 | 102, 104 | mpani 696 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℝ → (3 ≤
𝑁 → 2 ≤ 𝑁)) | 
| 106 | 97, 98, 105 | sylc 65 | . . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ≤ 𝑁) | 
| 107 |  | 1le2 12476 | . . . . . . . . 9
⊢ 1 ≤
2 | 
| 108 | 106, 107 | jctil 519 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘3) → (1 ≤ 2 ∧ 2 ≤ 𝑁)) | 
| 109 | 108 | adantr 480 | . . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (1 ≤ 2 ∧ 2 ≤
𝑁)) | 
| 110 |  | eluzelz 12889 | . . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) | 
| 111 | 110 | adantr 480 | . . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℤ) | 
| 112 |  | 2z 12651 | . . . . . . . . 9
⊢ 2 ∈
ℤ | 
| 113 |  | 1z 12649 | . . . . . . . . 9
⊢ 1 ∈
ℤ | 
| 114 |  | elfz 13554 | . . . . . . . . 9
⊢ ((2
∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 ∈ (1...𝑁) ↔ (1 ≤ 2 ∧ 2 ≤
𝑁))) | 
| 115 | 112, 113,
114 | mp3an12 1452 | . . . . . . . 8
⊢ (𝑁 ∈ ℤ → (2 ∈
(1...𝑁) ↔ (1 ≤ 2
∧ 2 ≤ 𝑁))) | 
| 116 | 111, 115 | syl 17 | . . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (2 ∈ (1...𝑁) ↔ (1 ≤ 2 ∧ 2 ≤
𝑁))) | 
| 117 | 109, 116 | mpbird 257 | . . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 2 ∈ (1...𝑁)) | 
| 118 |  | fzsplit 13591 | . . . . . 6
⊢ (2 ∈
(1...𝑁) → (1...𝑁) = ((1...2) ∪ ((2 +
1)...𝑁))) | 
| 119 | 117, 118 | syl 17 | . . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (1...𝑁) = ((1...2) ∪ ((2 + 1)...𝑁))) | 
| 120 | 12 | oveq1i 7442 | . . . . . 6
⊢
(3...𝑁) = ((2 +
1)...𝑁) | 
| 121 | 120 | uneq2i 4164 | . . . . 5
⊢ ((1...2)
∪ (3...𝑁)) = ((1...2)
∪ ((2 + 1)...𝑁)) | 
| 122 | 119, 121 | eqtr4di 2794 | . . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (1...𝑁) = ((1...2) ∪ (3...𝑁))) | 
| 123 |  | fzfid 14015 | . . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (1...𝑁) ∈ Fin) | 
| 124 | 65 | ad2antrr 726 | . . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑃 ∈ (𝔼‘𝑁)) | 
| 125 | 124, 74 | sylancom 588 | . . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑃‘𝑖) ∈ ℂ) | 
| 126 | 48, 49 | axlowdimlem5 28962 | . . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → ({〈1, 𝑋〉, 〈2, 𝑌〉} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁)) | 
| 127 | 45, 126 | eqeltrid 2844 | . . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝐴 ∈ (𝔼‘𝑁)) | 
| 128 | 1, 127 | syl 17 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝐴 ∈ (𝔼‘𝑁)) | 
| 129 | 128 | ad2antrr 726 | . . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → 𝐴 ∈ (𝔼‘𝑁)) | 
| 130 |  | fveecn 28918 | . . . . . . 7
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ) | 
| 131 | 129, 130 | sylancom 588 | . . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ) | 
| 132 | 125, 131 | subcld 11621 | . . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑃‘𝑖) − (𝐴‘𝑖)) ∈ ℂ) | 
| 133 | 132 | sqcld 14185 | . . . 4
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑃‘𝑖) − (𝐴‘𝑖))↑2) ∈ ℂ) | 
| 134 | 96, 122, 123, 133 | fsumsplit 15778 | . . 3
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (1...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = (Σ𝑖 ∈ (1...2)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) + Σ𝑖 ∈ (3...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2))) | 
| 135 | 87, 88 | sylan 580 | . . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑄‘𝑖) ∈ ℂ) | 
| 136 | 135, 131 | subcld 11621 | . . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑄‘𝑖) − (𝐴‘𝑖)) ∈ ℂ) | 
| 137 | 136 | sqcld 14185 | . . . 4
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑄‘𝑖) − (𝐴‘𝑖))↑2) ∈ ℂ) | 
| 138 | 96, 122, 123, 137 | fsumsplit 15778 | . . 3
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (1...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2) = (Σ𝑖 ∈ (1...2)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2) + Σ𝑖 ∈ (3...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2))) | 
| 139 | 95, 134, 138 | 3eqtr4d 2786 | . 2
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (1...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2)) | 
| 140 | 65 | adantr 480 | . . 3
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑃 ∈ (𝔼‘𝑁)) | 
| 141 | 128 | adantr 480 | . . 3
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝐴 ∈ (𝔼‘𝑁)) | 
| 142 |  | brcgr 28916 | . . 3
⊢ (((𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁))) → (〈𝑃, 𝐴〉Cgr〈𝑄, 𝐴〉 ↔ Σ𝑖 ∈ (1...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2))) | 
| 143 | 140, 141,
87, 141, 142 | syl22anc 838 | . 2
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (〈𝑃, 𝐴〉Cgr〈𝑄, 𝐴〉 ↔ Σ𝑖 ∈ (1...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2))) | 
| 144 | 139, 143 | mpbird 257 | 1
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 〈𝑃, 𝐴〉Cgr〈𝑄, 𝐴〉) |