Proof of Theorem 2zrngnmrid
| Step | Hyp | Ref
| Expression |
| 1 | | eldifsn 4786 |
. . . 4
⊢ (𝑎 ∈ (𝐸 ∖ {0}) ↔ (𝑎 ∈ 𝐸 ∧ 𝑎 ≠ 0)) |
| 2 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑧 = 𝑎 → (𝑧 = (2 · 𝑥) ↔ 𝑎 = (2 · 𝑥))) |
| 3 | 2 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑧 = 𝑎 → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ 𝑎 = (2 · 𝑥))) |
| 4 | | 2zrng.e |
. . . . . . 7
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} |
| 5 | 3, 4 | elrab2 3695 |
. . . . . 6
⊢ (𝑎 ∈ 𝐸 ↔ (𝑎 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑎 = (2 · 𝑥))) |
| 6 | | zcn 12618 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℂ) |
| 7 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝑎 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑎 = (2 · 𝑥)) → 𝑎 ∈ ℂ) |
| 8 | 5, 7 | sylbi 217 |
. . . . 5
⊢ (𝑎 ∈ 𝐸 → 𝑎 ∈ ℂ) |
| 9 | 8 | anim1i 615 |
. . . 4
⊢ ((𝑎 ∈ 𝐸 ∧ 𝑎 ≠ 0) → (𝑎 ∈ ℂ ∧ 𝑎 ≠ 0)) |
| 10 | 1, 9 | sylbi 217 |
. . 3
⊢ (𝑎 ∈ (𝐸 ∖ {0}) → (𝑎 ∈ ℂ ∧ 𝑎 ≠ 0)) |
| 11 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑧 = 𝑏 → (𝑧 = (2 · 𝑥) ↔ 𝑏 = (2 · 𝑥))) |
| 12 | 11 | rexbidv 3179 |
. . . . . 6
⊢ (𝑧 = 𝑏 → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) |
| 13 | 12, 4 | elrab2 3695 |
. . . . 5
⊢ (𝑏 ∈ 𝐸 ↔ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) |
| 14 | | zcn 12618 |
. . . . . 6
⊢ (𝑏 ∈ ℤ → 𝑏 ∈
ℂ) |
| 15 | 14 | adantr 480 |
. . . . 5
⊢ ((𝑏 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥)) → 𝑏 ∈ ℂ) |
| 16 | 13, 15 | sylbi 217 |
. . . 4
⊢ (𝑏 ∈ 𝐸 → 𝑏 ∈ ℂ) |
| 17 | 16 | ancli 548 |
. . 3
⊢ (𝑏 ∈ 𝐸 → (𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ)) |
| 18 | 4 | 1neven 48154 |
. . . . . . 7
⊢ 1 ∉
𝐸 |
| 19 | | elnelne2 3058 |
. . . . . . 7
⊢ ((𝑏 ∈ 𝐸 ∧ 1 ∉ 𝐸) → 𝑏 ≠ 1) |
| 20 | 18, 19 | mpan2 691 |
. . . . . 6
⊢ (𝑏 ∈ 𝐸 → 𝑏 ≠ 1) |
| 21 | 20 | ad2antrl 728 |
. . . . 5
⊢ (((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ (𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ)) → 𝑏 ≠ 1) |
| 22 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ) → 𝑏 ∈ ℂ) |
| 23 | 22 | anim2i 617 |
. . . . . . 7
⊢ (((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ (𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ)) → ((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ 𝑏 ∈ ℂ)) |
| 24 | | 3anass 1095 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ↔ (𝑏 ∈ ℂ ∧ (𝑎 ∈ ℂ ∧ 𝑎 ≠ 0))) |
| 25 | | ancom 460 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℂ ∧ (𝑎 ∈ ℂ ∧ 𝑎 ≠ 0)) ↔ ((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ 𝑏 ∈
ℂ)) |
| 26 | 24, 25 | bitri 275 |
. . . . . . 7
⊢ ((𝑏 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ↔ ((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ 𝑏 ∈
ℂ)) |
| 27 | 23, 26 | sylibr 234 |
. . . . . 6
⊢ (((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ (𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ)) → (𝑏 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0)) |
| 28 | | divcan3 11948 |
. . . . . 6
⊢ ((𝑏 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) → ((𝑎 · 𝑏) / 𝑎) = 𝑏) |
| 29 | 27, 28 | syl 17 |
. . . . 5
⊢ (((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ (𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ)) → ((𝑎 · 𝑏) / 𝑎) = 𝑏) |
| 30 | | divid 11953 |
. . . . . 6
⊢ ((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) → (𝑎 / 𝑎) = 1) |
| 31 | 30 | adantr 480 |
. . . . 5
⊢ (((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ (𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ)) → (𝑎 / 𝑎) = 1) |
| 32 | 21, 29, 31 | 3netr4d 3018 |
. . . 4
⊢ (((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ (𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ)) → ((𝑎 · 𝑏) / 𝑎) ≠ (𝑎 / 𝑎)) |
| 33 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) → 𝑎 ∈
ℂ) |
| 34 | | mulcl 11239 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 · 𝑏) ∈ ℂ) |
| 35 | 33, 22, 34 | syl2an 596 |
. . . . . . 7
⊢ (((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ (𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ)) → (𝑎 · 𝑏) ∈ ℂ) |
| 36 | 33 | adantr 480 |
. . . . . . 7
⊢ (((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ (𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ)) → 𝑎 ∈ ℂ) |
| 37 | | simpl 482 |
. . . . . . 7
⊢ (((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ (𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ)) → (𝑎 ∈ ℂ ∧ 𝑎 ≠ 0)) |
| 38 | | div11 11950 |
. . . . . . 7
⊢ (((𝑎 · 𝑏) ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ (𝑎 ∈ ℂ ∧ 𝑎 ≠ 0)) → (((𝑎 · 𝑏) / 𝑎) = (𝑎 / 𝑎) ↔ (𝑎 · 𝑏) = 𝑎)) |
| 39 | 35, 36, 37, 38 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ (𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ)) → (((𝑎 · 𝑏) / 𝑎) = (𝑎 / 𝑎) ↔ (𝑎 · 𝑏) = 𝑎)) |
| 40 | 39 | biimprd 248 |
. . . . 5
⊢ (((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ (𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ)) → ((𝑎 · 𝑏) = 𝑎 → ((𝑎 · 𝑏) / 𝑎) = (𝑎 / 𝑎))) |
| 41 | 40 | necon3d 2961 |
. . . 4
⊢ (((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ (𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ)) → (((𝑎 · 𝑏) / 𝑎) ≠ (𝑎 / 𝑎) → (𝑎 · 𝑏) ≠ 𝑎)) |
| 42 | 32, 41 | mpd 15 |
. . 3
⊢ (((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) ∧ (𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ)) → (𝑎 · 𝑏) ≠ 𝑎) |
| 43 | 10, 17, 42 | syl2an 596 |
. 2
⊢ ((𝑎 ∈ (𝐸 ∖ {0}) ∧ 𝑏 ∈ 𝐸) → (𝑎 · 𝑏) ≠ 𝑎) |
| 44 | 43 | rgen2 3199 |
1
⊢
∀𝑎 ∈
(𝐸 ∖
{0})∀𝑏 ∈ 𝐸 (𝑎 · 𝑏) ≠ 𝑎 |