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

Theorem ialgcvga 10827
Description: The countdown function 𝐶 remains 0 after 𝑁 steps. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypotheses
Ref Expression
algcvga.1 𝐹:𝑆𝑆
algcvga.2 𝑅 = seq0((𝐹 ∘ 1st ), (ℕ0 × {𝐴}), 𝑆)
algcvga.3 𝐶:𝑆⟶ℕ0
algcvga.4 (𝑧𝑆 → ((𝐶‘(𝐹𝑧)) ≠ 0 → (𝐶‘(𝐹𝑧)) < (𝐶𝑧)))
algcvga.5 𝑁 = (𝐶𝐴)
ialgcvga.s 𝑆𝑉
Assertion
Ref Expression
ialgcvga (𝐴𝑆 → (𝐾 ∈ (ℤ𝑁) → (𝐶‘(𝑅𝐾)) = 0))
Distinct variable groups:   𝑧,𝐶   𝑧,𝐹   𝑧,𝑅   𝑧,𝑆
Allowed substitution hints:   𝐴(𝑧)   𝐾(𝑧)   𝑁(𝑧)   𝑉(𝑧)

Proof of Theorem ialgcvga
Dummy variables 𝑘 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 algcvga.5 . . 3 𝑁 = (𝐶𝐴)
2 algcvga.3 . . . 4 𝐶:𝑆⟶ℕ0
32ffvelrni 5381 . . 3 (𝐴𝑆 → (𝐶𝐴) ∈ ℕ0)
41, 3syl5eqel 2171 . 2 (𝐴𝑆𝑁 ∈ ℕ0)
5 nn0z 8680 . . . 4 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
6 eluz1 8932 . . . . 5 (𝑁 ∈ ℤ → (𝐾 ∈ (ℤ𝑁) ↔ (𝐾 ∈ ℤ ∧ 𝑁𝐾)))
7 fveq2 5256 . . . . . . . . . 10 (𝑚 = 𝑁 → (𝑅𝑚) = (𝑅𝑁))
87fveq2d 5260 . . . . . . . . 9 (𝑚 = 𝑁 → (𝐶‘(𝑅𝑚)) = (𝐶‘(𝑅𝑁)))
98eqeq1d 2093 . . . . . . . 8 (𝑚 = 𝑁 → ((𝐶‘(𝑅𝑚)) = 0 ↔ (𝐶‘(𝑅𝑁)) = 0))
109imbi2d 228 . . . . . . 7 (𝑚 = 𝑁 → ((𝐴𝑆 → (𝐶‘(𝑅𝑚)) = 0) ↔ (𝐴𝑆 → (𝐶‘(𝑅𝑁)) = 0)))
11 fveq2 5256 . . . . . . . . . 10 (𝑚 = 𝑘 → (𝑅𝑚) = (𝑅𝑘))
1211fveq2d 5260 . . . . . . . . 9 (𝑚 = 𝑘 → (𝐶‘(𝑅𝑚)) = (𝐶‘(𝑅𝑘)))
1312eqeq1d 2093 . . . . . . . 8 (𝑚 = 𝑘 → ((𝐶‘(𝑅𝑚)) = 0 ↔ (𝐶‘(𝑅𝑘)) = 0))
1413imbi2d 228 . . . . . . 7 (𝑚 = 𝑘 → ((𝐴𝑆 → (𝐶‘(𝑅𝑚)) = 0) ↔ (𝐴𝑆 → (𝐶‘(𝑅𝑘)) = 0)))
15 fveq2 5256 . . . . . . . . . 10 (𝑚 = (𝑘 + 1) → (𝑅𝑚) = (𝑅‘(𝑘 + 1)))
1615fveq2d 5260 . . . . . . . . 9 (𝑚 = (𝑘 + 1) → (𝐶‘(𝑅𝑚)) = (𝐶‘(𝑅‘(𝑘 + 1))))
1716eqeq1d 2093 . . . . . . . 8 (𝑚 = (𝑘 + 1) → ((𝐶‘(𝑅𝑚)) = 0 ↔ (𝐶‘(𝑅‘(𝑘 + 1))) = 0))
1817imbi2d 228 . . . . . . 7 (𝑚 = (𝑘 + 1) → ((𝐴𝑆 → (𝐶‘(𝑅𝑚)) = 0) ↔ (𝐴𝑆 → (𝐶‘(𝑅‘(𝑘 + 1))) = 0)))
19 fveq2 5256 . . . . . . . . . 10 (𝑚 = 𝐾 → (𝑅𝑚) = (𝑅𝐾))
2019fveq2d 5260 . . . . . . . . 9 (𝑚 = 𝐾 → (𝐶‘(𝑅𝑚)) = (𝐶‘(𝑅𝐾)))
2120eqeq1d 2093 . . . . . . . 8 (𝑚 = 𝐾 → ((𝐶‘(𝑅𝑚)) = 0 ↔ (𝐶‘(𝑅𝐾)) = 0))
2221imbi2d 228 . . . . . . 7 (𝑚 = 𝐾 → ((𝐴𝑆 → (𝐶‘(𝑅𝑚)) = 0) ↔ (𝐴𝑆 → (𝐶‘(𝑅𝐾)) = 0)))
23 algcvga.1 . . . . . . . . 9 𝐹:𝑆𝑆
24 algcvga.2 . . . . . . . . 9 𝑅 = seq0((𝐹 ∘ 1st ), (ℕ0 × {𝐴}), 𝑆)
25 algcvga.4 . . . . . . . . 9 (𝑧𝑆 → ((𝐶‘(𝐹𝑧)) ≠ 0 → (𝐶‘(𝐹𝑧)) < (𝐶𝑧)))
26 ialgcvga.s . . . . . . . . 9 𝑆𝑉
2723, 24, 2, 25, 1, 26ialgcvg 10824 . . . . . . . 8 (𝐴𝑆 → (𝐶‘(𝑅𝑁)) = 0)
2827a1i 9 . . . . . . 7 (𝑁 ∈ ℤ → (𝐴𝑆 → (𝐶‘(𝑅𝑁)) = 0))
29 nn0ge0 8608 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)
3029adantr 270 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ0𝑘 ∈ ℤ) → 0 ≤ 𝑁)
31 nn0re 8592 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ0𝑁 ∈ ℝ)
32 zre 8664 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
33 0re 7409 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
34 letr 7489 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑘 ∈ ℝ) → ((0 ≤ 𝑁𝑁𝑘) → 0 ≤ 𝑘))
3533, 34mp3an1 1258 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℝ ∧ 𝑘 ∈ ℝ) → ((0 ≤ 𝑁𝑁𝑘) → 0 ≤ 𝑘))
3631, 32, 35syl2an 283 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ0𝑘 ∈ ℤ) → ((0 ≤ 𝑁𝑁𝑘) → 0 ≤ 𝑘))
3730, 36mpand 420 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0𝑘 ∈ ℤ) → (𝑁𝑘 → 0 ≤ 𝑘))
38 elnn0z 8673 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ0 ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘))
3938simplbi2 377 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℤ → (0 ≤ 𝑘𝑘 ∈ ℕ0))
4039adantl 271 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0𝑘 ∈ ℤ) → (0 ≤ 𝑘𝑘 ∈ ℕ0))
4137, 40syld 44 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0𝑘 ∈ ℤ) → (𝑁𝑘𝑘 ∈ ℕ0))
424, 41sylan 277 . . . . . . . . . . . . 13 ((𝐴𝑆𝑘 ∈ ℤ) → (𝑁𝑘𝑘 ∈ ℕ0))
4342impr 371 . . . . . . . . . . . 12 ((𝐴𝑆 ∧ (𝑘 ∈ ℤ ∧ 𝑁𝑘)) → 𝑘 ∈ ℕ0)
4443expcom 114 . . . . . . . . . . 11 ((𝑘 ∈ ℤ ∧ 𝑁𝑘) → (𝐴𝑆𝑘 ∈ ℕ0))
45443adant1 959 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑁𝑘) → (𝐴𝑆𝑘 ∈ ℕ0))
4645ancld 318 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑁𝑘) → (𝐴𝑆 → (𝐴𝑆𝑘 ∈ ℕ0)))
47 nn0uz 8962 . . . . . . . . . . . . 13 0 = (ℤ‘0)
48 0zd 8672 . . . . . . . . . . . . 13 (𝐴𝑆 → 0 ∈ ℤ)
49 id 19 . . . . . . . . . . . . 13 (𝐴𝑆𝐴𝑆)
5023a1i 9 . . . . . . . . . . . . 13 (𝐴𝑆𝐹:𝑆𝑆)
5126a1i 9 . . . . . . . . . . . . 13 (𝐴𝑆𝑆𝑉)
5247, 24, 48, 49, 50, 51ialgrf 10821 . . . . . . . . . . . 12 (𝐴𝑆𝑅:ℕ0𝑆)
5352ffvelrnda 5382 . . . . . . . . . . 11 ((𝐴𝑆𝑘 ∈ ℕ0) → (𝑅𝑘) ∈ 𝑆)
54 fveq2 5256 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑅𝑘) → (𝐹𝑧) = (𝐹‘(𝑅𝑘)))
5554fveq2d 5260 . . . . . . . . . . . . . . 15 (𝑧 = (𝑅𝑘) → (𝐶‘(𝐹𝑧)) = (𝐶‘(𝐹‘(𝑅𝑘))))
5655neeq1d 2269 . . . . . . . . . . . . . 14 (𝑧 = (𝑅𝑘) → ((𝐶‘(𝐹𝑧)) ≠ 0 ↔ (𝐶‘(𝐹‘(𝑅𝑘))) ≠ 0))
57 fveq2 5256 . . . . . . . . . . . . . . 15 (𝑧 = (𝑅𝑘) → (𝐶𝑧) = (𝐶‘(𝑅𝑘)))
5855, 57breq12d 3827 . . . . . . . . . . . . . 14 (𝑧 = (𝑅𝑘) → ((𝐶‘(𝐹𝑧)) < (𝐶𝑧) ↔ (𝐶‘(𝐹‘(𝑅𝑘))) < (𝐶‘(𝑅𝑘))))
5956, 58imbi12d 232 . . . . . . . . . . . . 13 (𝑧 = (𝑅𝑘) → (((𝐶‘(𝐹𝑧)) ≠ 0 → (𝐶‘(𝐹𝑧)) < (𝐶𝑧)) ↔ ((𝐶‘(𝐹‘(𝑅𝑘))) ≠ 0 → (𝐶‘(𝐹‘(𝑅𝑘))) < (𝐶‘(𝑅𝑘)))))
6059, 25vtoclga 2677 . . . . . . . . . . . 12 ((𝑅𝑘) ∈ 𝑆 → ((𝐶‘(𝐹‘(𝑅𝑘))) ≠ 0 → (𝐶‘(𝐹‘(𝑅𝑘))) < (𝐶‘(𝑅𝑘))))
6123, 2algcvgb 10826 . . . . . . . . . . . . 13 ((𝑅𝑘) ∈ 𝑆 → (((𝐶‘(𝐹‘(𝑅𝑘))) ≠ 0 → (𝐶‘(𝐹‘(𝑅𝑘))) < (𝐶‘(𝑅𝑘))) ↔ (((𝐶‘(𝑅𝑘)) ≠ 0 → (𝐶‘(𝐹‘(𝑅𝑘))) < (𝐶‘(𝑅𝑘))) ∧ ((𝐶‘(𝑅𝑘)) = 0 → (𝐶‘(𝐹‘(𝑅𝑘))) = 0))))
62 simpr 108 . . . . . . . . . . . . 13 ((((𝐶‘(𝑅𝑘)) ≠ 0 → (𝐶‘(𝐹‘(𝑅𝑘))) < (𝐶‘(𝑅𝑘))) ∧ ((𝐶‘(𝑅𝑘)) = 0 → (𝐶‘(𝐹‘(𝑅𝑘))) = 0)) → ((𝐶‘(𝑅𝑘)) = 0 → (𝐶‘(𝐹‘(𝑅𝑘))) = 0))
6361, 62syl6bi 161 . . . . . . . . . . . 12 ((𝑅𝑘) ∈ 𝑆 → (((𝐶‘(𝐹‘(𝑅𝑘))) ≠ 0 → (𝐶‘(𝐹‘(𝑅𝑘))) < (𝐶‘(𝑅𝑘))) → ((𝐶‘(𝑅𝑘)) = 0 → (𝐶‘(𝐹‘(𝑅𝑘))) = 0)))
6460, 63mpd 13 . . . . . . . . . . 11 ((𝑅𝑘) ∈ 𝑆 → ((𝐶‘(𝑅𝑘)) = 0 → (𝐶‘(𝐹‘(𝑅𝑘))) = 0))
6553, 64syl 14 . . . . . . . . . 10 ((𝐴𝑆𝑘 ∈ ℕ0) → ((𝐶‘(𝑅𝑘)) = 0 → (𝐶‘(𝐹‘(𝑅𝑘))) = 0))
6647, 24, 48, 49, 50, 51ialgrp1 10822 . . . . . . . . . . . 12 ((𝐴𝑆𝑘 ∈ ℕ0) → (𝑅‘(𝑘 + 1)) = (𝐹‘(𝑅𝑘)))
6766fveq2d 5260 . . . . . . . . . . 11 ((𝐴𝑆𝑘 ∈ ℕ0) → (𝐶‘(𝑅‘(𝑘 + 1))) = (𝐶‘(𝐹‘(𝑅𝑘))))
6867eqeq1d 2093 . . . . . . . . . 10 ((𝐴𝑆𝑘 ∈ ℕ0) → ((𝐶‘(𝑅‘(𝑘 + 1))) = 0 ↔ (𝐶‘(𝐹‘(𝑅𝑘))) = 0))
6965, 68sylibrd 167 . . . . . . . . 9 ((𝐴𝑆𝑘 ∈ ℕ0) → ((𝐶‘(𝑅𝑘)) = 0 → (𝐶‘(𝑅‘(𝑘 + 1))) = 0))
7046, 69syl6 33 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑁𝑘) → (𝐴𝑆 → ((𝐶‘(𝑅𝑘)) = 0 → (𝐶‘(𝑅‘(𝑘 + 1))) = 0)))
7170a2d 26 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑁𝑘) → ((𝐴𝑆 → (𝐶‘(𝑅𝑘)) = 0) → (𝐴𝑆 → (𝐶‘(𝑅‘(𝑘 + 1))) = 0)))
7210, 14, 18, 22, 28, 71uzind 8767 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁𝐾) → (𝐴𝑆 → (𝐶‘(𝑅𝐾)) = 0))
73723expib 1144 . . . . 5 (𝑁 ∈ ℤ → ((𝐾 ∈ ℤ ∧ 𝑁𝐾) → (𝐴𝑆 → (𝐶‘(𝑅𝐾)) = 0)))
746, 73sylbid 148 . . . 4 (𝑁 ∈ ℤ → (𝐾 ∈ (ℤ𝑁) → (𝐴𝑆 → (𝐶‘(𝑅𝐾)) = 0)))
755, 74syl 14 . . 3 (𝑁 ∈ ℕ0 → (𝐾 ∈ (ℤ𝑁) → (𝐴𝑆 → (𝐶‘(𝑅𝐾)) = 0)))
7675com3r 78 . 2 (𝐴𝑆 → (𝑁 ∈ ℕ0 → (𝐾 ∈ (ℤ𝑁) → (𝐶‘(𝑅𝐾)) = 0)))
774, 76mpd 13 1 (𝐴𝑆 → (𝐾 ∈ (ℤ𝑁) → (𝐶‘(𝑅𝐾)) = 0))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 922   = wceq 1287  wcel 1436  wne 2251  {csn 3425   class class class wbr 3814   × cxp 4402  ccom 4408  wf 4968  cfv 4972  (class class class)co 5594  1st c1st 5847  cr 7270  0cc0 7271  1c1 7272   + caddc 7274   < clt 7443  cle 7444  0cn0 8583  cz 8660  cuz 8928  seqcseq 9754
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3922  ax-sep 3925  ax-nul 3933  ax-pow 3977  ax-pr 4003  ax-un 4227  ax-setind 4319  ax-iinf 4369  ax-cnex 7357  ax-resscn 7358  ax-1cn 7359  ax-1re 7360  ax-icn 7361  ax-addcl 7362  ax-addrcl 7363  ax-mulcl 7364  ax-addcom 7366  ax-addass 7368  ax-distr 7370  ax-i2m1 7371  ax-0lt1 7372  ax-0id 7374  ax-rnegex 7375  ax-cnre 7377  ax-pre-ltirr 7378  ax-pre-ltwlin 7379  ax-pre-lttrn 7380  ax-pre-apti 7381  ax-pre-ltadd 7382
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-nel 2347  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2616  df-sbc 2829  df-csb 2922  df-dif 2988  df-un 2990  df-in 2992  df-ss 2999  df-nul 3273  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-int 3666  df-iun 3709  df-br 3815  df-opab 3869  df-mpt 3870  df-tr 3905  df-id 4087  df-iord 4160  df-on 4162  df-ilim 4163  df-suc 4165  df-iom 4372  df-xp 4410  df-rel 4411  df-cnv 4412  df-co 4413  df-dm 4414  df-rn 4415  df-res 4416  df-ima 4417  df-iota 4937  df-fun 4974  df-fn 4975  df-f 4976  df-f1 4977  df-fo 4978  df-f1o 4979  df-fv 4980  df-riota 5550  df-ov 5597  df-oprab 5598  df-mpt2 5599  df-1st 5849  df-2nd 5850  df-recs 6005  df-frec 6091  df-pnf 7445  df-mnf 7446  df-xr 7447  df-ltxr 7448  df-le 7449  df-sub 7576  df-neg 7577  df-inn 8335  df-n0 8584  df-z 8661  df-uz 8929  df-iseq 9755
This theorem is referenced by:  ialgfx  10828  eucialgcvga  10834
  Copyright terms: Public domain W3C validator