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

Theorem seq3id3 10121
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 9653 . . 3 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ (𝑀...𝑁))
3 fveqeq2 5362 . . . . 5 (𝑤 = 𝑀 → ((seq𝑀( + , 𝐹)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘𝑀) = 𝑍))
43imbi2d 229 . . . 4 (𝑤 = 𝑀 → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = 𝑍)))
5 fveqeq2 5362 . . . . 5 (𝑤 = 𝑘 → ((seq𝑀( + , 𝐹)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍))
65imbi2d 229 . . . 4 (𝑤 = 𝑘 → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘𝑘) = 𝑍)))
7 fveqeq2 5362 . . . . 5 (𝑤 = (𝑘 + 1) → ((seq𝑀( + , 𝐹)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = 𝑍))
87imbi2d 229 . . . 4 (𝑤 = (𝑘 + 1) → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = 𝑍)))
9 fveqeq2 5362 . . . . 5 (𝑤 = 𝑁 → ((seq𝑀( + , 𝐹)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘𝑁) = 𝑍))
109imbi2d 229 . . . 4 (𝑤 = 𝑁 → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍)))
11 eluzel2 9181 . . . . . . . 8 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
121, 11syl 14 . . . . . . 7 (𝜑𝑀 ∈ ℤ)
13 iseqid3s.f . . . . . . 7 ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ 𝑆)
14 iseqid3s.cl . . . . . . 7 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
1512, 13, 14seq3-1 10074 . . . . . 6 (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹𝑀))
16 iseqid3s.3 . . . . . . . 8 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝐹𝑥) = 𝑍)
1716ralrimiva 2464 . . . . . . 7 (𝜑 → ∀𝑥 ∈ (𝑀...𝑁)(𝐹𝑥) = 𝑍)
18 eluzfz1 9652 . . . . . . . 8 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑁))
19 fveqeq2 5362 . . . . . . . . 9 (𝑥 = 𝑀 → ((𝐹𝑥) = 𝑍 ↔ (𝐹𝑀) = 𝑍))
2019rspcv 2740 . . . . . . . 8 (𝑀 ∈ (𝑀...𝑁) → (∀𝑥 ∈ (𝑀...𝑁)(𝐹𝑥) = 𝑍 → (𝐹𝑀) = 𝑍))
211, 18, 203syl 17 . . . . . . 7 (𝜑 → (∀𝑥 ∈ (𝑀...𝑁)(𝐹𝑥) = 𝑍 → (𝐹𝑀) = 𝑍))
2217, 21mpd 13 . . . . . 6 (𝜑 → (𝐹𝑀) = 𝑍)
2315, 22eqtrd 2132 . . . . 5 (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = 𝑍)
2423a1i 9 . . . 4 (𝑁 ∈ (ℤ𝑀) → (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = 𝑍))
25 elfzouz 9769 . . . . . . . . . . 11 (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ (ℤ𝑀))
2625adantl 273 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ (ℤ𝑀))
2713adantlr 464 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ 𝑆)
2814adantlr 464 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀..^𝑁)) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
2926, 27, 28seq3p1 10076 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1))))
3029adantr 272 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1))))
31 simpr 109 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → (seq𝑀( + , 𝐹)‘𝑘) = 𝑍)
32 fveqeq2 5362 . . . . . . . . . . 11 (𝑥 = (𝑘 + 1) → ((𝐹𝑥) = 𝑍 ↔ (𝐹‘(𝑘 + 1)) = 𝑍))
3317adantr 272 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀...𝑁)(𝐹𝑥) = 𝑍)
34 fzofzp1 9845 . . . . . . . . . . . 12 (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁))
3534adantl 273 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁))
3632, 33, 35rspcdva 2749 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑘 + 1)) = 𝑍)
3736adantr 272 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → (𝐹‘(𝑘 + 1)) = 𝑍)
3831, 37oveq12d 5724 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1))) = (𝑍 + 𝑍))
39 iseqid3s.1 . . . . . . . . 9 (𝜑 → (𝑍 + 𝑍) = 𝑍)
4039ad2antrr 475 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → (𝑍 + 𝑍) = 𝑍)
4130, 38, 403eqtrd 2136 . . . . . . 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 9857 . . 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 1299  wcel 1448  wral 2375  cfv 5059  (class class class)co 5706  1c1 7501   + caddc 7503  cz 8906  cuz 9176  ...cfz 9631  ..^cfzo 9760  seqcseq 10059
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-coll 3983  ax-sep 3986  ax-nul 3994  ax-pow 4038  ax-pr 4069  ax-un 4293  ax-setind 4390  ax-iinf 4440  ax-cnex 7586  ax-resscn 7587  ax-1cn 7588  ax-1re 7589  ax-icn 7590  ax-addcl 7591  ax-addrcl 7592  ax-mulcl 7593  ax-addcom 7595  ax-addass 7597  ax-distr 7599  ax-i2m1 7600  ax-0lt1 7601  ax-0id 7603  ax-rnegex 7604  ax-cnre 7606  ax-pre-ltirr 7607  ax-pre-ltwlin 7608  ax-pre-lttrn 7609  ax-pre-ltadd 7611
This theorem depends on definitions:  df-bi 116  df-3or 931  df-3an 932  df-tru 1302  df-fal 1305  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ne 2268  df-nel 2363  df-ral 2380  df-rex 2381  df-reu 2382  df-rab 2384  df-v 2643  df-sbc 2863  df-csb 2956  df-dif 3023  df-un 3025  df-in 3027  df-ss 3034  df-nul 3311  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-int 3719  df-iun 3762  df-br 3876  df-opab 3930  df-mpt 3931  df-tr 3967  df-id 4153  df-iord 4226  df-on 4228  df-ilim 4229  df-suc 4231  df-iom 4443  df-xp 4483  df-rel 4484  df-cnv 4485  df-co 4486  df-dm 4487  df-rn 4488  df-res 4489  df-ima 4490  df-iota 5024  df-fun 5061  df-fn 5062  df-f 5063  df-f1 5064  df-fo 5065  df-f1o 5066  df-fv 5067  df-riota 5662  df-ov 5709  df-oprab 5710  df-mpo 5711  df-1st 5969  df-2nd 5970  df-recs 6132  df-frec 6218  df-pnf 7674  df-mnf 7675  df-xr 7676  df-ltxr 7677  df-le 7678  df-sub 7806  df-neg 7807  df-inn 8579  df-n0 8830  df-z 8907  df-uz 9177  df-fz 9632  df-fzo 9761  df-seqfrec 10060
This theorem is referenced by:  seq3id  10122  ser0  10128
  Copyright terms: Public domain W3C validator