Step | Hyp | Ref
| Expression |
1 | | reex 7845 |
. . . 4
⊢ ℝ
∈ V |
2 | 1 | mptex 5686 |
. . 3
⊢ (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) ∈
V |
3 | 2 | a1i 9 |
. 2
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 = 0 → (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) ∈ V) |
4 | | 0zd 9158 |
. . . . 5
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑦 ∈ ℝ) → 0 ∈
ℤ) |
5 | | 1zzd 9173 |
. . . . 5
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑦 ∈ ℝ) → 1 ∈
ℤ) |
6 | | eqeq1 2161 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 = 0 ↔ 𝑦 = 0)) |
7 | 6 | dcbid 824 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (DECID 𝑥 = 0 ↔ DECID
𝑦 = 0)) |
8 | 7 | rspccva 2812 |
. . . . 5
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑦 ∈ ℝ) → DECID
𝑦 = 0) |
9 | 4, 5, 8 | ifcldcd 3536 |
. . . 4
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑦 ∈ ℝ) → if(𝑦 = 0, 0, 1) ∈ ℤ) |
10 | 9 | fmpttd 5615 |
. . 3
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 = 0 → (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0,
1)):ℝ⟶ℤ) |
11 | | 0re 7857 |
. . . . . 6
⊢ 0 ∈
ℝ |
12 | | 0zd 9158 |
. . . . . . . 8
⊢ (⊤
→ 0 ∈ ℤ) |
13 | | 1zzd 9173 |
. . . . . . . 8
⊢ (⊤
→ 1 ∈ ℤ) |
14 | | eqid 2154 |
. . . . . . . . . . 11
⊢ 0 =
0 |
15 | 14 | orci 721 |
. . . . . . . . . 10
⊢ (0 = 0
∨ ¬ 0 = 0) |
16 | | df-dc 821 |
. . . . . . . . . 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 3536 |
. . . . . . 7
⊢ (⊤
→ if(0 = 0, 0, 1) ∈ ℤ) |
20 | 19 | mptru 1341 |
. . . . . 6
⊢ if(0 = 0,
0, 1) ∈ ℤ |
21 | | eqeq1 2161 |
. . . . . . . 8
⊢ (𝑦 = 0 → (𝑦 = 0 ↔ 0 = 0)) |
22 | 21 | ifbid 3522 |
. . . . . . 7
⊢ (𝑦 = 0 → if(𝑦 = 0, 0, 1) = if(0 = 0, 0,
1)) |
23 | | eqid 2154 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) = (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) |
24 | 22, 23 | fvmptg 5537 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ if(0 = 0, 0, 1) ∈ ℤ) → ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘0) = if(0 =
0, 0, 1)) |
25 | 11, 20, 24 | mp2an 423 |
. . . . 5
⊢ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘0) = if(0 =
0, 0, 1) |
26 | 14 | iftruei 3507 |
. . . . 5
⊢ if(0 = 0,
0, 1) = 0 |
27 | 25, 26 | eqtri 2175 |
. . . 4
⊢ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘0) =
0 |
28 | 27 | a1i 9 |
. . 3
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 = 0 → ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘0) = 0) |
29 | | 1ne0 8880 |
. . . . . 6
⊢ 1 ≠
0 |
30 | | eqeq1 2161 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (𝑦 = 0 ↔ 𝑧 = 0)) |
31 | 30 | ifbid 3522 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → if(𝑦 = 0, 0, 1) = if(𝑧 = 0, 0, 1)) |
32 | | rpre 9545 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ+
→ 𝑧 ∈
ℝ) |
33 | 32 | adantl 275 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → 𝑧 ∈
ℝ) |
34 | | 0zd 9158 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → 0 ∈
ℤ) |
35 | | 1zzd 9173 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → 1 ∈
ℤ) |
36 | | eqeq1 2161 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑥 = 0 ↔ 𝑧 = 0)) |
37 | 36 | dcbid 824 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (DECID 𝑥 = 0 ↔ DECID
𝑧 = 0)) |
38 | | simpl 108 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) →
∀𝑥 ∈ ℝ
DECID 𝑥 =
0) |
39 | 37, 38, 33 | rspcdva 2818 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) →
DECID 𝑧 =
0) |
40 | 34, 35, 39 | ifcldcd 3536 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → if(𝑧 = 0, 0, 1) ∈
ℤ) |
41 | 23, 31, 33, 40 | fvmptd3 5554 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑧) = if(𝑧 = 0, 0, 1)) |
42 | | rpne0 9554 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℝ+
→ 𝑧 ≠
0) |
43 | 42 | neneqd 2345 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ+
→ ¬ 𝑧 =
0) |
44 | 43 | iffalsed 3511 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℝ+
→ if(𝑧 = 0, 0, 1) =
1) |
45 | 44 | adantl 275 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → if(𝑧 = 0, 0, 1) =
1) |
46 | 41, 45 | eqtrd 2187 |
. . . . . . 7
⊢
((∀𝑥 ∈
ℝ DECID 𝑥 = 0 ∧ 𝑧 ∈ ℝ+) → ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑧) = 1) |
47 | 46 | neeq1d 2342 |
. . . . . 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 2527 |
. . . 4
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 = 0 → ∀𝑧 ∈ ℝ+ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑧) ≠ 0) |
50 | | fveq2 5461 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑧) = ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑥)) |
51 | 50 | neeq1d 2342 |
. . . . 5
⊢ (𝑧 = 𝑥 → (((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑧) ≠ 0 ↔ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑥) ≠ 0)) |
52 | 51 | cbvralv 2677 |
. . . 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 1162 |
. 2
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 = 0 → ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)):ℝ⟶ℤ ∧
((𝑦 ∈ ℝ ↦
if(𝑦 = 0, 0, 1))‘0) =
0 ∧ ∀𝑥 ∈
ℝ+ ((𝑦
∈ ℝ ↦ if(𝑦
= 0, 0, 1))‘𝑥) ≠
0)) |
55 | | feq1 5295 |
. . 3
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) → (𝑓:ℝ⟶ℤ ↔ (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0,
1)):ℝ⟶ℤ)) |
56 | | fveq1 5460 |
. . . 4
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) → (𝑓‘0) = ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘0)) |
57 | 56 | eqeq1d 2163 |
. . 3
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) → ((𝑓‘0) = 0 ↔ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘0) = 0)) |
58 | | fveq1 5460 |
. . . . 5
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) → (𝑓‘𝑥) = ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑥)) |
59 | 58 | neeq1d 2342 |
. . . 4
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) → ((𝑓‘𝑥) ≠ 0 ↔ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑥) ≠ 0)) |
60 | 59 | ralbidv 2454 |
. . 3
⊢ (𝑓 = (𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1)) → (∀𝑥 ∈ ℝ+
(𝑓‘𝑥) ≠ 0 ↔ ∀𝑥 ∈ ℝ+ ((𝑦 ∈ ℝ ↦ if(𝑦 = 0, 0, 1))‘𝑥) ≠ 0)) |
61 | 55, 57, 60 | 3anbi123d 1291 |
. 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 2853 |
1
⊢
(∀𝑥 ∈
ℝ DECID 𝑥 = 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧
∀𝑥 ∈
ℝ+ (𝑓‘𝑥) ≠ 0)) |