Proof of Theorem rexzrexnn0
Step | Hyp | Ref
| Expression |
1 | | elznn0 11726 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ ℕ0 ∨
-𝑥 ∈
ℕ0))) |
2 | 1 | simprbi 492 |
. . . . . 6
⊢ (𝑥 ∈ ℤ → (𝑥 ∈ ℕ0 ∨
-𝑥 ∈
ℕ0)) |
3 | 2 | adantr 474 |
. . . . 5
⊢ ((𝑥 ∈ ℤ ∧ 𝜑) → (𝑥 ∈ ℕ0 ∨ -𝑥 ∈
ℕ0)) |
4 | | simpr 479 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝜑) ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈
ℕ0) |
5 | | simplr 785 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝜑) ∧ 𝑥 ∈ ℕ0) → 𝜑) |
6 | | rexzrexnn0.1 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
7 | 6 | equcoms 2124 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) |
8 | 7 | bicomd 215 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝜓 ↔ 𝜑)) |
9 | 8 | rspcev 3526 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℕ0
∧ 𝜑) → ∃𝑦 ∈ ℕ0
𝜓) |
10 | 4, 5, 9 | syl2anc 579 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝜑) ∧ 𝑥 ∈ ℕ0) →
∃𝑦 ∈
ℕ0 𝜓) |
11 | 10 | ex 403 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝜑) → (𝑥 ∈ ℕ0 →
∃𝑦 ∈
ℕ0 𝜓)) |
12 | | simpr 479 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ -𝑥 ∈ ℕ0)
→ -𝑥 ∈
ℕ0) |
13 | | zcn 11716 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
14 | 13 | negnegd 10711 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ → --𝑥 = 𝑥) |
15 | 14 | eqcomd 2831 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℤ → 𝑥 = --𝑥) |
16 | | negeq 10600 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = -𝑥 → -𝑦 = --𝑥) |
17 | 16 | eqeq2d 2835 |
. . . . . . . . . . . . 13
⊢ (𝑦 = -𝑥 → (𝑥 = -𝑦 ↔ 𝑥 = --𝑥)) |
18 | 15, 17 | syl5ibrcom 239 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℤ → (𝑦 = -𝑥 → 𝑥 = -𝑦)) |
19 | 18 | imp 397 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 = -𝑥) → 𝑥 = -𝑦) |
20 | | rexzrexnn0.2 |
. . . . . . . . . . 11
⊢ (𝑥 = -𝑦 → (𝜑 ↔ 𝜒)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 = -𝑥) → (𝜑 ↔ 𝜒)) |
22 | 21 | bicomd 215 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 = -𝑥) → (𝜒 ↔ 𝜑)) |
23 | 22 | adantlr 706 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ -𝑥 ∈ ℕ0)
∧ 𝑦 = -𝑥) → (𝜒 ↔ 𝜑)) |
24 | 12, 23 | rspcedv 3530 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ -𝑥 ∈ ℕ0)
→ (𝜑 → ∃𝑦 ∈ ℕ0
𝜒)) |
25 | 24 | impancom 445 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝜑) → (-𝑥 ∈ ℕ0 →
∃𝑦 ∈
ℕ0 𝜒)) |
26 | 11, 25 | orim12d 992 |
. . . . 5
⊢ ((𝑥 ∈ ℤ ∧ 𝜑) → ((𝑥 ∈ ℕ0 ∨ -𝑥 ∈ ℕ0)
→ (∃𝑦 ∈
ℕ0 𝜓 ∨
∃𝑦 ∈
ℕ0 𝜒))) |
27 | 3, 26 | mpd 15 |
. . . 4
⊢ ((𝑥 ∈ ℤ ∧ 𝜑) → (∃𝑦 ∈ ℕ0
𝜓 ∨ ∃𝑦 ∈ ℕ0
𝜒)) |
28 | | r19.43 3303 |
. . . 4
⊢
(∃𝑦 ∈
ℕ0 (𝜓 ∨
𝜒) ↔ (∃𝑦 ∈ ℕ0
𝜓 ∨ ∃𝑦 ∈ ℕ0
𝜒)) |
29 | 27, 28 | sylibr 226 |
. . 3
⊢ ((𝑥 ∈ ℤ ∧ 𝜑) → ∃𝑦 ∈ ℕ0 (𝜓 ∨ 𝜒)) |
30 | 29 | rexlimiva 3237 |
. 2
⊢
(∃𝑥 ∈
ℤ 𝜑 → ∃𝑦 ∈ ℕ0
(𝜓 ∨ 𝜒)) |
31 | | nn0z 11735 |
. . . . 5
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℤ) |
32 | 6 | rspcev 3526 |
. . . . 5
⊢ ((𝑦 ∈ ℤ ∧ 𝜓) → ∃𝑥 ∈ ℤ 𝜑) |
33 | 31, 32 | sylan 575 |
. . . 4
⊢ ((𝑦 ∈ ℕ0
∧ 𝜓) → ∃𝑥 ∈ ℤ 𝜑) |
34 | | nn0negz 11750 |
. . . . 5
⊢ (𝑦 ∈ ℕ0
→ -𝑦 ∈
ℤ) |
35 | 20 | rspcev 3526 |
. . . . 5
⊢ ((-𝑦 ∈ ℤ ∧ 𝜒) → ∃𝑥 ∈ ℤ 𝜑) |
36 | 34, 35 | sylan 575 |
. . . 4
⊢ ((𝑦 ∈ ℕ0
∧ 𝜒) → ∃𝑥 ∈ ℤ 𝜑) |
37 | 33, 36 | jaodan 985 |
. . 3
⊢ ((𝑦 ∈ ℕ0
∧ (𝜓 ∨ 𝜒)) → ∃𝑥 ∈ ℤ 𝜑) |
38 | 37 | rexlimiva 3237 |
. 2
⊢
(∃𝑦 ∈
ℕ0 (𝜓 ∨
𝜒) → ∃𝑥 ∈ ℤ 𝜑) |
39 | 30, 38 | impbii 201 |
1
⊢
(∃𝑥 ∈
ℤ 𝜑 ↔ ∃𝑦 ∈ ℕ0
(𝜓 ∨ 𝜒)) |