Step | Hyp | Ref
| Expression |
1 | | reex 7908 |
. . . 4
⊢ ℝ
∈ V |
2 | 1 | mptex 5722 |
. . 3
⊢ (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) ∈
V |
3 | 2 | a1i 9 |
. 2
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 = 0 → (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) ∈ V) |
4 | | 0zd 9224 |
. . . . 5
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑦 ∈ ℝ) → 0 ∈
ℤ) |
5 | | 1zzd 9239 |
. . . . 5
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑦 ∈ ℝ) → 1 ∈
ℤ) |
6 | | eqeq1 2177 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 = 0 ↔ 𝑦 = 0)) |
7 | 6 | dcbid 833 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (DECID 𝑥 = 0 ↔ DECID
𝑦 = 0)) |
8 | 7 | rspccva 2833 |
. . . . 5
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑦 ∈ ℝ) → DECID
𝑦 = 0) |
9 | 4, 5, 8 | ifcldcd 3561 |
. . . 4
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑦 ∈ ℝ) → if(𝑦 = 0, 0, 1) ∈ ℤ) |
10 | 9 | fmpttd 5651 |
. . 3
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 = 0 → (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0,
1)):ℝ⟶ℤ) |
11 | | 0re 7920 |
. . . . . 6
⊢ 0 ∈
ℝ |
12 | | 0zd 9224 |
. . . . . . . 8
⊢ (⊤
→ 0 ∈ ℤ) |
13 | | 1zzd 9239 |
. . . . . . . 8
⊢ (⊤
→ 1 ∈ ℤ) |
14 | | eqid 2170 |
. . . . . . . . . . 11
⊢ 0 =
0 |
15 | 14 | orci 726 |
. . . . . . . . . 10
⊢ (0 = 0
∨ ¬ 0 = 0) |
16 | | df-dc 830 |
. . . . . . . . . 10
⊢
(DECID 0 = 0 ↔ (0 = 0 ∨ ¬ 0 =
0)) |
17 | 15, 16 | mpbir 145 |
. . . . . . . . 9
⊢
DECID 0 = 0 |
18 | 17 | a1i 9 |
. . . . . . . 8
⊢ (⊤
→ DECID 0 = 0) |
19 | 12, 13, 18 | ifcldcd 3561 |
. . . . . . 7
⊢ (⊤
→ if(0 = 0, 0, 1) ∈ ℤ) |
20 | 19 | mptru 1357 |
. . . . . 6
⊢ if(0 = 0,
0, 1) ∈ ℤ |
21 | | eqeq1 2177 |
. . . . . . . 8
⊢ (𝑦 = 0 → (𝑦 = 0 ↔ 0 = 0)) |
22 | 21 | ifbid 3547 |
. . . . . . 7
⊢ (𝑦 = 0 → if(𝑦 = 0, 0, 1) = if(0 = 0, 0,
1)) |
23 | | eqid 2170 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) = (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) |
24 | 22, 23 | fvmptg 5572 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ if(0 = 0, 0, 1) ∈ ℤ) → ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘0) = if(0 =
0, 0, 1)) |
25 | 11, 20, 24 | mp2an 424 |
. . . . 5
⊢ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘0) = if(0 =
0, 0, 1) |
26 | 14 | iftruei 3532 |
. . . . 5
⊢ if(0 = 0,
0, 1) = 0 |
27 | 25, 26 | eqtri 2191 |
. . . 4
⊢ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘0) =
0 |
28 | 27 | a1i 9 |
. . 3
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 = 0 → ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘0) = 0) |
29 | | 1ne0 8946 |
. . . . . 6
⊢ 1 ≠
0 |
30 | | eqeq1 2177 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (𝑦 = 0 ↔ 𝑧 = 0)) |
31 | 30 | ifbid 3547 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → if(𝑦 = 0, 0, 1) = if(𝑧 = 0, 0, 1)) |
32 | | rpre 9617 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ+
→ 𝑧 ∈
ℝ) |
33 | 32 | adantl 275 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → 𝑧 ∈
ℝ) |
34 | | 0zd 9224 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → 0 ∈
ℤ) |
35 | | 1zzd 9239 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → 1 ∈
ℤ) |
36 | | eqeq1 2177 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑥 = 0 ↔ 𝑧 = 0)) |
37 | 36 | dcbid 833 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (DECID 𝑥 = 0 ↔ DECID
𝑧 = 0)) |
38 | | simpl 108 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) →
∀𝑥 ∈ ℝ
DECID 𝑥 =
0) |
39 | 37, 38, 33 | rspcdva 2839 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) →
DECID 𝑧 =
0) |
40 | 34, 35, 39 | ifcldcd 3561 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → if(𝑧 = 0, 0, 1) ∈
ℤ) |
41 | 23, 31, 33, 40 | fvmptd3 5589 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑧) = if(𝑧 = 0, 0, 1)) |
42 | | rpne0 9626 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℝ+
→ 𝑧 ≠
0) |
43 | 42 | neneqd 2361 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ+
→ ¬ 𝑧 =
0) |
44 | 43 | iffalsed 3536 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℝ+
→ if(𝑧 = 0, 0, 1) =
1) |
45 | 44 | adantl 275 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → if(𝑧 = 0, 0, 1) =
1) |
46 | 41, 45 | eqtrd 2203 |
. . . . . . 7
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑧) = 1) |
47 | 46 | neeq1d 2358 |
. . . . . 6
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → (((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑧) ≠ 0 ↔ 1 ≠
0)) |
48 | 29, 47 | mpbiri 167 |
. . . . 5
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑧) ≠ 0) |
49 | 48 | ralrimiva 2543 |
. . . 4
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 = 0 → ∀𝑧 ∈ ℝ+ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑧) ≠ 0) |
50 | | fveq2 5496 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑧) = ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑥)) |
51 | 50 | neeq1d 2358 |
. . . . 5
⊢ (𝑧 = 𝑥 → (((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑧) ≠ 0 ↔ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑥) ≠ 0)) |
52 | 51 | cbvralv 2696 |
. . . 4
⊢
(∀𝑧 ∈
ℝ+ ((𝑦
∈ ℝ ↦ if(𝑦
= 0, 0, 1))‘𝑧) ≠ 0
↔ ∀𝑥 ∈
ℝ+ ((𝑦
∈ ℝ ↦ if(𝑦
= 0, 0, 1))‘𝑥) ≠
0) |
53 | 49, 52 | sylib 121 |
. . 3
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 = 0 → ∀𝑥 ∈ ℝ+ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑥) ≠ 0) |
54 | 10, 28, 53 | 3jca 1172 |
. 2
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 = 0 → ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)):ℝ⟶ℤ ∧
((𝑦 ∈ ℝ ↦
if(𝑦 = 0, 0, 1))‘0) =
0 ∧ ∀𝑥 ∈
ℝ+ ((𝑦
∈ ℝ ↦ if(𝑦
= 0, 0, 1))‘𝑥) ≠
0)) |
55 | | feq1 5330 |
. . 3
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) → (𝑓:ℝ⟶ℤ ↔ (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0,
1)):ℝ⟶ℤ)) |
56 | | fveq1 5495 |
. . . 4
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) → (𝑓‘0) = ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘0)) |
57 | 56 | eqeq1d 2179 |
. . 3
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) → ((𝑓‘0) = 0 ↔ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘0) = 0)) |
58 | | fveq1 5495 |
. . . . 5
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) → (𝑓‘𝑥) = ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑥)) |
59 | 58 | neeq1d 2358 |
. . . 4
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) → ((𝑓‘𝑥) ≠ 0 ↔ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑥) ≠ 0)) |
60 | 59 | ralbidv 2470 |
. . 3
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) → (∀𝑥 ∈ ℝ+
(𝑓‘𝑥) ≠ 0 ↔ ∀𝑥 ∈ ℝ+ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑥) ≠ 0)) |
61 | 55, 57, 60 | 3anbi123d 1307 |
. 2
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) → ((𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧
∀𝑥 ∈
ℝ+ (𝑓‘𝑥) ≠ 0) ↔ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)):ℝ⟶ℤ ∧
((𝑦 ∈ ℝ ↦
if(𝑦 = 0, 0, 1))‘0) =
0 ∧ ∀𝑥 ∈
ℝ+ ((𝑦
∈ ℝ ↦ if(𝑦
= 0, 0, 1))‘𝑥) ≠
0))) |
62 | 3, 54, 61 | elabd 2875 |
1
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 = 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧
∀𝑥 ∈
ℝ+ (𝑓‘𝑥) ≠ 0)) |