| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2zrng.e | . . 3
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} | 
| 2 |  | ssrab2 4080 | . . 3
⊢ {𝑧 ∈ ℤ ∣
∃𝑥 ∈ ℤ
𝑧 = (2 · 𝑥)} ⊆
ℤ | 
| 3 | 1, 2 | eqsstri 4030 | . 2
⊢ 𝐸 ⊆
ℤ | 
| 4 | 1 | 0even 48153 | . . 3
⊢ 0 ∈
𝐸 | 
| 5 | 4 | ne0ii 4344 | . 2
⊢ 𝐸 ≠ ∅ | 
| 6 |  | eqeq1 2741 | . . . . . . . 8
⊢ (𝑧 = 𝑗 → (𝑧 = (2 · 𝑥) ↔ 𝑗 = (2 · 𝑥))) | 
| 7 | 6 | rexbidv 3179 | . . . . . . 7
⊢ (𝑧 = 𝑗 → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ 𝑗 = (2 · 𝑥))) | 
| 8 | 7, 1 | elrab2 3695 | . . . . . 6
⊢ (𝑗 ∈ 𝐸 ↔ (𝑗 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑗 = (2 · 𝑥))) | 
| 9 |  | eqeq1 2741 | . . . . . . . 8
⊢ (𝑧 = 𝑘 → (𝑧 = (2 · 𝑥) ↔ 𝑘 = (2 · 𝑥))) | 
| 10 | 9 | rexbidv 3179 | . . . . . . 7
⊢ (𝑧 = 𝑘 → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ 𝑘 = (2 · 𝑥))) | 
| 11 | 10, 1 | elrab2 3695 | . . . . . 6
⊢ (𝑘 ∈ 𝐸 ↔ (𝑘 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑘 = (2 · 𝑥))) | 
| 12 | 8, 11 | anbi12i 628 | . . . . 5
⊢ ((𝑗 ∈ 𝐸 ∧ 𝑘 ∈ 𝐸) ↔ ((𝑗 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑗 = (2 · 𝑥)) ∧ (𝑘 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑘 = (2 · 𝑥)))) | 
| 13 |  | simpl 482 | . . . . . . . 8
⊢ ((𝑖 ∈ ℤ ∧ ((𝑗 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑗 = (2 · 𝑥)) ∧ (𝑘 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑘 = (2 · 𝑥)))) → 𝑖 ∈ ℤ) | 
| 14 |  | simprll 779 | . . . . . . . 8
⊢ ((𝑖 ∈ ℤ ∧ ((𝑗 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑗 = (2 · 𝑥)) ∧ (𝑘 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑘 = (2 · 𝑥)))) → 𝑗 ∈ ℤ) | 
| 15 | 13, 14 | zmulcld 12728 | . . . . . . 7
⊢ ((𝑖 ∈ ℤ ∧ ((𝑗 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑗 = (2 · 𝑥)) ∧ (𝑘 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑘 = (2 · 𝑥)))) → (𝑖 · 𝑗) ∈ ℤ) | 
| 16 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑘 = (2 · 𝑥)) → 𝑘 ∈ ℤ) | 
| 17 | 16 | adantl 481 | . . . . . . . 8
⊢ (((𝑗 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑗 = (2 · 𝑥)) ∧ (𝑘 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑘 = (2 · 𝑥))) → 𝑘 ∈ ℤ) | 
| 18 | 17 | adantl 481 | . . . . . . 7
⊢ ((𝑖 ∈ ℤ ∧ ((𝑗 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑗 = (2 · 𝑥)) ∧ (𝑘 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑘 = (2 · 𝑥)))) → 𝑘 ∈ ℤ) | 
| 19 | 15, 18 | zaddcld 12726 | . . . . . 6
⊢ ((𝑖 ∈ ℤ ∧ ((𝑗 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑗 = (2 · 𝑥)) ∧ (𝑘 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑘 = (2 · 𝑥)))) → ((𝑖 · 𝑗) + 𝑘) ∈ ℤ) | 
| 20 |  | oveq2 7439 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (2 · 𝑥) = (2 · 𝑎)) | 
| 21 | 20 | eqeq2d 2748 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (𝑗 = (2 · 𝑥) ↔ 𝑗 = (2 · 𝑎))) | 
| 22 | 21 | cbvrexvw 3238 | . . . . . . . . . 10
⊢
(∃𝑥 ∈
ℤ 𝑗 = (2 ·
𝑥) ↔ ∃𝑎 ∈ ℤ 𝑗 = (2 · 𝑎)) | 
| 23 |  | oveq2 7439 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑏 → (2 · 𝑥) = (2 · 𝑏)) | 
| 24 | 23 | eqeq2d 2748 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑏 → (𝑘 = (2 · 𝑥) ↔ 𝑘 = (2 · 𝑏))) | 
| 25 | 24 | cbvrexvw 3238 | . . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
ℤ 𝑘 = (2 ·
𝑥) ↔ ∃𝑏 ∈ ℤ 𝑘 = (2 · 𝑏)) | 
| 26 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → 𝑖 ∈ ℤ) | 
| 27 |  | simprll 779 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℤ ∧ 𝑘 = (2 · 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) → 𝑎 ∈ ℤ) | 
| 28 | 27 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → 𝑎 ∈ ℤ) | 
| 29 | 26, 28 | zmulcld 12728 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → (𝑖 · 𝑎) ∈ ℤ) | 
| 30 |  | simp-4l 783 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → 𝑏 ∈ ℤ) | 
| 31 | 29, 30 | zaddcld 12726 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → ((𝑖 · 𝑎) + 𝑏) ∈ ℤ) | 
| 32 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) → 𝑗 = (2 · 𝑎)) | 
| 33 | 32 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑏 ∈ ℤ ∧ 𝑘 = (2 · 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) → 𝑗 = (2 · 𝑎)) | 
| 34 | 33 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℤ ∧ 𝑘 = (2 · 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) → (𝑖 · 𝑗) = (𝑖 · (2 · 𝑎))) | 
| 35 |  | simpllr 776 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℤ ∧ 𝑘 = (2 · 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) → 𝑘 = (2 · 𝑏)) | 
| 36 | 34, 35 | oveq12d 7449 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℤ ∧ 𝑘 = (2 · 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) → ((𝑖 · 𝑗) + 𝑘) = ((𝑖 · (2 · 𝑎)) + (2 · 𝑏))) | 
| 37 | 36 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → ((𝑖 · 𝑗) + 𝑘) = ((𝑖 · (2 · 𝑎)) + (2 · 𝑏))) | 
| 38 |  | oveq2 7439 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ((𝑖 · 𝑎) + 𝑏) → (2 · 𝑥) = (2 · ((𝑖 · 𝑎) + 𝑏))) | 
| 39 | 37, 38 | eqeqan12d 2751 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) ∧ 𝑥 = ((𝑖 · 𝑎) + 𝑏)) → (((𝑖 · 𝑗) + 𝑘) = (2 · 𝑥) ↔ ((𝑖 · (2 · 𝑎)) + (2 · 𝑏)) = (2 · ((𝑖 · 𝑎) + 𝑏)))) | 
| 40 |  | zcn 12618 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
ℂ) | 
| 41 | 40 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → 𝑖 ∈ ℂ) | 
| 42 |  | 2cnd 12344 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → 2 ∈
ℂ) | 
| 43 |  | zcn 12618 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℂ) | 
| 44 | 43 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) → 𝑎 ∈ ℂ) | 
| 45 | 44 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑏 ∈ ℤ ∧ 𝑘 = (2 · 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) → 𝑎 ∈ ℂ) | 
| 46 | 45 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → 𝑎 ∈ ℂ) | 
| 47 | 41, 42, 46 | mul12d 11470 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → (𝑖 · (2 · 𝑎)) = (2 · (𝑖 · 𝑎))) | 
| 48 | 47 | oveq1d 7446 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → ((𝑖 · (2 · 𝑎)) + (2 · 𝑏)) = ((2 · (𝑖 · 𝑎)) + (2 · 𝑏))) | 
| 49 | 41, 46 | mulcld 11281 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → (𝑖 · 𝑎) ∈ ℂ) | 
| 50 |  | zcn 12618 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 ∈ ℤ → 𝑏 ∈
ℂ) | 
| 51 | 50 | ad4antr 732 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → 𝑏 ∈ ℂ) | 
| 52 | 42, 49, 51 | adddid 11285 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → (2 · ((𝑖 · 𝑎) + 𝑏)) = ((2 · (𝑖 · 𝑎)) + (2 · 𝑏))) | 
| 53 | 48, 52 | eqtr4d 2780 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → ((𝑖 · (2 · 𝑎)) + (2 · 𝑏)) = (2 · ((𝑖 · 𝑎) + 𝑏))) | 
| 54 | 31, 39, 53 | rspcedvd 3624 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑏 ∈
ℤ ∧ 𝑘 = (2
· 𝑏)) ∧ 𝑘 ∈ ℤ) ∧ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ)) ∧ 𝑖 ∈ ℤ) → ∃𝑥 ∈ ℤ ((𝑖 · 𝑗) + 𝑘) = (2 · 𝑥)) | 
| 55 | 54 | exp41 434 | . . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ 𝑘 = (2 · 𝑏)) → (𝑘 ∈ ℤ → (((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ) → (𝑖 ∈ ℤ → ∃𝑥 ∈ ℤ ((𝑖 · 𝑗) + 𝑘) = (2 · 𝑥))))) | 
| 56 | 55 | rexlimiva 3147 | . . . . . . . . . . . . . 14
⊢
(∃𝑏 ∈
ℤ 𝑘 = (2 ·
𝑏) → (𝑘 ∈ ℤ → (((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ) → (𝑖 ∈ ℤ → ∃𝑥 ∈ ℤ ((𝑖 · 𝑗) + 𝑘) = (2 · 𝑥))))) | 
| 57 | 25, 56 | sylbi 217 | . . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
ℤ 𝑘 = (2 ·
𝑥) → (𝑘 ∈ ℤ → (((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ) → (𝑖 ∈ ℤ → ∃𝑥 ∈ ℤ ((𝑖 · 𝑗) + 𝑘) = (2 · 𝑥))))) | 
| 58 | 57 | impcom 407 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑘 = (2 · 𝑥)) → (((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) ∧ 𝑗 ∈ ℤ) → (𝑖 ∈ ℤ → ∃𝑥 ∈ ℤ ((𝑖 · 𝑗) + 𝑘) = (2 · 𝑥)))) | 
| 59 | 58 | expdcom 414 | . . . . . . . . . . 11
⊢ ((𝑎 ∈ ℤ ∧ 𝑗 = (2 · 𝑎)) → (𝑗 ∈ ℤ → ((𝑘 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑘 = (2 · 𝑥)) → (𝑖 ∈ ℤ → ∃𝑥 ∈ ℤ ((𝑖 · 𝑗) + 𝑘) = (2 · 𝑥))))) | 
| 60 | 59 | rexlimiva 3147 | . . . . . . . . . 10
⊢
(∃𝑎 ∈
ℤ 𝑗 = (2 ·
𝑎) → (𝑗 ∈ ℤ → ((𝑘 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑘 = (2 · 𝑥)) → (𝑖 ∈ ℤ → ∃𝑥 ∈ ℤ ((𝑖 · 𝑗) + 𝑘) = (2 · 𝑥))))) | 
| 61 | 22, 60 | sylbi 217 | . . . . . . . . 9
⊢
(∃𝑥 ∈
ℤ 𝑗 = (2 ·
𝑥) → (𝑗 ∈ ℤ → ((𝑘 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑘 = (2 · 𝑥)) → (𝑖 ∈ ℤ → ∃𝑥 ∈ ℤ ((𝑖 · 𝑗) + 𝑘) = (2 · 𝑥))))) | 
| 62 | 61 | impcom 407 | . . . . . . . 8
⊢ ((𝑗 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑗 = (2 · 𝑥)) → ((𝑘 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑘 = (2 · 𝑥)) → (𝑖 ∈ ℤ → ∃𝑥 ∈ ℤ ((𝑖 · 𝑗) + 𝑘) = (2 · 𝑥)))) | 
| 63 | 62 | imp 406 | . . . . . . 7
⊢ (((𝑗 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑗 = (2 · 𝑥)) ∧ (𝑘 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑘 = (2 · 𝑥))) → (𝑖 ∈ ℤ → ∃𝑥 ∈ ℤ ((𝑖 · 𝑗) + 𝑘) = (2 · 𝑥))) | 
| 64 | 63 | impcom 407 | . . . . . 6
⊢ ((𝑖 ∈ ℤ ∧ ((𝑗 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑗 = (2 · 𝑥)) ∧ (𝑘 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑘 = (2 · 𝑥)))) → ∃𝑥 ∈ ℤ ((𝑖 · 𝑗) + 𝑘) = (2 · 𝑥)) | 
| 65 |  | eqeq1 2741 | . . . . . . . 8
⊢ (𝑧 = ((𝑖 · 𝑗) + 𝑘) → (𝑧 = (2 · 𝑥) ↔ ((𝑖 · 𝑗) + 𝑘) = (2 · 𝑥))) | 
| 66 | 65 | rexbidv 3179 | . . . . . . 7
⊢ (𝑧 = ((𝑖 · 𝑗) + 𝑘) → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ ((𝑖 · 𝑗) + 𝑘) = (2 · 𝑥))) | 
| 67 | 66, 1 | elrab2 3695 | . . . . . 6
⊢ (((𝑖 · 𝑗) + 𝑘) ∈ 𝐸 ↔ (((𝑖 · 𝑗) + 𝑘) ∈ ℤ ∧ ∃𝑥 ∈ ℤ ((𝑖 · 𝑗) + 𝑘) = (2 · 𝑥))) | 
| 68 | 19, 64, 67 | sylanbrc 583 | . . . . 5
⊢ ((𝑖 ∈ ℤ ∧ ((𝑗 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑗 = (2 · 𝑥)) ∧ (𝑘 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑘 = (2 · 𝑥)))) → ((𝑖 · 𝑗) + 𝑘) ∈ 𝐸) | 
| 69 | 12, 68 | sylan2b 594 | . . . 4
⊢ ((𝑖 ∈ ℤ ∧ (𝑗 ∈ 𝐸 ∧ 𝑘 ∈ 𝐸)) → ((𝑖 · 𝑗) + 𝑘) ∈ 𝐸) | 
| 70 | 69 | ralrimivva 3202 | . . 3
⊢ (𝑖 ∈ ℤ →
∀𝑗 ∈ 𝐸 ∀𝑘 ∈ 𝐸 ((𝑖 · 𝑗) + 𝑘) ∈ 𝐸) | 
| 71 | 70 | rgen 3063 | . 2
⊢
∀𝑖 ∈
ℤ ∀𝑗 ∈
𝐸 ∀𝑘 ∈ 𝐸 ((𝑖 · 𝑗) + 𝑘) ∈ 𝐸 | 
| 72 |  | 2zlidl.u | . . 3
⊢ 𝑈 =
(LIdeal‘ℤring) | 
| 73 |  | zringbas 21464 | . . 3
⊢ ℤ =
(Base‘ℤring) | 
| 74 |  | zringplusg 21465 | . . 3
⊢  + =
(+g‘ℤring) | 
| 75 |  | zringmulr 21468 | . . 3
⊢  ·
= (.r‘ℤring) | 
| 76 | 72, 73, 74, 75 | islidl 21225 | . 2
⊢ (𝐸 ∈ 𝑈 ↔ (𝐸 ⊆ ℤ ∧ 𝐸 ≠ ∅ ∧ ∀𝑖 ∈ ℤ ∀𝑗 ∈ 𝐸 ∀𝑘 ∈ 𝐸 ((𝑖 · 𝑗) + 𝑘) ∈ 𝐸)) | 
| 77 | 3, 5, 71, 76 | mpbir3an 1342 | 1
⊢ 𝐸 ∈ 𝑈 |