Mathbox for Jim Kingdon < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  nninffeq Unicode version

Theorem nninffeq 13027
 Description: Equality of two functions on ℕ∞ which agree at every integer and at the point at infinity. From an online post by Martin Escardo. (Contributed by Jim Kingdon, 4-Aug-2023.)
Hypotheses
Ref Expression
nninffeq.f
nninffeq.g
nninffeq.oo
nninffeq.n
Assertion
Ref Expression
nninffeq
Distinct variable groups:   ,,,   ,,,   ,,,

Proof of Theorem nninffeq
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nninffeq.f . . 3
21ffnd 5241 . 2
3 nninffeq.g . . 3
43ffnd 5241 . 2
5 eqid 2115 . . . . . . . 8
6 fveq2 5387 . . . . . . . . . 10
7 fveq2 5387 . . . . . . . . . 10
86, 7eqeq12d 2130 . . . . . . . . 9
98ifbid 3461 . . . . . . . 8
10 simpr 109 . . . . . . . 8
11 1onn 6382 . . . . . . . . . 10
1211a1i 9 . . . . . . . . 9
13 peano1 4476 . . . . . . . . . 10
1413a1i 9 . . . . . . . . 9
151ffvelrnda 5521 . . . . . . . . . . 11
1615nn0zd 9122 . . . . . . . . . 10
173ffvelrnda 5521 . . . . . . . . . . 11
1817nn0zd 9122 . . . . . . . . . 10
19 zdceq 9077 . . . . . . . . . 10 DECID
2016, 18, 19syl2anc 406 . . . . . . . . 9 DECID
2112, 14, 20ifcldcd 3475 . . . . . . . 8
225, 9, 10, 21fvmptd3 5480 . . . . . . 7
23 1lt2o 6305 . . . . . . . . . . . . 13
2423a1i 9 . . . . . . . . . . . 12
25 0lt2o 6304 . . . . . . . . . . . . 13
2625a1i 9 . . . . . . . . . . . 12
271ffvelrnda 5521 . . . . . . . . . . . . . 14
2827nn0zd 9122 . . . . . . . . . . . . 13
293ffvelrnda 5521 . . . . . . . . . . . . . 14
3029nn0zd 9122 . . . . . . . . . . . . 13
31 zdceq 9077 . . . . . . . . . . . . 13 DECID
3228, 30, 31syl2anc 406 . . . . . . . . . . . 12 DECID
3324, 26, 32ifcldcd 3475 . . . . . . . . . . 11
3433fmpttd 5541 . . . . . . . . . 10
35 2onn 6383 . . . . . . . . . . . 12
3635elexi 2670 . . . . . . . . . . 11
37 nninfex 13016 . . . . . . . . . . 11
3836, 37elmap 6537 . . . . . . . . . 10
3934, 38sylibr 133 . . . . . . . . 9
40 fveq2 5387 . . . . . . . . . . . . 13
41 fveq2 5387 . . . . . . . . . . . . 13
4240, 41eqeq12d 2130 . . . . . . . . . . . 12
4342ifbid 3461 . . . . . . . . . . 11
44 fconstmpt 4554 . . . . . . . . . . . . 13
45 infnninf 6988 . . . . . . . . . . . . 13
4644, 45eqeltrri 2189 . . . . . . . . . . . 12
4746a1i 9 . . . . . . . . . . 11
48 nninffeq.oo . . . . . . . . . . . . . 14
49 eqidd 2116 . . . . . . . . . . . . . . . 16
5049cbvmptv 3992 . . . . . . . . . . . . . . 15
5150fveq2i 5390 . . . . . . . . . . . . . 14
5250fveq2i 5390 . . . . . . . . . . . . . 14
5348, 51, 523eqtr3g 2171 . . . . . . . . . . . . 13
5453iftrued 3449 . . . . . . . . . . . 12
5554, 11syl6eqel 2206 . . . . . . . . . . 11
565, 43, 47, 55fvmptd3 5480 . . . . . . . . . 10
5756, 54eqtrd 2148 . . . . . . . . 9
58 nninffeq.n . . . . . . . . . 10
59 fveq2 5387 . . . . . . . . . . . . . . . 16
60 fveq2 5387 . . . . . . . . . . . . . . . 16
6159, 60eqeq12d 2130 . . . . . . . . . . . . . . 15
6261ifbid 3461 . . . . . . . . . . . . . 14
63 nnnninf 6989 . . . . . . . . . . . . . . 15
6463ad2antlr 478 . . . . . . . . . . . . . 14
65 simpr 109 . . . . . . . . . . . . . . . 16
6665iftrued 3449 . . . . . . . . . . . . . . 15
6766, 11syl6eqel 2206 . . . . . . . . . . . . . 14
685, 62, 64, 67fvmptd3 5480 . . . . . . . . . . . . 13
6968, 66eqtrd 2148 . . . . . . . . . . . 12
7069ex 114 . . . . . . . . . . 11
7170ralimdva 2474 . . . . . . . . . 10
7258, 71mpd 13 . . . . . . . . 9
7339, 57, 72nninfall 13015 . . . . . . . 8
7473r19.21bi 2495 . . . . . . 7
7522, 74eqtr3d 2150 . . . . . 6
7675adantr 272 . . . . 5
77 simpr 109 . . . . . 6
7877iffalsed 3452 . . . . 5
7976, 78eqtr3d 2150 . . . 4
80 1n0 6295 . . . . . 6
8180neii 2285 . . . . 5
8281a1i 9 . . . 4
8379, 82pm2.65da 633 . . 3
84 exmiddc 804 . . . 4 DECID
8520, 84syl 14 . . 3
8683, 85ecased 1310 . 2
872, 4, 86eqfnfvd 5487 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wo 680  DECID wdc 802   wceq 1314   wcel 1463  wral 2391  c0 3331  cif 3442  csn 3495   cmpt 3957  com 4472   cxp 4505  wf 5087  cfv 5091  (class class class)co 5740  c1o 6272  c2o 6273   cmap 6508  ℕ∞xnninf 6971  cn0 8928  cz 9005 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 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-iinf 4470  ax-cnex 7675  ax-resscn 7676  ax-1cn 7677  ax-1re 7678  ax-icn 7679  ax-addcl 7680  ax-addrcl 7681  ax-mulcl 7682  ax-addcom 7684  ax-addass 7686  ax-distr 7688  ax-i2m1 7689  ax-0lt1 7690  ax-0id 7692  ax-rnegex 7693  ax-cnre 7695  ax-pre-ltirr 7696  ax-pre-ltwlin 7697  ax-pre-lttrn 7698  ax-pre-ltadd 7700 This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-nel 2379  df-ral 2396  df-rex 2397  df-reu 2398  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-if 3443  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-iord 4256  df-on 4258  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-fv 5099  df-riota 5696  df-ov 5743  df-oprab 5744  df-mpo 5745  df-1o 6279  df-2o 6280  df-map 6510  df-nninf 6973  df-pnf 7766  df-mnf 7767  df-xr 7768  df-ltxr 7769  df-le 7770  df-sub 7899  df-neg 7900  df-inn 8678  df-n0 8929  df-z 9006 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator