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

Theorem axlowdimlem16 25882
 Description: Lemma for axlowdim 25886. 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 12390 . . . . . 6 (𝐼 ∈ (2...2) → 𝐼 = 2)
2 oveq1 6697 . . . . . . . . . . 11 (𝐼 = 2 → (𝐼 + 1) = (2 + 1))
3 df-3 11118 . . . . . . . . . . 11 3 = (2 + 1)
42, 3syl6reqr 2704 . . . . . . . . . 10 (𝐼 = 2 → 3 = (𝐼 + 1))
54, 4oveq12d 6708 . . . . . . . . 9 (𝐼 = 2 → (3...3) = ((𝐼 + 1)...(𝐼 + 1)))
65sumeq1d 14475 . . . . . . . 8 (𝐼 = 2 → Σ𝑖 ∈ (3...3)((𝑄𝑖)↑2) = Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄𝑖)↑2))
72, 3syl6eqr 2703 . . . . . . . . . 10 (𝐼 = 2 → (𝐼 + 1) = 3)
8 3z 11448 . . . . . . . . . 10 3 ∈ ℤ
97, 8syl6eqel 2738 . . . . . . . . 9 (𝐼 = 2 → (𝐼 + 1) ∈ ℤ)
10 ax-1cn 10032 . . . . . . . . . 10 1 ∈ ℂ
1110sqcli 12984 . . . . . . . . 9 (1↑2) ∈ ℂ
12 fveq2 6229 . . . . . . . . . . . 12 (𝑖 = (𝐼 + 1) → (𝑄𝑖) = (𝑄‘(𝐼 + 1)))
13 axlowdimlem16.2 . . . . . . . . . . . . 13 𝑄 = ({⟨(𝐼 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))
1413axlowdimlem11 25877 . . . . . . . . . . . 12 (𝑄‘(𝐼 + 1)) = 1
1512, 14syl6eq 2701 . . . . . . . . . . 11 (𝑖 = (𝐼 + 1) → (𝑄𝑖) = 1)
1615oveq1d 6705 . . . . . . . . . 10 (𝑖 = (𝐼 + 1) → ((𝑄𝑖)↑2) = (1↑2))
1716fsum1 14520 . . . . . . . . 9 (((𝐼 + 1) ∈ ℤ ∧ (1↑2) ∈ ℂ) → Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄𝑖)↑2) = (1↑2))
189, 11, 17sylancl 695 . . . . . . . 8 (𝐼 = 2 → Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄𝑖)↑2) = (1↑2))
196, 18eqtrd 2685 . . . . . . 7 (𝐼 = 2 → Σ𝑖 ∈ (3...3)((𝑄𝑖)↑2) = (1↑2))
20 fveq2 6229 . . . . . . . . . . . 12 (𝑖 = 3 → (𝑃𝑖) = (𝑃‘3))
21 axlowdimlem16.1 . . . . . . . . . . . . 13 𝑃 = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0}))
2221axlowdimlem8 25874 . . . . . . . . . . . 12 (𝑃‘3) = -1
2320, 22syl6eq 2701 . . . . . . . . . . 11 (𝑖 = 3 → (𝑃𝑖) = -1)
2423oveq1d 6705 . . . . . . . . . 10 (𝑖 = 3 → ((𝑃𝑖)↑2) = (-1↑2))
25 sqneg 12963 . . . . . . . . . . 11 (1 ∈ ℂ → (-1↑2) = (1↑2))
2610, 25ax-mp 5 . . . . . . . . . 10 (-1↑2) = (1↑2)
2724, 26syl6eq 2701 . . . . . . . . 9 (𝑖 = 3 → ((𝑃𝑖)↑2) = (1↑2))
2827fsum1 14520 . . . . . . . 8 ((3 ∈ ℤ ∧ (1↑2) ∈ ℂ) → Σ𝑖 ∈ (3...3)((𝑃𝑖)↑2) = (1↑2))
298, 11, 28mp2an 708 . . . . . . 7 Σ𝑖 ∈ (3...3)((𝑃𝑖)↑2) = (1↑2)
3019, 29syl6reqr 2704 . . . . . 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 6697 . . . . . . 7 (𝑁 = 3 → (𝑁 − 1) = (3 − 1))
34 3m1e2 11175 . . . . . . 7 (3 − 1) = 2
3533, 34syl6eq 2701 . . . . . 6 (𝑁 = 3 → (𝑁 − 1) = 2)
3635oveq2d 6706 . . . . 5 (𝑁 = 3 → (2...(𝑁 − 1)) = (2...2))
3736eleq2d 2716 . . . 4 (𝑁 = 3 → (𝐼 ∈ (2...(𝑁 − 1)) ↔ 𝐼 ∈ (2...2)))
38 oveq2 6698 . . . . . 6 (𝑁 = 3 → (3...𝑁) = (3...3))
3938sumeq1d 14475 . . . . 5 (𝑁 = 3 → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...3)((𝑃𝑖)↑2))
4038sumeq1d 14475 . . . . 5 (𝑁 = 3 → Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2) = Σ𝑖 ∈ (3...3)((𝑄𝑖)↑2))
4139, 40eqeq12d 2666 . . . 4 (𝑁 = 3 → (Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2) ↔ Σ𝑖 ∈ (3...3)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...3)((𝑄𝑖)↑2)))
4232, 37, 413imtr4d 283 . . 3 (𝑁 = 3 → (𝐼 ∈ (2...(𝑁 − 1)) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2)))
4342adantld 482 . 2 (𝑁 = 3 → ((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2)))
44 simprl 809 . . . 4 ((𝑁 ≠ 3 ∧ (𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈ (ℤ‘3))
45 eluzle 11738 . . . . . . 7 (𝑁 ∈ (ℤ‘3) → 3 ≤ 𝑁)
4645adantl 481 . . . . . 6 ((𝑁 ≠ 3 ∧ 𝑁 ∈ (ℤ‘3)) → 3 ≤ 𝑁)
47 simpl 472 . . . . . 6 ((𝑁 ≠ 3 ∧ 𝑁 ∈ (ℤ‘3)) → 𝑁 ≠ 3)
48 3re 11132 . . . . . . 7 3 ∈ ℝ
49 eluzelre 11736 . . . . . . . 8 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℝ)
5049adantl 481 . . . . . . 7 ((𝑁 ≠ 3 ∧ 𝑁 ∈ (ℤ‘3)) → 𝑁 ∈ ℝ)
51 ltlen 10176 . . . . . . 7 ((3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (3 < 𝑁 ↔ (3 ≤ 𝑁𝑁 ≠ 3)))
5248, 50, 51sylancr 696 . . . . . 6 ((𝑁 ≠ 3 ∧ 𝑁 ∈ (ℤ‘3)) → (3 < 𝑁 ↔ (3 ≤ 𝑁𝑁 ≠ 3)))
5346, 47, 52mpbir2and 977 . . . . 5 ((𝑁 ≠ 3 ∧ 𝑁 ∈ (ℤ‘3)) → 3 < 𝑁)
5453adantrr 753 . . . 4 ((𝑁 ≠ 3 ∧ (𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 3 < 𝑁)
55 simprr 811 . . . 4 ((𝑁 ≠ 3 ∧ (𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ∈ (2...(𝑁 − 1)))
56 fzssp1 12422 . . . . . . . . . . . . 13 (2...(𝑁 − 1)) ⊆ (2...((𝑁 − 1) + 1))
57 simp3 1083 . . . . . . . . . . . . 13 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ (2...(𝑁 − 1)))
5856, 57sseldi 3634 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ (2...((𝑁 − 1) + 1)))
59 eluzelz 11735 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℤ)
60593ad2ant1 1102 . . . . . . . . . . . . . . 15 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℤ)
6160zcnd 11521 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℂ)
62 npcan 10328 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
6361, 10, 62sylancl 695 . . . . . . . . . . . . 13 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
6463oveq2d 6706 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (2...((𝑁 − 1) + 1)) = (2...𝑁))
6558, 64eleqtrd 2732 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ (2...𝑁))
66 elfzelz 12380 . . . . . . . . . . 11 (𝐼 ∈ (2...𝑁) → 𝐼 ∈ ℤ)
6765, 66syl 17 . . . . . . . . . 10 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ ℤ)
6867zred 11520 . . . . . . . . 9 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ ℝ)
6968ltp1d 10992 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 < (𝐼 + 1))
70 fzdisj 12406 . . . . . . . 8 (𝐼 < (𝐼 + 1) → ((2...𝐼) ∩ ((𝐼 + 1)...𝑁)) = ∅)
7169, 70syl 17 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → ((2...𝐼) ∩ ((𝐼 + 1)...𝑁)) = ∅)
72 fzsplit 12405 . . . . . . . 8 (𝐼 ∈ (2...𝑁) → (2...𝑁) = ((2...𝐼) ∪ ((𝐼 + 1)...𝑁)))
7365, 72syl 17 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (2...𝑁) = ((2...𝐼) ∪ ((𝐼 + 1)...𝑁)))
74 fzfid 12812 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (2...𝑁) ∈ Fin)
75 eluzge3nn 11768 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℕ)
76 2eluzge1 11772 . . . . . . . . . . . . 13 2 ∈ (ℤ‘1)
77 fzss1 12418 . . . . . . . . . . . . 13 (2 ∈ (ℤ‘1) → (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1)))
7876, 77ax-mp 5 . . . . . . . . . . . 12 (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1))
7978sseli 3632 . . . . . . . . . . 11 (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ∈ (1...(𝑁 − 1)))
8013axlowdimlem10 25876 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 𝑄 ∈ (𝔼‘𝑁))
8175, 79, 80syl2an 493 . . . . . . . . . 10 ((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑄 ∈ (𝔼‘𝑁))
82 fzss1 12418 . . . . . . . . . . . 12 (2 ∈ (ℤ‘1) → (2...𝑁) ⊆ (1...𝑁))
8376, 82ax-mp 5 . . . . . . . . . . 11 (2...𝑁) ⊆ (1...𝑁)
8483sseli 3632 . . . . . . . . . 10 (𝑖 ∈ (2...𝑁) → 𝑖 ∈ (1...𝑁))
85 fveecn 25827 . . . . . . . . . 10 ((𝑄 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑄𝑖) ∈ ℂ)
8681, 84, 85syl2an 493 . . . . . . . . 9 (((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝑁)) → (𝑄𝑖) ∈ ℂ)
8786sqcld 13046 . . . . . . . 8 (((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝑁)) → ((𝑄𝑖)↑2) ∈ ℂ)
88873adantl2 1238 . . . . . . 7 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝑁)) → ((𝑄𝑖)↑2) ∈ ℂ)
8971, 73, 74, 88fsumsplit 14515 . . . . . 6 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (2...𝑁)((𝑄𝑖)↑2) = (Σ𝑖 ∈ (2...𝐼)((𝑄𝑖)↑2) + Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2)))
90 fzss1 12418 . . . . . . . . . . . . . . . 16 (2 ∈ (ℤ‘1) → (2...𝐼) ⊆ (1...𝐼))
9176, 90ax-mp 5 . . . . . . . . . . . . . . 15 (2...𝐼) ⊆ (1...𝐼)
9291sseli 3632 . . . . . . . . . . . . . 14 (𝑖 ∈ (2...𝐼) → 𝑖 ∈ (1...𝐼))
93 elfzelz 12380 . . . . . . . . . . . . . . . . . . . 20 (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ∈ ℤ)
9493zred 11520 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ∈ ℝ)
95943ad2ant3 1104 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ ℝ)
96493ad2ant1 1102 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℝ)
97 peano2rem 10386 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
9896, 97syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
99 elfzle2 12383 . . . . . . . . . . . . . . . . . . . 20 (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ≤ (𝑁 − 1))
100993ad2ant3 1104 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ≤ (𝑁 − 1))
10196ltm1d 10994 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
10295, 98, 96, 100, 101lelttrd 10233 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 < 𝑁)
10395, 96, 102ltled 10223 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼𝑁)
104933ad2ant3 1104 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝐼 ∈ ℤ)
105 eluz 11739 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ𝐼) ↔ 𝐼𝑁))
106104, 60, 105syl2anc 694 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝑁 ∈ (ℤ𝐼) ↔ 𝐼𝑁))
107103, 106mpbird 247 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ (ℤ𝐼))
108 fzss2 12419 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝐼) → (1...𝐼) ⊆ (1...𝑁))
109107, 108syl 17 . . . . . . . . . . . . . . 15 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (1...𝐼) ⊆ (1...𝑁))
110109sseld 3635 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝑖 ∈ (1...𝐼) → 𝑖 ∈ (1...𝑁)))
11192, 110syl5 34 . . . . . . . . . . . . 13 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝑖 ∈ (2...𝐼) → 𝑖 ∈ (1...𝑁)))
112111imp 444 . . . . . . . . . . . 12 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝑖 ∈ (1...𝑁))
113 elfzelz 12380 . . . . . . . . . . . . . . 15 (𝑖 ∈ (2...𝐼) → 𝑖 ∈ ℤ)
114113zred 11520 . . . . . . . . . . . . . 14 (𝑖 ∈ (2...𝐼) → 𝑖 ∈ ℝ)
115114adantl 481 . . . . . . . . . . . . 13 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝑖 ∈ ℝ)
11695adantr 480 . . . . . . . . . . . . . 14 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝐼 ∈ ℝ)
117 peano2re 10247 . . . . . . . . . . . . . . . . 17 (𝐼 ∈ ℝ → (𝐼 + 1) ∈ ℝ)
11894, 117syl 17 . . . . . . . . . . . . . . . 16 (𝐼 ∈ (2...(𝑁 − 1)) → (𝐼 + 1) ∈ ℝ)
1191183ad2ant3 1104 . . . . . . . . . . . . . . 15 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝐼 + 1) ∈ ℝ)
120119adantr 480 . . . . . . . . . . . . . 14 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → (𝐼 + 1) ∈ ℝ)
121 elfzle2 12383 . . . . . . . . . . . . . . 15 (𝑖 ∈ (2...𝐼) → 𝑖𝐼)
122121adantl 481 . . . . . . . . . . . . . 14 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝑖𝐼)
123116ltp1d 10992 . . . . . . . . . . . . . 14 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝐼 < (𝐼 + 1))
124115, 116, 120, 122, 123lelttrd 10233 . . . . . . . . . . . . 13 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝑖 < (𝐼 + 1))
125115, 124ltned 10211 . . . . . . . . . . . 12 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → 𝑖 ≠ (𝐼 + 1))
12613axlowdimlem12 25878 . . . . . . . . . . . 12 ((𝑖 ∈ (1...𝑁) ∧ 𝑖 ≠ (𝐼 + 1)) → (𝑄𝑖) = 0)
127112, 125, 126syl2anc 694 . . . . . . . . . . 11 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → (𝑄𝑖) = 0)
128127sq0id 12997 . . . . . . . . . 10 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (2...𝐼)) → ((𝑄𝑖)↑2) = 0)
129128sumeq2dv 14477 . . . . . . . . 9 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (2...𝐼)((𝑄𝑖)↑2) = Σ𝑖 ∈ (2...𝐼)0)
130 fzfi 12811 . . . . . . . . . . 11 (2...𝐼) ∈ Fin
131130olci 405 . . . . . . . . . 10 ((2...𝐼) ⊆ (ℤ‘1) ∨ (2...𝐼) ∈ Fin)
132 sumz 14497 . . . . . . . . . 10 (((2...𝐼) ⊆ (ℤ‘1) ∨ (2...𝐼) ∈ Fin) → Σ𝑖 ∈ (2...𝐼)0 = 0)
133131, 132ax-mp 5 . . . . . . . . 9 Σ𝑖 ∈ (2...𝐼)0 = 0
134129, 133syl6eq 2701 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (2...𝐼)((𝑄𝑖)↑2) = 0)
135104peano2zd 11523 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝐼 + 1) ∈ ℤ)
136 sq1 12998 . . . . . . . . . . . . 13 (1↑2) = 1
13716, 136syl6eq 2701 . . . . . . . . . . . 12 (𝑖 = (𝐼 + 1) → ((𝑄𝑖)↑2) = 1)
138137fsum1 14520 . . . . . . . . . . 11 (((𝐼 + 1) ∈ ℤ ∧ 1 ∈ ℂ) → Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄𝑖)↑2) = 1)
139135, 10, 138sylancl 695 . . . . . . . . . 10 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄𝑖)↑2) = 1)
140 oveq2 6698 . . . . . . . . . . . 12 ((𝐼 + 1) = 𝑁 → ((𝐼 + 1)...(𝐼 + 1)) = ((𝐼 + 1)...𝑁))
141140sumeq1d 14475 . . . . . . . . . . 11 ((𝐼 + 1) = 𝑁 → Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄𝑖)↑2) = Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2))
142141eqeq1d 2653 . . . . . . . . . 10 ((𝐼 + 1) = 𝑁 → (Σ𝑖 ∈ ((𝐼 + 1)...(𝐼 + 1))((𝑄𝑖)↑2) = 1 ↔ Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2) = 1))
143139, 142syl5ib 234 . . . . . . . . 9 ((𝐼 + 1) = 𝑁 → ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2) = 1))
144104adantl 481 . . . . . . . . . . . . . . . 16 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ∈ ℤ)
145144zred 11520 . . . . . . . . . . . . . . 15 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ∈ ℝ)
14660adantl 481 . . . . . . . . . . . . . . . . 17 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈ ℤ)
147146zred 11520 . . . . . . . . . . . . . . . 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 10994 . . . . . . . . . . . . . . 15 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝑁 − 1) < 𝑁)
151145, 148, 147, 149, 150lelttrd 10233 . . . . . . . . . . . . . 14 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 < 𝑁)
152 1red 10093 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ (2...(𝑁 − 1)) → 1 ∈ ℝ)
153 2re 11128 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
154153a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ (2...(𝑁 − 1)) → 2 ∈ ℝ)
155 1le2 11279 . . . . . . . . . . . . . . . . . . . 20 1 ≤ 2
156155a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ (2...(𝑁 − 1)) → 1 ≤ 2)
157 elfzle1 12382 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ (2...(𝑁 − 1)) → 2 ≤ 𝐼)
158152, 154, 94, 156, 157letrd 10232 . . . . . . . . . . . . . . . . . 18 (𝐼 ∈ (2...(𝑁 − 1)) → 1 ≤ 𝐼)
1591583ad2ant3 1104 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 1 ≤ 𝐼)
160159adantl 481 . . . . . . . . . . . . . . . 16 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 1 ≤ 𝐼)
161 elnnz1 11441 . . . . . . . . . . . . . . . 16 (𝐼 ∈ ℕ ↔ (𝐼 ∈ ℤ ∧ 1 ≤ 𝐼))
162144, 160, 161sylanbrc 699 . . . . . . . . . . . . . . 15 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ∈ ℕ)
163753ad2ant1 1102 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℕ)
164163adantl 481 . . . . . . . . . . . . . . 15 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈ ℕ)
165 nnltp1le 11471 . . . . . . . . . . . . . . 15 ((𝐼 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐼 < 𝑁 ↔ (𝐼 + 1) ≤ 𝑁))
166162, 164, 165syl2anc 694 . . . . . . . . . . . . . 14 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 < 𝑁 ↔ (𝐼 + 1) ≤ 𝑁))
167151, 166mpbid 222 . . . . . . . . . . . . 13 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 + 1) ≤ 𝑁)
168135adantl 481 . . . . . . . . . . . . . 14 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 + 1) ∈ ℤ)
169 eluz 11739 . . . . . . . . . . . . . 14 (((𝐼 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ‘(𝐼 + 1)) ↔ (𝐼 + 1) ≤ 𝑁))
170168, 146, 169syl2anc 694 . . . . . . . . . . . . 13 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝑁 ∈ (ℤ‘(𝐼 + 1)) ↔ (𝐼 + 1) ≤ 𝑁))
171167, 170mpbird 247 . . . . . . . . . . . 12 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈ (ℤ‘(𝐼 + 1)))
172 simpr1 1087 . . . . . . . . . . . . . . . 16 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝑁 ∈ (ℤ‘3))
173 simpr3 1089 . . . . . . . . . . . . . . . 16 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝐼 ∈ (2...(𝑁 − 1)))
174172, 173, 81syl2anc 694 . . . . . . . . . . . . . . 15 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → 𝑄 ∈ (𝔼‘𝑁))
175174adantr 480 . . . . . . . . . . . . . 14 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ ((𝐼 + 1)...𝑁)) → 𝑄 ∈ (𝔼‘𝑁))
176162peano2nnd 11075 . . . . . . . . . . . . . . . . 17 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 + 1) ∈ ℕ)
177 nnuz 11761 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
178176, 177syl6eleq 2740 . . . . . . . . . . . . . . . 16 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (𝐼 + 1) ∈ (ℤ‘1))
179 fzss1 12418 . . . . . . . . . . . . . . . 16 ((𝐼 + 1) ∈ (ℤ‘1) → ((𝐼 + 1)...𝑁) ⊆ (1...𝑁))
180178, 179syl 17 . . . . . . . . . . . . . . 15 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → ((𝐼 + 1)...𝑁) ⊆ (1...𝑁))
181180sselda 3636 . . . . . . . . . . . . . 14 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ ((𝐼 + 1)...𝑁)) → 𝑖 ∈ (1...𝑁))
182175, 181, 85syl2anc 694 . . . . . . . . . . . . 13 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ ((𝐼 + 1)...𝑁)) → (𝑄𝑖) ∈ ℂ)
183182sqcld 13046 . . . . . . . . . . . 12 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ ((𝐼 + 1)...𝑁)) → ((𝑄𝑖)↑2) ∈ ℂ)
18412oveq1d 6705 . . . . . . . . . . . . 13 (𝑖 = (𝐼 + 1) → ((𝑄𝑖)↑2) = ((𝑄‘(𝐼 + 1))↑2))
18514oveq1i 6700 . . . . . . . . . . . . . 14 ((𝑄‘(𝐼 + 1))↑2) = (1↑2)
186185, 136eqtri 2673 . . . . . . . . . . . . 13 ((𝑄‘(𝐼 + 1))↑2) = 1
187184, 186syl6eq 2701 . . . . . . . . . . . 12 (𝑖 = (𝐼 + 1) → ((𝑄𝑖)↑2) = 1)
188171, 183, 187fsum1p 14526 . . . . . . . . . . 11 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2) = (1 + Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)((𝑄𝑖)↑2)))
189176peano2nnd 11075 . . . . . . . . . . . . . . . . . . . 20 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → ((𝐼 + 1) + 1) ∈ ℕ)
190189, 177syl6eleq 2740 . . . . . . . . . . . . . . . . . . 19 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → ((𝐼 + 1) + 1) ∈ (ℤ‘1))
191 fzss1 12418 . . . . . . . . . . . . . . . . . . 19 (((𝐼 + 1) + 1) ∈ (ℤ‘1) → (((𝐼 + 1) + 1)...𝑁) ⊆ (1...𝑁))
192190, 191syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (((𝐼 + 1) + 1)...𝑁) ⊆ (1...𝑁))
193192sselda 3636 . . . . . . . . . . . . . . . . 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 10247 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 + 1) ∈ ℝ → ((𝐼 + 1) + 1) ∈ ℝ)
197195, 196syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → ((𝐼 + 1) + 1) ∈ ℝ)
198 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (((𝐼 + 1) + 1)...𝑁) → 𝑖 ∈ ℤ)
199198zred 11520 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (((𝐼 + 1) + 1)...𝑁) → 𝑖 ∈ ℝ)
200199adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → 𝑖 ∈ ℝ)
201195ltp1d 10992 . . . . . . . . . . . . . . . . . . 19 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → (𝐼 + 1) < ((𝐼 + 1) + 1))
202 elfzle1 12382 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (((𝐼 + 1) + 1)...𝑁) → ((𝐼 + 1) + 1) ≤ 𝑖)
203202adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → ((𝐼 + 1) + 1) ≤ 𝑖)
204195, 197, 200, 201, 203ltletrd 10235 . . . . . . . . . . . . . . . . . 18 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → (𝐼 + 1) < 𝑖)
205195, 204gtned 10210 . . . . . . . . . . . . . . . . 17 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → 𝑖 ≠ (𝐼 + 1))
206193, 205, 126syl2anc 694 . . . . . . . . . . . . . . . 16 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → (𝑄𝑖) = 0)
207206sq0id 12997 . . . . . . . . . . . . . . 15 ((((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) ∧ 𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)) → ((𝑄𝑖)↑2) = 0)
208207sumeq2dv 14477 . . . . . . . . . . . . . 14 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)((𝑄𝑖)↑2) = Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)0)
209 fzfi 12811 . . . . . . . . . . . . . . . 16 (((𝐼 + 1) + 1)...𝑁) ∈ Fin
210209olci 405 . . . . . . . . . . . . . . 15 ((((𝐼 + 1) + 1)...𝑁) ⊆ (ℤ‘1) ∨ (((𝐼 + 1) + 1)...𝑁) ∈ Fin)
211 sumz 14497 . . . . . . . . . . . . . . 15 (((((𝐼 + 1) + 1)...𝑁) ⊆ (ℤ‘1) ∨ (((𝐼 + 1) + 1)...𝑁) ∈ Fin) → Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)0 = 0)
212210, 211ax-mp 5 . . . . . . . . . . . . . 14 Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)0 = 0
213208, 212syl6eq 2701 . . . . . . . . . . . . 13 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)((𝑄𝑖)↑2) = 0)
214213oveq2d 6706 . . . . . . . . . . . 12 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (1 + Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)((𝑄𝑖)↑2)) = (1 + 0))
215 1p0e1 11171 . . . . . . . . . . . 12 (1 + 0) = 1
216214, 215syl6eq 2701 . . . . . . . . . . 11 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → (1 + Σ𝑖 ∈ (((𝐼 + 1) + 1)...𝑁)((𝑄𝑖)↑2)) = 1)
217188, 216eqtrd 2685 . . . . . . . . . 10 (((𝐼 + 1) ≠ 𝑁 ∧ (𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1)))) → Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2) = 1)
218217ex 449 . . . . . . . . 9 ((𝐼 + 1) ≠ 𝑁 → ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2) = 1))
219143, 218pm2.61ine 2906 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2) = 1)
220134, 219oveq12d 6708 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (Σ𝑖 ∈ (2...𝐼)((𝑄𝑖)↑2) + Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2)) = (0 + 1))
221 0p1e1 11170 . . . . . . 7 (0 + 1) = 1
222220, 221syl6eq 2701 . . . . . 6 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (Σ𝑖 ∈ (2...𝐼)((𝑄𝑖)↑2) + Σ𝑖 ∈ ((𝐼 + 1)...𝑁)((𝑄𝑖)↑2)) = 1)
22389, 222eqtrd 2685 . . . . 5 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (2...𝑁)((𝑄𝑖)↑2) = 1)
224 simp1 1081 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘3))
225 2lt3 11233 . . . . . . . . . 10 2 < 3
226153, 48, 225ltleii 10198 . . . . . . . . 9 2 ≤ 3
227 2z 11447 . . . . . . . . . 10 2 ∈ ℤ
228227eluz1i 11733 . . . . . . . . 9 (3 ∈ (ℤ‘2) ↔ (3 ∈ ℤ ∧ 2 ≤ 3))
2298, 226, 228mpbir2an 975 . . . . . . . 8 3 ∈ (ℤ‘2)
230 uztrn 11742 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 ∈ (ℤ‘2)) → 𝑁 ∈ (ℤ‘2))
231224, 229, 230sylancl 695 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘2))
232 fveq2 6229 . . . . . . . 8 (𝑖 = 2 → (𝑄𝑖) = (𝑄‘2))
233232oveq1d 6705 . . . . . . 7 (𝑖 = 2 → ((𝑄𝑖)↑2) = ((𝑄‘2)↑2))
234231, 88, 233fsum1p 14526 . . . . . 6 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (2...𝑁)((𝑄𝑖)↑2) = (((𝑄‘2)↑2) + Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄𝑖)↑2)))
23559adantr 480 . . . . . . . . . . . . . . 15 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → 𝑁 ∈ ℤ)
236235zred 11520 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → 𝑁 ∈ ℝ)
237 lttr 10152 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((2 < 3 ∧ 3 < 𝑁) → 2 < 𝑁))
238153, 48, 237mp3an12 1454 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℝ → ((2 < 3 ∧ 3 < 𝑁) → 2 < 𝑁))
239225, 238mpani 712 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℝ → (3 < 𝑁 → 2 < 𝑁))
24049, 239syl 17 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ‘3) → (3 < 𝑁 → 2 < 𝑁))
241240imp 444 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → 2 < 𝑁)
242 ltle 10164 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 < 𝑁 → 2 ≤ 𝑁))
243153, 242mpan 706 . . . . . . . . . . . . . 14 (𝑁 ∈ ℝ → (2 < 𝑁 → 2 ≤ 𝑁))
244236, 241, 243sylc 65 . . . . . . . . . . . . 13 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → 2 ≤ 𝑁)
245244, 155jctil 559 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → (1 ≤ 2 ∧ 2 ≤ 𝑁))
246 1z 11445 . . . . . . . . . . . . . 14 1 ∈ ℤ
247 elfz 12370 . . . . . . . . . . . . . 14 ((2 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 ∈ (1...𝑁) ↔ (1 ≤ 2 ∧ 2 ≤ 𝑁)))
248227, 246, 247mp3an12 1454 . . . . . . . . . . . . 13 (𝑁 ∈ ℤ → (2 ∈ (1...𝑁) ↔ (1 ≤ 2 ∧ 2 ≤ 𝑁)))
249235, 248syl 17 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → (2 ∈ (1...𝑁) ↔ (1 ≤ 2 ∧ 2 ≤ 𝑁)))
250245, 249mpbird 247 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → 2 ∈ (1...𝑁))
2512503adant3 1101 . . . . . . . . . 10 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 2 ∈ (1...𝑁))
25294ltp1d 10992 . . . . . . . . . . . . . 14 (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 < (𝐼 + 1))
253154, 94, 118, 157, 252lelttrd 10233 . . . . . . . . . . . . 13 (𝐼 ∈ (2...(𝑁 − 1)) → 2 < (𝐼 + 1))
2542533ad2ant3 1104 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 2 < (𝐼 + 1))
255 ltne 10172 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ 2 < (𝐼 + 1)) → (𝐼 + 1) ≠ 2)
256153, 254, 255sylancr 696 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝐼 + 1) ≠ 2)
257256necomd 2878 . . . . . . . . . 10 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → 2 ≠ (𝐼 + 1))
25813axlowdimlem12 25878 . . . . . . . . . 10 ((2 ∈ (1...𝑁) ∧ 2 ≠ (𝐼 + 1)) → (𝑄‘2) = 0)
259251, 257, 258syl2anc 694 . . . . . . . . 9 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (𝑄‘2) = 0)
260259sq0id 12997 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → ((𝑄‘2)↑2) = 0)
261260oveq1d 6705 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (((𝑄‘2)↑2) + Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄𝑖)↑2)) = (0 + Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄𝑖)↑2)))
2623oveq1i 6700 . . . . . . . . 9 (3...𝑁) = ((2 + 1)...𝑁)
263262sumeq1i 14472 . . . . . . . 8 Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2) = Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄𝑖)↑2)
264263oveq2i 6701 . . . . . . 7 (0 + Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2)) = (0 + Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄𝑖)↑2))
265261, 264syl6eqr 2703 . . . . . 6 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (((𝑄‘2)↑2) + Σ𝑖 ∈ ((2 + 1)...𝑁)((𝑄𝑖)↑2)) = (0 + Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2)))
266 fzfid 12812 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (3...𝑁) ∈ Fin)
267 3nn 11224 . . . . . . . . . . . . . 14 3 ∈ ℕ
268267, 177eleqtri 2728 . . . . . . . . . . . . 13 3 ∈ (ℤ‘1)
269 fzss1 12418 . . . . . . . . . . . . 13 (3 ∈ (ℤ‘1) → (3...𝑁) ⊆ (1...𝑁))
270268, 269ax-mp 5 . . . . . . . . . . . 12 (3...𝑁) ⊆ (1...𝑁)
271270sseli 3632 . . . . . . . . . . 11 (𝑖 ∈ (3...𝑁) → 𝑖 ∈ (1...𝑁))
27281, 271, 85syl2an 493 . . . . . . . . . 10 (((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → (𝑄𝑖) ∈ ℂ)
273272sqcld 13046 . . . . . . . . 9 (((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑄𝑖)↑2) ∈ ℂ)
2742733adantl2 1238 . . . . . . . 8 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑄𝑖)↑2) ∈ ℂ)
275266, 274fsumcl 14508 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2) ∈ ℂ)
276275addid2d 10275 . . . . . 6 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → (0 + Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2)) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2))
277234, 265, 2763eqtrrd 2690 . . . . 5 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2) = Σ𝑖 ∈ (2...𝑁)((𝑄𝑖)↑2))
278 simpl 472 . . . . . . . . 9 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → 𝑁 ∈ (ℤ‘3))
27921axlowdimlem7 25873 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘3) → 𝑃 ∈ (𝔼‘𝑁))
280279ad2antrr 762 . . . . . . . . . . 11 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ (3...𝑁)) → 𝑃 ∈ (𝔼‘𝑁))
281271adantl 481 . . . . . . . . . . 11 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ (3...𝑁)) → 𝑖 ∈ (1...𝑁))
282 fveecn 25827 . . . . . . . . . . 11 ((𝑃 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑃𝑖) ∈ ℂ)
283280, 281, 282syl2anc 694 . . . . . . . . . 10 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ (3...𝑁)) → (𝑃𝑖) ∈ ℂ)
284283sqcld 13046 . . . . . . . . 9 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑃𝑖)↑2) ∈ ℂ)
285 neg1sqe1 12999 . . . . . . . . . 10 (-1↑2) = 1
28624, 285syl6eq 2701 . . . . . . . . 9 (𝑖 = 3 → ((𝑃𝑖)↑2) = 1)
287278, 284, 286fsum1p 14526 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = (1 + Σ𝑖 ∈ ((3 + 1)...𝑁)((𝑃𝑖)↑2)))
288 1re 10077 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
289 zaddcl 11455 . . . . . . . . . . . . . . . . . . . 20 ((3 ∈ ℤ ∧ 1 ∈ ℤ) → (3 + 1) ∈ ℤ)
2908, 246, 289mp2an 708 . . . . . . . . . . . . . . . . . . 19 (3 + 1) ∈ ℤ
291290zrei 11421 . . . . . . . . . . . . . . . . . 18 (3 + 1) ∈ ℝ
292 1lt3 11234 . . . . . . . . . . . . . . . . . . 19 1 < 3
29348ltp1i 10965 . . . . . . . . . . . . . . . . . . 19 3 < (3 + 1)
294288, 48, 291lttri 10201 . . . . . . . . . . . . . . . . . . 19 ((1 < 3 ∧ 3 < (3 + 1)) → 1 < (3 + 1))
295292, 293, 294mp2an 708 . . . . . . . . . . . . . . . . . 18 1 < (3 + 1)
296288, 291, 295ltleii 10198 . . . . . . . . . . . . . . . . 17 1 ≤ (3 + 1)
297 eluz 11739 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℤ ∧ (3 + 1) ∈ ℤ) → ((3 + 1) ∈ (ℤ‘1) ↔ 1 ≤ (3 + 1)))
298246, 290, 297mp2an 708 . . . . . . . . . . . . . . . . 17 ((3 + 1) ∈ (ℤ‘1) ↔ 1 ≤ (3 + 1))
299296, 298mpbir 221 . . . . . . . . . . . . . . . 16 (3 + 1) ∈ (ℤ‘1)
300 fzss1 12418 . . . . . . . . . . . . . . . 16 ((3 + 1) ∈ (ℤ‘1) → ((3 + 1)...𝑁) ⊆ (1...𝑁))
301299, 300ax-mp 5 . . . . . . . . . . . . . . 15 ((3 + 1)...𝑁) ⊆ (1...𝑁)
302301sseli 3632 . . . . . . . . . . . . . 14 (𝑖 ∈ ((3 + 1)...𝑁) → 𝑖 ∈ (1...𝑁))
303302adantl 481 . . . . . . . . . . . . 13 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ ((3 + 1)...𝑁)) → 𝑖 ∈ (1...𝑁))
30448, 291ltnlei 10196 . . . . . . . . . . . . . . . . . . 19 (3 < (3 + 1) ↔ ¬ (3 + 1) ≤ 3)
305293, 304mpbi 220 . . . . . . . . . . . . . . . . . 18 ¬ (3 + 1) ≤ 3
306305intnanr 981 . . . . . . . . . . . . . . . . 17 ¬ ((3 + 1) ≤ 3 ∧ 3 ≤ 𝑁)
307 elfz 12370 . . . . . . . . . . . . . . . . . . 19 ((3 ∈ ℤ ∧ (3 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (3 ∈ ((3 + 1)...𝑁) ↔ ((3 + 1) ≤ 3 ∧ 3 ≤ 𝑁)))
3088, 290, 307mp3an12 1454 . . . . . . . . . . . . . . . . . 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 2718 . . . . . . . . . . . . . . . . 17 (𝑖 = 3 → (𝑖 ∈ ((3 + 1)...𝑁) ↔ 3 ∈ ((3 + 1)...𝑁)))
312311notbid 307 . . . . . . . . . . . . . . . 16 (𝑖 = 3 → (¬ 𝑖 ∈ ((3 + 1)...𝑁) ↔ ¬ 3 ∈ ((3 + 1)...𝑁)))
313310, 312syl5ibrcom 237 . . . . . . . . . . . . . . 15 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → (𝑖 = 3 → ¬ 𝑖 ∈ ((3 + 1)...𝑁)))
314313necon2ad 2838 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → (𝑖 ∈ ((3 + 1)...𝑁) → 𝑖 ≠ 3))
315314imp 444 . . . . . . . . . . . . 13 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ ((3 + 1)...𝑁)) → 𝑖 ≠ 3)
31621axlowdimlem9 25875 . . . . . . . . . . . . 13 ((𝑖 ∈ (1...𝑁) ∧ 𝑖 ≠ 3) → (𝑃𝑖) = 0)
317303, 315, 316syl2anc 694 . . . . . . . . . . . 12 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ ((3 + 1)...𝑁)) → (𝑃𝑖) = 0)
318317sq0id 12997 . . . . . . . . . . 11 (((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) ∧ 𝑖 ∈ ((3 + 1)...𝑁)) → ((𝑃𝑖)↑2) = 0)
319318sumeq2dv 14477 . . . . . . . . . 10 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → Σ𝑖 ∈ ((3 + 1)...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ ((3 + 1)...𝑁)0)
320 fzfi 12811 . . . . . . . . . . . 12 ((3 + 1)...𝑁) ∈ Fin
321320olci 405 . . . . . . . . . . 11 (((3 + 1)...𝑁) ⊆ (ℤ‘1) ∨ ((3 + 1)...𝑁) ∈ Fin)
322 sumz 14497 . . . . . . . . . . 11 ((((3 + 1)...𝑁) ⊆ (ℤ‘1) ∨ ((3 + 1)...𝑁) ∈ Fin) → Σ𝑖 ∈ ((3 + 1)...𝑁)0 = 0)
323321, 322ax-mp 5 . . . . . . . . . 10 Σ𝑖 ∈ ((3 + 1)...𝑁)0 = 0
324319, 323syl6eq 2701 . . . . . . . . 9 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → Σ𝑖 ∈ ((3 + 1)...𝑁)((𝑃𝑖)↑2) = 0)
325324oveq2d 6706 . . . . . . . 8 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → (1 + Σ𝑖 ∈ ((3 + 1)...𝑁)((𝑃𝑖)↑2)) = (1 + 0))
326287, 325eqtrd 2685 . . . . . . 7 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = (1 + 0))
327326, 215syl6eq 2701 . . . . . 6 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = 1)
3283273adant3 1101 . . . . 5 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = 1)
329223, 277, 3283eqtr4rd 2696 . . . 4 ((𝑁 ∈ (ℤ‘3) ∧ 3 < 𝑁𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2))
33044, 54, 55, 329syl3anc 1366 . . 3 ((𝑁 ≠ 3 ∧ (𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1)))) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2))
331330ex 449 . 2 (𝑁 ≠ 3 → ((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2)))
33243, 331pm2.61ine 2906 1 ((𝑁 ∈ (ℤ‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄𝑖)↑2))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823   ∖ cdif 3604   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  {csn 4210  ⟨cop 4216   class class class wbr 4685   × cxp 5141  ‘cfv 5926  (class class class)co 6690  Fincfn 7997  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   < clt 10112   ≤ cle 10113   − cmin 10304  -cneg 10305  ℕcn 11058  2c2 11108  3c3 11109  ℤcz 11415  ℤ≥cuz 11725  ...cfz 12364  ↑cexp 12900  Σcsu 14460  𝔼cee 25813 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-ee 25816 This theorem is referenced by:  axlowdimlem17  25883
 Copyright terms: Public domain W3C validator