Step | Hyp | Ref
| Expression |
1 | | reex 7867 |
. . . 4
⊢ ℝ
∈ V |
2 | 1 | mptex 5694 |
. . 3
⊢ (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) ∈
V |
3 | 2 | a1i 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)) |
7 | 6 | dcbid 824 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (DECID 𝑥 # 0 ↔ DECID
𝑦 # 0)) |
8 | 7 | rspccva 2815 |
. . . . 5
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 # 0 ∧ 𝑦 ∈ ℝ) → DECID
𝑦 # 0) |
9 | 4, 5, 8 | ifcldcd 3540 |
. . . 4
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 # 0 ∧ 𝑦 ∈ ℝ) → if(𝑦 # 0, 1, 0) ∈ ℤ) |
10 | 9 | fmpttd 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) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ¬ 0
# 0 |
17 | 16 | olci 722 |
. . . . . . . . . 10
⊢ (0 # 0
∨ ¬ 0 # 0) |
18 | | df-dc 821 |
. . . . . . . . . 10
⊢
(DECID 0 # 0 ↔ (0 # 0 ∨ ¬ 0 #
0)) |
19 | 17, 18 | mpbir 145 |
. . . . . . . . 9
⊢
DECID 0 # 0 |
20 | 19 | a1i 9 |
. . . . . . . 8
⊢ (⊤
→ DECID 0 # 0) |
21 | 12, 13, 20 | ifcldcd 3540 |
. . . . . . 7
⊢ (⊤
→ if(0 # 0, 1, 0) ∈ ℤ) |
22 | 21 | mptru 1344 |
. . . . . 6
⊢ if(0 # 0,
1, 0) ∈ ℤ |
23 | | breq1 3969 |
. . . . . . . 8
⊢ (𝑦 = 0 → (𝑦 # 0 ↔ 0 # 0)) |
24 | 23 | ifbid 3526 |
. . . . . . 7
⊢ (𝑦 = 0 → if(𝑦 # 0, 1, 0) = if(0 # 0, 1,
0)) |
25 | | eqid 2157 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) = (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) |
26 | 24, 25 | fvmptg 5545 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ if(0 # 0, 1, 0) ∈ ℤ) → ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘0) = if(0 #
0, 1, 0)) |
27 | 11, 22, 26 | mp2an 423 |
. . . . 5
⊢ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘0) = if(0 #
0, 1, 0) |
28 | 16 | iffalsei 3514 |
. . . . 5
⊢ if(0 # 0,
1, 0) = 0 |
29 | 27, 28 | eqtri 2178 |
. . . 4
⊢ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘0) =
0 |
30 | 29 | a1i 9 |
. . 3
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 # 0 → ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘0) = 0) |
31 | | 1ne0 8902 |
. . . . . 6
⊢ 1 ≠
0 |
32 | | breq1 3969 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (𝑦 # 0 ↔ 𝑧 # 0)) |
33 | 32 | ifbid 3526 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → if(𝑦 # 0, 1, 0) = if(𝑧 # 0, 1, 0)) |
34 | | rpre 9568 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ+
→ 𝑧 ∈
ℝ) |
35 | 34 | adantl 275 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → 𝑧 ∈
ℝ) |
36 | | 1zzd 9195 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → 1 ∈
ℤ) |
37 | | 0zd 9180 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → 0 ∈
ℤ) |
38 | | breq1 3969 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑥 # 0 ↔ 𝑧 # 0)) |
39 | 38 | dcbid 824 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (DECID 𝑥 # 0 ↔ DECID
𝑧 # 0)) |
40 | | simpl 108 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) →
∀𝑥 ∈ ℝ
DECID 𝑥 #
0) |
41 | 39, 40, 35 | rspcdva 2821 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) →
DECID 𝑧 #
0) |
42 | 36, 37, 41 | ifcldcd 3540 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → if(𝑧 # 0, 1, 0) ∈
ℤ) |
43 | 25, 33, 35, 42 | fvmptd3 5562 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑧) = if(𝑧 # 0, 1, 0)) |
44 | | rpap0 9578 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ+
→ 𝑧 #
0) |
45 | 44 | iftrued 3512 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℝ+
→ if(𝑧 # 0, 1, 0) =
1) |
46 | 45 | adantl 275 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → if(𝑧 # 0, 1, 0) =
1) |
47 | 43, 46 | eqtrd 2190 |
. . . . . . 7
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑧) = 1) |
48 | 47 | neeq1d 2345 |
. . . . . 6
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → (((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑧) ≠ 0 ↔ 1 ≠
0)) |
49 | 31, 48 | mpbiri 167 |
. . . . 5
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 # 0 ∧ 𝑧 ∈ ℝ+) → ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑧) ≠ 0) |
50 | 49 | ralrimiva 2530 |
. . . 4
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 # 0 → ∀𝑧 ∈ ℝ+ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑧) ≠ 0) |
51 | | fveq2 5469 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑧) = ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑥)) |
52 | 51 | neeq1d 2345 |
. . . . 5
⊢ (𝑧 = 𝑥 → (((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑧) ≠ 0 ↔ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑥) ≠ 0)) |
53 | 52 | cbvralv 2680 |
. . . 4
⊢
(∀𝑧 ∈
ℝ+ ((𝑦
∈ ℝ ↦ if(𝑦
# 0, 1, 0))‘𝑧) ≠ 0
↔ ∀𝑥 ∈
ℝ+ ((𝑦
∈ ℝ ↦ if(𝑦
# 0, 1, 0))‘𝑥) ≠
0) |
54 | 50, 53 | sylib 121 |
. . 3
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 # 0 → ∀𝑥 ∈ ℝ+ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑥) ≠ 0) |
55 | 10, 30, 54 | 3jca 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)) |
58 | 57 | eqeq1d 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))‘𝑥)) |
60 | 59 | neeq1d 2345 |
. . . 4
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) → ((𝑓‘𝑥) ≠ 0 ↔ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑥) ≠ 0)) |
61 | 60 | ralbidv 2457 |
. . 3
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) → (∀𝑥 ∈ ℝ+
(𝑓‘𝑥) ≠ 0 ↔ ∀𝑥 ∈ ℝ+ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0))‘𝑥) ≠ 0)) |
62 | 56, 58, 61 | 3anbi123d 1294 |
. 2
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)) → ((𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧
∀𝑥 ∈
ℝ+ (𝑓‘𝑥) ≠ 0) ↔ ((𝑦 ∈ ℝ ↦ if(𝑦 # 0, 1, 0)):ℝ⟶ℤ ∧
((𝑦 ∈ ℝ ↦
if(𝑦 # 0, 1, 0))‘0) =
0 ∧ ∀𝑥 ∈
ℝ+ ((𝑦
∈ ℝ ↦ if(𝑦
# 0, 1, 0))‘𝑥) ≠
0))) |
63 | 3, 55, 62 | elabd 2857 |
1
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 # 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧
∀𝑥 ∈
ℝ+ (𝑓‘𝑥) ≠ 0)) |