Proof of Theorem addsq2nreurex
Step | Hyp | Ref
| Expression |
1 | | peano2cnm 11144 |
. 2
⊢ (𝐶 ∈ ℂ → (𝐶 − 1) ∈
ℂ) |
2 | | id 22 |
. . 3
⊢ (𝐶 ∈ ℂ → 𝐶 ∈
ℂ) |
3 | | 4cn 11915 |
. . . 4
⊢ 4 ∈
ℂ |
4 | 3 | a1i 11 |
. . 3
⊢ (𝐶 ∈ ℂ → 4 ∈
ℂ) |
5 | 2, 4 | subcld 11189 |
. 2
⊢ (𝐶 ∈ ℂ → (𝐶 − 4) ∈
ℂ) |
6 | | 1cnd 10828 |
. . 3
⊢ (𝐶 ∈ ℂ → 1 ∈
ℂ) |
7 | | 1re 10833 |
. . . . 5
⊢ 1 ∈
ℝ |
8 | | 1lt4 12006 |
. . . . 5
⊢ 1 <
4 |
9 | 7, 8 | ltneii 10945 |
. . . 4
⊢ 1 ≠
4 |
10 | 9 | a1i 11 |
. . 3
⊢ (𝐶 ∈ ℂ → 1 ≠
4) |
11 | 2, 6, 4, 10 | subneintrd 11233 |
. 2
⊢ (𝐶 ∈ ℂ → (𝐶 − 1) ≠ (𝐶 − 4)) |
12 | | oveq1 7220 |
. . . . . 6
⊢ (𝑏 = 1 → (𝑏↑2) = (1↑2)) |
13 | 12 | oveq2d 7229 |
. . . . 5
⊢ (𝑏 = 1 → ((𝐶 − 1) + (𝑏↑2)) = ((𝐶 − 1) + (1↑2))) |
14 | 13 | eqeq1d 2739 |
. . . 4
⊢ (𝑏 = 1 → (((𝐶 − 1) + (𝑏↑2)) = 𝐶 ↔ ((𝐶 − 1) + (1↑2)) = 𝐶)) |
15 | 14 | adantl 485 |
. . 3
⊢ ((𝐶 ∈ ℂ ∧ 𝑏 = 1) → (((𝐶 − 1) + (𝑏↑2)) = 𝐶 ↔ ((𝐶 − 1) + (1↑2)) = 𝐶)) |
16 | | sq1 13764 |
. . . . 5
⊢
(1↑2) = 1 |
17 | 16 | oveq2i 7224 |
. . . 4
⊢ ((𝐶 − 1) + (1↑2)) =
((𝐶 − 1) +
1) |
18 | | npcan1 11257 |
. . . 4
⊢ (𝐶 ∈ ℂ → ((𝐶 − 1) + 1) = 𝐶) |
19 | 17, 18 | syl5eq 2790 |
. . 3
⊢ (𝐶 ∈ ℂ → ((𝐶 − 1) + (1↑2)) =
𝐶) |
20 | 6, 15, 19 | rspcedvd 3540 |
. 2
⊢ (𝐶 ∈ ℂ →
∃𝑏 ∈ ℂ
((𝐶 − 1) + (𝑏↑2)) = 𝐶) |
21 | | 2cnd 11908 |
. . 3
⊢ (𝐶 ∈ ℂ → 2 ∈
ℂ) |
22 | | oveq1 7220 |
. . . . . 6
⊢ (𝑏 = 2 → (𝑏↑2) = (2↑2)) |
23 | 22 | oveq2d 7229 |
. . . . 5
⊢ (𝑏 = 2 → ((𝐶 − 4) + (𝑏↑2)) = ((𝐶 − 4) + (2↑2))) |
24 | 23 | eqeq1d 2739 |
. . . 4
⊢ (𝑏 = 2 → (((𝐶 − 4) + (𝑏↑2)) = 𝐶 ↔ ((𝐶 − 4) + (2↑2)) = 𝐶)) |
25 | 24 | adantl 485 |
. . 3
⊢ ((𝐶 ∈ ℂ ∧ 𝑏 = 2) → (((𝐶 − 4) + (𝑏↑2)) = 𝐶 ↔ ((𝐶 − 4) + (2↑2)) = 𝐶)) |
26 | | 2cn 11905 |
. . . . . . 7
⊢ 2 ∈
ℂ |
27 | 26 | sqcli 13750 |
. . . . . 6
⊢
(2↑2) ∈ ℂ |
28 | 27 | a1i 11 |
. . . . 5
⊢ (𝐶 ∈ ℂ →
(2↑2) ∈ ℂ) |
29 | 2, 4, 28 | subadd23d 11211 |
. . . 4
⊢ (𝐶 ∈ ℂ → ((𝐶 − 4) + (2↑2)) =
(𝐶 + ((2↑2) −
4))) |
30 | | sq2 13766 |
. . . . . . 7
⊢
(2↑2) = 4 |
31 | 30 | a1i 11 |
. . . . . 6
⊢ (𝐶 ∈ ℂ →
(2↑2) = 4) |
32 | 28, 31 | subeq0bd 11258 |
. . . . 5
⊢ (𝐶 ∈ ℂ →
((2↑2) − 4) = 0) |
33 | 27, 3 | subcli 11154 |
. . . . . 6
⊢
((2↑2) − 4) ∈ ℂ |
34 | | addid0 11251 |
. . . . . 6
⊢ ((𝐶 ∈ ℂ ∧
((2↑2) − 4) ∈ ℂ) → ((𝐶 + ((2↑2) − 4)) = 𝐶 ↔ ((2↑2) − 4) =
0)) |
35 | 33, 34 | mpan2 691 |
. . . . 5
⊢ (𝐶 ∈ ℂ → ((𝐶 + ((2↑2) − 4)) =
𝐶 ↔ ((2↑2)
− 4) = 0)) |
36 | 32, 35 | mpbird 260 |
. . . 4
⊢ (𝐶 ∈ ℂ → (𝐶 + ((2↑2) − 4)) =
𝐶) |
37 | 29, 36 | eqtrd 2777 |
. . 3
⊢ (𝐶 ∈ ℂ → ((𝐶 − 4) + (2↑2)) =
𝐶) |
38 | 21, 25, 37 | rspcedvd 3540 |
. 2
⊢ (𝐶 ∈ ℂ →
∃𝑏 ∈ ℂ
((𝐶 − 4) + (𝑏↑2)) = 𝐶) |
39 | | oveq1 7220 |
. . . . . 6
⊢ (𝑎 = (𝐶 − 1) → (𝑎 + (𝑏↑2)) = ((𝐶 − 1) + (𝑏↑2))) |
40 | 39 | eqeq1d 2739 |
. . . . 5
⊢ (𝑎 = (𝐶 − 1) → ((𝑎 + (𝑏↑2)) = 𝐶 ↔ ((𝐶 − 1) + (𝑏↑2)) = 𝐶)) |
41 | 40 | rexbidv 3216 |
. . . 4
⊢ (𝑎 = (𝐶 − 1) → (∃𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶 ↔ ∃𝑏 ∈ ℂ ((𝐶 − 1) + (𝑏↑2)) = 𝐶)) |
42 | | oveq1 7220 |
. . . . . 6
⊢ (𝑎 = (𝐶 − 4) → (𝑎 + (𝑏↑2)) = ((𝐶 − 4) + (𝑏↑2))) |
43 | 42 | eqeq1d 2739 |
. . . . 5
⊢ (𝑎 = (𝐶 − 4) → ((𝑎 + (𝑏↑2)) = 𝐶 ↔ ((𝐶 − 4) + (𝑏↑2)) = 𝐶)) |
44 | 43 | rexbidv 3216 |
. . . 4
⊢ (𝑎 = (𝐶 − 4) → (∃𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶 ↔ ∃𝑏 ∈ ℂ ((𝐶 − 4) + (𝑏↑2)) = 𝐶)) |
45 | 41, 44 | 2nreu 4356 |
. . 3
⊢ (((𝐶 − 1) ∈ ℂ ∧
(𝐶 − 4) ∈
ℂ ∧ (𝐶 − 1)
≠ (𝐶 − 4)) →
((∃𝑏 ∈ ℂ
((𝐶 − 1) + (𝑏↑2)) = 𝐶 ∧ ∃𝑏 ∈ ℂ ((𝐶 − 4) + (𝑏↑2)) = 𝐶) → ¬ ∃!𝑎 ∈ ℂ ∃𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶)) |
46 | 45 | imp 410 |
. 2
⊢ ((((𝐶 − 1) ∈ ℂ ∧
(𝐶 − 4) ∈
ℂ ∧ (𝐶 − 1)
≠ (𝐶 − 4)) ∧
(∃𝑏 ∈ ℂ
((𝐶 − 1) + (𝑏↑2)) = 𝐶 ∧ ∃𝑏 ∈ ℂ ((𝐶 − 4) + (𝑏↑2)) = 𝐶)) → ¬ ∃!𝑎 ∈ ℂ ∃𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶) |
47 | 1, 5, 11, 20, 38, 46 | syl32anc 1380 |
1
⊢ (𝐶 ∈ ℂ → ¬
∃!𝑎 ∈ ℂ
∃𝑏 ∈ ℂ
(𝑎 + (𝑏↑2)) = 𝐶) |