| Step | Hyp | Ref
| Expression |
| 1 | | ax-1ne0 11224 |
. . 3
⊢ 1 ≠
0 |
| 2 | | ax-1cn 11213 |
. . . . 5
⊢ 1 ∈
ℂ |
| 3 | | cnre 11258 |
. . . . 5
⊢ (1 ∈
ℂ → ∃𝑎
∈ ℝ ∃𝑏
∈ ℝ 1 = (𝑎 + (i
· 𝑏))) |
| 4 | 2, 3 | ax-mp 5 |
. . . 4
⊢
∃𝑎 ∈
ℝ ∃𝑏 ∈
ℝ 1 = (𝑎 + (i
· 𝑏)) |
| 5 | | neeq1 3003 |
. . . . . . . 8
⊢ (1 =
(𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔
(𝑎 + (i · 𝑏)) ≠ 0)) |
| 6 | 5 | biimpcd 249 |
. . . . . . 7
⊢ (1 ≠ 0
→ (1 = (𝑎 + (i
· 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0)) |
| 7 | | 0cn 11253 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
| 8 | | cnre 11258 |
. . . . . . . 8
⊢ (0 ∈
ℂ → ∃𝑐
∈ ℝ ∃𝑑
∈ ℝ 0 = (𝑐 + (i
· 𝑑))) |
| 9 | 7, 8 | ax-mp 5 |
. . . . . . 7
⊢
∃𝑐 ∈
ℝ ∃𝑑 ∈
ℝ 0 = (𝑐 + (i
· 𝑑)) |
| 10 | | neeq2 3004 |
. . . . . . . . . 10
⊢ (0 =
(𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))) |
| 11 | 10 | biimpcd 249 |
. . . . . . . . 9
⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))) |
| 12 | 11 | reximdv 3170 |
. . . . . . . 8
⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))) |
| 13 | 12 | reximdv 3170 |
. . . . . . 7
⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))) |
| 14 | 6, 9, 13 | syl6mpi 67 |
. . . . . 6
⊢ (1 ≠ 0
→ (1 = (𝑎 + (i
· 𝑏)) →
∃𝑐 ∈ ℝ
∃𝑑 ∈ ℝ
(𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))) |
| 15 | 14 | reximdv 3170 |
. . . . 5
⊢ (1 ≠ 0
→ (∃𝑏 ∈
ℝ 1 = (𝑎 + (i
· 𝑏)) →
∃𝑏 ∈ ℝ
∃𝑐 ∈ ℝ
∃𝑑 ∈ ℝ
(𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))) |
| 16 | 15 | reximdv 3170 |
. . . 4
⊢ (1 ≠ 0
→ (∃𝑎 ∈
ℝ ∃𝑏 ∈
ℝ 1 = (𝑎 + (i
· 𝑏)) →
∃𝑎 ∈ ℝ
∃𝑏 ∈ ℝ
∃𝑐 ∈ ℝ
∃𝑑 ∈ ℝ
(𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))) |
| 17 | 4, 16 | mpi 20 |
. . 3
⊢ (1 ≠ 0
→ ∃𝑎 ∈
ℝ ∃𝑏 ∈
ℝ ∃𝑐 ∈
ℝ ∃𝑑 ∈
ℝ (𝑎 + (i ·
𝑏)) ≠ (𝑐 + (i · 𝑑))) |
| 18 | | ioran 986 |
. . . . . . . . 9
⊢ (¬
(𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑)) |
| 19 | | df-ne 2941 |
. . . . . . . . . . 11
⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐) |
| 20 | 19 | con2bii 357 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐) |
| 21 | | df-ne 2941 |
. . . . . . . . . . 11
⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑) |
| 22 | 21 | con2bii 357 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑) |
| 23 | 20, 22 | anbi12i 628 |
. . . . . . . . 9
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑)) |
| 24 | 18, 23 | bitr4i 278 |
. . . . . . . 8
⊢ (¬
(𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) |
| 25 | | id 22 |
. . . . . . . . 9
⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐) |
| 26 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑)) |
| 27 | 25, 26 | oveqan12d 7450 |
. . . . . . . 8
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))) |
| 28 | 24, 27 | sylbi 217 |
. . . . . . 7
⊢ (¬
(𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))) |
| 29 | 28 | necon1ai 2968 |
. . . . . 6
⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑)) |
| 30 | | neeq1 3003 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦)) |
| 31 | | neeq2 3004 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐)) |
| 32 | 30, 31 | rspc2ev 3635 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦) |
| 33 | 32 | 3expia 1122 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)) |
| 34 | 33 | ad2ant2r 747 |
. . . . . . 7
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)) |
| 35 | | neeq1 3003 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦)) |
| 36 | | neeq2 3004 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑)) |
| 37 | 35, 36 | rspc2ev 3635 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦) |
| 38 | 37 | 3expia 1122 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)) |
| 39 | 38 | ad2ant2l 746 |
. . . . . . 7
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)) |
| 40 | 34, 39 | jaod 860 |
. . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)) |
| 41 | 29, 40 | syl5 34 |
. . . . 5
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)) |
| 42 | 41 | rexlimdvva 3213 |
. . . 4
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) →
(∃𝑐 ∈ ℝ
∃𝑑 ∈ ℝ
(𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)) |
| 43 | 42 | rexlimivv 3201 |
. . 3
⊢
(∃𝑎 ∈
ℝ ∃𝑏 ∈
ℝ ∃𝑐 ∈
ℝ ∃𝑑 ∈
ℝ (𝑎 + (i ·
𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦) |
| 44 | 1, 17, 43 | mp2b 10 |
. 2
⊢
∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ 𝑥 ≠ 𝑦 |
| 45 | | eqtr3 2763 |
. . . . . . . . 9
⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦) |
| 46 | 45 | ex 412 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦)) |
| 47 | 46 | necon3d 2961 |
. . . . . . 7
⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0)) |
| 48 | | neeq1 3003 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0)) |
| 49 | 48 | rspcev 3622 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0) |
| 50 | 49 | expcom 413 |
. . . . . . 7
⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ →
∃𝑧 ∈ ℝ
𝑧 ≠ 0)) |
| 51 | 47, 50 | syl6 35 |
. . . . . 6
⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))) |
| 52 | 51 | com23 86 |
. . . . 5
⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))) |
| 53 | 52 | adantld 490 |
. . . 4
⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))) |
| 54 | | neeq1 3003 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0)) |
| 55 | 54 | rspcev 3622 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0) |
| 56 | 55 | expcom 413 |
. . . . . 6
⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ →
∃𝑧 ∈ ℝ
𝑧 ≠ 0)) |
| 57 | 56 | adantrd 491 |
. . . . 5
⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
∃𝑧 ∈ ℝ
𝑧 ≠ 0)) |
| 58 | 57 | a1dd 50 |
. . . 4
⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))) |
| 59 | 53, 58 | pm2.61ine 3025 |
. . 3
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)) |
| 60 | 59 | rexlimivv 3201 |
. 2
⊢
(∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0) |
| 61 | | ax-rrecex 11227 |
. . . 4
⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1) |
| 62 | | remulcl 11240 |
. . . . . . 7
⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ) |
| 63 | 62 | adantlr 715 |
. . . . . 6
⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ) |
| 64 | | eleq1 2829 |
. . . . . 6
⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈
ℝ)) |
| 65 | 63, 64 | syl5ibcom 245 |
. . . . 5
⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈
ℝ)) |
| 66 | 65 | rexlimdva 3155 |
. . . 4
⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈
ℝ)) |
| 67 | 61, 66 | mpd 15 |
. . 3
⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈
ℝ) |
| 68 | 67 | rexlimiva 3147 |
. 2
⊢
(∃𝑧 ∈
ℝ 𝑧 ≠ 0 → 1
∈ ℝ) |
| 69 | 44, 60, 68 | mp2b 10 |
1
⊢ 1 ∈
ℝ |