Step | Hyp | Ref
| Expression |
1 | | sn-1ne2 40002 |
. 2
⊢ 1 ≠
2 |
2 | | elre0re 39998 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → 0 ∈
ℝ) |
3 | | id 22 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ) |
4 | 2, 3 | remulcld 10863 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (0
· 𝐴) ∈
ℝ) |
5 | | ax-rrecex 10801 |
. . . . . 6
⊢ (((0
· 𝐴) ∈ ℝ
∧ (0 · 𝐴) ≠
0) → ∃𝑥 ∈
ℝ ((0 · 𝐴)
· 𝑥) =
1) |
6 | 4, 5 | sylan 583 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) →
∃𝑥 ∈ ℝ ((0
· 𝐴) · 𝑥) = 1) |
7 | | simprr 773 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → ((0 ·
𝐴) · 𝑥) = 1) |
8 | | df-2 11893 |
. . . . . . . . . . . . 13
⊢ 2 = (1 +
1) |
9 | 8 | oveq1i 7223 |
. . . . . . . . . . . 12
⊢ (2
· 0) = ((1 + 1) · 0) |
10 | | re0m0e0 40093 |
. . . . . . . . . . . . . . 15
⊢ (0
−ℝ 0) = 0 |
11 | 10 | eqcomi 2746 |
. . . . . . . . . . . . . 14
⊢ 0 = (0
−ℝ 0) |
12 | 11 | oveq2i 7224 |
. . . . . . . . . . . . 13
⊢ ((1 + 1)
· 0) = ((1 + 1) · (0 −ℝ
0)) |
13 | | 1re 10833 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
14 | 13, 13 | readdcli 10848 |
. . . . . . . . . . . . . 14
⊢ (1 + 1)
∈ ℝ |
15 | | sn-00idlem1 40089 |
. . . . . . . . . . . . . 14
⊢ ((1 + 1)
∈ ℝ → ((1 + 1) · (0 −ℝ 0)) = ((1
+ 1) −ℝ (1 + 1))) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((1 + 1)
· (0 −ℝ 0)) = ((1 + 1) −ℝ
(1 + 1)) |
17 | | repnpcan 40083 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ 1 ∈ ℝ ∧ 1 ∈ ℝ) → ((1 + 1)
−ℝ (1 + 1)) = (1 −ℝ
1)) |
18 | 13, 13, 13, 17 | mp3an 1463 |
. . . . . . . . . . . . . 14
⊢ ((1 + 1)
−ℝ (1 + 1)) = (1 −ℝ
1) |
19 | | re1m1e0m0 40088 |
. . . . . . . . . . . . . 14
⊢ (1
−ℝ 1) = (0 −ℝ 0) |
20 | 18, 19, 10 | 3eqtri 2769 |
. . . . . . . . . . . . 13
⊢ ((1 + 1)
−ℝ (1 + 1)) = 0 |
21 | 12, 16, 20 | 3eqtri 2769 |
. . . . . . . . . . . 12
⊢ ((1 + 1)
· 0) = 0 |
22 | 9, 21 | eqtr2i 2766 |
. . . . . . . . . . 11
⊢ 0 = (2
· 0) |
23 | 22 | oveq1i 7223 |
. . . . . . . . . 10
⊢ (0
· 𝐴) = ((2 ·
0) · 𝐴) |
24 | 23 | oveq1i 7223 |
. . . . . . . . 9
⊢ ((0
· 𝐴) · 𝑥) = (((2 · 0) ·
𝐴) · 𝑥) |
25 | 24 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → ((0 ·
𝐴) · 𝑥) = (((2 · 0) ·
𝐴) · 𝑥)) |
26 | | 2cnd 11908 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → 2 ∈
ℂ) |
27 | | 0cnd 10826 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → 0 ∈
ℂ) |
28 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → 𝐴 ∈ ℝ) |
29 | 28 | recnd 10861 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → 𝐴 ∈ ℂ) |
30 | 26, 27, 29 | mulassd 10856 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → ((2 · 0)
· 𝐴) = (2 ·
(0 · 𝐴))) |
31 | 30 | oveq1d 7228 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → (((2 · 0)
· 𝐴) · 𝑥) = ((2 · (0 ·
𝐴)) · 𝑥)) |
32 | 4 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → (0 · 𝐴) ∈
ℝ) |
33 | 32 | recnd 10861 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → (0 · 𝐴) ∈
ℂ) |
34 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → 𝑥 ∈
ℝ) |
35 | 34 | recnd 10861 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → 𝑥 ∈
ℂ) |
36 | 26, 33, 35 | mulassd 10856 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → ((2 · (0
· 𝐴)) · 𝑥) = (2 · ((0 ·
𝐴) · 𝑥))) |
37 | 25, 31, 36 | 3eqtrd 2781 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → ((0 ·
𝐴) · 𝑥) = (2 · ((0 ·
𝐴) · 𝑥))) |
38 | 7 | oveq2d 7229 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → (2 · ((0
· 𝐴) · 𝑥)) = (2 ·
1)) |
39 | | 2re 11904 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
40 | | ax-1rid 10799 |
. . . . . . . 8
⊢ (2 ∈
ℝ → (2 · 1) = 2) |
41 | 39, 40 | mp1i 13 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → (2 · 1) =
2) |
42 | 37, 38, 41 | 3eqtrd 2781 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → ((0 ·
𝐴) · 𝑥) = 2) |
43 | 7, 42 | eqtr3d 2779 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
(𝑥 ∈ ℝ ∧ ((0
· 𝐴) · 𝑥) = 1)) → 1 =
2) |
44 | 6, 43 | rexlimddv 3210 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) →
1 = 2) |
45 | 44 | ex 416 |
. . 3
⊢ (𝐴 ∈ ℝ → ((0
· 𝐴) ≠ 0 → 1
= 2)) |
46 | 45 | necon1d 2962 |
. 2
⊢ (𝐴 ∈ ℝ → (1 ≠ 2
→ (0 · 𝐴) =
0)) |
47 | 1, 46 | mpi 20 |
1
⊢ (𝐴 ∈ ℝ → (0
· 𝐴) =
0) |