Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sumnnodd Structured version   Visualization version   GIF version

Theorem sumnnodd 44333
Description: A series indexed by β„• with only odd terms. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
sumnnodd.1 (πœ‘ β†’ 𝐹:β„•βŸΆβ„‚)
sumnnodd.even0 ((πœ‘ ∧ π‘˜ ∈ β„• ∧ (π‘˜ / 2) ∈ β„•) β†’ (πΉβ€˜π‘˜) = 0)
sumnnodd.sc (πœ‘ β†’ seq1( + , 𝐹) ⇝ 𝐡)
Assertion
Ref Expression
sumnnodd (πœ‘ β†’ (seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))) ⇝ 𝐡 ∧ Ξ£π‘˜ ∈ β„• (πΉβ€˜π‘˜) = Ξ£π‘˜ ∈ β„• (πΉβ€˜((2 Β· π‘˜) βˆ’ 1))))
Distinct variable groups:   π‘˜,𝐹   πœ‘,π‘˜
Allowed substitution hint:   𝐡(π‘˜)

Proof of Theorem sumnnodd
Dummy variables 𝐢 𝑗 𝑖 𝑛 π‘š π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1918 . . 3 β„²π‘˜πœ‘
2 nfcv 2904 . . 3 β„²π‘˜seq1( + , 𝐹)
3 nfcv 2904 . . . 4 β„²π‘˜1
4 nfcv 2904 . . . 4 β„²π‘˜ +
5 nfmpt1 5256 . . . 4 β„²π‘˜(π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))
63, 4, 5nfseq 13973 . . 3 β„²π‘˜seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1))))
7 nfmpt1 5256 . . 3 β„²π‘˜(π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))
8 nnuz 12862 . . 3 β„• = (β„€β‰₯β€˜1)
9 1zzd 12590 . . 3 (πœ‘ β†’ 1 ∈ β„€)
10 seqex 13965 . . . 4 seq1( + , 𝐹) ∈ V
1110a1i 11 . . 3 (πœ‘ β†’ seq1( + , 𝐹) ∈ V)
12 sumnnodd.1 . . . . . 6 (πœ‘ β†’ 𝐹:β„•βŸΆβ„‚)
1312ffvelcdmda 7084 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜) ∈ β„‚)
148, 9, 13serf 13993 . . . 4 (πœ‘ β†’ seq1( + , 𝐹):β„•βŸΆβ„‚)
1514ffvelcdmda 7084 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐹)β€˜π‘˜) ∈ β„‚)
16 sumnnodd.sc . . 3 (πœ‘ β†’ seq1( + , 𝐹) ⇝ 𝐡)
17 1nn 12220 . . . . . . 7 1 ∈ β„•
18 oveq2 7414 . . . . . . . . 9 (π‘˜ = 1 β†’ (2 Β· π‘˜) = (2 Β· 1))
1918oveq1d 7421 . . . . . . . 8 (π‘˜ = 1 β†’ ((2 Β· π‘˜) βˆ’ 1) = ((2 Β· 1) βˆ’ 1))
20 eqid 2733 . . . . . . . 8 (π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1)) = (π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))
21 ovex 7439 . . . . . . . 8 ((2 Β· 1) βˆ’ 1) ∈ V
2219, 20, 21fvmpt 6996 . . . . . . 7 (1 ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜1) = ((2 Β· 1) βˆ’ 1))
2317, 22ax-mp 5 . . . . . 6 ((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜1) = ((2 Β· 1) βˆ’ 1)
24 2t1e2 12372 . . . . . . 7 (2 Β· 1) = 2
2524oveq1i 7416 . . . . . 6 ((2 Β· 1) βˆ’ 1) = (2 βˆ’ 1)
26 2m1e1 12335 . . . . . 6 (2 βˆ’ 1) = 1
2723, 25, 263eqtri 2765 . . . . 5 ((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜1) = 1
2827, 17eqeltri 2830 . . . 4 ((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜1) ∈ β„•
2928a1i 11 . . 3 (πœ‘ β†’ ((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜1) ∈ β„•)
30 2z 12591 . . . . . . . 8 2 ∈ β„€
3130a1i 11 . . . . . . 7 (π‘˜ ∈ β„• β†’ 2 ∈ β„€)
32 nnz 12576 . . . . . . 7 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„€)
3331, 32zmulcld 12669 . . . . . 6 (π‘˜ ∈ β„• β†’ (2 Β· π‘˜) ∈ β„€)
3432peano2zd 12666 . . . . . . . 8 (π‘˜ ∈ β„• β†’ (π‘˜ + 1) ∈ β„€)
3531, 34zmulcld 12669 . . . . . . 7 (π‘˜ ∈ β„• β†’ (2 Β· (π‘˜ + 1)) ∈ β„€)
36 1zzd 12590 . . . . . . 7 (π‘˜ ∈ β„• β†’ 1 ∈ β„€)
3735, 36zsubcld 12668 . . . . . 6 (π‘˜ ∈ β„• β†’ ((2 Β· (π‘˜ + 1)) βˆ’ 1) ∈ β„€)
38 2re 12283 . . . . . . . . . 10 2 ∈ ℝ
3938a1i 11 . . . . . . . . 9 (π‘˜ ∈ β„• β†’ 2 ∈ ℝ)
40 nnre 12216 . . . . . . . . 9 (π‘˜ ∈ β„• β†’ π‘˜ ∈ ℝ)
4139, 40remulcld 11241 . . . . . . . 8 (π‘˜ ∈ β„• β†’ (2 Β· π‘˜) ∈ ℝ)
4241lep1d 12142 . . . . . . 7 (π‘˜ ∈ β„• β†’ (2 Β· π‘˜) ≀ ((2 Β· π‘˜) + 1))
43 2cnd 12287 . . . . . . . . . . 11 (π‘˜ ∈ β„• β†’ 2 ∈ β„‚)
44 nncn 12217 . . . . . . . . . . 11 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„‚)
45 1cnd 11206 . . . . . . . . . . 11 (π‘˜ ∈ β„• β†’ 1 ∈ β„‚)
4643, 44, 45adddid 11235 . . . . . . . . . 10 (π‘˜ ∈ β„• β†’ (2 Β· (π‘˜ + 1)) = ((2 Β· π‘˜) + (2 Β· 1)))
4724oveq2i 7417 . . . . . . . . . 10 ((2 Β· π‘˜) + (2 Β· 1)) = ((2 Β· π‘˜) + 2)
4846, 47eqtrdi 2789 . . . . . . . . 9 (π‘˜ ∈ β„• β†’ (2 Β· (π‘˜ + 1)) = ((2 Β· π‘˜) + 2))
4948oveq1d 7421 . . . . . . . 8 (π‘˜ ∈ β„• β†’ ((2 Β· (π‘˜ + 1)) βˆ’ 1) = (((2 Β· π‘˜) + 2) βˆ’ 1))
5043, 44mulcld 11231 . . . . . . . . 9 (π‘˜ ∈ β„• β†’ (2 Β· π‘˜) ∈ β„‚)
5150, 43, 45addsubassd 11588 . . . . . . . 8 (π‘˜ ∈ β„• β†’ (((2 Β· π‘˜) + 2) βˆ’ 1) = ((2 Β· π‘˜) + (2 βˆ’ 1)))
5226oveq2i 7417 . . . . . . . . 9 ((2 Β· π‘˜) + (2 βˆ’ 1)) = ((2 Β· π‘˜) + 1)
5352a1i 11 . . . . . . . 8 (π‘˜ ∈ β„• β†’ ((2 Β· π‘˜) + (2 βˆ’ 1)) = ((2 Β· π‘˜) + 1))
5449, 51, 533eqtrrd 2778 . . . . . . 7 (π‘˜ ∈ β„• β†’ ((2 Β· π‘˜) + 1) = ((2 Β· (π‘˜ + 1)) βˆ’ 1))
5542, 54breqtrd 5174 . . . . . 6 (π‘˜ ∈ β„• β†’ (2 Β· π‘˜) ≀ ((2 Β· (π‘˜ + 1)) βˆ’ 1))
56 eluz2 12825 . . . . . 6 (((2 Β· (π‘˜ + 1)) βˆ’ 1) ∈ (β„€β‰₯β€˜(2 Β· π‘˜)) ↔ ((2 Β· π‘˜) ∈ β„€ ∧ ((2 Β· (π‘˜ + 1)) βˆ’ 1) ∈ β„€ ∧ (2 Β· π‘˜) ≀ ((2 Β· (π‘˜ + 1)) βˆ’ 1)))
5733, 37, 55, 56syl3anbrc 1344 . . . . 5 (π‘˜ ∈ β„• β†’ ((2 Β· (π‘˜ + 1)) βˆ’ 1) ∈ (β„€β‰₯β€˜(2 Β· π‘˜)))
58 oveq2 7414 . . . . . . . 8 (π‘˜ = 𝑗 β†’ (2 Β· π‘˜) = (2 Β· 𝑗))
5958oveq1d 7421 . . . . . . 7 (π‘˜ = 𝑗 β†’ ((2 Β· π‘˜) βˆ’ 1) = ((2 Β· 𝑗) βˆ’ 1))
6059cbvmptv 5261 . . . . . 6 (π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1)) = (𝑗 ∈ β„• ↦ ((2 Β· 𝑗) βˆ’ 1))
61 oveq2 7414 . . . . . . 7 (𝑗 = (π‘˜ + 1) β†’ (2 Β· 𝑗) = (2 Β· (π‘˜ + 1)))
6261oveq1d 7421 . . . . . 6 (𝑗 = (π‘˜ + 1) β†’ ((2 Β· 𝑗) βˆ’ 1) = ((2 Β· (π‘˜ + 1)) βˆ’ 1))
63 peano2nn 12221 . . . . . 6 (π‘˜ ∈ β„• β†’ (π‘˜ + 1) ∈ β„•)
6460, 62, 63, 37fvmptd3 7019 . . . . 5 (π‘˜ ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜(π‘˜ + 1)) = ((2 Β· (π‘˜ + 1)) βˆ’ 1))
6533, 36zsubcld 12668 . . . . . . . . 9 (π‘˜ ∈ β„• β†’ ((2 Β· π‘˜) βˆ’ 1) ∈ β„€)
6620fvmpt2 7007 . . . . . . . . 9 ((π‘˜ ∈ β„• ∧ ((2 Β· π‘˜) βˆ’ 1) ∈ β„€) β†’ ((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜) = ((2 Β· π‘˜) βˆ’ 1))
6765, 66mpdan 686 . . . . . . . 8 (π‘˜ ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜) = ((2 Β· π‘˜) βˆ’ 1))
6867oveq1d 7421 . . . . . . 7 (π‘˜ ∈ β„• β†’ (((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜) + 1) = (((2 Β· π‘˜) βˆ’ 1) + 1))
6950, 45npcand 11572 . . . . . . 7 (π‘˜ ∈ β„• β†’ (((2 Β· π‘˜) βˆ’ 1) + 1) = (2 Β· π‘˜))
7068, 69eqtrd 2773 . . . . . 6 (π‘˜ ∈ β„• β†’ (((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜) + 1) = (2 Β· π‘˜))
7170fveq2d 6893 . . . . 5 (π‘˜ ∈ β„• β†’ (β„€β‰₯β€˜(((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜) + 1)) = (β„€β‰₯β€˜(2 Β· π‘˜)))
7257, 64, 713eltr4d 2849 . . . 4 (π‘˜ ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜(π‘˜ + 1)) ∈ (β„€β‰₯β€˜(((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜) + 1)))
7372adantl 483 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜(π‘˜ + 1)) ∈ (β„€β‰₯β€˜(((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜) + 1)))
74 seqex 13965 . . . 4 seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))) ∈ V
7574a1i 11 . . 3 (πœ‘ β†’ seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))) ∈ V)
76 incom 4201 . . . . . . . . . 10 (((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∩ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) = (((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∩ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}))
77 inss2 4229 . . . . . . . . . . 11 ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) βŠ† {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}
78 ssrin 4233 . . . . . . . . . . 11 (((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) βŠ† {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•} β†’ (((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∩ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) βŠ† ({𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•} ∩ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})))
7977, 78ax-mp 5 . . . . . . . . . 10 (((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∩ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) βŠ† ({𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•} ∩ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}))
8076, 79eqsstri 4016 . . . . . . . . 9 (((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∩ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) βŠ† ({𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•} ∩ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}))
81 disjdif 4471 . . . . . . . . 9 ({𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•} ∩ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) = βˆ…
8280, 81sseqtri 4018 . . . . . . . 8 (((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∩ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) βŠ† βˆ…
83 ss0 4398 . . . . . . . 8 ((((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∩ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) βŠ† βˆ… β†’ (((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∩ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) = βˆ…)
8482, 83mp1i 13 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∩ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) = βˆ…)
85 uncom 4153 . . . . . . . . 9 (((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) βˆͺ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) = (((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) βˆͺ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}))
86 inundif 4478 . . . . . . . . 9 (((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) βˆͺ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) = (1...((2 Β· π‘˜) βˆ’ 1))
8785, 86eqtr2i 2762 . . . . . . . 8 (1...((2 Β· π‘˜) βˆ’ 1)) = (((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) βˆͺ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}))
8887a1i 11 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1...((2 Β· π‘˜) βˆ’ 1)) = (((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) βˆͺ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})))
89 fzfid 13935 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1...((2 Β· π‘˜) βˆ’ 1)) ∈ Fin)
9012adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))) β†’ 𝐹:β„•βŸΆβ„‚)
91 elfznn 13527 . . . . . . . . . 10 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ 𝑗 ∈ β„•)
9291adantl 483 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))) β†’ 𝑗 ∈ β„•)
9390, 92ffvelcdmd 7085 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))) β†’ (πΉβ€˜π‘—) ∈ β„‚)
9493adantlr 714 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))) β†’ (πΉβ€˜π‘—) ∈ β„‚)
9584, 88, 89, 94fsumsplit 15684 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))(πΉβ€˜π‘—) = (Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘—) + Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘—)))
96 simpl 484 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ πœ‘)
97 ssrab2 4077 . . . . . . . . . . . . . 14 {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•} βŠ† β„•
9877sseli 3978 . . . . . . . . . . . . . 14 (𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) β†’ 𝑗 ∈ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})
9997, 98sselid 3980 . . . . . . . . . . . . 13 (𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) β†’ 𝑗 ∈ β„•)
10099adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ 𝑗 ∈ β„•)
101 oveq1 7413 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑗 β†’ (π‘˜ / 2) = (𝑗 / 2))
102101eleq1d 2819 . . . . . . . . . . . . . . 15 (π‘˜ = 𝑗 β†’ ((π‘˜ / 2) ∈ β„• ↔ (𝑗 / 2) ∈ β„•))
103 oveq1 7413 . . . . . . . . . . . . . . . . . 18 (𝑛 = π‘˜ β†’ (𝑛 / 2) = (π‘˜ / 2))
104103eleq1d 2819 . . . . . . . . . . . . . . . . 17 (𝑛 = π‘˜ β†’ ((𝑛 / 2) ∈ β„• ↔ (π‘˜ / 2) ∈ β„•))
105104elrab 3683 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•} ↔ (π‘˜ ∈ β„• ∧ (π‘˜ / 2) ∈ β„•))
106105simprbi 498 . . . . . . . . . . . . . . 15 (π‘˜ ∈ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•} β†’ (π‘˜ / 2) ∈ β„•)
107102, 106vtoclga 3566 . . . . . . . . . . . . . 14 (𝑗 ∈ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•} β†’ (𝑗 / 2) ∈ β„•)
10898, 107syl 17 . . . . . . . . . . . . 13 (𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) β†’ (𝑗 / 2) ∈ β„•)
109108adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ (𝑗 / 2) ∈ β„•)
110 eleq1w 2817 . . . . . . . . . . . . . . 15 (π‘˜ = 𝑗 β†’ (π‘˜ ∈ β„• ↔ 𝑗 ∈ β„•))
111110, 1023anbi23d 1440 . . . . . . . . . . . . . 14 (π‘˜ = 𝑗 β†’ ((πœ‘ ∧ π‘˜ ∈ β„• ∧ (π‘˜ / 2) ∈ β„•) ↔ (πœ‘ ∧ 𝑗 ∈ β„• ∧ (𝑗 / 2) ∈ β„•)))
112 fveqeq2 6898 . . . . . . . . . . . . . 14 (π‘˜ = 𝑗 β†’ ((πΉβ€˜π‘˜) = 0 ↔ (πΉβ€˜π‘—) = 0))
113111, 112imbi12d 345 . . . . . . . . . . . . 13 (π‘˜ = 𝑗 β†’ (((πœ‘ ∧ π‘˜ ∈ β„• ∧ (π‘˜ / 2) ∈ β„•) β†’ (πΉβ€˜π‘˜) = 0) ↔ ((πœ‘ ∧ 𝑗 ∈ β„• ∧ (𝑗 / 2) ∈ β„•) β†’ (πΉβ€˜π‘—) = 0)))
114 sumnnodd.even0 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„• ∧ (π‘˜ / 2) ∈ β„•) β†’ (πΉβ€˜π‘˜) = 0)
115113, 114chvarvv 2003 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ (𝑗 / 2) ∈ β„•) β†’ (πΉβ€˜π‘—) = 0)
11696, 100, 109, 115syl3anc 1372 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ (πΉβ€˜π‘—) = 0)
117116sumeq2dv 15646 . . . . . . . . . 10 (πœ‘ β†’ Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘—) = Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})0)
118 fzfid 13935 . . . . . . . . . . . . 13 (πœ‘ β†’ (1...((2 Β· π‘˜) βˆ’ 1)) ∈ Fin)
119 inss1 4228 . . . . . . . . . . . . . 14 ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) βŠ† (1...((2 Β· π‘˜) βˆ’ 1))
120119a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) βŠ† (1...((2 Β· π‘˜) βˆ’ 1)))
121 ssfi 9170 . . . . . . . . . . . . 13 (((1...((2 Β· π‘˜) βˆ’ 1)) ∈ Fin ∧ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) βŠ† (1...((2 Β· π‘˜) βˆ’ 1))) β†’ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∈ Fin)
122118, 120, 121syl2anc 585 . . . . . . . . . . . 12 (πœ‘ β†’ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∈ Fin)
123122olcd 873 . . . . . . . . . . 11 (πœ‘ β†’ (((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) βŠ† (β„€β‰₯β€˜πΆ) ∨ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∈ Fin))
124 sumz 15665 . . . . . . . . . . 11 ((((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) βŠ† (β„€β‰₯β€˜πΆ) ∨ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∈ Fin) β†’ Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})0 = 0)
125123, 124syl 17 . . . . . . . . . 10 (πœ‘ β†’ Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})0 = 0)
126117, 125eqtrd 2773 . . . . . . . . 9 (πœ‘ β†’ Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘—) = 0)
127126adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘—) = 0)
128127oveq2d 7422 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘—) + Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘—)) = (Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘—) + 0))
129 fzfi 13934 . . . . . . . . . . . 12 (1...((2 Β· π‘˜) βˆ’ 1)) ∈ Fin
130 difss 4131 . . . . . . . . . . . 12 ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) βŠ† (1...((2 Β· π‘˜) βˆ’ 1))
131 ssfi 9170 . . . . . . . . . . . 12 (((1...((2 Β· π‘˜) βˆ’ 1)) ∈ Fin ∧ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) βŠ† (1...((2 Β· π‘˜) βˆ’ 1))) β†’ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∈ Fin)
132129, 130, 131mp2an 691 . . . . . . . . . . 11 ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∈ Fin
133132a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∈ Fin)
134130sseli 3978 . . . . . . . . . . . 12 (𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) β†’ 𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)))
135134, 93sylan2 594 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ (πΉβ€˜π‘—) ∈ β„‚)
136135adantlr 714 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ (πΉβ€˜π‘—) ∈ β„‚)
137133, 136fsumcl 15676 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘—) ∈ β„‚)
138137addridd 11411 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘—) + 0) = Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘—))
139 fveq2 6889 . . . . . . . . 9 (𝑗 = 𝑖 β†’ (πΉβ€˜π‘—) = (πΉβ€˜π‘–))
140139cbvsumv 15639 . . . . . . . 8 Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘—) = Σ𝑖 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘–)
141138, 140eqtrdi 2789 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘—) + 0) = Σ𝑖 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘–))
142128, 141eqtrd 2773 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘—) + Σ𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) ∩ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘—)) = Σ𝑖 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘–))
143 fveq2 6889 . . . . . . 7 (𝑖 = ((2 Β· 𝑗) βˆ’ 1) β†’ (πΉβ€˜π‘–) = (πΉβ€˜((2 Β· 𝑗) βˆ’ 1)))
144 fzfid 13935 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1...π‘˜) ∈ Fin)
145 1zzd 12590 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ 1 ∈ β„€)
14665adantr 482 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ ((2 Β· π‘˜) βˆ’ 1) ∈ β„€)
14730a1i 11 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...π‘˜) β†’ 2 ∈ β„€)
148 elfzelz 13498 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...π‘˜) β†’ 𝑖 ∈ β„€)
149147, 148zmulcld 12669 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...π‘˜) β†’ (2 Β· 𝑖) ∈ β„€)
150 1zzd 12590 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...π‘˜) β†’ 1 ∈ β„€)
151149, 150zsubcld 12668 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...π‘˜) β†’ ((2 Β· 𝑖) βˆ’ 1) ∈ β„€)
152151adantl 483 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ ((2 Β· 𝑖) βˆ’ 1) ∈ β„€)
15325, 26eqtr2i 2762 . . . . . . . . . . . . . . 15 1 = ((2 Β· 1) βˆ’ 1)
154 1re 11211 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
15538, 154remulcli 11227 . . . . . . . . . . . . . . . . 17 (2 Β· 1) ∈ ℝ
156155a1i 11 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...π‘˜) β†’ (2 Β· 1) ∈ ℝ)
157149zred 12663 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...π‘˜) β†’ (2 Β· 𝑖) ∈ ℝ)
158 1red 11212 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...π‘˜) β†’ 1 ∈ ℝ)
159148zred 12663 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...π‘˜) β†’ 𝑖 ∈ ℝ)
16038a1i 11 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...π‘˜) β†’ 2 ∈ ℝ)
161 0le2 12311 . . . . . . . . . . . . . . . . . 18 0 ≀ 2
162161a1i 11 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...π‘˜) β†’ 0 ≀ 2)
163 elfzle1 13501 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...π‘˜) β†’ 1 ≀ 𝑖)
164158, 159, 160, 162, 163lemul2ad 12151 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...π‘˜) β†’ (2 Β· 1) ≀ (2 Β· 𝑖))
165156, 157, 158, 164lesub1dd 11827 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...π‘˜) β†’ ((2 Β· 1) βˆ’ 1) ≀ ((2 Β· 𝑖) βˆ’ 1))
166153, 165eqbrtrid 5183 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...π‘˜) β†’ 1 ≀ ((2 Β· 𝑖) βˆ’ 1))
167166adantl 483 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ 1 ≀ ((2 Β· 𝑖) βˆ’ 1))
168157adantl 483 . . . . . . . . . . . . . 14 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ (2 Β· 𝑖) ∈ ℝ)
16941adantr 482 . . . . . . . . . . . . . 14 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ (2 Β· π‘˜) ∈ ℝ)
170 1red 11212 . . . . . . . . . . . . . 14 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ 1 ∈ ℝ)
171159adantl 483 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ 𝑖 ∈ ℝ)
17240adantr 482 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ π‘˜ ∈ ℝ)
17338a1i 11 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ 2 ∈ ℝ)
174161a1i 11 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ 0 ≀ 2)
175 elfzle2 13502 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...π‘˜) β†’ 𝑖 ≀ π‘˜)
176175adantl 483 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ 𝑖 ≀ π‘˜)
177171, 172, 173, 174, 176lemul2ad 12151 . . . . . . . . . . . . . 14 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ (2 Β· 𝑖) ≀ (2 Β· π‘˜))
178168, 169, 170, 177lesub1dd 11827 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ ((2 Β· 𝑖) βˆ’ 1) ≀ ((2 Β· π‘˜) βˆ’ 1))
179145, 146, 152, 167, 178elfzd 13489 . . . . . . . . . . . 12 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ ((2 Β· 𝑖) βˆ’ 1) ∈ (1...((2 Β· π‘˜) βˆ’ 1)))
180149zcnd 12664 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...π‘˜) β†’ (2 Β· 𝑖) ∈ β„‚)
181 1cnd 11206 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...π‘˜) β†’ 1 ∈ β„‚)
182 2cnd 12287 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...π‘˜) β†’ 2 ∈ β„‚)
183 2ne0 12313 . . . . . . . . . . . . . . . . . . 19 2 β‰  0
184183a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...π‘˜) β†’ 2 β‰  0)
185180, 181, 182, 184divsubdird 12026 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...π‘˜) β†’ (((2 Β· 𝑖) βˆ’ 1) / 2) = (((2 Β· 𝑖) / 2) βˆ’ (1 / 2)))
186148zcnd 12664 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...π‘˜) β†’ 𝑖 ∈ β„‚)
187186, 182, 184divcan3d 11992 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...π‘˜) β†’ ((2 Β· 𝑖) / 2) = 𝑖)
188187oveq1d 7421 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...π‘˜) β†’ (((2 Β· 𝑖) / 2) βˆ’ (1 / 2)) = (𝑖 βˆ’ (1 / 2)))
189185, 188eqtrd 2773 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...π‘˜) β†’ (((2 Β· 𝑖) βˆ’ 1) / 2) = (𝑖 βˆ’ (1 / 2)))
190148, 150zsubcld 12668 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...π‘˜) β†’ (𝑖 βˆ’ 1) ∈ β„€)
191160, 184rereccld 12038 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...π‘˜) β†’ (1 / 2) ∈ ℝ)
192 halflt1 12427 . . . . . . . . . . . . . . . . . . . 20 (1 / 2) < 1
193192a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...π‘˜) β†’ (1 / 2) < 1)
194191, 158, 159, 193ltsub2dd 11824 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...π‘˜) β†’ (𝑖 βˆ’ 1) < (𝑖 βˆ’ (1 / 2)))
195 2rp 12976 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℝ+
196 rpreccl 12997 . . . . . . . . . . . . . . . . . . . . 21 (2 ∈ ℝ+ β†’ (1 / 2) ∈ ℝ+)
197195, 196mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (1...π‘˜) β†’ (1 / 2) ∈ ℝ+)
198159, 197ltsubrpd 13045 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...π‘˜) β†’ (𝑖 βˆ’ (1 / 2)) < 𝑖)
199186, 181npcand 11572 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...π‘˜) β†’ ((𝑖 βˆ’ 1) + 1) = 𝑖)
200198, 199breqtrrd 5176 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...π‘˜) β†’ (𝑖 βˆ’ (1 / 2)) < ((𝑖 βˆ’ 1) + 1))
201 btwnnz 12635 . . . . . . . . . . . . . . . . . 18 (((𝑖 βˆ’ 1) ∈ β„€ ∧ (𝑖 βˆ’ 1) < (𝑖 βˆ’ (1 / 2)) ∧ (𝑖 βˆ’ (1 / 2)) < ((𝑖 βˆ’ 1) + 1)) β†’ Β¬ (𝑖 βˆ’ (1 / 2)) ∈ β„€)
202190, 194, 200, 201syl3anc 1372 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...π‘˜) β†’ Β¬ (𝑖 βˆ’ (1 / 2)) ∈ β„€)
203 nnz 12576 . . . . . . . . . . . . . . . . 17 ((𝑖 βˆ’ (1 / 2)) ∈ β„• β†’ (𝑖 βˆ’ (1 / 2)) ∈ β„€)
204202, 203nsyl 140 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...π‘˜) β†’ Β¬ (𝑖 βˆ’ (1 / 2)) ∈ β„•)
205189, 204eqneltrd 2854 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...π‘˜) β†’ Β¬ (((2 Β· 𝑖) βˆ’ 1) / 2) ∈ β„•)
206205intnand 490 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...π‘˜) β†’ Β¬ (((2 Β· 𝑖) βˆ’ 1) ∈ β„• ∧ (((2 Β· 𝑖) βˆ’ 1) / 2) ∈ β„•))
207 oveq1 7413 . . . . . . . . . . . . . . . 16 (𝑛 = ((2 Β· 𝑖) βˆ’ 1) β†’ (𝑛 / 2) = (((2 Β· 𝑖) βˆ’ 1) / 2))
208207eleq1d 2819 . . . . . . . . . . . . . . 15 (𝑛 = ((2 Β· 𝑖) βˆ’ 1) β†’ ((𝑛 / 2) ∈ β„• ↔ (((2 Β· 𝑖) βˆ’ 1) / 2) ∈ β„•))
209208elrab 3683 . . . . . . . . . . . . . 14 (((2 Β· 𝑖) βˆ’ 1) ∈ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•} ↔ (((2 Β· 𝑖) βˆ’ 1) ∈ β„• ∧ (((2 Β· 𝑖) βˆ’ 1) / 2) ∈ β„•))
210206, 209sylnibr 329 . . . . . . . . . . . . 13 (𝑖 ∈ (1...π‘˜) β†’ Β¬ ((2 Β· 𝑖) βˆ’ 1) ∈ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})
211210adantl 483 . . . . . . . . . . . 12 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ Β¬ ((2 Β· 𝑖) βˆ’ 1) ∈ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})
212179, 211eldifd 3959 . . . . . . . . . . 11 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (1...π‘˜)) β†’ ((2 Β· 𝑖) βˆ’ 1) ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}))
213212fmpttd 7112 . . . . . . . . . 10 (π‘˜ ∈ β„• β†’ (𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)):(1...π‘˜)⟢((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}))
214 eqidd 2734 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (1...π‘˜) β†’ (𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)) = (𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)))
215 oveq2 7414 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = π‘₯ β†’ (2 Β· 𝑖) = (2 Β· π‘₯))
216215oveq1d 7421 . . . . . . . . . . . . . . . . . . 19 (𝑖 = π‘₯ β†’ ((2 Β· 𝑖) βˆ’ 1) = ((2 Β· π‘₯) βˆ’ 1))
217216adantl 483 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ (1...π‘˜) ∧ 𝑖 = π‘₯) β†’ ((2 Β· 𝑖) βˆ’ 1) = ((2 Β· π‘₯) βˆ’ 1))
218 id 22 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (1...π‘˜) β†’ π‘₯ ∈ (1...π‘˜))
219 ovexd 7441 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (1...π‘˜) β†’ ((2 Β· π‘₯) βˆ’ 1) ∈ V)
220214, 217, 218, 219fvmptd 7003 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (1...π‘˜) β†’ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘₯) = ((2 Β· π‘₯) βˆ’ 1))
221220eqcomd 2739 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (1...π‘˜) β†’ ((2 Β· π‘₯) βˆ’ 1) = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘₯))
222221ad2antrr 725 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘₯) = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘¦)) β†’ ((2 Β· π‘₯) βˆ’ 1) = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘₯))
223 simpr 486 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘₯) = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘¦)) β†’ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘₯) = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘¦))
224 eqidd 2734 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...π‘˜) β†’ (𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)) = (𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)))
225 oveq2 7414 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑦 β†’ (2 Β· 𝑖) = (2 Β· 𝑦))
226225oveq1d 7421 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑦 β†’ ((2 Β· 𝑖) βˆ’ 1) = ((2 Β· 𝑦) βˆ’ 1))
227226adantl 483 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (1...π‘˜) ∧ 𝑖 = 𝑦) β†’ ((2 Β· 𝑖) βˆ’ 1) = ((2 Β· 𝑦) βˆ’ 1))
228 id 22 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...π‘˜) β†’ 𝑦 ∈ (1...π‘˜))
229 ovexd 7441 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...π‘˜) β†’ ((2 Β· 𝑦) βˆ’ 1) ∈ V)
230224, 227, 228, 229fvmptd 7003 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (1...π‘˜) β†’ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘¦) = ((2 Β· 𝑦) βˆ’ 1))
231230ad2antlr 726 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘₯) = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘¦)) β†’ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘¦) = ((2 Β· 𝑦) βˆ’ 1))
232222, 223, 2313eqtrd 2777 . . . . . . . . . . . . . 14 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘₯) = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘¦)) β†’ ((2 Β· π‘₯) βˆ’ 1) = ((2 Β· 𝑦) βˆ’ 1))
233 2cnd 12287 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (1...π‘˜) β†’ 2 ∈ β„‚)
234 elfzelz 13498 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ (1...π‘˜) β†’ π‘₯ ∈ β„€)
235234zcnd 12664 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (1...π‘˜) β†’ π‘₯ ∈ β„‚)
236233, 235mulcld 11231 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (1...π‘˜) β†’ (2 Β· π‘₯) ∈ β„‚)
237236ad2antrr 725 . . . . . . . . . . . . . . . 16 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ ((2 Β· π‘₯) βˆ’ 1) = ((2 Β· 𝑦) βˆ’ 1)) β†’ (2 Β· π‘₯) ∈ β„‚)
238 2cnd 12287 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...π‘˜) β†’ 2 ∈ β„‚)
239 elfzelz 13498 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (1...π‘˜) β†’ 𝑦 ∈ β„€)
240239zcnd 12664 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...π‘˜) β†’ 𝑦 ∈ β„‚)
241238, 240mulcld 11231 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...π‘˜) β†’ (2 Β· 𝑦) ∈ β„‚)
242241ad2antlr 726 . . . . . . . . . . . . . . . 16 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ ((2 Β· π‘₯) βˆ’ 1) = ((2 Β· 𝑦) βˆ’ 1)) β†’ (2 Β· 𝑦) ∈ β„‚)
243 1cnd 11206 . . . . . . . . . . . . . . . 16 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ ((2 Β· π‘₯) βˆ’ 1) = ((2 Β· 𝑦) βˆ’ 1)) β†’ 1 ∈ β„‚)
244 simpr 486 . . . . . . . . . . . . . . . 16 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ ((2 Β· π‘₯) βˆ’ 1) = ((2 Β· 𝑦) βˆ’ 1)) β†’ ((2 Β· π‘₯) βˆ’ 1) = ((2 Β· 𝑦) βˆ’ 1))
245237, 242, 243, 244subcan2d 11610 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ ((2 Β· π‘₯) βˆ’ 1) = ((2 Β· 𝑦) βˆ’ 1)) β†’ (2 Β· π‘₯) = (2 Β· 𝑦))
246235ad2antrr 725 . . . . . . . . . . . . . . . 16 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ (2 Β· π‘₯) = (2 Β· 𝑦)) β†’ π‘₯ ∈ β„‚)
247240ad2antlr 726 . . . . . . . . . . . . . . . 16 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ (2 Β· π‘₯) = (2 Β· 𝑦)) β†’ 𝑦 ∈ β„‚)
248 2cnd 12287 . . . . . . . . . . . . . . . 16 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ (2 Β· π‘₯) = (2 Β· 𝑦)) β†’ 2 ∈ β„‚)
249183a1i 11 . . . . . . . . . . . . . . . 16 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ (2 Β· π‘₯) = (2 Β· 𝑦)) β†’ 2 β‰  0)
250 simpr 486 . . . . . . . . . . . . . . . 16 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ (2 Β· π‘₯) = (2 Β· 𝑦)) β†’ (2 Β· π‘₯) = (2 Β· 𝑦))
251246, 247, 248, 249, 250mulcanad 11846 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ (2 Β· π‘₯) = (2 Β· 𝑦)) β†’ π‘₯ = 𝑦)
252245, 251syldan 592 . . . . . . . . . . . . . 14 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ ((2 Β· π‘₯) βˆ’ 1) = ((2 Β· 𝑦) βˆ’ 1)) β†’ π‘₯ = 𝑦)
253232, 252syldan 592 . . . . . . . . . . . . 13 (((π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜)) ∧ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘₯) = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘¦)) β†’ π‘₯ = 𝑦)
254253adantll 713 . . . . . . . . . . . 12 (((π‘˜ ∈ β„• ∧ (π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜))) ∧ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘₯) = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘¦)) β†’ π‘₯ = 𝑦)
255254ex 414 . . . . . . . . . . 11 ((π‘˜ ∈ β„• ∧ (π‘₯ ∈ (1...π‘˜) ∧ 𝑦 ∈ (1...π‘˜))) β†’ (((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘₯) = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘¦) β†’ π‘₯ = 𝑦))
256255ralrimivva 3201 . . . . . . . . . 10 (π‘˜ ∈ β„• β†’ βˆ€π‘₯ ∈ (1...π‘˜)βˆ€π‘¦ ∈ (1...π‘˜)(((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘₯) = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘¦) β†’ π‘₯ = 𝑦))
257 dff13 7251 . . . . . . . . . 10 ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)):(1...π‘˜)–1-1β†’((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ↔ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)):(1...π‘˜)⟢((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∧ βˆ€π‘₯ ∈ (1...π‘˜)βˆ€π‘¦ ∈ (1...π‘˜)(((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘₯) = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘¦) β†’ π‘₯ = 𝑦)))
258213, 256, 257sylanbrc 584 . . . . . . . . 9 (π‘˜ ∈ β„• β†’ (𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)):(1...π‘˜)–1-1β†’((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}))
259 1zzd 12590 . . . . . . . . . . . . . 14 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ 1 ∈ β„€)
26032adantr 482 . . . . . . . . . . . . . 14 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ π‘˜ ∈ β„€)
261134elfzelzd 13499 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) β†’ 𝑗 ∈ β„€)
262 zeo 12645 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ β„€ β†’ ((𝑗 / 2) ∈ β„€ ∨ ((𝑗 + 1) / 2) ∈ β„€))
263261, 262syl 17 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) β†’ ((𝑗 / 2) ∈ β„€ ∨ ((𝑗 + 1) / 2) ∈ β„€))
264263adantl 483 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ ((𝑗 / 2) ∈ β„€ ∨ ((𝑗 + 1) / 2) ∈ β„€))
265 eldifn 4127 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) β†’ Β¬ 𝑗 ∈ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})
266134, 91syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) β†’ 𝑗 ∈ β„•)
267266adantr 482 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∧ (𝑗 / 2) ∈ β„€) β†’ 𝑗 ∈ β„•)
268 simpr 486 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∧ (𝑗 / 2) ∈ β„€) β†’ (𝑗 / 2) ∈ β„€)
269267nnred 12224 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∧ (𝑗 / 2) ∈ β„€) β†’ 𝑗 ∈ ℝ)
27038a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∧ (𝑗 / 2) ∈ β„€) β†’ 2 ∈ ℝ)
271267nngt0d 12258 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∧ (𝑗 / 2) ∈ β„€) β†’ 0 < 𝑗)
272 2pos 12312 . . . . . . . . . . . . . . . . . . . . 21 0 < 2
273272a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∧ (𝑗 / 2) ∈ β„€) β†’ 0 < 2)
274269, 270, 271, 273divgt0d 12146 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∧ (𝑗 / 2) ∈ β„€) β†’ 0 < (𝑗 / 2))
275 elnnz 12565 . . . . . . . . . . . . . . . . . . 19 ((𝑗 / 2) ∈ β„• ↔ ((𝑗 / 2) ∈ β„€ ∧ 0 < (𝑗 / 2)))
276268, 274, 275sylanbrc 584 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∧ (𝑗 / 2) ∈ β„€) β†’ (𝑗 / 2) ∈ β„•)
277 oveq1 7413 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑗 β†’ (𝑛 / 2) = (𝑗 / 2))
278277eleq1d 2819 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑗 β†’ ((𝑛 / 2) ∈ β„• ↔ (𝑗 / 2) ∈ β„•))
279278elrab 3683 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•} ↔ (𝑗 ∈ β„• ∧ (𝑗 / 2) ∈ β„•))
280267, 276, 279sylanbrc 584 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∧ (𝑗 / 2) ∈ β„€) β†’ 𝑗 ∈ {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})
281265, 280mtand 815 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) β†’ Β¬ (𝑗 / 2) ∈ β„€)
282281adantl 483 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ Β¬ (𝑗 / 2) ∈ β„€)
283 pm2.53 850 . . . . . . . . . . . . . . 15 (((𝑗 / 2) ∈ β„€ ∨ ((𝑗 + 1) / 2) ∈ β„€) β†’ (Β¬ (𝑗 / 2) ∈ β„€ β†’ ((𝑗 + 1) / 2) ∈ β„€))
284264, 282, 283sylc 65 . . . . . . . . . . . . . 14 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ ((𝑗 + 1) / 2) ∈ β„€)
285 1p1e2 12334 . . . . . . . . . . . . . . . . . . 19 (1 + 1) = 2
286285oveq1i 7416 . . . . . . . . . . . . . . . . . 18 ((1 + 1) / 2) = (2 / 2)
287 2div2e1 12350 . . . . . . . . . . . . . . . . . 18 (2 / 2) = 1
288286, 287eqtr2i 2762 . . . . . . . . . . . . . . . . 17 1 = ((1 + 1) / 2)
289 1red 11212 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ 1 ∈ ℝ)
290289, 289readdcld 11240 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ (1 + 1) ∈ ℝ)
29191nnred 12224 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ 𝑗 ∈ ℝ)
292291, 289readdcld 11240 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ (𝑗 + 1) ∈ ℝ)
293195a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ 2 ∈ ℝ+)
294 elfzle1 13501 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ 1 ≀ 𝑗)
295289, 291, 289, 294leadd1dd 11825 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ (1 + 1) ≀ (𝑗 + 1))
296290, 292, 293, 295lediv1dd 13071 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ ((1 + 1) / 2) ≀ ((𝑗 + 1) / 2))
297288, 296eqbrtrid 5183 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ 1 ≀ ((𝑗 + 1) / 2))
298134, 297syl 17 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) β†’ 1 ≀ ((𝑗 + 1) / 2))
299298adantl 483 . . . . . . . . . . . . . 14 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ 1 ≀ ((𝑗 + 1) / 2))
300 elfzel2 13496 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ ((2 Β· π‘˜) βˆ’ 1) ∈ β„€)
301300zred 12663 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ ((2 Β· π‘˜) βˆ’ 1) ∈ ℝ)
302301, 289readdcld 11240 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ (((2 Β· π‘˜) βˆ’ 1) + 1) ∈ ℝ)
303 elfzle2 13502 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ 𝑗 ≀ ((2 Β· π‘˜) βˆ’ 1))
304291, 301, 289, 303leadd1dd 11825 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ (𝑗 + 1) ≀ (((2 Β· π‘˜) βˆ’ 1) + 1))
305292, 302, 293, 304lediv1dd 13071 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)) β†’ ((𝑗 + 1) / 2) ≀ ((((2 Β· π‘˜) βˆ’ 1) + 1) / 2))
306305adantl 483 . . . . . . . . . . . . . . . 16 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))) β†’ ((𝑗 + 1) / 2) ≀ ((((2 Β· π‘˜) βˆ’ 1) + 1) / 2))
30750adantr 482 . . . . . . . . . . . . . . . . . . 19 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))) β†’ (2 Β· π‘˜) ∈ β„‚)
308 1cnd 11206 . . . . . . . . . . . . . . . . . . 19 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))) β†’ 1 ∈ β„‚)
309307, 308npcand 11572 . . . . . . . . . . . . . . . . . 18 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))) β†’ (((2 Β· π‘˜) βˆ’ 1) + 1) = (2 Β· π‘˜))
310309oveq1d 7421 . . . . . . . . . . . . . . . . 17 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))) β†’ ((((2 Β· π‘˜) βˆ’ 1) + 1) / 2) = ((2 Β· π‘˜) / 2))
311183a1i 11 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ β„• β†’ 2 β‰  0)
31244, 43, 311divcan3d 11992 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ β„• β†’ ((2 Β· π‘˜) / 2) = π‘˜)
313312adantr 482 . . . . . . . . . . . . . . . . 17 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))) β†’ ((2 Β· π‘˜) / 2) = π‘˜)
314310, 313eqtrd 2773 . . . . . . . . . . . . . . . 16 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))) β†’ ((((2 Β· π‘˜) βˆ’ 1) + 1) / 2) = π‘˜)
315306, 314breqtrd 5174 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))) β†’ ((𝑗 + 1) / 2) ≀ π‘˜)
316134, 315sylan2 594 . . . . . . . . . . . . . 14 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ ((𝑗 + 1) / 2) ≀ π‘˜)
317259, 260, 284, 299, 316elfzd 13489 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ ((𝑗 + 1) / 2) ∈ (1...π‘˜))
318266nncnd 12225 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) β†’ 𝑗 ∈ β„‚)
319 peano2cn 11383 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ β„‚ β†’ (𝑗 + 1) ∈ β„‚)
320 2cnd 12287 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ β„‚ β†’ 2 ∈ β„‚)
321183a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ β„‚ β†’ 2 β‰  0)
322319, 320, 321divcan2d 11989 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ β„‚ β†’ (2 Β· ((𝑗 + 1) / 2)) = (𝑗 + 1))
323322oveq1d 7421 . . . . . . . . . . . . . . . 16 (𝑗 ∈ β„‚ β†’ ((2 Β· ((𝑗 + 1) / 2)) βˆ’ 1) = ((𝑗 + 1) βˆ’ 1))
324 pncan1 11635 . . . . . . . . . . . . . . . 16 (𝑗 ∈ β„‚ β†’ ((𝑗 + 1) βˆ’ 1) = 𝑗)
325323, 324eqtr2d 2774 . . . . . . . . . . . . . . 15 (𝑗 ∈ β„‚ β†’ 𝑗 = ((2 Β· ((𝑗 + 1) / 2)) βˆ’ 1))
326318, 325syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) β†’ 𝑗 = ((2 Β· ((𝑗 + 1) / 2)) βˆ’ 1))
327326adantl 483 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ 𝑗 = ((2 Β· ((𝑗 + 1) / 2)) βˆ’ 1))
328 oveq2 7414 . . . . . . . . . . . . . . 15 (π‘š = ((𝑗 + 1) / 2) β†’ (2 Β· π‘š) = (2 Β· ((𝑗 + 1) / 2)))
329328oveq1d 7421 . . . . . . . . . . . . . 14 (π‘š = ((𝑗 + 1) / 2) β†’ ((2 Β· π‘š) βˆ’ 1) = ((2 Β· ((𝑗 + 1) / 2)) βˆ’ 1))
330329rspceeqv 3633 . . . . . . . . . . . . 13 ((((𝑗 + 1) / 2) ∈ (1...π‘˜) ∧ 𝑗 = ((2 Β· ((𝑗 + 1) / 2)) βˆ’ 1)) β†’ βˆƒπ‘š ∈ (1...π‘˜)𝑗 = ((2 Β· π‘š) βˆ’ 1))
331317, 327, 330syl2anc 585 . . . . . . . . . . . 12 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ βˆƒπ‘š ∈ (1...π‘˜)𝑗 = ((2 Β· π‘š) βˆ’ 1))
332 eqidd 2734 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ (1...π‘˜) ∧ 𝑗 = ((2 Β· π‘š) βˆ’ 1)) β†’ (𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)) = (𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)))
333 oveq2 7414 . . . . . . . . . . . . . . . . . . 19 (𝑖 = π‘š β†’ (2 Β· 𝑖) = (2 Β· π‘š))
334333oveq1d 7421 . . . . . . . . . . . . . . . . . 18 (𝑖 = π‘š β†’ ((2 Β· 𝑖) βˆ’ 1) = ((2 Β· π‘š) βˆ’ 1))
335334adantl 483 . . . . . . . . . . . . . . . . 17 (((π‘š ∈ (1...π‘˜) ∧ 𝑗 = ((2 Β· π‘š) βˆ’ 1)) ∧ 𝑖 = π‘š) β†’ ((2 Β· 𝑖) βˆ’ 1) = ((2 Β· π‘š) βˆ’ 1))
336 simpl 484 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ (1...π‘˜) ∧ 𝑗 = ((2 Β· π‘š) βˆ’ 1)) β†’ π‘š ∈ (1...π‘˜))
337 ovexd 7441 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ (1...π‘˜) ∧ 𝑗 = ((2 Β· π‘š) βˆ’ 1)) β†’ ((2 Β· π‘š) βˆ’ 1) ∈ V)
338332, 335, 336, 337fvmptd 7003 . . . . . . . . . . . . . . . 16 ((π‘š ∈ (1...π‘˜) ∧ 𝑗 = ((2 Β· π‘š) βˆ’ 1)) β†’ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘š) = ((2 Β· π‘š) βˆ’ 1))
339 id 22 . . . . . . . . . . . . . . . . . 18 (𝑗 = ((2 Β· π‘š) βˆ’ 1) β†’ 𝑗 = ((2 Β· π‘š) βˆ’ 1))
340339eqcomd 2739 . . . . . . . . . . . . . . . . 17 (𝑗 = ((2 Β· π‘š) βˆ’ 1) β†’ ((2 Β· π‘š) βˆ’ 1) = 𝑗)
341340adantl 483 . . . . . . . . . . . . . . . 16 ((π‘š ∈ (1...π‘˜) ∧ 𝑗 = ((2 Β· π‘š) βˆ’ 1)) β†’ ((2 Β· π‘š) βˆ’ 1) = 𝑗)
342338, 341eqtr2d 2774 . . . . . . . . . . . . . . 15 ((π‘š ∈ (1...π‘˜) ∧ 𝑗 = ((2 Β· π‘š) βˆ’ 1)) β†’ 𝑗 = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘š))
343342ex 414 . . . . . . . . . . . . . 14 (π‘š ∈ (1...π‘˜) β†’ (𝑗 = ((2 Β· π‘š) βˆ’ 1) β†’ 𝑗 = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘š)))
344343adantl 483 . . . . . . . . . . . . 13 (((π‘˜ ∈ β„• ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) ∧ π‘š ∈ (1...π‘˜)) β†’ (𝑗 = ((2 Β· π‘š) βˆ’ 1) β†’ 𝑗 = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘š)))
345344reximdva 3169 . . . . . . . . . . . 12 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ (βˆƒπ‘š ∈ (1...π‘˜)𝑗 = ((2 Β· π‘š) βˆ’ 1) β†’ βˆƒπ‘š ∈ (1...π‘˜)𝑗 = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘š)))
346331, 345mpd 15 . . . . . . . . . . 11 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ βˆƒπ‘š ∈ (1...π‘˜)𝑗 = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘š))
347346ralrimiva 3147 . . . . . . . . . 10 (π‘˜ ∈ β„• β†’ βˆ€π‘— ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})βˆƒπ‘š ∈ (1...π‘˜)𝑗 = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘š))
348 dffo3 7101 . . . . . . . . . 10 ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)):(1...π‘˜)–ontoβ†’((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ↔ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)):(1...π‘˜)⟢((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∧ βˆ€π‘— ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})βˆƒπ‘š ∈ (1...π‘˜)𝑗 = ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘š)))
349213, 347, 348sylanbrc 584 . . . . . . . . 9 (π‘˜ ∈ β„• β†’ (𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)):(1...π‘˜)–ontoβ†’((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}))
350 df-f1o 6548 . . . . . . . . 9 ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)):(1...π‘˜)–1-1-ontoβ†’((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ↔ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)):(1...π‘˜)–1-1β†’((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ∧ (𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)):(1...π‘˜)–ontoβ†’((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})))
351258, 349, 350sylanbrc 584 . . . . . . . 8 (π‘˜ ∈ β„• β†’ (𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)):(1...π‘˜)–1-1-ontoβ†’((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}))
352351adantl 483 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)):(1...π‘˜)–1-1-ontoβ†’((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}))
353 eqidd 2734 . . . . . . . . 9 (𝑗 ∈ (1...π‘˜) β†’ (𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)) = (𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1)))
354 oveq2 7414 . . . . . . . . . . 11 (𝑖 = 𝑗 β†’ (2 Β· 𝑖) = (2 Β· 𝑗))
355354oveq1d 7421 . . . . . . . . . 10 (𝑖 = 𝑗 β†’ ((2 Β· 𝑖) βˆ’ 1) = ((2 Β· 𝑗) βˆ’ 1))
356355adantl 483 . . . . . . . . 9 ((𝑗 ∈ (1...π‘˜) ∧ 𝑖 = 𝑗) β†’ ((2 Β· 𝑖) βˆ’ 1) = ((2 Β· 𝑗) βˆ’ 1))
357 id 22 . . . . . . . . 9 (𝑗 ∈ (1...π‘˜) β†’ 𝑗 ∈ (1...π‘˜))
358 ovexd 7441 . . . . . . . . 9 (𝑗 ∈ (1...π‘˜) β†’ ((2 Β· 𝑗) βˆ’ 1) ∈ V)
359353, 356, 357, 358fvmptd 7003 . . . . . . . 8 (𝑗 ∈ (1...π‘˜) β†’ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘—) = ((2 Β· 𝑗) βˆ’ 1))
360359adantl 483 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...π‘˜)) β†’ ((𝑖 ∈ (1...π‘˜) ↦ ((2 Β· 𝑖) βˆ’ 1))β€˜π‘—) = ((2 Β· 𝑗) βˆ’ 1))
361 eleq1w 2817 . . . . . . . . . 10 (𝑗 = 𝑖 β†’ (𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}) ↔ 𝑖 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})))
362361anbi2d 630 . . . . . . . . 9 (𝑗 = 𝑖 β†’ (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) ↔ ((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑖 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•}))))
363139eleq1d 2819 . . . . . . . . 9 (𝑗 = 𝑖 β†’ ((πΉβ€˜π‘—) ∈ β„‚ ↔ (πΉβ€˜π‘–) ∈ β„‚))
364362, 363imbi12d 345 . . . . . . . 8 (𝑗 = 𝑖 β†’ ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ (πΉβ€˜π‘—) ∈ β„‚) ↔ (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑖 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ (πΉβ€˜π‘–) ∈ β„‚)))
365364, 136chvarvv 2003 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑖 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})) β†’ (πΉβ€˜π‘–) ∈ β„‚)
366143, 144, 352, 360, 365fsumf1o 15666 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ Σ𝑖 ∈ ((1...((2 Β· π‘˜) βˆ’ 1)) βˆ– {𝑛 ∈ β„• ∣ (𝑛 / 2) ∈ β„•})(πΉβ€˜π‘–) = Σ𝑗 ∈ (1...π‘˜)(πΉβ€˜((2 Β· 𝑗) βˆ’ 1)))
36795, 142, 3663eqtrrd 2778 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (1...π‘˜)(πΉβ€˜((2 Β· 𝑗) βˆ’ 1)) = Σ𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))(πΉβ€˜π‘—))
368 ovex 7439 . . . . . . . . . 10 ((2 Β· π‘˜) βˆ’ 1) ∈ V
36920fvmpt2 7007 . . . . . . . . . 10 ((π‘˜ ∈ β„• ∧ ((2 Β· π‘˜) βˆ’ 1) ∈ V) β†’ ((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜) = ((2 Β· π‘˜) βˆ’ 1))
370368, 369mpan2 690 . . . . . . . . 9 (π‘˜ ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜) = ((2 Β· π‘˜) βˆ’ 1))
371370oveq2d 7422 . . . . . . . 8 (π‘˜ ∈ β„• β†’ (1...((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜)) = (1...((2 Β· π‘˜) βˆ’ 1)))
372371eqcomd 2739 . . . . . . 7 (π‘˜ ∈ β„• β†’ (1...((2 Β· π‘˜) βˆ’ 1)) = (1...((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜)))
373372sumeq1d 15644 . . . . . 6 (π‘˜ ∈ β„• β†’ Σ𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))(πΉβ€˜π‘—) = Σ𝑗 ∈ (1...((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜))(πΉβ€˜π‘—))
374373adantl 483 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1))(πΉβ€˜π‘—) = Σ𝑗 ∈ (1...((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜))(πΉβ€˜π‘—))
375367, 374eqtrd 2773 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (1...π‘˜)(πΉβ€˜((2 Β· 𝑗) βˆ’ 1)) = Σ𝑗 ∈ (1...((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜))(πΉβ€˜π‘—))
376 elfznn 13527 . . . . . . 7 (𝑗 ∈ (1...π‘˜) β†’ 𝑗 ∈ β„•)
377376adantl 483 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...π‘˜)) β†’ 𝑗 ∈ β„•)
37812adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (1...π‘˜)) β†’ 𝐹:β„•βŸΆβ„‚)
37930a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ (1...π‘˜) β†’ 2 ∈ β„€)
380 elfzelz 13498 . . . . . . . . . . . 12 (𝑗 ∈ (1...π‘˜) β†’ 𝑗 ∈ β„€)
381379, 380zmulcld 12669 . . . . . . . . . . 11 (𝑗 ∈ (1...π‘˜) β†’ (2 Β· 𝑗) ∈ β„€)
382 1zzd 12590 . . . . . . . . . . 11 (𝑗 ∈ (1...π‘˜) β†’ 1 ∈ β„€)
383381, 382zsubcld 12668 . . . . . . . . . 10 (𝑗 ∈ (1...π‘˜) β†’ ((2 Β· 𝑗) βˆ’ 1) ∈ β„€)
384 0red 11214 . . . . . . . . . . 11 (𝑗 ∈ (1...π‘˜) β†’ 0 ∈ ℝ)
38538a1i 11 . . . . . . . . . . . . 13 (𝑗 ∈ (1...π‘˜) β†’ 2 ∈ ℝ)
38624, 385eqeltrid 2838 . . . . . . . . . . . 12 (𝑗 ∈ (1...π‘˜) β†’ (2 Β· 1) ∈ ℝ)
387 1red 11212 . . . . . . . . . . . 12 (𝑗 ∈ (1...π‘˜) β†’ 1 ∈ ℝ)
388386, 387resubcld 11639 . . . . . . . . . . 11 (𝑗 ∈ (1...π‘˜) β†’ ((2 Β· 1) βˆ’ 1) ∈ ℝ)
389383zred 12663 . . . . . . . . . . 11 (𝑗 ∈ (1...π‘˜) β†’ ((2 Β· 𝑗) βˆ’ 1) ∈ ℝ)
390 0lt1 11733 . . . . . . . . . . . 12 0 < 1
391153a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ (1...π‘˜) β†’ 1 = ((2 Β· 1) βˆ’ 1))
392390, 391breqtrid 5185 . . . . . . . . . . 11 (𝑗 ∈ (1...π‘˜) β†’ 0 < ((2 Β· 1) βˆ’ 1))
393381zred 12663 . . . . . . . . . . . 12 (𝑗 ∈ (1...π‘˜) β†’ (2 Β· 𝑗) ∈ ℝ)
394376nnred 12224 . . . . . . . . . . . . 13 (𝑗 ∈ (1...π‘˜) β†’ 𝑗 ∈ ℝ)
395161a1i 11 . . . . . . . . . . . . 13 (𝑗 ∈ (1...π‘˜) β†’ 0 ≀ 2)
396 elfzle1 13501 . . . . . . . . . . . . 13 (𝑗 ∈ (1...π‘˜) β†’ 1 ≀ 𝑗)
397387, 394, 385, 395, 396lemul2ad 12151 . . . . . . . . . . . 12 (𝑗 ∈ (1...π‘˜) β†’ (2 Β· 1) ≀ (2 Β· 𝑗))
398386, 393, 387, 397lesub1dd 11827 . . . . . . . . . . 11 (𝑗 ∈ (1...π‘˜) β†’ ((2 Β· 1) βˆ’ 1) ≀ ((2 Β· 𝑗) βˆ’ 1))
399384, 388, 389, 392, 398ltletrd 11371 . . . . . . . . . 10 (𝑗 ∈ (1...π‘˜) β†’ 0 < ((2 Β· 𝑗) βˆ’ 1))
400 elnnz 12565 . . . . . . . . . 10 (((2 Β· 𝑗) βˆ’ 1) ∈ β„• ↔ (((2 Β· 𝑗) βˆ’ 1) ∈ β„€ ∧ 0 < ((2 Β· 𝑗) βˆ’ 1)))
401383, 399, 400sylanbrc 584 . . . . . . . . 9 (𝑗 ∈ (1...π‘˜) β†’ ((2 Β· 𝑗) βˆ’ 1) ∈ β„•)
402401adantl 483 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (1...π‘˜)) β†’ ((2 Β· 𝑗) βˆ’ 1) ∈ β„•)
403378, 402ffvelcdmd 7085 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (1...π‘˜)) β†’ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1)) ∈ β„‚)
404403adantlr 714 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...π‘˜)) β†’ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1)) ∈ β„‚)
40559fveq2d 6893 . . . . . . . 8 (π‘˜ = 𝑗 β†’ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)) = (πΉβ€˜((2 Β· 𝑗) βˆ’ 1)))
406405cbvmptv 5261 . . . . . . 7 (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1))) = (𝑗 ∈ β„• ↦ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1)))
407406fvmpt2 7007 . . . . . 6 ((𝑗 ∈ β„• ∧ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1)) ∈ β„‚) β†’ ((π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))β€˜π‘—) = (πΉβ€˜((2 Β· 𝑗) βˆ’ 1)))
408377, 404, 407syl2anc 585 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...π‘˜)) β†’ ((π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))β€˜π‘—) = (πΉβ€˜((2 Β· 𝑗) βˆ’ 1)))
409 simpr 486 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
410409, 8eleqtrdi 2844 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ (β„€β‰₯β€˜1))
411408, 410, 404fsumser 15673 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (1...π‘˜)(πΉβ€˜((2 Β· 𝑗) βˆ’ 1)) = (seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1))))β€˜π‘˜))
412 eqidd 2734 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜))) β†’ (πΉβ€˜π‘—) = (πΉβ€˜π‘—))
413155a1i 11 . . . . . . . . . 10 (π‘˜ ∈ β„• β†’ (2 Β· 1) ∈ ℝ)
414 1red 11212 . . . . . . . . . 10 (π‘˜ ∈ β„• β†’ 1 ∈ ℝ)
415161a1i 11 . . . . . . . . . . 11 (π‘˜ ∈ β„• β†’ 0 ≀ 2)
416 nnge1 12237 . . . . . . . . . . 11 (π‘˜ ∈ β„• β†’ 1 ≀ π‘˜)
417414, 40, 39, 415, 416lemul2ad 12151 . . . . . . . . . 10 (π‘˜ ∈ β„• β†’ (2 Β· 1) ≀ (2 Β· π‘˜))
418413, 41, 414, 417lesub1dd 11827 . . . . . . . . 9 (π‘˜ ∈ β„• β†’ ((2 Β· 1) βˆ’ 1) ≀ ((2 Β· π‘˜) βˆ’ 1))
419153, 418eqbrtrid 5183 . . . . . . . 8 (π‘˜ ∈ β„• β†’ 1 ≀ ((2 Β· π‘˜) βˆ’ 1))
420 eluz2 12825 . . . . . . . 8 (((2 Β· π‘˜) βˆ’ 1) ∈ (β„€β‰₯β€˜1) ↔ (1 ∈ β„€ ∧ ((2 Β· π‘˜) βˆ’ 1) ∈ β„€ ∧ 1 ≀ ((2 Β· π‘˜) βˆ’ 1)))
42136, 65, 419, 420syl3anbrc 1344 . . . . . . 7 (π‘˜ ∈ β„• β†’ ((2 Β· π‘˜) βˆ’ 1) ∈ (β„€β‰₯β€˜1))
42267, 421eqeltrd 2834 . . . . . 6 (π‘˜ ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜) ∈ (β„€β‰₯β€˜1))
423422adantl 483 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜) ∈ (β„€β‰₯β€˜1))
424 simpll 766 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜))) β†’ πœ‘)
425 simpr 486 . . . . . . . 8 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ (1...((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜))) β†’ 𝑗 ∈ (1...((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜)))
426371adantr 482 . . . . . . . 8 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ (1...((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜))) β†’ (1...((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜)) = (1...((2 Β· π‘˜) βˆ’ 1)))
427425, 426eleqtrd 2836 . . . . . . 7 ((π‘˜ ∈ β„• ∧ 𝑗 ∈ (1...((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜))) β†’ 𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)))
428427adantll 713 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜))) β†’ 𝑗 ∈ (1...((2 Β· π‘˜) βˆ’ 1)))
429424, 428, 93syl2anc 585 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜))) β†’ (πΉβ€˜π‘—) ∈ β„‚)
430412, 423, 429fsumser 15673 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (1...((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜))(πΉβ€˜π‘—) = (seq1( + , 𝐹)β€˜((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜)))
431375, 411, 4303eqtr3d 2781 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1))))β€˜π‘˜) = (seq1( + , 𝐹)β€˜((π‘˜ ∈ β„• ↦ ((2 Β· π‘˜) βˆ’ 1))β€˜π‘˜)))
4321, 2, 6, 7, 8, 9, 11, 15, 16, 29, 73, 75, 431climsuse 44311 . 2 (πœ‘ β†’ seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))) ⇝ 𝐡)
433 eqidd 2734 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜) = (πΉβ€˜π‘˜))
4348, 9, 433, 13isum 15662 . . 3 (πœ‘ β†’ Ξ£π‘˜ ∈ β„• (πΉβ€˜π‘˜) = ( ⇝ β€˜seq1( + , 𝐹)))
435 climrel 15433 . . . . . . 7 Rel ⇝
436435releldmi 5946 . . . . . 6 (seq1( + , 𝐹) ⇝ 𝐡 β†’ seq1( + , 𝐹) ∈ dom ⇝ )
43716, 436syl 17 . . . . 5 (πœ‘ β†’ seq1( + , 𝐹) ∈ dom ⇝ )
438 climdm 15495 . . . . 5 (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq1( + , 𝐹) ⇝ ( ⇝ β€˜seq1( + , 𝐹)))
439437, 438sylib 217 . . . 4 (πœ‘ β†’ seq1( + , 𝐹) ⇝ ( ⇝ β€˜seq1( + , 𝐹)))
440 climuni 15493 . . . 4 ((seq1( + , 𝐹) ⇝ ( ⇝ β€˜seq1( + , 𝐹)) ∧ seq1( + , 𝐹) ⇝ 𝐡) β†’ ( ⇝ β€˜seq1( + , 𝐹)) = 𝐡)
441439, 16, 440syl2anc 585 . . 3 (πœ‘ β†’ ( ⇝ β€˜seq1( + , 𝐹)) = 𝐡)
442435a1i 11 . . . . . . . 8 (πœ‘ β†’ Rel ⇝ )
443 releldm 5942 . . . . . . . 8 ((Rel ⇝ ∧ seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))) ⇝ 𝐡) β†’ seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))) ∈ dom ⇝ )
444442, 432, 443syl2anc 585 . . . . . . 7 (πœ‘ β†’ seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))) ∈ dom ⇝ )
445 climdm 15495 . . . . . . 7 (seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))) ∈ dom ⇝ ↔ seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))) ⇝ ( ⇝ β€˜seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1))))))
446444, 445sylib 217 . . . . . 6 (πœ‘ β†’ seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))) ⇝ ( ⇝ β€˜seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1))))))
447406a1i 11 . . . . . . . 8 (πœ‘ β†’ (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1))) = (𝑗 ∈ β„• ↦ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1))))
448447seqeq3d 13971 . . . . . . 7 (πœ‘ β†’ seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))) = seq1( + , (𝑗 ∈ β„• ↦ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1)))))
449448fveq2d 6893 . . . . . 6 (πœ‘ β†’ ( ⇝ β€˜seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1))))) = ( ⇝ β€˜seq1( + , (𝑗 ∈ β„• ↦ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1))))))
450446, 449breqtrd 5174 . . . . 5 (πœ‘ β†’ seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))) ⇝ ( ⇝ β€˜seq1( + , (𝑗 ∈ β„• ↦ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1))))))
451 climuni 15493 . . . . 5 ((seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))) ⇝ 𝐡 ∧ seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))) ⇝ ( ⇝ β€˜seq1( + , (𝑗 ∈ β„• ↦ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1)))))) β†’ 𝐡 = ( ⇝ β€˜seq1( + , (𝑗 ∈ β„• ↦ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1))))))
452432, 450, 451syl2anc 585 . . . 4 (πœ‘ β†’ 𝐡 = ( ⇝ β€˜seq1( + , (𝑗 ∈ β„• ↦ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1))))))
453 eqidd 2734 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (𝑗 ∈ β„• ↦ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1))) = (𝑗 ∈ β„• ↦ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1))))
454 eqcom 2740 . . . . . . . 8 (π‘˜ = 𝑗 ↔ 𝑗 = π‘˜)
455 eqcom 2740 . . . . . . . 8 ((πΉβ€˜((2 Β· π‘˜) βˆ’ 1)) = (πΉβ€˜((2 Β· 𝑗) βˆ’ 1)) ↔ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1)) = (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))
456405, 454, 4553imtr3i 291 . . . . . . 7 (𝑗 = π‘˜ β†’ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1)) = (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))
457456adantl 483 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 = π‘˜) β†’ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1)) = (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))
45812adantr 482 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐹:β„•βŸΆβ„‚)
459421, 8eleqtrrdi 2845 . . . . . . . 8 (π‘˜ ∈ β„• β†’ ((2 Β· π‘˜) βˆ’ 1) ∈ β„•)
460459adantl 483 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) βˆ’ 1) ∈ β„•)
461458, 460ffvelcdmd 7085 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)) ∈ β„‚)
462453, 457, 409, 461fvmptd 7003 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((𝑗 ∈ β„• ↦ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1)))β€˜π‘˜) = (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))
4638, 9, 462, 461isum 15662 . . . 4 (πœ‘ β†’ Ξ£π‘˜ ∈ β„• (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)) = ( ⇝ β€˜seq1( + , (𝑗 ∈ β„• ↦ (πΉβ€˜((2 Β· 𝑗) βˆ’ 1))))))
464452, 463eqtr4d 2776 . . 3 (πœ‘ β†’ 𝐡 = Ξ£π‘˜ ∈ β„• (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))
465434, 441, 4643eqtrd 2777 . 2 (πœ‘ β†’ Ξ£π‘˜ ∈ β„• (πΉβ€˜π‘˜) = Ξ£π‘˜ ∈ β„• (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))
466432, 465jca 513 1 (πœ‘ β†’ (seq1( + , (π‘˜ ∈ β„• ↦ (πΉβ€˜((2 Β· π‘˜) βˆ’ 1)))) ⇝ 𝐡 ∧ Ξ£π‘˜ ∈ β„• (πΉβ€˜π‘˜) = Ξ£π‘˜ ∈ β„• (πΉβ€˜((2 Β· π‘˜) βˆ’ 1))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322   class class class wbr 5148   ↦ cmpt 5231  dom cdm 5676  Rel wrel 5681  βŸΆwf 6537  β€“1-1β†’wf1 6538  β€“ontoβ†’wfo 6539  β€“1-1-ontoβ†’wf1o 6540  β€˜cfv 6541  (class class class)co 7406  Fincfn 8936  β„‚cc 11105  β„cr 11106  0cc0 11107  1c1 11108   + caddc 11110   Β· cmul 11112   < clt 11245   ≀ cle 11246   βˆ’ cmin 11441   / cdiv 11868  β„•cn 12209  2c2 12264  β„€cz 12555  β„€β‰₯cuz 12819  β„+crp 12971  ...cfz 13481  seqcseq 13963   ⇝ cli 15425  Ξ£csu 15629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-sup 9434  df-oi 9502  df-card 9931  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-n0 12470  df-z 12556  df-uz 12820  df-rp 12972  df-fz 13482  df-fzo 13625  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429  df-sum 15630
This theorem is referenced by:  fouriersw  44934
  Copyright terms: Public domain W3C validator