Proof of Theorem axlowdimlem16
Step | Hyp | Ref
| Expression |
1 | | elfz1eq 13136 |
. . . . . 6
⊢ (𝐼 ∈ (2...2) → 𝐼 = 2) |
2 | | 3z 12223 |
. . . . . . . 8
⊢ 3 ∈
ℤ |
3 | | ax-1cn 10800 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
4 | 3 | sqcli 13763 |
. . . . . . . 8
⊢
(1↑2) ∈ ℂ |
5 | | fveq2 6726 |
. . . . . . . . . . . 12
⊢ (𝑖 = 3 → (𝑃‘𝑖) = (𝑃‘3)) |
6 | | axlowdimlem16.1 |
. . . . . . . . . . . . 13
⊢ 𝑃 = ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})) |
7 | 6 | axlowdimlem8 27053 |
. . . . . . . . . . . 12
⊢ (𝑃‘3) = -1 |
8 | 5, 7 | eqtrdi 2795 |
. . . . . . . . . . 11
⊢ (𝑖 = 3 → (𝑃‘𝑖) = -1) |
9 | 8 | oveq1d 7237 |
. . . . . . . . . 10
⊢ (𝑖 = 3 → ((𝑃‘𝑖)↑2) = (-1↑2)) |
10 | | sqneg 13701 |
. . . . . . . . . . 11
⊢ (1 ∈
ℂ → (-1↑2) = (1↑2)) |
11 | 3, 10 | ax-mp 5 |
. . . . . . . . . 10
⊢
(-1↑2) = (1↑2) |
12 | 9, 11 | eqtrdi 2795 |
. . . . . . . . 9
⊢ (𝑖 = 3 → ((𝑃‘𝑖)↑2) = (1↑2)) |
13 | 12 | fsum1 15324 |
. . . . . . . 8
⊢ ((3
∈ ℤ ∧ (1↑2) ∈ ℂ) → Σ𝑖 ∈ (3...3)((𝑃‘𝑖)↑2) = (1↑2)) |
14 | 2, 4, 13 | mp2an 692 |
. . . . . . 7
⊢
Σ𝑖 ∈
(3...3)((𝑃‘𝑖)↑2) =
(1↑2) |
15 | | df-3 11907 |
. . . . . . . . . . 11
⊢ 3 = (2 +
1) |
16 | | oveq1 7229 |
. . . . . . . . . . 11
⊢ (𝐼 = 2 → (𝐼 + 1) = (2 + 1)) |
17 | 15, 16 | eqtr4id 2798 |
. . . . . . . . . 10
⊢ (𝐼 = 2 → 3 = (𝐼 + 1)) |
18 | 17, 17 | oveq12d 7240 |
. . . . . . . . 9
⊢ (𝐼 = 2 → (3...3) = ((𝐼 + 1)...(𝐼 + 1))) |
19 | 18 | sumeq1d 15278 |
. . . . . . . 8
⊢ (𝐼 = 2 → Σ𝑖 ∈ (3...3)((𝑄‘𝑖)↑2) = Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄‘𝑖)↑2)) |
20 | 16, 15 | eqtr4di 2797 |
. . . . . . . . . 10
⊢ (𝐼 = 2 → (𝐼 + 1) = 3) |
21 | 20, 2 | eqeltrdi 2847 |
. . . . . . . . 9
⊢ (𝐼 = 2 → (𝐼 + 1) ∈ ℤ) |
22 | | fveq2 6726 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝐼 + 1) → (𝑄‘𝑖) = (𝑄‘(𝐼 + 1))) |
23 | | axlowdimlem16.2 |
. . . . . . . . . . . . 13
⊢ 𝑄 = ({〈(𝐼 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0})) |
24 | 23 | axlowdimlem11 27056 |
. . . . . . . . . . . 12
⊢ (𝑄‘(𝐼 + 1)) = 1 |
25 | 22, 24 | eqtrdi 2795 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝐼 + 1) → (𝑄‘𝑖) = 1) |
26 | 25 | oveq1d 7237 |
. . . . . . . . . 10
⊢ (𝑖 = (𝐼 + 1) → ((𝑄‘𝑖)↑2) = (1↑2)) |
27 | 26 | fsum1 15324 |
. . . . . . . . 9
⊢ (((𝐼 + 1) ∈ ℤ ∧
(1↑2) ∈ ℂ) → Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄‘𝑖)↑2) = (1↑2)) |
28 | 21, 4, 27 | sylancl 589 |
. . . . . . . 8
⊢ (𝐼 = 2 → Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄‘𝑖)↑2) = (1↑2)) |
29 | 19, 28 | eqtrd 2778 |
. . . . . . 7
⊢ (𝐼 = 2 → Σ𝑖 ∈ (3...3)((𝑄‘𝑖)↑2) = (1↑2)) |
30 | 14, 29 | eqtr4id 2798 |
. . . . . 6
⊢ (𝐼 = 2 → Σ𝑖 ∈ (3...3)((𝑃‘𝑖)↑2) = Σ𝑖 ∈ (3...3)((𝑄‘𝑖)↑2)) |
31 | 1, 30 | syl 17 |
. . . . 5
⊢ (𝐼 ∈ (2...2) →
Σ𝑖 ∈
(3...3)((𝑃‘𝑖)↑2) = Σ𝑖 ∈ (3...3)((𝑄‘𝑖)↑2)) |
32 | 31 | a1i 11 |
. . . 4
⊢ (𝑁 = 3 → (𝐼 ∈ (2...2) → Σ𝑖 ∈ (3...3)((𝑃‘𝑖)↑2) = Σ𝑖 ∈ (3...3)((𝑄‘𝑖)↑2))) |
33 | | oveq1 7229 |
. . . . . . 7
⊢ (𝑁 = 3 → (𝑁 − 1) = (3 −
1)) |
34 | | 3m1e2 11971 |
. . . . . . 7
⊢ (3
− 1) = 2 |
35 | 33, 34 | eqtrdi 2795 |
. . . . . 6
⊢ (𝑁 = 3 → (𝑁 − 1) = 2) |
36 | 35 | oveq2d 7238 |
. . . . 5
⊢ (𝑁 = 3 → (2...(𝑁 − 1)) =
(2...2)) |
37 | 36 | eleq2d 2824 |
. . . 4
⊢ (𝑁 = 3 → (𝐼 ∈ (2...(𝑁 − 1)) ↔ 𝐼 ∈ (2...2))) |
38 | | oveq2 7230 |
. . . . . 6
⊢ (𝑁 = 3 → (3...𝑁) = (3...3)) |
39 | 38 | sumeq1d 15278 |
. . . . 5
⊢ (𝑁 = 3 → Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2) = Σ𝑖 ∈ (3...3)((𝑃‘𝑖)↑2)) |
40 | 38 | sumeq1d 15278 |
. . . . 5
⊢ (𝑁 = 3 → Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2) = Σ𝑖 ∈ (3...3)((𝑄‘𝑖)↑2)) |
41 | 39, 40 | eqeq12d 2754 |
. . . 4
⊢ (𝑁 = 3 → (Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2) ↔ Σ𝑖 ∈ (3...3)((𝑃‘𝑖)↑2) = Σ𝑖 ∈ (3...3)((𝑄‘𝑖)↑2))) |
42 | 32, 37, 41 | 3imtr4d 297 |
. . 3
⊢ (𝑁 = 3 → (𝐼 ∈ (2...(𝑁 − 1)) → Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2))) |
43 | 42 | adantld 494 |
. 2
⊢ (𝑁 = 3 → ((𝑁 ∈ (ℤ≥‘3)
∧ 𝐼 ∈ (2...(𝑁 − 1))) →
Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2))) |
44 | | simprl 771 |
. . . 4
⊢ ((𝑁 ≠ 3 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈
(ℤ≥‘3)) |
45 | | eluzle 12464 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ≤ 𝑁) |
46 | 45 | adantl 485 |
. . . . . 6
⊢ ((𝑁 ≠ 3 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 3 ≤ 𝑁) |
47 | | simpl 486 |
. . . . . 6
⊢ ((𝑁 ≠ 3 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑁 ≠
3) |
48 | | 3re 11923 |
. . . . . . 7
⊢ 3 ∈
ℝ |
49 | | eluzelre 12462 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℝ) |
50 | 49 | adantl 485 |
. . . . . . 7
⊢ ((𝑁 ≠ 3 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑁 ∈
ℝ) |
51 | | ltlen 10946 |
. . . . . . 7
⊢ ((3
∈ ℝ ∧ 𝑁
∈ ℝ) → (3 < 𝑁 ↔ (3 ≤ 𝑁 ∧ 𝑁 ≠ 3))) |
52 | 48, 50, 51 | sylancr 590 |
. . . . . 6
⊢ ((𝑁 ≠ 3 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (3 < 𝑁 ↔ (3
≤ 𝑁 ∧ 𝑁 ≠ 3))) |
53 | 46, 47, 52 | mpbir2and 713 |
. . . . 5
⊢ ((𝑁 ≠ 3 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 3 < 𝑁) |
54 | 53 | adantrr 717 |
. . . 4
⊢ ((𝑁 ≠ 3 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 3 <
𝑁) |
55 | | simprr 773 |
. . . 4
⊢ ((𝑁 ≠ 3 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ∈ (2...(𝑁 − 1))) |
56 | | fzssp1 13168 |
. . . . . . . . . . . . 13
⊢
(2...(𝑁 − 1))
⊆ (2...((𝑁 − 1)
+ 1)) |
57 | | simp3 1140 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ (2...(𝑁 − 1))) |
58 | 56, 57 | sselid 3907 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ (2...((𝑁 − 1) + 1))) |
59 | | eluzelz 12461 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) |
60 | 59 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℤ) |
61 | 60 | zcnd 12296 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℂ) |
62 | | npcan 11100 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
63 | 61, 3, 62 | sylancl 589 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁) |
64 | 63 | oveq2d 7238 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (2...((𝑁 − 1) + 1)) = (2...𝑁)) |
65 | 58, 64 | eleqtrd 2841 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ (2...𝑁)) |
66 | | elfzelz 13125 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (2...𝑁) → 𝐼 ∈ ℤ) |
67 | 65, 66 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ ℤ) |
68 | 67 | zred 12295 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ ℝ) |
69 | 68 | ltp1d 11775 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 < (𝐼 + 1)) |
70 | | fzdisj 13152 |
. . . . . . . 8
⊢ (𝐼 < (𝐼 + 1) → ((2...𝐼) ∩ ((𝐼 + 1)...𝑁)) = ∅) |
71 | 69, 70 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → ((2...𝐼) ∩ ((𝐼 + 1)...𝑁)) = ∅) |
72 | | fzsplit 13151 |
. . . . . . . 8
⊢ (𝐼 ∈ (2...𝑁) → (2...𝑁) = ((2...𝐼) ∪ ((𝐼 + 1)...𝑁))) |
73 | 65, 72 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (2...𝑁) = ((2...𝐼) ∪ ((𝐼 + 1)...𝑁))) |
74 | | fzfid 13559 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (2...𝑁) ∈ Fin) |
75 | | eluzge3nn 12499 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℕ) |
76 | | 2eluzge1 12503 |
. . . . . . . . . . . . 13
⊢ 2 ∈
(ℤ≥‘1) |
77 | | fzss1 13164 |
. . . . . . . . . . . . 13
⊢ (2 ∈
(ℤ≥‘1) → (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1))) |
78 | 76, 77 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(2...(𝑁 − 1))
⊆ (1...(𝑁 −
1)) |
79 | 78 | sseli 3905 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ∈ (1...(𝑁 − 1))) |
80 | 23 | axlowdimlem10 27055 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 𝑄 ∈ (𝔼‘𝑁)) |
81 | 75, 79, 80 | syl2an 599 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑄 ∈ (𝔼‘𝑁)) |
82 | | fzss1 13164 |
. . . . . . . . . . . 12
⊢ (2 ∈
(ℤ≥‘1) → (2...𝑁) ⊆ (1...𝑁)) |
83 | 76, 82 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(2...𝑁) ⊆
(1...𝑁) |
84 | 83 | sseli 3905 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (2...𝑁) → 𝑖 ∈ (1...𝑁)) |
85 | | fveecn 27006 |
. . . . . . . . . 10
⊢ ((𝑄 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑄‘𝑖) ∈ ℂ) |
86 | 81, 84, 85 | syl2an 599 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝑁)) → (𝑄‘𝑖) ∈ ℂ) |
87 | 86 | sqcld 13727 |
. . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝑁)) → ((𝑄‘𝑖)↑2) ∈ ℂ) |
88 | 87 | 3adantl2 1169 |
. . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝑁)) → ((𝑄‘𝑖)↑2) ∈ ℂ) |
89 | 71, 73, 74, 88 | fsumsplit 15318 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (2...𝑁)((𝑄‘𝑖)↑2) = (Σ𝑖 ∈ (2...𝐼)((𝑄‘𝑖)↑2) + Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄‘𝑖)↑2))) |
90 | | elfzelz 13125 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ∈ ℤ) |
91 | 90 | zred 12295 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ∈ ℝ) |
92 | 91 | 3ad2ant3 1137 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ ℝ) |
93 | 49 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℝ) |
94 | | peano2rem 11158 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ) |
96 | | elfzle2 13129 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ≤ (𝑁 − 1)) |
97 | 96 | 3ad2ant3 1137 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ≤ (𝑁 − 1)) |
98 | 93 | ltm1d 11777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (𝑁 − 1) < 𝑁) |
99 | 92, 95, 93, 97, 98 | lelttrd 11003 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 < 𝑁) |
100 | 92, 93, 99 | ltled 10993 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ≤ 𝑁) |
101 | 90 | 3ad2ant3 1137 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ ℤ) |
102 | | eluz 12465 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘𝐼) ↔ 𝐼 ≤ 𝑁)) |
103 | 101, 60, 102 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (𝑁 ∈ (ℤ≥‘𝐼) ↔ 𝐼 ≤ 𝑁)) |
104 | 100, 103 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ (ℤ≥‘𝐼)) |
105 | | fzss2 13165 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘𝐼) → (1...𝐼) ⊆ (1...𝑁)) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (1...𝐼) ⊆ (1...𝑁)) |
107 | 106 | sseld 3909 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (𝑖 ∈ (1...𝐼) → 𝑖 ∈ (1...𝑁))) |
108 | | fzss1 13164 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
(ℤ≥‘1) → (2...𝐼) ⊆ (1...𝐼)) |
109 | 76, 108 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(2...𝐼) ⊆
(1...𝐼) |
110 | 109 | sseli 3905 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (2...𝐼) → 𝑖 ∈ (1...𝐼)) |
111 | 107, 110 | impel 509 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝑖 ∈ (1...𝑁)) |
112 | | elfzelz 13125 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (2...𝐼) → 𝑖 ∈ ℤ) |
113 | 112 | zred 12295 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (2...𝐼) → 𝑖 ∈ ℝ) |
114 | 113 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝑖 ∈ ℝ) |
115 | 92 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝐼 ∈ ℝ) |
116 | | peano2re 11018 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ ℝ → (𝐼 + 1) ∈
ℝ) |
117 | 91, 116 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ (2...(𝑁 − 1)) → (𝐼 + 1) ∈ ℝ) |
118 | 117 | 3ad2ant3 1137 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (𝐼 + 1) ∈ ℝ) |
119 | 118 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → (𝐼 + 1) ∈ ℝ) |
120 | | elfzle2 13129 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (2...𝐼) → 𝑖 ≤ 𝐼) |
121 | 120 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝑖 ≤ 𝐼) |
122 | 115 | ltp1d 11775 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝐼 < (𝐼 + 1)) |
123 | 114, 115,
119, 121, 122 | lelttrd 11003 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝑖 < (𝐼 + 1)) |
124 | 114, 123 | ltned 10981 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝑖 ≠ (𝐼 + 1)) |
125 | 23 | axlowdimlem12 27057 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑖 ≠ (𝐼 + 1)) → (𝑄‘𝑖) = 0) |
126 | 111, 124,
125 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → (𝑄‘𝑖) = 0) |
127 | 126 | sq0id 13776 |
. . . . . . . . . 10
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → ((𝑄‘𝑖)↑2) = 0) |
128 | 127 | sumeq2dv 15280 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (2...𝐼)((𝑄‘𝑖)↑2) = Σ𝑖 ∈ (2...𝐼)0) |
129 | | fzfi 13558 |
. . . . . . . . . . 11
⊢
(2...𝐼) ∈
Fin |
130 | 129 | olci 866 |
. . . . . . . . . 10
⊢
((2...𝐼) ⊆
(ℤ≥‘1) ∨ (2...𝐼) ∈ Fin) |
131 | | sumz 15299 |
. . . . . . . . . 10
⊢
(((2...𝐼) ⊆
(ℤ≥‘1) ∨ (2...𝐼) ∈ Fin) → Σ𝑖 ∈ (2...𝐼)0 = 0) |
132 | 130, 131 | ax-mp 5 |
. . . . . . . . 9
⊢
Σ𝑖 ∈
(2...𝐼)0 =
0 |
133 | 128, 132 | eqtrdi 2795 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (2...𝐼)((𝑄‘𝑖)↑2) = 0) |
134 | 101 | peano2zd 12298 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (𝐼 + 1) ∈ ℤ) |
135 | | sq1 13777 |
. . . . . . . . . . . . 13
⊢
(1↑2) = 1 |
136 | 26, 135 | eqtrdi 2795 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝐼 + 1) → ((𝑄‘𝑖)↑2) = 1) |
137 | 136 | fsum1 15324 |
. . . . . . . . . . 11
⊢ (((𝐼 + 1) ∈ ℤ ∧ 1
∈ ℂ) → Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄‘𝑖)↑2) = 1) |
138 | 134, 3, 137 | sylancl 589 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄‘𝑖)↑2) = 1) |
139 | | oveq2 7230 |
. . . . . . . . . . . 12
⊢ ((𝐼 + 1) = 𝑁 → ((𝐼 + 1)...(𝐼 + 1)) = ((𝐼 + 1)...𝑁)) |
140 | 139 | sumeq1d 15278 |
. . . . . . . . . . 11
⊢ ((𝐼 + 1) = 𝑁 → Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄‘𝑖)↑2) = Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄‘𝑖)↑2)) |
141 | 140 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ ((𝐼 + 1) = 𝑁 → (Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄‘𝑖)↑2) = 1 ↔ Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄‘𝑖)↑2) = 1)) |
142 | 138, 141 | syl5ib 247 |
. . . . . . . . 9
⊢ ((𝐼 + 1) = 𝑁 → ((𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄‘𝑖)↑2) = 1)) |
143 | 101 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ∈ ℤ) |
144 | 143 | zred 12295 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ∈ ℝ) |
145 | 60 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈ ℤ) |
146 | 145 | zred 12295 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈ ℝ) |
147 | 146, 94 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → (𝑁 − 1) ∈ ℝ) |
148 | 97 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ≤ (𝑁 − 1)) |
149 | 146 | ltm1d 11777 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → (𝑁 − 1) < 𝑁) |
150 | 144, 147,
146, 148, 149 | lelttrd 11003 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 < 𝑁) |
151 | | 1red 10847 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ (2...(𝑁 − 1)) → 1 ∈
ℝ) |
152 | | 2re 11917 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
153 | 152 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ (2...(𝑁 − 1)) → 2 ∈
ℝ) |
154 | | 1le2 12052 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ≤
2 |
155 | 154 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ (2...(𝑁 − 1)) → 1 ≤
2) |
156 | | elfzle1 13128 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ (2...(𝑁 − 1)) → 2 ≤ 𝐼) |
157 | 151, 153,
91, 155, 156 | letrd 11002 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈ (2...(𝑁 − 1)) → 1 ≤ 𝐼) |
158 | 157 | 3ad2ant3 1137 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 1 ≤ 𝐼) |
159 | 158 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 1 ≤ 𝐼) |
160 | | elnnz1 12216 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ ℕ ↔ (𝐼 ∈ ℤ ∧ 1 ≤
𝐼)) |
161 | 143, 159,
160 | sylanbrc 586 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ∈ ℕ) |
162 | 75 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℕ) |
163 | 162 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈ ℕ) |
164 | | nnltp1le 12246 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐼 < 𝑁 ↔ (𝐼 + 1) ≤ 𝑁)) |
165 | 161, 163,
164 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 < 𝑁 ↔ (𝐼 + 1) ≤ 𝑁)) |
166 | 150, 165 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 + 1) ≤ 𝑁) |
167 | | eluz 12465 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘(𝐼 + 1)) ↔ (𝐼 + 1) ≤ 𝑁)) |
168 | 134, 145,
167 | syl2an2 686 |
. . . . . . . . . . . . 13
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → (𝑁 ∈ (ℤ≥‘(𝐼 + 1)) ↔ (𝐼 + 1) ≤ 𝑁)) |
169 | 166, 168 | mpbird 260 |
. . . . . . . . . . . 12
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈ (ℤ≥‘(𝐼 + 1))) |
170 | | simpr1 1196 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈
(ℤ≥‘3)) |
171 | | simpr3 1198 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ∈ (2...(𝑁 − 1))) |
172 | 170, 171,
81 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝑄 ∈ (𝔼‘𝑁)) |
173 | 172 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ ((𝐼 + 1)...𝑁)) → 𝑄 ∈ (𝔼‘𝑁)) |
174 | 161 | peano2nnd 11860 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 + 1) ∈ ℕ) |
175 | | nnuz 12490 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ =
(ℤ≥‘1) |
176 | 174, 175 | eleqtrdi 2849 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 + 1) ∈
(ℤ≥‘1)) |
177 | | fzss1 13164 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 + 1) ∈
(ℤ≥‘1) → ((𝐼 + 1)...𝑁) ⊆ (1...𝑁)) |
178 | 176, 177 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → ((𝐼 + 1)...𝑁) ⊆ (1...𝑁)) |
179 | 178 | sselda 3910 |
. . . . . . . . . . . . . 14
⊢ ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ ((𝐼 + 1)...𝑁)) → 𝑖 ∈ (1...𝑁)) |
180 | 173, 179,
85 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ ((𝐼 + 1)...𝑁)) → (𝑄‘𝑖) ∈ ℂ) |
181 | 180 | sqcld 13727 |
. . . . . . . . . . . 12
⊢ ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ ((𝐼 + 1)...𝑁)) → ((𝑄‘𝑖)↑2) ∈ ℂ) |
182 | 22 | oveq1d 7237 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝐼 + 1) → ((𝑄‘𝑖)↑2) = ((𝑄‘(𝐼 + 1))↑2)) |
183 | 24 | oveq1i 7232 |
. . . . . . . . . . . . . 14
⊢ ((𝑄‘(𝐼 + 1))↑2) = (1↑2) |
184 | 183, 135 | eqtri 2766 |
. . . . . . . . . . . . 13
⊢ ((𝑄‘(𝐼 + 1))↑2) = 1 |
185 | 182, 184 | eqtrdi 2795 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝐼 + 1) → ((𝑄‘𝑖)↑2) = 1) |
186 | 169, 181,
185 | fsum1p 15330 |
. . . . . . . . . . 11
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄‘𝑖)↑2) = (1 + Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)((𝑄‘𝑖)↑2))) |
187 | 174 | peano2nnd 11860 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → ((𝐼 + 1) + 1) ∈ ℕ) |
188 | 187, 175 | eleqtrdi 2849 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → ((𝐼 + 1) + 1) ∈
(ℤ≥‘1)) |
189 | | fzss1 13164 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 + 1) + 1) ∈
(ℤ≥‘1) → (((𝐼 + 1) + 1)...𝑁) ⊆ (1...𝑁)) |
190 | 188, 189 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → (((𝐼 + 1) + 1)...𝑁) ⊆ (1...𝑁)) |
191 | 190 | sselda 3910 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → 𝑖 ∈ (1...𝑁)) |
192 | 144, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 + 1) ∈ ℝ) |
193 | 192 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → (𝐼 + 1) ∈ ℝ) |
194 | | peano2re 11018 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 + 1) ∈ ℝ →
((𝐼 + 1) + 1) ∈
ℝ) |
195 | 193, 194 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → ((𝐼 + 1) + 1) ∈ ℝ) |
196 | | elfzelz 13125 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (((𝐼 + 1) + 1)...𝑁) → 𝑖 ∈ ℤ) |
197 | 196 | zred 12295 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (((𝐼 + 1) + 1)...𝑁) → 𝑖 ∈ ℝ) |
198 | 197 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → 𝑖 ∈ ℝ) |
199 | 193 | ltp1d 11775 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → (𝐼 + 1) < ((𝐼 + 1) + 1)) |
200 | | elfzle1 13128 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (((𝐼 + 1) + 1)...𝑁) → ((𝐼 + 1) + 1) ≤ 𝑖) |
201 | 200 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → ((𝐼 + 1) + 1) ≤ 𝑖) |
202 | 193, 195,
198, 199, 201 | ltletrd 11005 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → (𝐼 + 1) < 𝑖) |
203 | 193, 202 | gtned 10980 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → 𝑖 ≠ (𝐼 + 1)) |
204 | 191, 203,
125 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → (𝑄‘𝑖) = 0) |
205 | 204 | sq0id 13776 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → ((𝑄‘𝑖)↑2) = 0) |
206 | 205 | sumeq2dv 15280 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)((𝑄‘𝑖)↑2) = Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)0) |
207 | | fzfi 13558 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐼 + 1) + 1)...𝑁) ∈ Fin |
208 | 207 | olci 866 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐼 + 1) + 1)...𝑁) ⊆ (ℤ≥‘1)
∨ (((𝐼 + 1) + 1)...𝑁) ∈ Fin) |
209 | | sumz 15299 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐼 + 1) +
1)...𝑁) ⊆
(ℤ≥‘1) ∨ (((𝐼 + 1) + 1)...𝑁) ∈ Fin) → Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)0 = 0) |
210 | 208, 209 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
Σ𝑖 ∈
(((𝐼 + 1) + 1)...𝑁)0 = 0 |
211 | 206, 210 | eqtrdi 2795 |
. . . . . . . . . . . . 13
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)((𝑄‘𝑖)↑2) = 0) |
212 | 211 | oveq2d 7238 |
. . . . . . . . . . . 12
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → (1 + Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)((𝑄‘𝑖)↑2)) = (1 + 0)) |
213 | | 1p0e1 11967 |
. . . . . . . . . . . 12
⊢ (1 + 0) =
1 |
214 | 212, 213 | eqtrdi 2795 |
. . . . . . . . . . 11
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → (1 + Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)((𝑄‘𝑖)↑2)) = 1) |
215 | 186, 214 | eqtrd 2778 |
. . . . . . . . . 10
⊢ (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄‘𝑖)↑2) = 1) |
216 | 215 | ex 416 |
. . . . . . . . 9
⊢ ((𝐼 + 1) ≠ 𝑁 → ((𝑁 ∈ (ℤ≥‘3)
∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄‘𝑖)↑2) = 1)) |
217 | 142, 216 | pm2.61ine 3026 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄‘𝑖)↑2) = 1) |
218 | 133, 217 | oveq12d 7240 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (Σ𝑖 ∈ (2...𝐼)((𝑄‘𝑖)↑2) + Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄‘𝑖)↑2)) = (0 + 1)) |
219 | | 0p1e1 11965 |
. . . . . . 7
⊢ (0 + 1) =
1 |
220 | 218, 219 | eqtrdi 2795 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (Σ𝑖 ∈ (2...𝐼)((𝑄‘𝑖)↑2) + Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄‘𝑖)↑2)) = 1) |
221 | 89, 220 | eqtrd 2778 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (2...𝑁)((𝑄‘𝑖)↑2) = 1) |
222 | | simp1 1138 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈
(ℤ≥‘3)) |
223 | | 2lt3 12015 |
. . . . . . . . . 10
⊢ 2 <
3 |
224 | 152, 48, 223 | ltleii 10968 |
. . . . . . . . 9
⊢ 2 ≤
3 |
225 | | 2z 12222 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
226 | 225 | eluz1i 12459 |
. . . . . . . . 9
⊢ (3 ∈
(ℤ≥‘2) ↔ (3 ∈ ℤ ∧ 2 ≤
3)) |
227 | 2, 224, 226 | mpbir2an 711 |
. . . . . . . 8
⊢ 3 ∈
(ℤ≥‘2) |
228 | | uztrn 12469 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 ∈
(ℤ≥‘2)) → 𝑁 ∈
(ℤ≥‘2)) |
229 | 222, 227,
228 | sylancl 589 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈
(ℤ≥‘2)) |
230 | | fveq2 6726 |
. . . . . . . 8
⊢ (𝑖 = 2 → (𝑄‘𝑖) = (𝑄‘2)) |
231 | 230 | oveq1d 7237 |
. . . . . . 7
⊢ (𝑖 = 2 → ((𝑄‘𝑖)↑2) = ((𝑄‘2)↑2)) |
232 | 229, 88, 231 | fsum1p 15330 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (2...𝑁)((𝑄‘𝑖)↑2) = (((𝑄‘2)↑2) + Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄‘𝑖)↑2))) |
233 | 59 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → 𝑁 ∈ ℤ) |
234 | 233 | zred 12295 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → 𝑁 ∈ ℝ) |
235 | | lttr 10922 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((2 < 3 ∧ 3
< 𝑁) → 2 < 𝑁)) |
236 | 152, 48, 235 | mp3an12 1453 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℝ → ((2 <
3 ∧ 3 < 𝑁) → 2
< 𝑁)) |
237 | 223, 236 | mpani 696 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℝ → (3 <
𝑁 → 2 < 𝑁)) |
238 | 49, 237 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘3) → (3 < 𝑁 → 2 < 𝑁)) |
239 | 238 | imp 410 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → 2 < 𝑁) |
240 | | ltle 10934 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ) → (2 < 𝑁 → 2 ≤ 𝑁)) |
241 | 152, 240 | mpan 690 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℝ → (2 <
𝑁 → 2 ≤ 𝑁)) |
242 | 234, 239,
241 | sylc 65 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → 2 ≤ 𝑁) |
243 | 242, 154 | jctil 523 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → (1 ≤ 2 ∧ 2 ≤ 𝑁)) |
244 | | 1z 12220 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℤ |
245 | | elfz 13114 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 ∈ (1...𝑁) ↔ (1 ≤ 2 ∧ 2 ≤
𝑁))) |
246 | 225, 244,
233, 245 | mp3an12i 1467 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → (2 ∈ (1...𝑁) ↔ (1 ≤ 2 ∧ 2 ≤ 𝑁))) |
247 | 243, 246 | mpbird 260 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → 2 ∈ (1...𝑁)) |
248 | 247 | 3adant3 1134 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 2 ∈ (1...𝑁)) |
249 | 91 | ltp1d 11775 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 < (𝐼 + 1)) |
250 | 153, 91, 117, 156, 249 | lelttrd 11003 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∈ (2...(𝑁 − 1)) → 2 < (𝐼 + 1)) |
251 | 250 | 3ad2ant3 1137 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 2 < (𝐼 + 1)) |
252 | | ltne 10942 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ 2 < (𝐼 + 1)) → (𝐼 + 1) ≠ 2) |
253 | 152, 251,
252 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (𝐼 + 1) ≠ 2) |
254 | 253 | necomd 2997 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 2 ≠ (𝐼 + 1)) |
255 | 23 | axlowdimlem12 27057 |
. . . . . . . . . 10
⊢ ((2
∈ (1...𝑁) ∧ 2 ≠
(𝐼 + 1)) → (𝑄‘2) = 0) |
256 | 248, 254,
255 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (𝑄‘2) = 0) |
257 | 256 | sq0id 13776 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → ((𝑄‘2)↑2) = 0) |
258 | 257 | oveq1d 7237 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (((𝑄‘2)↑2) + Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄‘𝑖)↑2)) = (0 + Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄‘𝑖)↑2))) |
259 | 15 | oveq1i 7232 |
. . . . . . . . 9
⊢
(3...𝑁) = ((2 +
1)...𝑁) |
260 | 259 | sumeq1i 15275 |
. . . . . . . 8
⊢
Σ𝑖 ∈
(3...𝑁)((𝑄‘𝑖)↑2) = Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄‘𝑖)↑2) |
261 | 260 | oveq2i 7233 |
. . . . . . 7
⊢ (0 +
Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2)) = (0 + Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄‘𝑖)↑2)) |
262 | 258, 261 | eqtr4di 2797 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (((𝑄‘2)↑2) + Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄‘𝑖)↑2)) = (0 + Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2))) |
263 | | fzfid 13559 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (3...𝑁) ∈ Fin) |
264 | | 3nn 11922 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
ℕ |
265 | 264, 175 | eleqtri 2837 |
. . . . . . . . . . . . 13
⊢ 3 ∈
(ℤ≥‘1) |
266 | | fzss1 13164 |
. . . . . . . . . . . . 13
⊢ (3 ∈
(ℤ≥‘1) → (3...𝑁) ⊆ (1...𝑁)) |
267 | 265, 266 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(3...𝑁) ⊆
(1...𝑁) |
268 | 267 | sseli 3905 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (3...𝑁) → 𝑖 ∈ (1...𝑁)) |
269 | 81, 268, 85 | syl2an 599 |
. . . . . . . . . 10
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → (𝑄‘𝑖) ∈ ℂ) |
270 | 269 | sqcld 13727 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑄‘𝑖)↑2) ∈ ℂ) |
271 | 270 | 3adantl2 1169 |
. . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑄‘𝑖)↑2) ∈ ℂ) |
272 | 263, 271 | fsumcl 15310 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2) ∈ ℂ) |
273 | 272 | addid2d 11046 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (0 + Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2)) = Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2)) |
274 | 232, 262,
273 | 3eqtrrd 2783 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2) = Σ𝑖 ∈ (2...𝑁)((𝑄‘𝑖)↑2)) |
275 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → 𝑁 ∈
(ℤ≥‘3)) |
276 | 6 | axlowdimlem7 27052 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑃 ∈ (𝔼‘𝑁)) |
277 | 276 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ (3...𝑁)) → 𝑃 ∈ (𝔼‘𝑁)) |
278 | 268 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ (3...𝑁)) → 𝑖 ∈ (1...𝑁)) |
279 | | fveecn 27006 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑃‘𝑖) ∈ ℂ) |
280 | 277, 278,
279 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ (3...𝑁)) → (𝑃‘𝑖) ∈ ℂ) |
281 | 280 | sqcld 13727 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑃‘𝑖)↑2) ∈ ℂ) |
282 | | neg1sqe1 13778 |
. . . . . . . . . 10
⊢
(-1↑2) = 1 |
283 | 9, 282 | eqtrdi 2795 |
. . . . . . . . 9
⊢ (𝑖 = 3 → ((𝑃‘𝑖)↑2) = 1) |
284 | 275, 281,
283 | fsum1p 15330 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2) = (1 + Σ𝑖 ∈ ((3 + 1)...𝑁)((𝑃‘𝑖)↑2))) |
285 | | 1re 10846 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ |
286 | | zaddcl 12230 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((3
∈ ℤ ∧ 1 ∈ ℤ) → (3 + 1) ∈
ℤ) |
287 | 2, 244, 286 | mp2an 692 |
. . . . . . . . . . . . . . . . . 18
⊢ (3 + 1)
∈ ℤ |
288 | 287 | zrei 12195 |
. . . . . . . . . . . . . . . . 17
⊢ (3 + 1)
∈ ℝ |
289 | | 1lt3 12016 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 <
3 |
290 | 48 | ltp1i 11749 |
. . . . . . . . . . . . . . . . . 18
⊢ 3 < (3
+ 1) |
291 | 285, 48, 288 | lttri 10971 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 <
3 ∧ 3 < (3 + 1)) → 1 < (3 + 1)) |
292 | 289, 290,
291 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ 1 < (3
+ 1) |
293 | 285, 288,
292 | ltleii 10968 |
. . . . . . . . . . . . . . . 16
⊢ 1 ≤ (3
+ 1) |
294 | | eluz 12465 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℤ ∧ (3 + 1) ∈ ℤ) → ((3 + 1) ∈
(ℤ≥‘1) ↔ 1 ≤ (3 + 1))) |
295 | 244, 287,
294 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ ((3 + 1)
∈ (ℤ≥‘1) ↔ 1 ≤ (3 + 1)) |
296 | 293, 295 | mpbir 234 |
. . . . . . . . . . . . . . 15
⊢ (3 + 1)
∈ (ℤ≥‘1) |
297 | | fzss1 13164 |
. . . . . . . . . . . . . . 15
⊢ ((3 + 1)
∈ (ℤ≥‘1) → ((3 + 1)...𝑁) ⊆ (1...𝑁)) |
298 | 296, 297 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((3 +
1)...𝑁) ⊆ (1...𝑁) |
299 | 298 | sseli 3905 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ((3 + 1)...𝑁) → 𝑖 ∈ (1...𝑁)) |
300 | 48, 288 | ltnlei 10966 |
. . . . . . . . . . . . . . . . . . 19
⊢ (3 <
(3 + 1) ↔ ¬ (3 + 1) ≤ 3) |
301 | 290, 300 | mpbi 233 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬ (3
+ 1) ≤ 3 |
302 | 301 | intnanr 491 |
. . . . . . . . . . . . . . . . 17
⊢ ¬
((3 + 1) ≤ 3 ∧ 3 ≤ 𝑁) |
303 | | elfz 13114 |
. . . . . . . . . . . . . . . . . 18
⊢ ((3
∈ ℤ ∧ (3 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (3 ∈ ((3 +
1)...𝑁) ↔ ((3 + 1)
≤ 3 ∧ 3 ≤ 𝑁))) |
304 | 2, 287, 233, 303 | mp3an12i 1467 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → (3 ∈ ((3 + 1)...𝑁) ↔ ((3 + 1) ≤ 3 ∧ 3
≤ 𝑁))) |
305 | 302, 304 | mtbiri 330 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → ¬ 3 ∈ ((3 + 1)...𝑁)) |
306 | | eleq1 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 3 → (𝑖 ∈ ((3 + 1)...𝑁) ↔ 3 ∈ ((3 + 1)...𝑁))) |
307 | 306 | notbid 321 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 3 → (¬ 𝑖 ∈ ((3 + 1)...𝑁) ↔ ¬ 3 ∈ ((3 +
1)...𝑁))) |
308 | 305, 307 | syl5ibrcom 250 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → (𝑖 = 3 → ¬ 𝑖 ∈ ((3 + 1)...𝑁))) |
309 | 308 | necon2ad 2956 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → (𝑖 ∈ ((3 + 1)...𝑁) → 𝑖 ≠ 3)) |
310 | 309 | imp 410 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ ((3 + 1)...𝑁)) → 𝑖 ≠ 3) |
311 | 6 | axlowdimlem9 27054 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑖 ≠ 3) → (𝑃‘𝑖) = 0) |
312 | 299, 310,
311 | syl2an2 686 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ ((3 + 1)...𝑁)) → (𝑃‘𝑖) = 0) |
313 | 312 | sq0id 13776 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ ((3 + 1)...𝑁)) → ((𝑃‘𝑖)↑2) = 0) |
314 | 313 | sumeq2dv 15280 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → Σ𝑖 ∈ ((3 + 1)...𝑁)((𝑃‘𝑖)↑2) = Σ𝑖 ∈ ((3 + 1)...𝑁)0) |
315 | | fzfi 13558 |
. . . . . . . . . . . 12
⊢ ((3 +
1)...𝑁) ∈
Fin |
316 | 315 | olci 866 |
. . . . . . . . . . 11
⊢ (((3 +
1)...𝑁) ⊆
(ℤ≥‘1) ∨ ((3 + 1)...𝑁) ∈ Fin) |
317 | | sumz 15299 |
. . . . . . . . . . 11
⊢ ((((3 +
1)...𝑁) ⊆
(ℤ≥‘1) ∨ ((3 + 1)...𝑁) ∈ Fin) → Σ𝑖 ∈ ((3 + 1)...𝑁)0 = 0) |
318 | 316, 317 | ax-mp 5 |
. . . . . . . . . 10
⊢
Σ𝑖 ∈ ((3
+ 1)...𝑁)0 =
0 |
319 | 314, 318 | eqtrdi 2795 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → Σ𝑖 ∈ ((3 + 1)...𝑁)((𝑃‘𝑖)↑2) = 0) |
320 | 319 | oveq2d 7238 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → (1 + Σ𝑖 ∈ ((3 + 1)...𝑁)((𝑃‘𝑖)↑2)) = (1 + 0)) |
321 | 284, 320 | eqtrd 2778 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2) = (1 + 0)) |
322 | 321, 213 | eqtrdi 2795 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁) → Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2) = 1) |
323 | 322 | 3adant3 1134 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2) = 1) |
324 | 221, 274,
323 | 3eqtr4rd 2789 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 3 < 𝑁 ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2)) |
325 | 44, 54, 55, 324 | syl3anc 1373 |
. . 3
⊢ ((𝑁 ≠ 3 ∧ (𝑁 ∈ (ℤ≥‘3)
∧ 𝐼 ∈ (2...(𝑁 − 1)))) →
Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2)) |
326 | 325 | ex 416 |
. 2
⊢ (𝑁 ≠ 3 → ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2))) |
327 | 43, 326 | pm2.61ine 3026 |
1
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2)) |