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

Theorem iserodd 16832
Description: Collect the odd terms in a sequence. (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 10-Jul-2022.)
Hypotheses
Ref Expression
iserodd.f ((𝜑𝑘 ∈ ℕ0) → 𝐶 ∈ ℂ)
iserodd.h (𝑛 = ((2 · 𝑘) + 1) → 𝐵 = 𝐶)
Assertion
Ref Expression
iserodd (𝜑 → (seq0( + , (𝑘 ∈ ℕ0𝐶)) ⇝ 𝐴 ↔ seq1( + , (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))) ⇝ 𝐴))
Distinct variable groups:   𝐵,𝑘   𝐶,𝑛   𝑘,𝑛,𝜑
Allowed substitution hints:   𝐴(𝑘,𝑛)   𝐵(𝑛)   𝐶(𝑘)

Proof of Theorem iserodd
Dummy variables 𝑖 𝑗 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0uz 12911 . 2 0 = (ℤ‘0)
2 nnuz 12912 . 2 ℕ = (ℤ‘1)
3 0zd 12617 . 2 (𝜑 → 0 ∈ ℤ)
4 1zzd 12640 . 2 (𝜑 → 1 ∈ ℤ)
5 2nn0 12536 . . . . . 6 2 ∈ ℕ0
65a1i 11 . . . . 5 (𝜑 → 2 ∈ ℕ0)
7 nn0mulcl 12555 . . . . 5 ((2 ∈ ℕ0𝑚 ∈ ℕ0) → (2 · 𝑚) ∈ ℕ0)
86, 7sylan 578 . . . 4 ((𝜑𝑚 ∈ ℕ0) → (2 · 𝑚) ∈ ℕ0)
9 nn0p1nn 12558 . . . 4 ((2 · 𝑚) ∈ ℕ0 → ((2 · 𝑚) + 1) ∈ ℕ)
108, 9syl 17 . . 3 ((𝜑𝑚 ∈ ℕ0) → ((2 · 𝑚) + 1) ∈ ℕ)
1110fmpttd 7128 . 2 (𝜑 → (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)):ℕ0⟶ℕ)
12 nn0mulcl 12555 . . . . . 6 ((2 ∈ ℕ0𝑖 ∈ ℕ0) → (2 · 𝑖) ∈ ℕ0)
136, 12sylan 578 . . . . 5 ((𝜑𝑖 ∈ ℕ0) → (2 · 𝑖) ∈ ℕ0)
1413nn0red 12580 . . . 4 ((𝜑𝑖 ∈ ℕ0) → (2 · 𝑖) ∈ ℝ)
15 peano2nn0 12559 . . . . . 6 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
16 nn0mulcl 12555 . . . . . 6 ((2 ∈ ℕ0 ∧ (𝑖 + 1) ∈ ℕ0) → (2 · (𝑖 + 1)) ∈ ℕ0)
176, 15, 16syl2an 594 . . . . 5 ((𝜑𝑖 ∈ ℕ0) → (2 · (𝑖 + 1)) ∈ ℕ0)
1817nn0red 12580 . . . 4 ((𝜑𝑖 ∈ ℕ0) → (2 · (𝑖 + 1)) ∈ ℝ)
19 1red 11261 . . . 4 ((𝜑𝑖 ∈ ℕ0) → 1 ∈ ℝ)
20 nn0re 12528 . . . . . . 7 (𝑖 ∈ ℕ0𝑖 ∈ ℝ)
2120adantl 480 . . . . . 6 ((𝜑𝑖 ∈ ℕ0) → 𝑖 ∈ ℝ)
2221ltp1d 12191 . . . . 5 ((𝜑𝑖 ∈ ℕ0) → 𝑖 < (𝑖 + 1))
23 1red 11261 . . . . . . . 8 (𝑖 ∈ ℕ0 → 1 ∈ ℝ)
2420, 23readdcld 11289 . . . . . . 7 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℝ)
25 2rp 13028 . . . . . . . 8 2 ∈ ℝ+
2625a1i 11 . . . . . . 7 (𝑖 ∈ ℕ0 → 2 ∈ ℝ+)
2720, 24, 26ltmul2d 13107 . . . . . 6 (𝑖 ∈ ℕ0 → (𝑖 < (𝑖 + 1) ↔ (2 · 𝑖) < (2 · (𝑖 + 1))))
2827adantl 480 . . . . 5 ((𝜑𝑖 ∈ ℕ0) → (𝑖 < (𝑖 + 1) ↔ (2 · 𝑖) < (2 · (𝑖 + 1))))
2922, 28mpbid 231 . . . 4 ((𝜑𝑖 ∈ ℕ0) → (2 · 𝑖) < (2 · (𝑖 + 1)))
3014, 18, 19, 29ltadd1dd 11871 . . 3 ((𝜑𝑖 ∈ ℕ0) → ((2 · 𝑖) + 1) < ((2 · (𝑖 + 1)) + 1))
31 oveq2 7431 . . . . . 6 (𝑚 = 𝑖 → (2 · 𝑚) = (2 · 𝑖))
3231oveq1d 7438 . . . . 5 (𝑚 = 𝑖 → ((2 · 𝑚) + 1) = ((2 · 𝑖) + 1))
33 eqid 2725 . . . . 5 (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)) = (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))
34 ovex 7456 . . . . 5 ((2 · 𝑖) + 1) ∈ V
3532, 33, 34fvmpt 7008 . . . 4 (𝑖 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖) = ((2 · 𝑖) + 1))
3635adantl 480 . . 3 ((𝜑𝑖 ∈ ℕ0) → ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖) = ((2 · 𝑖) + 1))
3715adantl 480 . . . 4 ((𝜑𝑖 ∈ ℕ0) → (𝑖 + 1) ∈ ℕ0)
38 oveq2 7431 . . . . . 6 (𝑚 = (𝑖 + 1) → (2 · 𝑚) = (2 · (𝑖 + 1)))
3938oveq1d 7438 . . . . 5 (𝑚 = (𝑖 + 1) → ((2 · 𝑚) + 1) = ((2 · (𝑖 + 1)) + 1))
40 ovex 7456 . . . . 5 ((2 · (𝑖 + 1)) + 1) ∈ V
4139, 33, 40fvmpt 7008 . . . 4 ((𝑖 + 1) ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘(𝑖 + 1)) = ((2 · (𝑖 + 1)) + 1))
4237, 41syl 17 . . 3 ((𝜑𝑖 ∈ ℕ0) → ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘(𝑖 + 1)) = ((2 · (𝑖 + 1)) + 1))
4330, 36, 423brtr4d 5184 . 2 ((𝜑𝑖 ∈ ℕ0) → ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖) < ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘(𝑖 + 1)))
44 eldifi 4125 . . . . . . 7 (𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))) → 𝑛 ∈ ℕ)
45 simpr 483 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
46 0cnd 11253 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 2 ∥ 𝑛) → 0 ∈ ℂ)
47 nnz 12626 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
4847adantl 480 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
49 odd2np1 16338 . . . . . . . . . . . . 13 (𝑛 ∈ ℤ → (¬ 2 ∥ 𝑛 ↔ ∃𝑘 ∈ ℤ ((2 · 𝑘) + 1) = 𝑛))
5048, 49syl 17 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (¬ 2 ∥ 𝑛 ↔ ∃𝑘 ∈ ℤ ((2 · 𝑘) + 1) = 𝑛))
51 simprl 769 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 𝑘 ∈ ℤ)
52 nnm1nn0 12560 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
5352ad2antlr 725 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → (𝑛 − 1) ∈ ℕ0)
5453nn0red 12580 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → (𝑛 − 1) ∈ ℝ)
5525a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 2 ∈ ℝ+)
5653nn0ge0d 12582 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 0 ≤ (𝑛 − 1))
5754, 55, 56divge0d 13105 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 0 ≤ ((𝑛 − 1) / 2))
58 simprr 771 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → ((2 · 𝑘) + 1) = 𝑛)
5958oveq1d 7438 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → (((2 · 𝑘) + 1) − 1) = (𝑛 − 1))
60 2cn 12334 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℂ
61 zcn 12610 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
6261ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 𝑘 ∈ ℂ)
63 mulcl 11238 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · 𝑘) ∈ ℂ)
6460, 62, 63sylancr 585 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → (2 · 𝑘) ∈ ℂ)
65 ax-1cn 11212 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℂ
66 pncan 11512 . . . . . . . . . . . . . . . . . . . . 21 (((2 · 𝑘) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑘) + 1) − 1) = (2 · 𝑘))
6764, 65, 66sylancl 584 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → (((2 · 𝑘) + 1) − 1) = (2 · 𝑘))
6859, 67eqtr3d 2767 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → (𝑛 − 1) = (2 · 𝑘))
6968oveq1d 7438 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → ((𝑛 − 1) / 2) = ((2 · 𝑘) / 2))
70 2cnd 12337 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 2 ∈ ℂ)
71 2ne0 12363 . . . . . . . . . . . . . . . . . . . 20 2 ≠ 0
7271a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 2 ≠ 0)
7362, 70, 72divcan3d 12042 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → ((2 · 𝑘) / 2) = 𝑘)
7469, 73eqtrd 2765 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → ((𝑛 − 1) / 2) = 𝑘)
7557, 74breqtrd 5178 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 0 ≤ 𝑘)
76 elnn0z 12618 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘))
7751, 75, 76sylanbrc 581 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 𝑘 ∈ ℕ0)
7877ex 411 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛) → 𝑘 ∈ ℕ0))
79 simpr 483 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛) → ((2 · 𝑘) + 1) = 𝑛)
8079eqcomd 2731 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛) → 𝑛 = ((2 · 𝑘) + 1))
8178, 80jca2 512 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛) → (𝑘 ∈ ℕ0𝑛 = ((2 · 𝑘) + 1))))
8281reximdv2 3153 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (∃𝑘 ∈ ℤ ((2 · 𝑘) + 1) = 𝑛 → ∃𝑘 ∈ ℕ0 𝑛 = ((2 · 𝑘) + 1)))
8350, 82sylbid 239 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (¬ 2 ∥ 𝑛 → ∃𝑘 ∈ ℕ0 𝑛 = ((2 · 𝑘) + 1)))
84 iserodd.f . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → 𝐶 ∈ ℂ)
85 iserodd.h . . . . . . . . . . . . . . 15 (𝑛 = ((2 · 𝑘) + 1) → 𝐵 = 𝐶)
8685eleq1d 2810 . . . . . . . . . . . . . 14 (𝑛 = ((2 · 𝑘) + 1) → (𝐵 ∈ ℂ ↔ 𝐶 ∈ ℂ))
8784, 86syl5ibrcom 246 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (𝑛 = ((2 · 𝑘) + 1) → 𝐵 ∈ ℂ))
8887rexlimdva 3144 . . . . . . . . . . . 12 (𝜑 → (∃𝑘 ∈ ℕ0 𝑛 = ((2 · 𝑘) + 1) → 𝐵 ∈ ℂ))
8988adantr 479 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (∃𝑘 ∈ ℕ0 𝑛 = ((2 · 𝑘) + 1) → 𝐵 ∈ ℂ))
9083, 89syld 47 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (¬ 2 ∥ 𝑛𝐵 ∈ ℂ))
9190imp 405 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ ¬ 2 ∥ 𝑛) → 𝐵 ∈ ℂ)
9246, 91ifclda 4567 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → if(2 ∥ 𝑛, 0, 𝐵) ∈ ℂ)
93 eqid 2725 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵)) = (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))
9493fvmpt2 7019 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ if(2 ∥ 𝑛, 0, 𝐵) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = if(2 ∥ 𝑛, 0, 𝐵))
9545, 92, 94syl2anc 582 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = if(2 ∥ 𝑛, 0, 𝐵))
9644, 95sylan2 591 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = if(2 ∥ 𝑛, 0, 𝐵))
97 eldif 3956 . . . . . . . 8 (𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))) ↔ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))))
98 oveq2 7431 . . . . . . . . . . . . . . 15 (𝑚 = 𝑘 → (2 · 𝑚) = (2 · 𝑘))
9998oveq1d 7438 . . . . . . . . . . . . . 14 (𝑚 = 𝑘 → ((2 · 𝑚) + 1) = ((2 · 𝑘) + 1))
10099cbvmptv 5265 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)) = (𝑘 ∈ ℕ0 ↦ ((2 · 𝑘) + 1))
101100elrnmpt 5961 . . . . . . . . . . . 12 (𝑛 ∈ V → (𝑛 ∈ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)) ↔ ∃𝑘 ∈ ℕ0 𝑛 = ((2 · 𝑘) + 1)))
102101elv 3467 . . . . . . . . . . 11 (𝑛 ∈ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)) ↔ ∃𝑘 ∈ ℕ0 𝑛 = ((2 · 𝑘) + 1))
10383, 102imbitrrdi 251 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (¬ 2 ∥ 𝑛𝑛 ∈ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))))
104103con1d 145 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (¬ 𝑛 ∈ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)) → 2 ∥ 𝑛))
105104impr 453 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))) → 2 ∥ 𝑛)
10697, 105sylan2b 592 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))) → 2 ∥ 𝑛)
107106iftrued 4540 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))) → if(2 ∥ 𝑛, 0, 𝐵) = 0)
10896, 107eqtrd 2765 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = 0)
109108ralrimiva 3135 . . . 4 (𝜑 → ∀𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = 0)
110 nfv 1909 . . . . 5 𝑗((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = 0
111 nffvmpt1 6911 . . . . . 6 𝑛((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑗)
112111nfeq1 2907 . . . . 5 𝑛((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑗) = 0
113 fveqeq2 6909 . . . . 5 (𝑛 = 𝑗 → (((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = 0 ↔ ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑗) = 0))
114110, 112, 113cbvralw 3293 . . . 4 (∀𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = 0 ↔ ∀𝑗 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑗) = 0)
115109, 114sylib 217 . . 3 (𝜑 → ∀𝑗 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑗) = 0)
116115r19.21bi 3238 . 2 ((𝜑𝑗 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑗) = 0)
11792fmpttd 7128 . . 3 (𝜑 → (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵)):ℕ⟶ℂ)
118117ffvelcdmda 7097 . 2 ((𝜑𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑗) ∈ ℂ)
119 simpr 483 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
120 eqid 2725 . . . . . . . 8 (𝑘 ∈ ℕ0𝐶) = (𝑘 ∈ ℕ0𝐶)
121120fvmpt2 7019 . . . . . . 7 ((𝑘 ∈ ℕ0𝐶 ∈ ℂ) → ((𝑘 ∈ ℕ0𝐶)‘𝑘) = 𝐶)
122119, 84, 121syl2anc 582 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝑘 ∈ ℕ0𝐶)‘𝑘) = 𝐶)
123 ovex 7456 . . . . . . . . . 10 ((2 · 𝑘) + 1) ∈ V
12499, 33, 123fvmpt 7008 . . . . . . . . 9 (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘) = ((2 · 𝑘) + 1))
125124adantl 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘) = ((2 · 𝑘) + 1))
126125fveq2d 6904 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘)) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((2 · 𝑘) + 1)))
127 breq2 5156 . . . . . . . . 9 (𝑛 = ((2 · 𝑘) + 1) → (2 ∥ 𝑛 ↔ 2 ∥ ((2 · 𝑘) + 1)))
128127, 85ifbieq2d 4558 . . . . . . . 8 (𝑛 = ((2 · 𝑘) + 1) → if(2 ∥ 𝑛, 0, 𝐵) = if(2 ∥ ((2 · 𝑘) + 1), 0, 𝐶))
129 nn0mulcl 12555 . . . . . . . . . 10 ((2 ∈ ℕ0𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℕ0)
1306, 129sylan 578 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℕ0)
131 nn0p1nn 12558 . . . . . . . . 9 ((2 · 𝑘) ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ)
132130, 131syl 17 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ∈ ℕ)
133 2z 12641 . . . . . . . . . . . 12 2 ∈ ℤ
134 nn0z 12630 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
135134adantl 480 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℤ)
136 dvdsmul1 16275 . . . . . . . . . . . 12 ((2 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 2 ∥ (2 · 𝑘))
137133, 135, 136sylancr 585 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 2 ∥ (2 · 𝑘))
138130nn0zd 12631 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℤ)
139 2nn 12332 . . . . . . . . . . . . 13 2 ∈ ℕ
140139a1i 11 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 2 ∈ ℕ)
141 1lt2 12430 . . . . . . . . . . . . 13 1 < 2
142141a1i 11 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 1 < 2)
143 ndvdsp1 16408 . . . . . . . . . . . 12 (((2 · 𝑘) ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2) → (2 ∥ (2 · 𝑘) → ¬ 2 ∥ ((2 · 𝑘) + 1)))
144138, 140, 142, 143syl3anc 1368 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (2 ∥ (2 · 𝑘) → ¬ 2 ∥ ((2 · 𝑘) + 1)))
145137, 144mpd 15 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ¬ 2 ∥ ((2 · 𝑘) + 1))
146145iffalsed 4543 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → if(2 ∥ ((2 · 𝑘) + 1), 0, 𝐶) = 𝐶)
147146, 84eqeltrd 2825 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → if(2 ∥ ((2 · 𝑘) + 1), 0, 𝐶) ∈ ℂ)
14893, 128, 132, 147fvmptd3 7031 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((2 · 𝑘) + 1)) = if(2 ∥ ((2 · 𝑘) + 1), 0, 𝐶))
149126, 148, 1463eqtrd 2769 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘)) = 𝐶)
150122, 149eqtr4d 2768 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((𝑘 ∈ ℕ0𝐶)‘𝑘) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘)))
151150ralrimiva 3135 . . . 4 (𝜑 → ∀𝑘 ∈ ℕ0 ((𝑘 ∈ ℕ0𝐶)‘𝑘) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘)))
152 nfv 1909 . . . . 5 𝑖((𝑘 ∈ ℕ0𝐶)‘𝑘) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘))
153 nffvmpt1 6911 . . . . . 6 𝑘((𝑘 ∈ ℕ0𝐶)‘𝑖)
154153nfeq1 2907 . . . . 5 𝑘((𝑘 ∈ ℕ0𝐶)‘𝑖) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖))
155 fveq2 6900 . . . . . 6 (𝑘 = 𝑖 → ((𝑘 ∈ ℕ0𝐶)‘𝑘) = ((𝑘 ∈ ℕ0𝐶)‘𝑖))
156 2fveq3 6905 . . . . . 6 (𝑘 = 𝑖 → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘)) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖)))
157155, 156eqeq12d 2741 . . . . 5 (𝑘 = 𝑖 → (((𝑘 ∈ ℕ0𝐶)‘𝑘) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘)) ↔ ((𝑘 ∈ ℕ0𝐶)‘𝑖) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖))))
158152, 154, 157cbvralw 3293 . . . 4 (∀𝑘 ∈ ℕ0 ((𝑘 ∈ ℕ0𝐶)‘𝑘) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘)) ↔ ∀𝑖 ∈ ℕ0 ((𝑘 ∈ ℕ0𝐶)‘𝑖) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖)))
159151, 158sylib 217 . . 3 (𝜑 → ∀𝑖 ∈ ℕ0 ((𝑘 ∈ ℕ0𝐶)‘𝑖) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖)))
160159r19.21bi 3238 . 2 ((𝜑𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0𝐶)‘𝑖) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖)))
1611, 2, 3, 4, 11, 43, 116, 118, 160isercoll2 15668 1 (𝜑 → (seq0( + , (𝑘 ∈ ℕ0𝐶)) ⇝ 𝐴 ↔ seq1( + , (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))) ⇝ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  wne 2929  wral 3050  wrex 3059  Vcvv 3461  cdif 3943  ifcif 4532   class class class wbr 5152  cmpt 5235  ran crn 5682  cfv 6553  (class class class)co 7423  cc 11152  cr 11153  0cc0 11154  1c1 11155   + caddc 11157   · cmul 11159   < clt 11294  cle 11295  cmin 11490   / cdiv 11917  cn 12259  2c2 12314  0cn0 12519  cz 12605  +crp 13023  seqcseq 14016  cli 15481  cdvds 16251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745  ax-inf2 9680  ax-cnex 11210  ax-resscn 11211  ax-1cn 11212  ax-icn 11213  ax-addcl 11214  ax-addrcl 11215  ax-mulcl 11216  ax-mulrcl 11217  ax-mulcom 11218  ax-addass 11219  ax-mulass 11220  ax-distr 11221  ax-i2m1 11222  ax-1ne0 11223  ax-1rid 11224  ax-rnegex 11225  ax-rrecex 11226  ax-cnre 11227  ax-pre-lttri 11228  ax-pre-lttrn 11229  ax-pre-ltadd 11230  ax-pre-mulgt0 11231  ax-pre-sup 11232
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5579  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-we 5638  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-pred 6311  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7379  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7876  df-1st 8002  df-2nd 8003  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-oadd 8499  df-er 8733  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-sup 9481  df-inf 9482  df-card 9978  df-pnf 11296  df-mnf 11297  df-xr 11298  df-ltxr 11299  df-le 11300  df-sub 11492  df-neg 11493  df-div 11918  df-nn 12260  df-2 12322  df-3 12323  df-n0 12520  df-xnn0 12592  df-z 12606  df-uz 12870  df-rp 13024  df-fz 13534  df-seq 14017  df-exp 14077  df-hash 14343  df-shft 15067  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236  df-clim 15485  df-dvds 16252
This theorem is referenced by:  atantayl3  26959  leibpilem2  26961
  Copyright terms: Public domain W3C validator