Proof of Theorem addsq2nreurex
Step | Hyp | Ref
| Expression |
1 | | peano2cnm 11287 |
. 2
⊢ (𝐶 ∈ ℂ → (𝐶 − 1) ∈
ℂ) |
2 | | id 22 |
. . 3
⊢ (𝐶 ∈ ℂ → 𝐶 ∈
ℂ) |
3 | | 4cn 12058 |
. . . 4
⊢ 4 ∈
ℂ |
4 | 3 | a1i 11 |
. . 3
⊢ (𝐶 ∈ ℂ → 4 ∈
ℂ) |
5 | 2, 4 | subcld 11332 |
. 2
⊢ (𝐶 ∈ ℂ → (𝐶 − 4) ∈
ℂ) |
6 | | 1cnd 10971 |
. . 3
⊢ (𝐶 ∈ ℂ → 1 ∈
ℂ) |
7 | | 1re 10976 |
. . . . 5
⊢ 1 ∈
ℝ |
8 | | 1lt4 12149 |
. . . . 5
⊢ 1 <
4 |
9 | 7, 8 | ltneii 11088 |
. . . 4
⊢ 1 ≠
4 |
10 | 9 | a1i 11 |
. . 3
⊢ (𝐶 ∈ ℂ → 1 ≠
4) |
11 | 2, 6, 4, 10 | subneintrd 11376 |
. 2
⊢ (𝐶 ∈ ℂ → (𝐶 − 1) ≠ (𝐶 − 4)) |
12 | | oveq1 7278 |
. . . . . 6
⊢ (𝑏 = 1 → (𝑏↑2) = (1↑2)) |
13 | 12 | oveq2d 7287 |
. . . . 5
⊢ (𝑏 = 1 → ((𝐶 − 1) + (𝑏↑2)) = ((𝐶 − 1) + (1↑2))) |
14 | 13 | eqeq1d 2742 |
. . . 4
⊢ (𝑏 = 1 → (((𝐶 − 1) + (𝑏↑2)) = 𝐶 ↔ ((𝐶 − 1) + (1↑2)) = 𝐶)) |
15 | 14 | adantl 482 |
. . 3
⊢ ((𝐶 ∈ ℂ ∧ 𝑏 = 1) → (((𝐶 − 1) + (𝑏↑2)) = 𝐶 ↔ ((𝐶 − 1) + (1↑2)) = 𝐶)) |
16 | | sq1 13910 |
. . . . 5
⊢
(1↑2) = 1 |
17 | 16 | oveq2i 7282 |
. . . 4
⊢ ((𝐶 − 1) + (1↑2)) =
((𝐶 − 1) +
1) |
18 | | npcan1 11400 |
. . . 4
⊢ (𝐶 ∈ ℂ → ((𝐶 − 1) + 1) = 𝐶) |
19 | 17, 18 | eqtrid 2792 |
. . 3
⊢ (𝐶 ∈ ℂ → ((𝐶 − 1) + (1↑2)) =
𝐶) |
20 | 6, 15, 19 | rspcedvd 3564 |
. 2
⊢ (𝐶 ∈ ℂ →
∃𝑏 ∈ ℂ
((𝐶 − 1) + (𝑏↑2)) = 𝐶) |
21 | | 2cnd 12051 |
. . 3
⊢ (𝐶 ∈ ℂ → 2 ∈
ℂ) |
22 | | oveq1 7278 |
. . . . . 6
⊢ (𝑏 = 2 → (𝑏↑2) = (2↑2)) |
23 | 22 | oveq2d 7287 |
. . . . 5
⊢ (𝑏 = 2 → ((𝐶 − 4) + (𝑏↑2)) = ((𝐶 − 4) + (2↑2))) |
24 | 23 | eqeq1d 2742 |
. . . 4
⊢ (𝑏 = 2 → (((𝐶 − 4) + (𝑏↑2)) = 𝐶 ↔ ((𝐶 − 4) + (2↑2)) = 𝐶)) |
25 | 24 | adantl 482 |
. . 3
⊢ ((𝐶 ∈ ℂ ∧ 𝑏 = 2) → (((𝐶 − 4) + (𝑏↑2)) = 𝐶 ↔ ((𝐶 − 4) + (2↑2)) = 𝐶)) |
26 | | 2cn 12048 |
. . . . . . 7
⊢ 2 ∈
ℂ |
27 | 26 | sqcli 13896 |
. . . . . 6
⊢
(2↑2) ∈ ℂ |
28 | 27 | a1i 11 |
. . . . 5
⊢ (𝐶 ∈ ℂ →
(2↑2) ∈ ℂ) |
29 | 2, 4, 28 | subadd23d 11354 |
. . . 4
⊢ (𝐶 ∈ ℂ → ((𝐶 − 4) + (2↑2)) =
(𝐶 + ((2↑2) −
4))) |
30 | | sq2 13912 |
. . . . . . 7
⊢
(2↑2) = 4 |
31 | 30 | a1i 11 |
. . . . . 6
⊢ (𝐶 ∈ ℂ →
(2↑2) = 4) |
32 | 28, 31 | subeq0bd 11401 |
. . . . 5
⊢ (𝐶 ∈ ℂ →
((2↑2) − 4) = 0) |
33 | 27, 3 | subcli 11297 |
. . . . . 6
⊢
((2↑2) − 4) ∈ ℂ |
34 | | addid0 11394 |
. . . . . 6
⊢ ((𝐶 ∈ ℂ ∧
((2↑2) − 4) ∈ ℂ) → ((𝐶 + ((2↑2) − 4)) = 𝐶 ↔ ((2↑2) − 4) =
0)) |
35 | 33, 34 | mpan2 688 |
. . . . 5
⊢ (𝐶 ∈ ℂ → ((𝐶 + ((2↑2) − 4)) =
𝐶 ↔ ((2↑2)
− 4) = 0)) |
36 | 32, 35 | mpbird 256 |
. . . 4
⊢ (𝐶 ∈ ℂ → (𝐶 + ((2↑2) − 4)) =
𝐶) |
37 | 29, 36 | eqtrd 2780 |
. . 3
⊢ (𝐶 ∈ ℂ → ((𝐶 − 4) + (2↑2)) =
𝐶) |
38 | 21, 25, 37 | rspcedvd 3564 |
. 2
⊢ (𝐶 ∈ ℂ →
∃𝑏 ∈ ℂ
((𝐶 − 4) + (𝑏↑2)) = 𝐶) |
39 | | oveq1 7278 |
. . . . . 6
⊢ (𝑎 = (𝐶 − 1) → (𝑎 + (𝑏↑2)) = ((𝐶 − 1) + (𝑏↑2))) |
40 | 39 | eqeq1d 2742 |
. . . . 5
⊢ (𝑎 = (𝐶 − 1) → ((𝑎 + (𝑏↑2)) = 𝐶 ↔ ((𝐶 − 1) + (𝑏↑2)) = 𝐶)) |
41 | 40 | rexbidv 3228 |
. . . 4
⊢ (𝑎 = (𝐶 − 1) → (∃𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶 ↔ ∃𝑏 ∈ ℂ ((𝐶 − 1) + (𝑏↑2)) = 𝐶)) |
42 | | oveq1 7278 |
. . . . . 6
⊢ (𝑎 = (𝐶 − 4) → (𝑎 + (𝑏↑2)) = ((𝐶 − 4) + (𝑏↑2))) |
43 | 42 | eqeq1d 2742 |
. . . . 5
⊢ (𝑎 = (𝐶 − 4) → ((𝑎 + (𝑏↑2)) = 𝐶 ↔ ((𝐶 − 4) + (𝑏↑2)) = 𝐶)) |
44 | 43 | rexbidv 3228 |
. . . 4
⊢ (𝑎 = (𝐶 − 4) → (∃𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶 ↔ ∃𝑏 ∈ ℂ ((𝐶 − 4) + (𝑏↑2)) = 𝐶)) |
45 | 41, 44 | 2nreu 4381 |
. . 3
⊢ (((𝐶 − 1) ∈ ℂ ∧
(𝐶 − 4) ∈
ℂ ∧ (𝐶 − 1)
≠ (𝐶 − 4)) →
((∃𝑏 ∈ ℂ
((𝐶 − 1) + (𝑏↑2)) = 𝐶 ∧ ∃𝑏 ∈ ℂ ((𝐶 − 4) + (𝑏↑2)) = 𝐶) → ¬ ∃!𝑎 ∈ ℂ ∃𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶)) |
46 | 45 | imp 407 |
. 2
⊢ ((((𝐶 − 1) ∈ ℂ ∧
(𝐶 − 4) ∈
ℂ ∧ (𝐶 − 1)
≠ (𝐶 − 4)) ∧
(∃𝑏 ∈ ℂ
((𝐶 − 1) + (𝑏↑2)) = 𝐶 ∧ ∃𝑏 ∈ ℂ ((𝐶 − 4) + (𝑏↑2)) = 𝐶)) → ¬ ∃!𝑎 ∈ ℂ ∃𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶) |
47 | 1, 5, 11, 20, 38, 46 | syl32anc 1377 |
1
⊢ (𝐶 ∈ ℂ → ¬
∃!𝑎 ∈ ℂ
∃𝑏 ∈ ℂ
(𝑎 + (𝑏↑2)) = 𝐶) |