Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  seq3id3 GIF version

Theorem seq3id3 10292
 Description: A sequence that consists entirely of "zeroes" sums to "zero". More precisely, a constant sequence with value an element which is a + -idempotent sums (or "+'s") to that element. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Jim Kingdon, 8-Apr-2023.)
Hypotheses
Ref Expression
iseqid3s.1 (𝜑 → (𝑍 + 𝑍) = 𝑍)
iseqid3s.2 (𝜑𝑁 ∈ (ℤ𝑀))
iseqid3s.3 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝐹𝑥) = 𝑍)
iseqid3s.z (𝜑𝑍𝑆)
iseqid3s.f ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ 𝑆)
iseqid3s.cl ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
Assertion
Ref Expression
seq3id3 (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍)
Distinct variable groups:   𝑥,𝑦, +   𝑥,𝐹,𝑦   𝑥,𝑀,𝑦   𝜑,𝑥,𝑦   𝑥,𝑍,𝑦   𝑥,𝑁,𝑦   𝑥,𝑆,𝑦

Proof of Theorem seq3id3
Dummy variables 𝑘 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iseqid3s.2 . . 3 (𝜑𝑁 ∈ (ℤ𝑀))
2 eluzfz2 9824 . . 3 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ (𝑀...𝑁))
3 fveqeq2 5430 . . . . 5 (𝑤 = 𝑀 → ((seq𝑀( + , 𝐹)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘𝑀) = 𝑍))
43imbi2d 229 . . . 4 (𝑤 = 𝑀 → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = 𝑍)))
5 fveqeq2 5430 . . . . 5 (𝑤 = 𝑘 → ((seq𝑀( + , 𝐹)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍))
65imbi2d 229 . . . 4 (𝑤 = 𝑘 → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘𝑘) = 𝑍)))
7 fveqeq2 5430 . . . . 5 (𝑤 = (𝑘 + 1) → ((seq𝑀( + , 𝐹)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = 𝑍))
87imbi2d 229 . . . 4 (𝑤 = (𝑘 + 1) → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = 𝑍)))
9 fveqeq2 5430 . . . . 5 (𝑤 = 𝑁 → ((seq𝑀( + , 𝐹)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘𝑁) = 𝑍))
109imbi2d 229 . . . 4 (𝑤 = 𝑁 → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍)))
11 eluzel2 9343 . . . . . . . 8 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
121, 11syl 14 . . . . . . 7 (𝜑𝑀 ∈ ℤ)
13 iseqid3s.f . . . . . . 7 ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ 𝑆)
14 iseqid3s.cl . . . . . . 7 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
1512, 13, 14seq3-1 10245 . . . . . 6 (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹𝑀))
16 iseqid3s.3 . . . . . . . 8 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝐹𝑥) = 𝑍)
1716ralrimiva 2505 . . . . . . 7 (𝜑 → ∀𝑥 ∈ (𝑀...𝑁)(𝐹𝑥) = 𝑍)
18 eluzfz1 9823 . . . . . . . 8 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑁))
19 fveqeq2 5430 . . . . . . . . 9 (𝑥 = 𝑀 → ((𝐹𝑥) = 𝑍 ↔ (𝐹𝑀) = 𝑍))
2019rspcv 2785 . . . . . . . 8 (𝑀 ∈ (𝑀...𝑁) → (∀𝑥 ∈ (𝑀...𝑁)(𝐹𝑥) = 𝑍 → (𝐹𝑀) = 𝑍))
211, 18, 203syl 17 . . . . . . 7 (𝜑 → (∀𝑥 ∈ (𝑀...𝑁)(𝐹𝑥) = 𝑍 → (𝐹𝑀) = 𝑍))
2217, 21mpd 13 . . . . . 6 (𝜑 → (𝐹𝑀) = 𝑍)
2315, 22eqtrd 2172 . . . . 5 (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = 𝑍)
2423a1i 9 . . . 4 (𝑁 ∈ (ℤ𝑀) → (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = 𝑍))
25 elfzouz 9940 . . . . . . . . . . 11 (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ (ℤ𝑀))
2625adantl 275 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ (ℤ𝑀))
2713adantlr 468 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ 𝑆)
2814adantlr 468 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀..^𝑁)) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
2926, 27, 28seq3p1 10247 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1))))
3029adantr 274 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1))))
31 simpr 109 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → (seq𝑀( + , 𝐹)‘𝑘) = 𝑍)
32 fveqeq2 5430 . . . . . . . . . . 11 (𝑥 = (𝑘 + 1) → ((𝐹𝑥) = 𝑍 ↔ (𝐹‘(𝑘 + 1)) = 𝑍))
3317adantr 274 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀...𝑁)(𝐹𝑥) = 𝑍)
34 fzofzp1 10016 . . . . . . . . . . . 12 (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁))
3534adantl 275 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁))
3632, 33, 35rspcdva 2794 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑘 + 1)) = 𝑍)
3736adantr 274 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → (𝐹‘(𝑘 + 1)) = 𝑍)
3831, 37oveq12d 5792 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1))) = (𝑍 + 𝑍))
39 iseqid3s.1 . . . . . . . . 9 (𝜑 → (𝑍 + 𝑍) = 𝑍)
4039ad2antrr 479 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → (𝑍 + 𝑍) = 𝑍)
4130, 38, 403eqtrd 2176 . . . . . . 7 (((𝜑𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = 𝑍)
4241ex 114 . . . . . 6 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → ((seq𝑀( + , 𝐹)‘𝑘) = 𝑍 → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = 𝑍))
4342expcom 115 . . . . 5 (𝑘 ∈ (𝑀..^𝑁) → (𝜑 → ((seq𝑀( + , 𝐹)‘𝑘) = 𝑍 → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = 𝑍)))
4443a2d 26 . . . 4 (𝑘 ∈ (𝑀..^𝑁) → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → (𝜑 → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = 𝑍)))
454, 6, 8, 10, 24, 44fzind2 10028 . . 3 (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍))
461, 2, 453syl 17 . 2 (𝜑 → (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍))
4746pm2.43i 49 1 (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1331   ∈ wcel 1480  ∀wral 2416  ‘cfv 5123  (class class class)co 5774  1c1 7633   + caddc 7635  ℤcz 9066  ℤ≥cuz 9338  ...cfz 9802  ..^cfzo 9931  seqcseq 10230 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7723  ax-resscn 7724  ax-1cn 7725  ax-1re 7726  ax-icn 7727  ax-addcl 7728  ax-addrcl 7729  ax-mulcl 7730  ax-addcom 7732  ax-addass 7734  ax-distr 7736  ax-i2m1 7737  ax-0lt1 7738  ax-0id 7740  ax-rnegex 7741  ax-cnre 7743  ax-pre-ltirr 7744  ax-pre-ltwlin 7745  ax-pre-lttrn 7746  ax-pre-ltadd 7748 This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-frec 6288  df-pnf 7814  df-mnf 7815  df-xr 7816  df-ltxr 7817  df-le 7818  df-sub 7947  df-neg 7948  df-inn 8733  df-n0 8990  df-z 9067  df-uz 9339  df-fz 9803  df-fzo 9932  df-seqfrec 10231 This theorem is referenced by:  seq3id  10293  ser0  10299  prodf1  11323
 Copyright terms: Public domain W3C validator