Users' Mathboxes Mathbox for Jim Kingdon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  dcapnconst GIF version

Theorem dcapnconst 13673
Description: Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See trilpo 13656 for more discussion of decidability of real number apartness.

This is a weaker form of dceqnconst 13672 and in fact this theorem can be proved using dceqnconst 13672 as shown at dcapnconstALT 13674. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.)

Assertion
Ref Expression
dcapnconst (∀𝑥 ∈ ℝ DECID 𝑥 # 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧ ∀𝑥 ∈ ℝ+ (𝑓𝑥) ≠ 0))
Distinct variable group:   𝑥,𝑓

Proof of Theorem dcapnconst
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reex 7867 . . . 4 ℝ ∈ V
21mptex 5694 . . 3 (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) ∈ V
32a1i 9 . 2 (∀𝑥 ∈ ℝ DECID 𝑥 # 0 → (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) ∈ V)
4 1zzd 9195 . . . . 5 ((∀𝑥 ∈ ℝ DECID 𝑥 # 0 ∧ 𝑦 ∈ ℝ) → 1 ∈ ℤ)
5 0zd 9180 . . . . 5 ((∀𝑥 ∈ ℝ DECID 𝑥 # 0 ∧ 𝑦 ∈ ℝ) → 0 ∈ ℤ)
6 breq1 3969 . . . . . . 7 (𝑥 = 𝑦 → (𝑥 # 0 ↔ 𝑦 # 0))
76dcbid 824 . . . . . 6 (𝑥 = 𝑦 → (DECID 𝑥 # 0 ↔ DECID 𝑦 # 0))
87rspccva 2815 . . . . 5 ((∀𝑥 ∈ ℝ DECID 𝑥 # 0 ∧ 𝑦 ∈ ℝ) → DECID 𝑦 # 0)
94, 5, 8ifcldcd 3540 . . . 4 ((∀𝑥 ∈ ℝ DECID 𝑥 # 0 ∧ 𝑦 ∈ ℝ) → if(𝑦 # 0, 1, 0) ∈ ℤ)
109fmpttd 5623 . . 3 (∀𝑥 ∈ ℝ DECID 𝑥 # 0 → (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)):ℝ⟶ℤ)
11 0re 7879 . . . . . 6 0 ∈ ℝ
12 1zzd 9195 . . . . . . . 8 (⊤ → 1 ∈ ℤ)
13 0zd 9180 . . . . . . . 8 (⊤ → 0 ∈ ℤ)
14 0cn 7871 . . . . . . . . . . . 12 0 ∈ ℂ
15 apirr 8481 . . . . . . . . . . . 12 (0 ∈ ℂ → ¬ 0 # 0)
1614, 15ax-mp 5 . . . . . . . . . . 11 ¬ 0 # 0
1716olci 722 . . . . . . . . . 10 (0 # 0 ∨ ¬ 0 # 0)
18 df-dc 821 . . . . . . . . . 10 (DECID 0 # 0 ↔ (0 # 0 ∨ ¬ 0 # 0))
1917, 18mpbir 145 . . . . . . . . 9 DECID 0 # 0
2019a1i 9 . . . . . . . 8 (⊤ → DECID 0 # 0)
2112, 13, 20ifcldcd 3540 . . . . . . 7 (⊤ → if(0 # 0, 1, 0) ∈ ℤ)
2221mptru 1344 . . . . . 6 if(0 # 0, 1, 0) ∈ ℤ
23 breq1 3969 . . . . . . . 8 (𝑦 = 0 → (𝑦 # 0 ↔ 0 # 0))
2423ifbid 3526 . . . . . . 7 (𝑦 = 0 → if(𝑦 # 0, 1, 0) = if(0 # 0, 1, 0))
25 eqid 2157 . . . . . . 7 (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) = (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))
2624, 25fvmptg 5545 . . . . . 6 ((0 ∈ ℝ ∧ if(0 # 0, 1, 0) ∈ ℤ) → ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘0) = if(0 # 0, 1, 0))
2711, 22, 26mp2an 423 . . . . 5 ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘0) = if(0 # 0, 1, 0)
2816iffalsei 3514 . . . . 5 if(0 # 0, 1, 0) = 0
2927, 28eqtri 2178 . . . 4 ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘0) = 0
3029a1i 9 . . 3 (∀𝑥 ∈ ℝ DECID 𝑥 # 0 → ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘0) = 0)
31 1ne0 8902 . . . . . 6 1 ≠ 0
32 breq1 3969 . . . . . . . . . 10 (𝑦 = 𝑧 → (𝑦 # 0 ↔ 𝑧 # 0))
3332ifbid 3526 . . . . . . . . 9 (𝑦 = 𝑧 → if(𝑦 # 0, 1, 0) = if(𝑧 # 0, 1, 0))
34 rpre 9568 . . . . . . . . . 10 (𝑧 ∈ ℝ+𝑧 ∈ ℝ)
3534adantl 275 . . . . . . . . 9 ((∀𝑥 ∈ ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → 𝑧 ∈ ℝ)
36 1zzd 9195 . . . . . . . . . 10 ((∀𝑥 ∈ ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → 1 ∈ ℤ)
37 0zd 9180 . . . . . . . . . 10 ((∀𝑥 ∈ ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → 0 ∈ ℤ)
38 breq1 3969 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝑥 # 0 ↔ 𝑧 # 0))
3938dcbid 824 . . . . . . . . . . 11 (𝑥 = 𝑧 → (DECID 𝑥 # 0 ↔ DECID 𝑧 # 0))
40 simpl 108 . . . . . . . . . . 11 ((∀𝑥 ∈ ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → ∀𝑥 ∈ ℝ DECID 𝑥 # 0)
4139, 40, 35rspcdva 2821 . . . . . . . . . 10 ((∀𝑥 ∈ ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → DECID 𝑧 # 0)
4236, 37, 41ifcldcd 3540 . . . . . . . . 9 ((∀𝑥 ∈ ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → if(𝑧 # 0, 1, 0) ∈ ℤ)
4325, 33, 35, 42fvmptd3 5562 . . . . . . . 8 ((∀𝑥 ∈ ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑧) = if(𝑧 # 0, 1, 0))
44 rpap0 9578 . . . . . . . . . 10 (𝑧 ∈ ℝ+𝑧 # 0)
4544iftrued 3512 . . . . . . . . 9 (𝑧 ∈ ℝ+ → if(𝑧 # 0, 1, 0) = 1)
4645adantl 275 . . . . . . . 8 ((∀𝑥 ∈ ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → if(𝑧 # 0, 1, 0) = 1)
4743, 46eqtrd 2190 . . . . . . 7 ((∀𝑥 ∈ ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑧) = 1)
4847neeq1d 2345 . . . . . 6 ((∀𝑥 ∈ ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → (((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑧) ≠ 0 ↔ 1 ≠ 0))
4931, 48mpbiri 167 . . . . 5 ((∀𝑥 ∈ ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑧) ≠ 0)
5049ralrimiva 2530 . . . 4 (∀𝑥 ∈ ℝ DECID 𝑥 # 0 → ∀𝑧 ∈ ℝ+ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑧) ≠ 0)
51 fveq2 5469 . . . . . 6 (𝑧 = 𝑥 → ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑧) = ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑥))
5251neeq1d 2345 . . . . 5 (𝑧 = 𝑥 → (((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑧) ≠ 0 ↔ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑥) ≠ 0))
5352cbvralv 2680 . . . 4 (∀𝑧 ∈ ℝ+ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑧) ≠ 0 ↔ ∀𝑥 ∈ ℝ+ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑥) ≠ 0)
5450, 53sylib 121 . . 3 (∀𝑥 ∈ ℝ DECID 𝑥 # 0 → ∀𝑥 ∈ ℝ+ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑥) ≠ 0)
5510, 30, 543jca 1162 . 2 (∀𝑥 ∈ ℝ DECID 𝑥 # 0 → ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)):ℝ⟶ℤ ∧ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘0) = 0 ∧ ∀𝑥 ∈ ℝ+ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑥) ≠ 0))
56 feq1 5303 . . 3 (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) → (𝑓:ℝ⟶ℤ ↔ (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)):ℝ⟶ℤ))
57 fveq1 5468 . . . 4 (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) → (𝑓‘0) = ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘0))
5857eqeq1d 2166 . . 3 (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) → ((𝑓‘0) = 0 ↔ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘0) = 0))
59 fveq1 5468 . . . . 5 (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) → (𝑓𝑥) = ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑥))
6059neeq1d 2345 . . . 4 (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) → ((𝑓𝑥) ≠ 0 ↔ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑥) ≠ 0))
6160ralbidv 2457 . . 3 (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) → (∀𝑥 ∈ ℝ+ (𝑓𝑥) ≠ 0 ↔ ∀𝑥 ∈ ℝ+ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑥) ≠ 0))
6256, 58, 613anbi123d 1294 . 2 (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) → ((𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧ ∀𝑥 ∈ ℝ+ (𝑓𝑥) ≠ 0) ↔ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)):ℝ⟶ℤ ∧ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘0) = 0 ∧ ∀𝑥 ∈ ℝ+ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑥) ≠ 0)))
633, 55, 62elabd 2857 1 (∀𝑥 ∈ ℝ DECID 𝑥 # 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧ ∀𝑥 ∈ ℝ+ (𝑓𝑥) ≠ 0))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wo 698  DECID wdc 820  w3a 963   = wceq 1335  wtru 1336  wex 1472  wcel 2128  wne 2327  wral 2435  Vcvv 2712  ifcif 3505   class class class wbr 3966  cmpt 4026  wf 5167  cfv 5171  cc 7731  cr 7732  0cc0 7733  1c1 7734   # cap 8457  cz 9168  +crp 9561
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 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4080  ax-sep 4083  ax-pow 4136  ax-pr 4170  ax-un 4394  ax-setind 4497  ax-cnex 7824  ax-resscn 7825  ax-1cn 7826  ax-1re 7827  ax-icn 7828  ax-addcl 7829  ax-addrcl 7830  ax-mulcl 7831  ax-mulrcl 7832  ax-addcom 7833  ax-mulcom 7834  ax-addass 7835  ax-mulass 7836  ax-distr 7837  ax-i2m1 7838  ax-0lt1 7839  ax-1rid 7840  ax-0id 7841  ax-rnegex 7842  ax-precex 7843  ax-cnre 7844  ax-pre-ltirr 7845  ax-pre-ltwlin 7846  ax-pre-lttrn 7847  ax-pre-apti 7848  ax-pre-ltadd 7849  ax-pre-mulgt0 7850
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3774  df-int 3809  df-iun 3852  df-br 3967  df-opab 4027  df-mpt 4028  df-id 4254  df-xp 4593  df-rel 4594  df-cnv 4595  df-co 4596  df-dm 4597  df-rn 4598  df-res 4599  df-ima 4600  df-iota 5136  df-fun 5173  df-fn 5174  df-f 5175  df-f1 5176  df-fo 5177  df-f1o 5178  df-fv 5179  df-riota 5781  df-ov 5828  df-oprab 5829  df-mpo 5830  df-pnf 7915  df-mnf 7916  df-xr 7917  df-ltxr 7918  df-le 7919  df-sub 8049  df-neg 8050  df-reap 8451  df-ap 8458  df-inn 8835  df-z 9169  df-rp 9562
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator