| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . . . 7
⊢ ((𝐴 · 0) = 1 → (2
· (𝐴 · 0)) =
(2 · 1)) |
| 2 | 1 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) → (2
· (𝐴 · 0)) =
(2 · 1)) |
| 3 | | 2re 12340 |
. . . . . . 7
⊢ 2 ∈
ℝ |
| 4 | | ax-1rid 11225 |
. . . . . . 7
⊢ (2 ∈
ℝ → (2 · 1) = 2) |
| 5 | 3, 4 | mp1i 13 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) → (2
· 1) = 2) |
| 6 | 2, 5 | eqtrd 2777 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) → (2
· (𝐴 · 0)) =
2) |
| 7 | 3 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) → 2
∈ ℝ) |
| 8 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) → 𝐴 ∈
ℝ) |
| 9 | | 0red 11264 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) → 0
∈ ℝ) |
| 10 | 8, 9 | remulcld 11291 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) → (𝐴 · 0) ∈
ℝ) |
| 11 | 7, 10 | remulcld 11291 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) → (2
· (𝐴 · 0))
∈ ℝ) |
| 12 | | sn-0ne2 42436 |
. . . . . . . . . . . 12
⊢ 0 ≠
2 |
| 13 | 12 | necomi 2995 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
| 14 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ ((2
· (𝐴 · 0)) =
2 → 2 ≠ 0) |
| 15 | | eqtr2 2761 |
. . . . . . . . . 10
⊢ (((2
· (𝐴 · 0)) =
2 ∧ (2 · (𝐴
· 0)) = 0) → 2 = 0) |
| 16 | 14, 15 | mteqand 3033 |
. . . . . . . . 9
⊢ ((2
· (𝐴 · 0)) =
2 → (2 · (𝐴
· 0)) ≠ 0) |
| 17 | | ax-rrecex 11227 |
. . . . . . . . 9
⊢ (((2
· (𝐴 · 0))
∈ ℝ ∧ (2 · (𝐴 · 0)) ≠ 0) → ∃𝑥 ∈ ℝ ((2 ·
(𝐴 · 0)) ·
𝑥) = 1) |
| 18 | 11, 16, 17 | syl2an 596 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) → ∃𝑥 ∈
ℝ ((2 · (𝐴
· 0)) · 𝑥) =
1) |
| 19 | | 2cnd 12344 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → 2 ∈ ℂ) |
| 20 | | simplll 775 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → 𝐴 ∈
ℝ) |
| 21 | | 0red 11264 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → 0 ∈ ℝ) |
| 22 | 20, 21 | remulcld 11291 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → (𝐴 · 0)
∈ ℝ) |
| 23 | 22 | recnd 11289 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → (𝐴 · 0)
∈ ℂ) |
| 24 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → 𝑥 ∈
ℝ) |
| 25 | 24 | recnd 11289 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → 𝑥 ∈
ℂ) |
| 26 | 19, 23, 25 | mulassd 11284 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → ((2 · (𝐴
· 0)) · 𝑥) =
(2 · ((𝐴 · 0)
· 𝑥))) |
| 27 | | simprr 773 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → ((2 · (𝐴
· 0)) · 𝑥) =
1) |
| 28 | 20 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → 𝐴 ∈
ℂ) |
| 29 | | 0cnd 11254 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → 0 ∈ ℂ) |
| 30 | 28, 29, 25 | mulassd 11284 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → ((𝐴 · 0)
· 𝑥) = (𝐴 · (0 · 𝑥))) |
| 31 | | remul02 42435 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ → (0
· 𝑥) =
0) |
| 32 | 31 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → (0 · 𝑥) =
0) |
| 33 | 32 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → (𝐴 · (0
· 𝑥)) = (𝐴 · 0)) |
| 34 | 30, 33 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → ((𝐴 · 0)
· 𝑥) = (𝐴 · 0)) |
| 35 | 34 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → (2 · ((𝐴
· 0) · 𝑥)) =
(2 · (𝐴 ·
0))) |
| 36 | 26, 27, 35 | 3eqtr3rd 2786 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) ∧ (𝑥 ∈ ℝ
∧ ((2 · (𝐴
· 0)) · 𝑥) =
1)) → (2 · (𝐴
· 0)) = 1) |
| 37 | 18, 36 | rexlimddv 3161 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) ∧ (2
· (𝐴 · 0)) =
2) → (2 · (𝐴
· 0)) = 1) |
| 38 | 6, 37 | mpdan 687 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) → (2
· (𝐴 · 0)) =
1) |
| 39 | | sn-1ne2 42300 |
. . . . . . 7
⊢ 1 ≠
2 |
| 40 | 39 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) → 1 ≠
2) |
| 41 | 38, 40 | eqnetrd 3008 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) → (2
· (𝐴 · 0))
≠ 2) |
| 42 | 6, 41 | pm2.21ddne 3026 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 · 0) = 1) → ¬
(𝐴 · 0) =
1) |
| 43 | 42 | ex 412 |
. . 3
⊢ (𝐴 ∈ ℝ → ((𝐴 · 0) = 1 → ¬
(𝐴 · 0) =
1)) |
| 44 | | pm2.01 188 |
. . . 4
⊢ (((𝐴 · 0) = 1 → ¬
(𝐴 · 0) = 1) →
¬ (𝐴 · 0) =
1) |
| 45 | 44 | neqned 2947 |
. . 3
⊢ (((𝐴 · 0) = 1 → ¬
(𝐴 · 0) = 1) →
(𝐴 · 0) ≠
1) |
| 46 | 43, 45 | syl 17 |
. 2
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) ≠
1) |
| 47 | | id 22 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ) |
| 48 | | elre0re 42295 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → 0 ∈
ℝ) |
| 49 | 47, 48 | remulcld 11291 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) ∈
ℝ) |
| 50 | | ax-rrecex 11227 |
. . . . . 6
⊢ (((𝐴 · 0) ∈ ℝ
∧ (𝐴 · 0) ≠
0) → ∃𝑥 ∈
ℝ ((𝐴 · 0)
· 𝑥) =
1) |
| 51 | 49, 50 | sylan 580 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 · 0) ≠ 0) →
∃𝑥 ∈ ℝ
((𝐴 · 0) ·
𝑥) = 1) |
| 52 | | simpll 767 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝐴 · 0) ≠ 0) ∧
(𝑥 ∈ ℝ ∧
((𝐴 · 0) ·
𝑥) = 1)) → 𝐴 ∈
ℝ) |
| 53 | 52 | recnd 11289 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝐴 · 0) ≠ 0) ∧
(𝑥 ∈ ℝ ∧
((𝐴 · 0) ·
𝑥) = 1)) → 𝐴 ∈
ℂ) |
| 54 | | 0cnd 11254 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝐴 · 0) ≠ 0) ∧
(𝑥 ∈ ℝ ∧
((𝐴 · 0) ·
𝑥) = 1)) → 0 ∈
ℂ) |
| 55 | | simprl 771 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝐴 · 0) ≠ 0) ∧
(𝑥 ∈ ℝ ∧
((𝐴 · 0) ·
𝑥) = 1)) → 𝑥 ∈
ℝ) |
| 56 | 55 | recnd 11289 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝐴 · 0) ≠ 0) ∧
(𝑥 ∈ ℝ ∧
((𝐴 · 0) ·
𝑥) = 1)) → 𝑥 ∈
ℂ) |
| 57 | 53, 54, 56 | mulassd 11284 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (𝐴 · 0) ≠ 0) ∧
(𝑥 ∈ ℝ ∧
((𝐴 · 0) ·
𝑥) = 1)) → ((𝐴 · 0) · 𝑥) = (𝐴 · (0 · 𝑥))) |
| 58 | | simprr 773 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (𝐴 · 0) ≠ 0) ∧
(𝑥 ∈ ℝ ∧
((𝐴 · 0) ·
𝑥) = 1)) → ((𝐴 · 0) · 𝑥) = 1) |
| 59 | 31 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → (𝐴 · (0 · 𝑥)) = (𝐴 · 0)) |
| 60 | 59 | ad2antrl 728 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (𝐴 · 0) ≠ 0) ∧
(𝑥 ∈ ℝ ∧
((𝐴 · 0) ·
𝑥) = 1)) → (𝐴 · (0 · 𝑥)) = (𝐴 · 0)) |
| 61 | 57, 58, 60 | 3eqtr3rd 2786 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (𝐴 · 0) ≠ 0) ∧
(𝑥 ∈ ℝ ∧
((𝐴 · 0) ·
𝑥) = 1)) → (𝐴 · 0) =
1) |
| 62 | 51, 61 | rexlimddv 3161 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 · 0) ≠ 0) →
(𝐴 · 0) =
1) |
| 63 | 62 | ex 412 |
. . 3
⊢ (𝐴 ∈ ℝ → ((𝐴 · 0) ≠ 0 →
(𝐴 · 0) =
1)) |
| 64 | 63 | necon1d 2962 |
. 2
⊢ (𝐴 ∈ ℝ → ((𝐴 · 0) ≠ 1 →
(𝐴 · 0) =
0)) |
| 65 | 46, 64 | mpd 15 |
1
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) =
0) |