MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axlowdimlem16 Structured version   Visualization version   GIF version

Theorem axlowdimlem16 25637
Description: Lemma for axlowdim 25641. Set up a summation that will help establish distance. (Contributed by Scott Fenton, 21-Apr-2013.)
Hypotheses
Ref Expression
axlowdimlem16.1 𝑃 = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0}))
axlowdimlem16.2 𝑄 = ({⟨(𝐼 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))
Assertion
Ref Expression
axlowdimlem16 ((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2))
Distinct variable groups:   𝑃,𝑖   𝑖,𝐼   𝑖,𝑁   𝑄,𝑖

Proof of Theorem axlowdimlem16
StepHypRef Expression
1 elfz1eq 12223 . . . . . 6 (𝐼 ∈ (2...2) → 𝐼 = 2)
2 oveq1 6556 . . . . . . . . . . 11 (𝐼 = 2 → (𝐼 + 1) = (2 + 1))
3 df-3 10957 . . . . . . . . . . 11 3 = (2 + 1)
42, 3syl6reqr 2663 . . . . . . . . . 10 (𝐼 = 2 → 3 = (𝐼 + 1))
54, 4oveq12d 6567 . . . . . . . . 9 (𝐼 = 2 → (3...3) = ((𝐼 + 1)...(𝐼 + 1)))
65sumeq1d 14279 . . . . . . . 8 (𝐼 = 2 → Σ𝑖 ∈ (3...3)((𝑄𝑖)↑2) = Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄𝑖)↑2))
72, 3syl6eqr 2662 . . . . . . . . . 10 (𝐼 = 2 → (𝐼 + 1) = 3)
8 3z 11287 . . . . . . . . . 10 3 ∈ ℤ
97, 8syl6eqel 2696 . . . . . . . . 9 (𝐼 = 2 → (𝐼 + 1) ∈ ℤ)
10 ax-1cn 9873 . . . . . . . . . 10 1 ∈ ℂ
1110sqcli 12806 . . . . . . . . 9 (1↑2) ∈ ℂ
12 fveq2 6103 . . . . . . . . . . . 12 (𝑖 = (𝐼 + 1) → (𝑄𝑖) = (𝑄‘(𝐼 + 1)))
13 axlowdimlem16.2 . . . . . . . . . . . . 13 𝑄 = ({⟨(𝐼 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))
1413axlowdimlem11 25632 . . . . . . . . . . . 12 (𝑄‘(𝐼 + 1)) = 1
1512, 14syl6eq 2660 . . . . . . . . . . 11 (𝑖 = (𝐼 + 1) → (𝑄𝑖) = 1)
1615oveq1d 6564 . . . . . . . . . 10 (𝑖 = (𝐼 + 1) → ((𝑄𝑖)↑2) = (1↑2))
1716fsum1 14320 . . . . . . . . 9 (((𝐼 + 1) ∈ ℤ ∧ (1↑2) ∈ ℂ) → Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄𝑖)↑2) = (1↑2))
189, 11, 17sylancl 693 . . . . . . . 8 (𝐼 = 2 → Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄𝑖)↑2) = (1↑2))
196, 18eqtrd 2644 . . . . . . 7 (𝐼 = 2 → Σ𝑖 ∈ (3...3)((𝑄𝑖)↑2) = (1↑2))
20 fveq2 6103 . . . . . . . . . . . 12 (𝑖 = 3 → (𝑃𝑖) = (𝑃‘3))
21 axlowdimlem16.1 . . . . . . . . . . . . 13 𝑃 = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0}))
2221axlowdimlem8 25629 . . . . . . . . . . . 12 (𝑃‘3) = -1
2320, 22syl6eq 2660 . . . . . . . . . . 11 (𝑖 = 3 → (𝑃𝑖) = -1)
2423oveq1d 6564 . . . . . . . . . 10 (𝑖 = 3 → ((𝑃𝑖)↑2) = (-1↑2))
25 sqneg 12785 . . . . . . . . . . 11 (1 ∈ ℂ → (-1↑2) = (1↑2))
2610, 25ax-mp 5 . . . . . . . . . 10 (-1↑2) = (1↑2)
2724, 26syl6eq 2660 . . . . . . . . 9 (𝑖 = 3 → ((𝑃𝑖)↑2) = (1↑2))
2827fsum1 14320 . . . . . . . 8 ((3 ∈ ℤ ∧ (1↑2) ∈ ℂ) → Σ𝑖 ∈ (3...3)((𝑃𝑖)↑2) = (1↑2))
298, 11, 28mp2an 704 . . . . . . 7 Σ𝑖 ∈ (3...3)((𝑃𝑖)↑2) = (1↑2)
3019, 29syl6reqr 2663 . . . . . 6 (𝐼 = 2 → Σ𝑖 ∈ (3...3)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...3)((𝑄𝑖)↑2))
311, 30syl 17 . . . . 5 (𝐼 ∈ (2...2) → Σ𝑖 ∈ (3...3)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...3)((𝑄𝑖)↑2))
3231a1i 11 . . . 4 (𝑁 = 3 → (𝐼 ∈ (2...2) → Σ𝑖 ∈ (3...3)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...3)((𝑄𝑖)↑2)))
33 oveq1 6556 . . . . . . 7 (𝑁 = 3 → (𝑁 − 1) = (3 − 1))
34 3m1e2 11014 . . . . . . 7 (3 − 1) = 2
3533, 34syl6eq 2660 . . . . . 6 (𝑁 = 3 → (𝑁 − 1) = 2)
3635oveq2d 6565 . . . . 5 (𝑁 = 3 → (2...(𝑁 − 1)) = (2...2))
3736eleq2d 2673 . . . 4 (𝑁 = 3 → (𝐼 ∈ (2...(𝑁 − 1)) ↔ 𝐼 ∈ (2...2)))
38 oveq2 6557 . . . . . 6 (𝑁 = 3 → (3...𝑁) = (3...3))
3938sumeq1d 14279 . . . . 5 (𝑁 = 3 → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...3)((𝑃𝑖)↑2))
4038sumeq1d 14279 . . . . 5 (𝑁 = 3 → Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2) = Σ𝑖 ∈ (3...3)((𝑄𝑖)↑2))
4139, 40eqeq12d 2625 . . . 4 (𝑁 = 3 → (Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2) ↔ Σ𝑖 ∈ (3...3)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...3)((𝑄𝑖)↑2)))
4232, 37, 413imtr4d 282 . . 3 (𝑁 = 3 → (𝐼 ∈ (2...(𝑁 − 1)) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2)))
4342adantld 482 . 2 (𝑁 = 3 → ((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2)))
44 simprl 790 . . . 4 ((𝑁 ≠ 3 ∧ (𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈ (ℤ‘3))
45 eluzle 11576 . . . . . . 7 (𝑁 ∈ (ℤ‘3) → 3 ≤ 𝑁)
4645adantl 481 . . . . . 6 ((𝑁 ≠ 3 ∧ 𝑁 ∈ (ℤ‘3)) → 3 ≤ 𝑁)
47 simpl 472 . . . . . 6 ((𝑁 ≠ 3 ∧ 𝑁 ∈ (ℤ‘3)) → 𝑁 ≠ 3)
48 3re 10971 . . . . . . 7 3 ∈ ℝ
49 eluzelre 11574 . . . . . . . 8 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℝ)
5049adantl 481 . . . . . . 7 ((𝑁 ≠ 3 ∧ 𝑁 ∈ (ℤ‘3)) → 𝑁 ∈ ℝ)
51 ltlen 10017 . . . . . . 7 ((3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (3 < 𝑁 ↔ (3 ≤ 𝑁𝑁 ≠ 3)))
5248, 50, 51sylancr 694 . . . . . 6 ((𝑁 ≠ 3 ∧ 𝑁 ∈ (ℤ‘3)) → (3 < 𝑁 ↔ (3 ≤ 𝑁𝑁 ≠ 3)))
5346, 47, 52mpbir2and 959 . . . . 5 ((𝑁 ≠ 3 ∧ 𝑁 ∈ (ℤ‘3)) → 3 < 𝑁)
5453adantrr 749 . . . 4 ((𝑁 ≠ 3 ∧ (𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 3 < 𝑁)
55 simprr 792 . . . 4 ((𝑁 ≠ 3 ∧ (𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ∈ (2...(𝑁 − 1)))
56 fzssp1 12255 . . . . . . . . . . . . 13 (2...(𝑁 − 1)) ⊆ (2...((𝑁 − 1) + 1))
57 simp3 1056 . . . . . . . . . . . . 13 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ (2...(𝑁 − 1)))
5856, 57sseldi 3566 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ (2...((𝑁 − 1) + 1)))
59 eluzelz 11573 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℤ)
60593ad2ant1 1075 . . . . . . . . . . . . . . 15 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℤ)
6160zcnd 11359 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℂ)
62 npcan 10169 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
6361, 10, 62sylancl 693 . . . . . . . . . . . . 13 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
6463oveq2d 6565 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (2...((𝑁 − 1) + 1)) = (2...𝑁))
6558, 64eleqtrd 2690 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ (2...𝑁))
66 elfzelz 12213 . . . . . . . . . . 11 (𝐼 ∈ (2...𝑁) → 𝐼 ∈ ℤ)
6765, 66syl 17 . . . . . . . . . 10 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ ℤ)
6867zred 11358 . . . . . . . . 9 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ ℝ)
6968ltp1d 10833 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 < (𝐼 + 1))
70 fzdisj 12239 . . . . . . . 8 (𝐼 < (𝐼 + 1) → ((2...𝐼) ∩ ((𝐼 + 1)...𝑁)) = ∅)
7169, 70syl 17 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → ((2...𝐼) ∩ ((𝐼 + 1)...𝑁)) = ∅)
72 fzsplit 12238 . . . . . . . 8 (𝐼 ∈ (2...𝑁) → (2...𝑁) = ((2...𝐼) ∪ ((𝐼 + 1)...𝑁)))
7365, 72syl 17 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (2...𝑁) = ((2...𝐼) ∪ ((𝐼 + 1)...𝑁)))
74 fzfid 12634 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (2...𝑁) ∈ Fin)
75 eluzge3nn 11606 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℕ)
76 2eluzge1 11610 . . . . . . . . . . . . 13 2 ∈ (ℤ‘1)
77 fzss1 12251 . . . . . . . . . . . . 13 (2 ∈ (ℤ‘1) → (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1)))
7876, 77ax-mp 5 . . . . . . . . . . . 12 (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1))
7978sseli 3564 . . . . . . . . . . 11 (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ∈ (1...(𝑁 − 1)))
8013axlowdimlem10 25631 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 𝑄 ∈ (𝔼‘𝑁))
8175, 79, 80syl2an 493 . . . . . . . . . 10 ((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑄 ∈ (𝔼‘𝑁))
82 fzss1 12251 . . . . . . . . . . . 12 (2 ∈ (ℤ‘1) → (2...𝑁) ⊆ (1...𝑁))
8376, 82ax-mp 5 . . . . . . . . . . 11 (2...𝑁) ⊆ (1...𝑁)
8483sseli 3564 . . . . . . . . . 10 (𝑖 ∈ (2...𝑁) → 𝑖 ∈ (1...𝑁))
85 fveecn 25582 . . . . . . . . . 10 ((𝑄 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑄𝑖) ∈ ℂ)
8681, 84, 85syl2an 493 . . . . . . . . 9 (((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝑁)) → (𝑄𝑖) ∈ ℂ)
8786sqcld 12868 . . . . . . . 8 (((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝑁)) → ((𝑄𝑖)↑2) ∈ ℂ)
88873adantl2 1211 . . . . . . 7 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝑁)) → ((𝑄𝑖)↑2) ∈ ℂ)
8971, 73, 74, 88fsumsplit 14318 . . . . . 6 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (2...𝑁)((𝑄𝑖)↑2) = (Σ𝑖 ∈ (2...𝐼)((𝑄𝑖)↑2) + Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2)))
90 fzss1 12251 . . . . . . . . . . . . . . . 16 (2 ∈ (ℤ‘1) → (2...𝐼) ⊆ (1...𝐼))
9176, 90ax-mp 5 . . . . . . . . . . . . . . 15 (2...𝐼) ⊆ (1...𝐼)
9291sseli 3564 . . . . . . . . . . . . . 14 (𝑖 ∈ (2...𝐼) → 𝑖 ∈ (1...𝐼))
93 elfzelz 12213 . . . . . . . . . . . . . . . . . . . 20 (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ∈ ℤ)
9493zred 11358 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ∈ ℝ)
95943ad2ant3 1077 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ ℝ)
96493ad2ant1 1075 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℝ)
97 peano2rem 10227 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
9896, 97syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
99 elfzle2 12216 . . . . . . . . . . . . . . . . . . . 20 (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ≤ (𝑁 − 1))
100993ad2ant3 1077 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ≤ (𝑁 − 1))
10196ltm1d 10835 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
10295, 98, 96, 100, 101lelttrd 10074 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 < 𝑁)
10395, 96, 102ltled 10064 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼𝑁)
104933ad2ant3 1077 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ ℤ)
105 eluz 11577 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ𝐼) ↔ 𝐼𝑁))
106104, 60, 105syl2anc 691 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝑁 ∈ (ℤ𝐼) ↔ 𝐼𝑁))
107103, 106mpbird 246 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ (ℤ𝐼))
108 fzss2 12252 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝐼) → (1...𝐼) ⊆ (1...𝑁))
109107, 108syl 17 . . . . . . . . . . . . . . 15 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (1...𝐼) ⊆ (1...𝑁))
110109sseld 3567 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝑖 ∈ (1...𝐼) → 𝑖 ∈ (1...𝑁)))
11192, 110syl5 33 . . . . . . . . . . . . 13 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝑖 ∈ (2...𝐼) → 𝑖 ∈ (1...𝑁)))
112111imp 444 . . . . . . . . . . . 12 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝑖 ∈ (1...𝑁))
113 elfzelz 12213 . . . . . . . . . . . . . . 15 (𝑖 ∈ (2...𝐼) → 𝑖 ∈ ℤ)
114113zred 11358 . . . . . . . . . . . . . 14 (𝑖 ∈ (2...𝐼) → 𝑖 ∈ ℝ)
115114adantl 481 . . . . . . . . . . . . 13 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝑖 ∈ ℝ)
11695adantr 480 . . . . . . . . . . . . . 14 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝐼 ∈ ℝ)
117 peano2re 10088 . . . . . . . . . . . . . . . . 17 (𝐼 ∈ ℝ → (𝐼 + 1) ∈ ℝ)
11894, 117syl 17 . . . . . . . . . . . . . . . 16 (𝐼 ∈ (2...(𝑁 − 1)) → (𝐼 + 1) ∈ ℝ)
1191183ad2ant3 1077 . . . . . . . . . . . . . . 15 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝐼 + 1) ∈ ℝ)
120119adantr 480 . . . . . . . . . . . . . 14 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → (𝐼 + 1) ∈ ℝ)
121 elfzle2 12216 . . . . . . . . . . . . . . 15 (𝑖 ∈ (2...𝐼) → 𝑖𝐼)
122121adantl 481 . . . . . . . . . . . . . 14 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝑖𝐼)
123116ltp1d 10833 . . . . . . . . . . . . . 14 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝐼 < (𝐼 + 1))
124115, 116, 120, 122, 123lelttrd 10074 . . . . . . . . . . . . 13 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝑖 < (𝐼 + 1))
125115, 124ltned 10052 . . . . . . . . . . . 12 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝑖 ≠ (𝐼 + 1))
12613axlowdimlem12 25633 . . . . . . . . . . . 12 ((𝑖 ∈ (1...𝑁) ∧ 𝑖 ≠ (𝐼 + 1)) → (𝑄𝑖) = 0)
127112, 125, 126syl2anc 691 . . . . . . . . . . 11 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → (𝑄𝑖) = 0)
128127sq0id 12819 . . . . . . . . . 10 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → ((𝑄𝑖)↑2) = 0)
129128sumeq2dv 14281 . . . . . . . . 9 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (2...𝐼)((𝑄𝑖)↑2) = Σ𝑖 ∈ (2...𝐼)0)
130 fzfi 12633 . . . . . . . . . . 11 (2...𝐼) ∈ Fin
131130olci 405 . . . . . . . . . 10 ((2...𝐼) ⊆ (ℤ‘1) ∨ (2...𝐼) ∈ Fin)
132 sumz 14300 . . . . . . . . . 10 (((2...𝐼) ⊆ (ℤ‘1) ∨ (2...𝐼) ∈ Fin) → Σ𝑖 ∈ (2...𝐼)0 = 0)
133131, 132ax-mp 5 . . . . . . . . 9 Σ𝑖 ∈ (2...𝐼)0 = 0
134129, 133syl6eq 2660 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (2...𝐼)((𝑄𝑖)↑2) = 0)
135104peano2zd 11361 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝐼 + 1) ∈ ℤ)
136 sq1 12820 . . . . . . . . . . . . 13 (1↑2) = 1
13716, 136syl6eq 2660 . . . . . . . . . . . 12 (𝑖 = (𝐼 + 1) → ((𝑄𝑖)↑2) = 1)
138137fsum1 14320 . . . . . . . . . . 11 (((𝐼 + 1) ∈ ℤ ∧ 1 ∈ ℂ) → Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄𝑖)↑2) = 1)
139135, 10, 138sylancl 693 . . . . . . . . . 10 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄𝑖)↑2) = 1)
140 oveq2 6557 . . . . . . . . . . . 12 ((𝐼 + 1) = 𝑁 → ((𝐼 + 1)...(𝐼 + 1)) = ((𝐼 + 1)...𝑁))
141140sumeq1d 14279 . . . . . . . . . . 11 ((𝐼 + 1) = 𝑁 → Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄𝑖)↑2) = Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2))
142141eqeq1d 2612 . . . . . . . . . 10 ((𝐼 + 1) = 𝑁 → (Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄𝑖)↑2) = 1 ↔ Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2) = 1))
143139, 142syl5ib 233 . . . . . . . . 9 ((𝐼 + 1) = 𝑁 → ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2) = 1))
144104adantl 481 . . . . . . . . . . . . . . . 16 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ∈ ℤ)
145144zred 11358 . . . . . . . . . . . . . . 15 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ∈ ℝ)
14660adantl 481 . . . . . . . . . . . . . . . . 17 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈ ℤ)
147146zred 11358 . . . . . . . . . . . . . . . 16 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈ ℝ)
148147, 97syl 17 . . . . . . . . . . . . . . 15 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝑁 − 1) ∈ ℝ)
149100adantl 481 . . . . . . . . . . . . . . 15 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ≤ (𝑁 − 1))
150147ltm1d 10835 . . . . . . . . . . . . . . 15 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝑁 − 1) < 𝑁)
151145, 148, 147, 149, 150lelttrd 10074 . . . . . . . . . . . . . 14 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 < 𝑁)
152 1red 9934 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ (2...(𝑁 − 1)) → 1 ∈ ℝ)
153 2re 10967 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
154153a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ (2...(𝑁 − 1)) → 2 ∈ ℝ)
155 1le2 11118 . . . . . . . . . . . . . . . . . . . 20 1 ≤ 2
156155a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ (2...(𝑁 − 1)) → 1 ≤ 2)
157 elfzle1 12215 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ (2...(𝑁 − 1)) → 2 ≤ 𝐼)
158152, 154, 94, 156, 157letrd 10073 . . . . . . . . . . . . . . . . . 18 (𝐼 ∈ (2...(𝑁 − 1)) → 1 ≤ 𝐼)
1591583ad2ant3 1077 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 1 ≤ 𝐼)
160159adantl 481 . . . . . . . . . . . . . . . 16 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 1 ≤ 𝐼)
161 elnnz1 11280 . . . . . . . . . . . . . . . 16 (𝐼 ∈ ℕ ↔ (𝐼 ∈ ℤ ∧ 1 ≤ 𝐼))
162144, 160, 161sylanbrc 695 . . . . . . . . . . . . . . 15 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ∈ ℕ)
163753ad2ant1 1075 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℕ)
164163adantl 481 . . . . . . . . . . . . . . 15 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈ ℕ)
165 nnltp1le 11310 . . . . . . . . . . . . . . 15 ((𝐼 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐼 < 𝑁 ↔ (𝐼 + 1) ≤ 𝑁))
166162, 164, 165syl2anc 691 . . . . . . . . . . . . . 14 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 < 𝑁 ↔ (𝐼 + 1) ≤ 𝑁))
167151, 166mpbid 221 . . . . . . . . . . . . 13 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 + 1) ≤ 𝑁)
168135adantl 481 . . . . . . . . . . . . . 14 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 + 1) ∈ ℤ)
169 eluz 11577 . . . . . . . . . . . . . 14 (((𝐼 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ‘(𝐼 + 1)) ↔ (𝐼 + 1) ≤ 𝑁))
170168, 146, 169syl2anc 691 . . . . . . . . . . . . 13 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝑁 ∈ (ℤ‘(𝐼 + 1)) ↔ (𝐼 + 1) ≤ 𝑁))
171167, 170mpbird 246 . . . . . . . . . . . 12 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈ (ℤ‘(𝐼 + 1)))
172 simpr1 1060 . . . . . . . . . . . . . . . 16 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈ (ℤ‘3))
173 simpr3 1062 . . . . . . . . . . . . . . . 16 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ∈ (2...(𝑁 − 1)))
174172, 173, 81syl2anc 691 . . . . . . . . . . . . . . 15 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝑄 ∈ (𝔼‘𝑁))
175174adantr 480 . . . . . . . . . . . . . 14 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ ((𝐼 + 1)...𝑁)) → 𝑄 ∈ (𝔼‘𝑁))
176162peano2nnd 10914 . . . . . . . . . . . . . . . . 17 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 + 1) ∈ ℕ)
177 nnuz 11599 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
178176, 177syl6eleq 2698 . . . . . . . . . . . . . . . 16 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 + 1) ∈ (ℤ‘1))
179 fzss1 12251 . . . . . . . . . . . . . . . 16 ((𝐼 + 1) ∈ (ℤ‘1) → ((𝐼 + 1)...𝑁) ⊆ (1...𝑁))
180178, 179syl 17 . . . . . . . . . . . . . . 15 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → ((𝐼 + 1)...𝑁) ⊆ (1...𝑁))
181180sselda 3568 . . . . . . . . . . . . . 14 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ ((𝐼 + 1)...𝑁)) → 𝑖 ∈ (1...𝑁))
182175, 181, 85syl2anc 691 . . . . . . . . . . . . 13 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ ((𝐼 + 1)...𝑁)) → (𝑄𝑖) ∈ ℂ)
183182sqcld 12868 . . . . . . . . . . . 12 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ ((𝐼 + 1)...𝑁)) → ((𝑄𝑖)↑2) ∈ ℂ)
18412oveq1d 6564 . . . . . . . . . . . . 13 (𝑖 = (𝐼 + 1) → ((𝑄𝑖)↑2) = ((𝑄‘(𝐼 + 1))↑2))
18514oveq1i 6559 . . . . . . . . . . . . . 14 ((𝑄‘(𝐼 + 1))↑2) = (1↑2)
186185, 136eqtri 2632 . . . . . . . . . . . . 13 ((𝑄‘(𝐼 + 1))↑2) = 1
187184, 186syl6eq 2660 . . . . . . . . . . . 12 (𝑖 = (𝐼 + 1) → ((𝑄𝑖)↑2) = 1)
188171, 183, 187fsum1p 14326 . . . . . . . . . . 11 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2) = (1 + Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)((𝑄𝑖)↑2)))
189176peano2nnd 10914 . . . . . . . . . . . . . . . . . . . 20 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → ((𝐼 + 1) + 1) ∈ ℕ)
190189, 177syl6eleq 2698 . . . . . . . . . . . . . . . . . . 19 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → ((𝐼 + 1) + 1) ∈ (ℤ‘1))
191 fzss1 12251 . . . . . . . . . . . . . . . . . . 19 (((𝐼 + 1) + 1) ∈ (ℤ‘1) → (((𝐼 + 1) + 1)...𝑁) ⊆ (1...𝑁))
192190, 191syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (((𝐼 + 1) + 1)...𝑁) ⊆ (1...𝑁))
193192sselda 3568 . . . . . . . . . . . . . . . . 17 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → 𝑖 ∈ (1...𝑁))
194145, 117syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 + 1) ∈ ℝ)
195194adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → (𝐼 + 1) ∈ ℝ)
196 peano2re 10088 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 + 1) ∈ ℝ → ((𝐼 + 1) + 1) ∈ ℝ)
197195, 196syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → ((𝐼 + 1) + 1) ∈ ℝ)
198 elfzelz 12213 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (((𝐼 + 1) + 1)...𝑁) → 𝑖 ∈ ℤ)
199198zred 11358 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (((𝐼 + 1) + 1)...𝑁) → 𝑖 ∈ ℝ)
200199adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → 𝑖 ∈ ℝ)
201195ltp1d 10833 . . . . . . . . . . . . . . . . . . 19 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → (𝐼 + 1) < ((𝐼 + 1) + 1))
202 elfzle1 12215 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (((𝐼 + 1) + 1)...𝑁) → ((𝐼 + 1) + 1) ≤ 𝑖)
203202adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → ((𝐼 + 1) + 1) ≤ 𝑖)
204195, 197, 200, 201, 203ltletrd 10076 . . . . . . . . . . . . . . . . . 18 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → (𝐼 + 1) < 𝑖)
205195, 204gtned 10051 . . . . . . . . . . . . . . . . 17 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → 𝑖 ≠ (𝐼 + 1))
206193, 205, 126syl2anc 691 . . . . . . . . . . . . . . . 16 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → (𝑄𝑖) = 0)
207206sq0id 12819 . . . . . . . . . . . . . . 15 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → ((𝑄𝑖)↑2) = 0)
208207sumeq2dv 14281 . . . . . . . . . . . . . 14 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)((𝑄𝑖)↑2) = Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)0)
209 fzfi 12633 . . . . . . . . . . . . . . . 16 (((𝐼 + 1) + 1)...𝑁) ∈ Fin
210209olci 405 . . . . . . . . . . . . . . 15 ((((𝐼 + 1) + 1)...𝑁) ⊆ (ℤ‘1) ∨ (((𝐼 + 1) + 1)...𝑁) ∈ Fin)
211 sumz 14300 . . . . . . . . . . . . . . 15 (((((𝐼 + 1) + 1)...𝑁) ⊆ (ℤ‘1) ∨ (((𝐼 + 1) + 1)...𝑁) ∈ Fin) → Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)0 = 0)
212210, 211ax-mp 5 . . . . . . . . . . . . . 14 Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)0 = 0
213208, 212syl6eq 2660 . . . . . . . . . . . . 13 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)((𝑄𝑖)↑2) = 0)
214213oveq2d 6565 . . . . . . . . . . . 12 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (1 + Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)((𝑄𝑖)↑2)) = (1 + 0))
215 1p0e1 11010 . . . . . . . . . . . 12 (1 + 0) = 1
216214, 215syl6eq 2660 . . . . . . . . . . 11 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (1 + Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)((𝑄𝑖)↑2)) = 1)
217188, 216eqtrd 2644 . . . . . . . . . 10 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2) = 1)
218217ex 449 . . . . . . . . 9 ((𝐼 + 1) ≠ 𝑁 → ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2) = 1))
219143, 218pm2.61ine 2865 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2) = 1)
220134, 219oveq12d 6567 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (Σ𝑖 ∈ (2...𝐼)((𝑄𝑖)↑2) + Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2)) = (0 + 1))
221 0p1e1 11009 . . . . . . 7 (0 + 1) = 1
222220, 221syl6eq 2660 . . . . . 6 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (Σ𝑖 ∈ (2...𝐼)((𝑄𝑖)↑2) + Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2)) = 1)
22389, 222eqtrd 2644 . . . . 5 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (2...𝑁)((𝑄𝑖)↑2) = 1)
224 simp1 1054 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘3))
225 2lt3 11072 . . . . . . . . . 10 2 < 3
226153, 48, 225ltleii 10039 . . . . . . . . 9 2 ≤ 3
227 2z 11286 . . . . . . . . . 10 2 ∈ ℤ
228227eluz1i 11571 . . . . . . . . 9 (3 ∈ (ℤ‘2) ↔ (3 ∈ ℤ ∧ 2 ≤ 3))
2298, 226, 228mpbir2an 957 . . . . . . . 8 3 ∈ (ℤ‘2)
230 uztrn 11580 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 ∈ (ℤ‘2)) → 𝑁 ∈ (ℤ‘2))
231224, 229, 230sylancl 693 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘2))
232 fveq2 6103 . . . . . . . 8 (𝑖 = 2 → (𝑄𝑖) = (𝑄‘2))
233232oveq1d 6564 . . . . . . 7 (𝑖 = 2 → ((𝑄𝑖)↑2) = ((𝑄‘2)↑2))
234231, 88, 233fsum1p 14326 . . . . . 6 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (2...𝑁)((𝑄𝑖)↑2) = (((𝑄‘2)↑2) + Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄𝑖)↑2)))
23559adantr 480 . . . . . . . . . . . . . . 15 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → 𝑁 ∈ ℤ)
236235zred 11358 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → 𝑁 ∈ ℝ)
237 lttr 9993 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((2 < 3 ∧ 3 < 𝑁) → 2 < 𝑁))
238153, 48, 237mp3an12 1406 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℝ → ((2 < 3 ∧ 3 < 𝑁) → 2 < 𝑁))
239225, 238mpani 708 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℝ → (3 < 𝑁 → 2 < 𝑁))
24049, 239syl 17 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ‘3) → (3 < 𝑁 → 2 < 𝑁))
241240imp 444 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → 2 < 𝑁)
242 ltle 10005 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 < 𝑁 → 2 ≤ 𝑁))
243153, 242mpan 702 . . . . . . . . . . . . . 14 (𝑁 ∈ ℝ → (2 < 𝑁 → 2 ≤ 𝑁))
244236, 241, 243sylc 63 . . . . . . . . . . . . 13 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → 2 ≤ 𝑁)
245244, 155jctil 558 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → (1 ≤ 2 ∧ 2 ≤ 𝑁))
246 1z 11284 . . . . . . . . . . . . . 14 1 ∈ ℤ
247 elfz 12203 . . . . . . . . . . . . . 14 ((2 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 ∈ (1...𝑁) ↔ (1 ≤ 2 ∧ 2 ≤ 𝑁)))
248227, 246, 247mp3an12 1406 . . . . . . . . . . . . 13 (𝑁 ∈ ℤ → (2 ∈ (1...𝑁) ↔ (1 ≤ 2 ∧ 2 ≤ 𝑁)))
249235, 248syl 17 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → (2 ∈ (1...𝑁) ↔ (1 ≤ 2 ∧ 2 ≤ 𝑁)))
250245, 249mpbird 246 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → 2 ∈ (1...𝑁))
2512503adant3 1074 . . . . . . . . . 10 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 2 ∈ (1...𝑁))
25294ltp1d 10833 . . . . . . . . . . . . . 14 (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 < (𝐼 + 1))
253154, 94, 118, 157, 252lelttrd 10074 . . . . . . . . . . . . 13 (𝐼 ∈ (2...(𝑁 − 1)) → 2 < (𝐼 + 1))
2542533ad2ant3 1077 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 2 < (𝐼 + 1))
255 ltne 10013 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ 2 < (𝐼 + 1)) → (𝐼 + 1) ≠ 2)
256153, 254, 255sylancr 694 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝐼 + 1) ≠ 2)
257256necomd 2837 . . . . . . . . . 10 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 2 ≠ (𝐼 + 1))
25813axlowdimlem12 25633 . . . . . . . . . 10 ((2 ∈ (1...𝑁) ∧ 2 ≠ (𝐼 + 1)) → (𝑄‘2) = 0)
259251, 257, 258syl2anc 691 . . . . . . . . 9 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝑄‘2) = 0)
260259sq0id 12819 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → ((𝑄‘2)↑2) = 0)
261260oveq1d 6564 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (((𝑄‘2)↑2) + Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄𝑖)↑2)) = (0 + Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄𝑖)↑2)))
2623oveq1i 6559 . . . . . . . . 9 (3...𝑁) = ((2 + 1)...𝑁)
263262sumeq1i 14276 . . . . . . . 8 Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2) = Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄𝑖)↑2)
264263oveq2i 6560 . . . . . . 7 (0 + Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2)) = (0 + Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄𝑖)↑2))
265261, 264syl6eqr 2662 . . . . . 6 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (((𝑄‘2)↑2) + Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄𝑖)↑2)) = (0 + Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2)))
266 fzfid 12634 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (3...𝑁) ∈ Fin)
267 3nn 11063 . . . . . . . . . . . . . 14 3 ∈ ℕ
268267, 177eleqtri 2686 . . . . . . . . . . . . 13 3 ∈ (ℤ‘1)
269 fzss1 12251 . . . . . . . . . . . . 13 (3 ∈ (ℤ‘1) → (3...𝑁) ⊆ (1...𝑁))
270268, 269ax-mp 5 . . . . . . . . . . . 12 (3...𝑁) ⊆ (1...𝑁)
271270sseli 3564 . . . . . . . . . . 11 (𝑖 ∈ (3...𝑁) → 𝑖 ∈ (1...𝑁))
27281, 271, 85syl2an 493 . . . . . . . . . 10 (((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → (𝑄𝑖) ∈ ℂ)
273272sqcld 12868 . . . . . . . . 9 (((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑄𝑖)↑2) ∈ ℂ)
2742733adantl2 1211 . . . . . . . 8 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑄𝑖)↑2) ∈ ℂ)
275266, 274fsumcl 14311 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2) ∈ ℂ)
276275addid2d 10116 . . . . . 6 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (0 + Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2)) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2))
277234, 265, 2763eqtrrd 2649 . . . . 5 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2) = Σ𝑖 ∈ (2...𝑁)((𝑄𝑖)↑2))
278 simpl 472 . . . . . . . . 9 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → 𝑁 ∈ (ℤ‘3))
27921axlowdimlem7 25628 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘3) → 𝑃 ∈ (𝔼‘𝑁))
280279ad2antrr 758 . . . . . . . . . . 11 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ (3...𝑁)) → 𝑃 ∈ (𝔼‘𝑁))
281271adantl 481 . . . . . . . . . . 11 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ (3...𝑁)) → 𝑖 ∈ (1...𝑁))
282 fveecn 25582 . . . . . . . . . . 11 ((𝑃 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑃𝑖) ∈ ℂ)
283280, 281, 282syl2anc 691 . . . . . . . . . 10 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ (3...𝑁)) → (𝑃𝑖) ∈ ℂ)
284283sqcld 12868 . . . . . . . . 9 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑃𝑖)↑2) ∈ ℂ)
285 neg1sqe1 12821 . . . . . . . . . 10 (-1↑2) = 1
28624, 285syl6eq 2660 . . . . . . . . 9 (𝑖 = 3 → ((𝑃𝑖)↑2) = 1)
287278, 284, 286fsum1p 14326 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = (1 + Σ𝑖 ∈ ((3 + 1)...𝑁)((𝑃𝑖)↑2)))
288 1re 9918 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
289 zaddcl 11294 . . . . . . . . . . . . . . . . . . . 20 ((3 ∈ ℤ ∧ 1 ∈ ℤ) → (3 + 1) ∈ ℤ)
2908, 246, 289mp2an 704 . . . . . . . . . . . . . . . . . . 19 (3 + 1) ∈ ℤ
291290zrei 11260 . . . . . . . . . . . . . . . . . 18 (3 + 1) ∈ ℝ
292 1lt3 11073 . . . . . . . . . . . . . . . . . . 19 1 < 3
29348ltp1i 10806 . . . . . . . . . . . . . . . . . . 19 3 < (3 + 1)
294288, 48, 291lttri 10042 . . . . . . . . . . . . . . . . . . 19 ((1 < 3 ∧ 3 < (3 + 1)) → 1 < (3 + 1))
295292, 293, 294mp2an 704 . . . . . . . . . . . . . . . . . 18 1 < (3 + 1)
296288, 291, 295ltleii 10039 . . . . . . . . . . . . . . . . 17 1 ≤ (3 + 1)
297 eluz 11577 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℤ ∧ (3 + 1) ∈ ℤ) → ((3 + 1) ∈ (ℤ‘1) ↔ 1 ≤ (3 + 1)))
298246, 290, 297mp2an 704 . . . . . . . . . . . . . . . . 17 ((3 + 1) ∈ (ℤ‘1) ↔ 1 ≤ (3 + 1))
299296, 298mpbir 220 . . . . . . . . . . . . . . . 16 (3 + 1) ∈ (ℤ‘1)
300 fzss1 12251 . . . . . . . . . . . . . . . 16 ((3 + 1) ∈ (ℤ‘1) → ((3 + 1)...𝑁) ⊆ (1...𝑁))
301299, 300ax-mp 5 . . . . . . . . . . . . . . 15 ((3 + 1)...𝑁) ⊆ (1...𝑁)
302301sseli 3564 . . . . . . . . . . . . . 14 (𝑖 ∈ ((3 + 1)...𝑁) → 𝑖 ∈ (1...𝑁))
303302adantl 481 . . . . . . . . . . . . 13 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ ((3 + 1)...𝑁)) → 𝑖 ∈ (1...𝑁))
30448, 291ltnlei 10037 . . . . . . . . . . . . . . . . . . 19 (3 < (3 + 1) ↔ ¬ (3 + 1) ≤ 3)
305293, 304mpbi 219 . . . . . . . . . . . . . . . . . 18 ¬ (3 + 1) ≤ 3
306305intnanr 952 . . . . . . . . . . . . . . . . 17 ¬ ((3 + 1) ≤ 3 ∧ 3 ≤ 𝑁)
307 elfz 12203 . . . . . . . . . . . . . . . . . . 19 ((3 ∈ ℤ ∧ (3 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (3 ∈ ((3 + 1)...𝑁) ↔ ((3 + 1) ≤ 3 ∧ 3 ≤ 𝑁)))
3088, 290, 307mp3an12 1406 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℤ → (3 ∈ ((3 + 1)...𝑁) ↔ ((3 + 1) ≤ 3 ∧ 3 ≤ 𝑁)))
309235, 308syl 17 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → (3 ∈ ((3 + 1)...𝑁) ↔ ((3 + 1) ≤ 3 ∧ 3 ≤ 𝑁)))
310306, 309mtbiri 316 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → ¬ 3 ∈ ((3 + 1)...𝑁))
311 eleq1 2676 . . . . . . . . . . . . . . . . 17 (𝑖 = 3 → (𝑖 ∈ ((3 + 1)...𝑁) ↔ 3 ∈ ((3 + 1)...𝑁)))
312311notbid 307 . . . . . . . . . . . . . . . 16 (𝑖 = 3 → (¬ 𝑖 ∈ ((3 + 1)...𝑁) ↔ ¬ 3 ∈ ((3 + 1)...𝑁)))
313310, 312syl5ibrcom 236 . . . . . . . . . . . . . . 15 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → (𝑖 = 3 → ¬ 𝑖 ∈ ((3 + 1)...𝑁)))
314313necon2ad 2797 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → (𝑖 ∈ ((3 + 1)...𝑁) → 𝑖 ≠ 3))
315314imp 444 . . . . . . . . . . . . 13 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ ((3 + 1)...𝑁)) → 𝑖 ≠ 3)
31621axlowdimlem9 25630 . . . . . . . . . . . . 13 ((𝑖 ∈ (1...𝑁) ∧ 𝑖 ≠ 3) → (𝑃𝑖) = 0)
317303, 315, 316syl2anc 691 . . . . . . . . . . . 12 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ ((3 + 1)...𝑁)) → (𝑃𝑖) = 0)
318317sq0id 12819 . . . . . . . . . . 11 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ ((3 + 1)...𝑁)) → ((𝑃𝑖)↑2) = 0)
319318sumeq2dv 14281 . . . . . . . . . 10 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → Σ𝑖 ∈ ((3 + 1)...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ ((3 + 1)...𝑁)0)
320 fzfi 12633 . . . . . . . . . . . 12 ((3 + 1)...𝑁) ∈ Fin
321320olci 405 . . . . . . . . . . 11 (((3 + 1)...𝑁) ⊆ (ℤ‘1) ∨ ((3 + 1)...𝑁) ∈ Fin)
322 sumz 14300 . . . . . . . . . . 11 ((((3 + 1)...𝑁) ⊆ (ℤ‘1) ∨ ((3 + 1)...𝑁) ∈ Fin) → Σ𝑖 ∈ ((3 + 1)...𝑁)0 = 0)
323321, 322ax-mp 5 . . . . . . . . . 10 Σ𝑖 ∈ ((3 + 1)...𝑁)0 = 0
324319, 323syl6eq 2660 . . . . . . . . 9 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → Σ𝑖 ∈ ((3 + 1)...𝑁)((𝑃𝑖)↑2) = 0)
325324oveq2d 6565 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → (1 + Σ𝑖 ∈ ((3 + 1)...𝑁)((𝑃𝑖)↑2)) = (1 + 0))
326287, 325eqtrd 2644 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = (1 + 0))
327326, 215syl6eq 2660 . . . . . 6 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = 1)
3283273adant3 1074 . . . . 5 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = 1)
329223, 277, 3283eqtr4rd 2655 . . . 4 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2))
33044, 54, 55, 329syl3anc 1318 . . 3 ((𝑁 ≠ 3 ∧ (𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2))
331330ex 449 . 2 (𝑁 ≠ 3 → ((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2)))
33243, 331pm2.61ine 2865 1 ((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wo 382  wa 383  w3a 1031   = wceq 1475  wcel 1977  wne 2780  cdif 3537  cun 3538  cin 3539  wss 3540  c0 3874  {csn 4125  cop 4131   class class class wbr 4583   × cxp 5036  cfv 5804  (class class class)co 6549  Fincfn 7841  cc 9813  cr 9814  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953  cle 9954  cmin 10145  -cneg 10146  cn 10897  2c2 10947  3c3 10948  cz 11254  cuz 11563  ...cfz 12197  cexp 12722  Σcsu 14264  𝔼cee 25568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-fz 12198  df-fzo 12335  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-ee 25571
This theorem is referenced by:  axlowdimlem17  25638
  Copyright terms: Public domain W3C validator