Metamath Proof Explorer

Theorem 2zrngnmlid

Description: R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020)

Ref Expression
Hypotheses 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2zrngbas.r ⊢ R = ℂ fld ↾ 𝑠 E
2zrngmmgm.1 ⊢ M = mulGrp R
Assertion 2zrngnmlid ⊢ ∀ b ∈ E ∃ a ∈ E b ⁢ a ≠ a

Proof

Step Hyp Ref Expression
1 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2 2zrngbas.r ⊢ R = ℂ fld ↾ 𝑠 E
3 2zrngmmgm.1 ⊢ M = mulGrp R
4 1 2even ⊢ 2 ∈ E
5 4 a1i ⊢ b ∈ E → 2 ∈ E
6 oveq2 ⊢ a = 2 → b ⁢ a = b ⋅ 2
7 id ⊢ a = 2 → a = 2
8 6 7 neeq12d ⊢ a = 2 → b ⁢ a ≠ a ↔ b ⋅ 2 ≠ 2
9 8 adantl ⊢ b ∈ E ∧ a = 2 → b ⁢ a ≠ a ↔ b ⋅ 2 ≠ 2
10 elrabi ⊢ b ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → b ∈ ℤ
11 10 zcnd ⊢ b ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → b ∈ ℂ
12 11 1 eleq2s ⊢ b ∈ E → b ∈ ℂ
13 1 1neven ⊢ 1 ∉ E
14 elnelne2 ⊢ b ∈ E ∧ 1 ∉ E → b ≠ 1
15 13 14 mpan2 ⊢ b ∈ E → b ≠ 1
16 15 adantr ⊢ b ∈ E ∧ b ∈ ℂ → b ≠ 1
17 simpr ⊢ b ∈ E ∧ b ∈ ℂ → b ∈ ℂ
18 2cnd ⊢ b ∈ E ∧ b ∈ ℂ → 2 ∈ ℂ
19 2ne0 ⊢ 2 ≠ 0
20 19 a1i ⊢ b ∈ E ∧ b ∈ ℂ → 2 ≠ 0
21 17 18 20 divcan4d ⊢ b ∈ E ∧ b ∈ ℂ → b ⋅ 2 2 = b
22 2cnne0 ⊢ 2 ∈ ℂ ∧ 2 ≠ 0
23 divid ⊢ 2 ∈ ℂ ∧ 2 ≠ 0 → 2 2 = 1
24 22 23 mp1i ⊢ b ∈ E ∧ b ∈ ℂ → 2 2 = 1
25 16 21 24 3netr4d ⊢ b ∈ E ∧ b ∈ ℂ → b ⋅ 2 2 ≠ 2 2
26 17 18 mulcld ⊢ b ∈ E ∧ b ∈ ℂ → b ⋅ 2 ∈ ℂ
27 22 a1i ⊢ b ∈ E ∧ b ∈ ℂ → 2 ∈ ℂ ∧ 2 ≠ 0
28 div11 ⊢ b ⋅ 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 → b ⋅ 2 2 = 2 2 ↔ b ⋅ 2 = 2
29 26 18 27 28 syl3anc ⊢ b ∈ E ∧ b ∈ ℂ → b ⋅ 2 2 = 2 2 ↔ b ⋅ 2 = 2
30 29 biimprd ⊢ b ∈ E ∧ b ∈ ℂ → b ⋅ 2 = 2 → b ⋅ 2 2 = 2 2
31 30 necon3d ⊢ b ∈ E ∧ b ∈ ℂ → b ⋅ 2 2 ≠ 2 2 → b ⋅ 2 ≠ 2
32 25 31 mpd ⊢ b ∈ E ∧ b ∈ ℂ → b ⋅ 2 ≠ 2
33 12 32 mpdan ⊢ b ∈ E → b ⋅ 2 ≠ 2
34 5 9 33 rspcedvd ⊢ b ∈ E → ∃ a ∈ E b ⁢ a ≠ a
35 34 rgen ⊢ ∀ b ∈ E ∃ a ∈ E b ⁢ a ≠ a