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

Theorem iserodd 15378
Description: Collect the odd terms in a sequence. (Contributed by Mario Carneiro, 7-Apr-2015.)
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 11598 . 2 0 = (ℤ‘0)
2 nnuz 11599 . 2 ℕ = (ℤ‘1)
3 0zd 11266 . 2 (𝜑 → 0 ∈ ℤ)
4 1zzd 11285 . 2 (𝜑 → 1 ∈ ℤ)
5 2nn0 11186 . . . . . 6 2 ∈ ℕ0
65a1i 11 . . . . 5 (𝜑 → 2 ∈ ℕ0)
7 nn0mulcl 11206 . . . . 5 ((2 ∈ ℕ0𝑚 ∈ ℕ0) → (2 · 𝑚) ∈ ℕ0)
86, 7sylan 487 . . . 4 ((𝜑𝑚 ∈ ℕ0) → (2 · 𝑚) ∈ ℕ0)
9 nn0p1nn 11209 . . . 4 ((2 · 𝑚) ∈ ℕ0 → ((2 · 𝑚) + 1) ∈ ℕ)
108, 9syl 17 . . 3 ((𝜑𝑚 ∈ ℕ0) → ((2 · 𝑚) + 1) ∈ ℕ)
11 eqid 2610 . . 3 (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)) = (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))
1210, 11fmptd 6292 . 2 (𝜑 → (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)):ℕ0⟶ℕ)
13 nn0mulcl 11206 . . . . . 6 ((2 ∈ ℕ0𝑖 ∈ ℕ0) → (2 · 𝑖) ∈ ℕ0)
146, 13sylan 487 . . . . 5 ((𝜑𝑖 ∈ ℕ0) → (2 · 𝑖) ∈ ℕ0)
1514nn0red 11229 . . . 4 ((𝜑𝑖 ∈ ℕ0) → (2 · 𝑖) ∈ ℝ)
16 peano2nn0 11210 . . . . . 6 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
17 nn0mulcl 11206 . . . . . 6 ((2 ∈ ℕ0 ∧ (𝑖 + 1) ∈ ℕ0) → (2 · (𝑖 + 1)) ∈ ℕ0)
186, 16, 17syl2an 493 . . . . 5 ((𝜑𝑖 ∈ ℕ0) → (2 · (𝑖 + 1)) ∈ ℕ0)
1918nn0red 11229 . . . 4 ((𝜑𝑖 ∈ ℕ0) → (2 · (𝑖 + 1)) ∈ ℝ)
20 1red 9934 . . . 4 ((𝜑𝑖 ∈ ℕ0) → 1 ∈ ℝ)
21 nn0re 11178 . . . . . . 7 (𝑖 ∈ ℕ0𝑖 ∈ ℝ)
2221adantl 481 . . . . . 6 ((𝜑𝑖 ∈ ℕ0) → 𝑖 ∈ ℝ)
2322ltp1d 10833 . . . . 5 ((𝜑𝑖 ∈ ℕ0) → 𝑖 < (𝑖 + 1))
2416adantl 481 . . . . . . 7 ((𝜑𝑖 ∈ ℕ0) → (𝑖 + 1) ∈ ℕ0)
2524nn0red 11229 . . . . . 6 ((𝜑𝑖 ∈ ℕ0) → (𝑖 + 1) ∈ ℝ)
26 2re 10967 . . . . . . 7 2 ∈ ℝ
2726a1i 11 . . . . . 6 ((𝜑𝑖 ∈ ℕ0) → 2 ∈ ℝ)
28 2pos 10989 . . . . . . 7 0 < 2
2928a1i 11 . . . . . 6 ((𝜑𝑖 ∈ ℕ0) → 0 < 2)
30 ltmul2 10753 . . . . . 6 ((𝑖 ∈ ℝ ∧ (𝑖 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑖 < (𝑖 + 1) ↔ (2 · 𝑖) < (2 · (𝑖 + 1))))
3122, 25, 27, 29, 30syl112anc 1322 . . . . 5 ((𝜑𝑖 ∈ ℕ0) → (𝑖 < (𝑖 + 1) ↔ (2 · 𝑖) < (2 · (𝑖 + 1))))
3223, 31mpbid 221 . . . 4 ((𝜑𝑖 ∈ ℕ0) → (2 · 𝑖) < (2 · (𝑖 + 1)))
3315, 19, 20, 32ltadd1dd 10517 . . 3 ((𝜑𝑖 ∈ ℕ0) → ((2 · 𝑖) + 1) < ((2 · (𝑖 + 1)) + 1))
34 oveq2 6557 . . . . . 6 (𝑚 = 𝑖 → (2 · 𝑚) = (2 · 𝑖))
3534oveq1d 6564 . . . . 5 (𝑚 = 𝑖 → ((2 · 𝑚) + 1) = ((2 · 𝑖) + 1))
36 ovex 6577 . . . . 5 ((2 · 𝑖) + 1) ∈ V
3735, 11, 36fvmpt 6191 . . . 4 (𝑖 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖) = ((2 · 𝑖) + 1))
3837adantl 481 . . 3 ((𝜑𝑖 ∈ ℕ0) → ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖) = ((2 · 𝑖) + 1))
39 oveq2 6557 . . . . . 6 (𝑚 = (𝑖 + 1) → (2 · 𝑚) = (2 · (𝑖 + 1)))
4039oveq1d 6564 . . . . 5 (𝑚 = (𝑖 + 1) → ((2 · 𝑚) + 1) = ((2 · (𝑖 + 1)) + 1))
41 ovex 6577 . . . . 5 ((2 · (𝑖 + 1)) + 1) ∈ V
4240, 11, 41fvmpt 6191 . . . 4 ((𝑖 + 1) ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘(𝑖 + 1)) = ((2 · (𝑖 + 1)) + 1))
4324, 42syl 17 . . 3 ((𝜑𝑖 ∈ ℕ0) → ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘(𝑖 + 1)) = ((2 · (𝑖 + 1)) + 1))
4433, 38, 433brtr4d 4615 . 2 ((𝜑𝑖 ∈ ℕ0) → ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖) < ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘(𝑖 + 1)))
45 eldifi 3694 . . . . . . 7 (𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))) → 𝑛 ∈ ℕ)
46 simpr 476 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
47 0cnd 9912 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 2 ∥ 𝑛) → 0 ∈ ℂ)
48 nnz 11276 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
4948adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
50 odd2np1 14903 . . . . . . . . . . . . 13 (𝑛 ∈ ℤ → (¬ 2 ∥ 𝑛 ↔ ∃𝑘 ∈ ℤ ((2 · 𝑘) + 1) = 𝑛))
5149, 50syl 17 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (¬ 2 ∥ 𝑛 ↔ ∃𝑘 ∈ ℤ ((2 · 𝑘) + 1) = 𝑛))
52 simprl 790 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 𝑘 ∈ ℤ)
53 nnm1nn0 11211 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
5453ad2antlr 759 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → (𝑛 − 1) ∈ ℕ0)
5554nn0red 11229 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → (𝑛 − 1) ∈ ℝ)
5654nn0ge0d 11231 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 0 ≤ (𝑛 − 1))
5726a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 2 ∈ ℝ)
5828a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 0 < 2)
59 divge0 10771 . . . . . . . . . . . . . . . . . 18 ((((𝑛 − 1) ∈ ℝ ∧ 0 ≤ (𝑛 − 1)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑛 − 1) / 2))
6055, 56, 57, 58, 59syl22anc 1319 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 0 ≤ ((𝑛 − 1) / 2))
61 simprr 792 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → ((2 · 𝑘) + 1) = 𝑛)
6261oveq1d 6564 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → (((2 · 𝑘) + 1) − 1) = (𝑛 − 1))
63 2cn 10968 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℂ
64 zcn 11259 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
6564ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 𝑘 ∈ ℂ)
66 mulcl 9899 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · 𝑘) ∈ ℂ)
6763, 65, 66sylancr 694 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → (2 · 𝑘) ∈ ℂ)
68 ax-1cn 9873 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℂ
69 pncan 10166 . . . . . . . . . . . . . . . . . . . . 21 (((2 · 𝑘) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑘) + 1) − 1) = (2 · 𝑘))
7067, 68, 69sylancl 693 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → (((2 · 𝑘) + 1) − 1) = (2 · 𝑘))
7162, 70eqtr3d 2646 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → (𝑛 − 1) = (2 · 𝑘))
7271oveq1d 6564 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → ((𝑛 − 1) / 2) = ((2 · 𝑘) / 2))
73 2cnd 10970 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 2 ∈ ℂ)
74 2ne0 10990 . . . . . . . . . . . . . . . . . . . 20 2 ≠ 0
7574a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 2 ≠ 0)
7665, 73, 75divcan3d 10685 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → ((2 · 𝑘) / 2) = 𝑘)
7772, 76eqtrd 2644 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → ((𝑛 − 1) / 2) = 𝑘)
7860, 77breqtrd 4609 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 0 ≤ 𝑘)
79 elnn0z 11267 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘))
8052, 78, 79sylanbrc 695 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛)) → 𝑘 ∈ ℕ0)
8180ex 449 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛) → 𝑘 ∈ ℕ0))
82 simpr 476 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛) → ((2 · 𝑘) + 1) = 𝑛)
8382eqcomd 2616 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛) → 𝑛 = ((2 · 𝑘) + 1))
8483a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛) → 𝑛 = ((2 · 𝑘) + 1)))
8581, 84jcad 554 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = 𝑛) → (𝑘 ∈ ℕ0𝑛 = ((2 · 𝑘) + 1))))
8685reximdv2 2997 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (∃𝑘 ∈ ℤ ((2 · 𝑘) + 1) = 𝑛 → ∃𝑘 ∈ ℕ0 𝑛 = ((2 · 𝑘) + 1)))
8751, 86sylbid 229 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (¬ 2 ∥ 𝑛 → ∃𝑘 ∈ ℕ0 𝑛 = ((2 · 𝑘) + 1)))
88 iserodd.f . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → 𝐶 ∈ ℂ)
89 iserodd.h . . . . . . . . . . . . . . 15 (𝑛 = ((2 · 𝑘) + 1) → 𝐵 = 𝐶)
9089eleq1d 2672 . . . . . . . . . . . . . 14 (𝑛 = ((2 · 𝑘) + 1) → (𝐵 ∈ ℂ ↔ 𝐶 ∈ ℂ))
9188, 90syl5ibrcom 236 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (𝑛 = ((2 · 𝑘) + 1) → 𝐵 ∈ ℂ))
9291rexlimdva 3013 . . . . . . . . . . . 12 (𝜑 → (∃𝑘 ∈ ℕ0 𝑛 = ((2 · 𝑘) + 1) → 𝐵 ∈ ℂ))
9392adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (∃𝑘 ∈ ℕ0 𝑛 = ((2 · 𝑘) + 1) → 𝐵 ∈ ℂ))
9487, 93syld 46 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (¬ 2 ∥ 𝑛𝐵 ∈ ℂ))
9594imp 444 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ ¬ 2 ∥ 𝑛) → 𝐵 ∈ ℂ)
9647, 95ifclda 4070 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → if(2 ∥ 𝑛, 0, 𝐵) ∈ ℂ)
97 eqid 2610 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵)) = (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))
9897fvmpt2 6200 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ if(2 ∥ 𝑛, 0, 𝐵) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = if(2 ∥ 𝑛, 0, 𝐵))
9946, 96, 98syl2anc 691 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = if(2 ∥ 𝑛, 0, 𝐵))
10045, 99sylan2 490 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = if(2 ∥ 𝑛, 0, 𝐵))
101 eldif 3550 . . . . . . . 8 (𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))) ↔ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))))
102 vex 3176 . . . . . . . . . . . 12 𝑛 ∈ V
103 oveq2 6557 . . . . . . . . . . . . . . 15 (𝑚 = 𝑘 → (2 · 𝑚) = (2 · 𝑘))
104103oveq1d 6564 . . . . . . . . . . . . . 14 (𝑚 = 𝑘 → ((2 · 𝑚) + 1) = ((2 · 𝑘) + 1))
105104cbvmptv 4678 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)) = (𝑘 ∈ ℕ0 ↦ ((2 · 𝑘) + 1))
106105elrnmpt 5293 . . . . . . . . . . . 12 (𝑛 ∈ V → (𝑛 ∈ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)) ↔ ∃𝑘 ∈ ℕ0 𝑛 = ((2 · 𝑘) + 1)))
107102, 106ax-mp 5 . . . . . . . . . . 11 (𝑛 ∈ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)) ↔ ∃𝑘 ∈ ℕ0 𝑛 = ((2 · 𝑘) + 1))
10887, 107syl6ibr 241 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (¬ 2 ∥ 𝑛𝑛 ∈ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))))
109108con1d 138 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (¬ 𝑛 ∈ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)) → 2 ∥ 𝑛))
110109impr 647 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))) → 2 ∥ 𝑛)
111101, 110sylan2b 491 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))) → 2 ∥ 𝑛)
112111iftrued 4044 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))) → if(2 ∥ 𝑛, 0, 𝐵) = 0)
113100, 112eqtrd 2644 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = 0)
114113ralrimiva 2949 . . . 4 (𝜑 → ∀𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = 0)
115 nfv 1830 . . . . 5 𝑗((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = 0
116 nffvmpt1 6111 . . . . . 6 𝑛((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑗)
117116nfeq1 2764 . . . . 5 𝑛((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑗) = 0
118 fveq2 6103 . . . . . 6 (𝑛 = 𝑗 → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑗))
119118eqeq1d 2612 . . . . 5 (𝑛 = 𝑗 → (((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = 0 ↔ ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑗) = 0))
120115, 117, 119cbvral 3143 . . . 4 (∀𝑛 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑛) = 0 ↔ ∀𝑗 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑗) = 0)
121114, 120sylib 207 . . 3 (𝜑 → ∀𝑗 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑗) = 0)
122121r19.21bi 2916 . 2 ((𝜑𝑗 ∈ (ℕ ∖ ran (𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1)))) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑗) = 0)
12396, 97fmptd 6292 . . 3 (𝜑 → (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵)):ℕ⟶ℂ)
124123ffvelrnda 6267 . 2 ((𝜑𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘𝑗) ∈ ℂ)
125 simpr 476 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
126 eqid 2610 . . . . . . . 8 (𝑘 ∈ ℕ0𝐶) = (𝑘 ∈ ℕ0𝐶)
127126fvmpt2 6200 . . . . . . 7 ((𝑘 ∈ ℕ0𝐶 ∈ ℂ) → ((𝑘 ∈ ℕ0𝐶)‘𝑘) = 𝐶)
128125, 88, 127syl2anc 691 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝑘 ∈ ℕ0𝐶)‘𝑘) = 𝐶)
129 ovex 6577 . . . . . . . . . 10 ((2 · 𝑘) + 1) ∈ V
130104, 11, 129fvmpt 6191 . . . . . . . . 9 (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘) = ((2 · 𝑘) + 1))
131130adantl 481 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘) = ((2 · 𝑘) + 1))
132131fveq2d 6107 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘)) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((2 · 𝑘) + 1)))
133 nn0mulcl 11206 . . . . . . . . . 10 ((2 ∈ ℕ0𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℕ0)
1346, 133sylan 487 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℕ0)
135 nn0p1nn 11209 . . . . . . . . 9 ((2 · 𝑘) ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ)
136134, 135syl 17 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ∈ ℕ)
137 2z 11286 . . . . . . . . . . . 12 2 ∈ ℤ
138 nn0z 11277 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
139138adantl 481 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℤ)
140 dvdsmul1 14841 . . . . . . . . . . . 12 ((2 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 2 ∥ (2 · 𝑘))
141137, 139, 140sylancr 694 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 2 ∥ (2 · 𝑘))
142134nn0zd 11356 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℤ)
143 2nn 11062 . . . . . . . . . . . . 13 2 ∈ ℕ
144143a1i 11 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 2 ∈ ℕ)
145 1lt2 11071 . . . . . . . . . . . . 13 1 < 2
146145a1i 11 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 1 < 2)
147 ndvdsp1 14973 . . . . . . . . . . . 12 (((2 · 𝑘) ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2) → (2 ∥ (2 · 𝑘) → ¬ 2 ∥ ((2 · 𝑘) + 1)))
148142, 144, 146, 147syl3anc 1318 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (2 ∥ (2 · 𝑘) → ¬ 2 ∥ ((2 · 𝑘) + 1)))
149141, 148mpd 15 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ¬ 2 ∥ ((2 · 𝑘) + 1))
150149iffalsed 4047 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → if(2 ∥ ((2 · 𝑘) + 1), 0, 𝐶) = 𝐶)
151150, 88eqeltrd 2688 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → if(2 ∥ ((2 · 𝑘) + 1), 0, 𝐶) ∈ ℂ)
152 breq2 4587 . . . . . . . . . 10 (𝑛 = ((2 · 𝑘) + 1) → (2 ∥ 𝑛 ↔ 2 ∥ ((2 · 𝑘) + 1)))
153152, 89ifbieq2d 4061 . . . . . . . . 9 (𝑛 = ((2 · 𝑘) + 1) → if(2 ∥ 𝑛, 0, 𝐵) = if(2 ∥ ((2 · 𝑘) + 1), 0, 𝐶))
154153, 97fvmptg 6189 . . . . . . . 8 ((((2 · 𝑘) + 1) ∈ ℕ ∧ if(2 ∥ ((2 · 𝑘) + 1), 0, 𝐶) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((2 · 𝑘) + 1)) = if(2 ∥ ((2 · 𝑘) + 1), 0, 𝐶))
155136, 151, 154syl2anc 691 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((2 · 𝑘) + 1)) = if(2 ∥ ((2 · 𝑘) + 1), 0, 𝐶))
156132, 155, 1503eqtrd 2648 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘)) = 𝐶)
157128, 156eqtr4d 2647 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((𝑘 ∈ ℕ0𝐶)‘𝑘) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘)))
158157ralrimiva 2949 . . . 4 (𝜑 → ∀𝑘 ∈ ℕ0 ((𝑘 ∈ ℕ0𝐶)‘𝑘) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘)))
159 nfv 1830 . . . . 5 𝑖((𝑘 ∈ ℕ0𝐶)‘𝑘) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘))
160 nffvmpt1 6111 . . . . . 6 𝑘((𝑘 ∈ ℕ0𝐶)‘𝑖)
161160nfeq1 2764 . . . . 5 𝑘((𝑘 ∈ ℕ0𝐶)‘𝑖) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖))
162 fveq2 6103 . . . . . 6 (𝑘 = 𝑖 → ((𝑘 ∈ ℕ0𝐶)‘𝑘) = ((𝑘 ∈ ℕ0𝐶)‘𝑖))
163 fveq2 6103 . . . . . . 7 (𝑘 = 𝑖 → ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘) = ((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖))
164163fveq2d 6107 . . . . . 6 (𝑘 = 𝑖 → ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘)) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖)))
165162, 164eqeq12d 2625 . . . . 5 (𝑘 = 𝑖 → (((𝑘 ∈ ℕ0𝐶)‘𝑘) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘)) ↔ ((𝑘 ∈ ℕ0𝐶)‘𝑖) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖))))
166159, 161, 165cbvral 3143 . . . 4 (∀𝑘 ∈ ℕ0 ((𝑘 ∈ ℕ0𝐶)‘𝑘) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑘)) ↔ ∀𝑖 ∈ ℕ0 ((𝑘 ∈ ℕ0𝐶)‘𝑖) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖)))
167158, 166sylib 207 . . 3 (𝜑 → ∀𝑖 ∈ ℕ0 ((𝑘 ∈ ℕ0𝐶)‘𝑖) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖)))
168167r19.21bi 2916 . 2 ((𝜑𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0𝐶)‘𝑖) = ((𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))‘((𝑚 ∈ ℕ0 ↦ ((2 · 𝑚) + 1))‘𝑖)))
1691, 2, 3, 4, 12, 44, 122, 124, 168isercoll2 14247 1 (𝜑 → (seq0( + , (𝑘 ∈ ℕ0𝐶)) ⇝ 𝐴 ↔ seq1( + , (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))) ⇝ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  wne 2780  wral 2896  wrex 2897  Vcvv 3173  cdif 3537  ifcif 4036   class class class wbr 4583  cmpt 4643  ran crn 5039  cfv 5804  (class class class)co 6549  cc 9813  cr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   < clt 9953  cle 9954  cmin 10145   / cdiv 10563  cn 10897  2c2 10947  0cn0 11169  cz 11254  seqcseq 12663  cli 14063  cdvds 14821
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-xnn0 11241  df-z 11255  df-uz 11564  df-rp 11709  df-fz 12198  df-seq 12664  df-exp 12723  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-dvds 14822
This theorem is referenced by:  atantayl3  24466  leibpilem2  24468
  Copyright terms: Public domain W3C validator