Proof of Theorem addsqnreup
| Step | Hyp | Ref
| Expression |
| 1 | | ax-1cn 11213 |
. . . . . . 7
⊢ 1 ∈
ℂ |
| 2 | | 0cn 11253 |
. . . . . . 7
⊢ 0 ∈
ℂ |
| 3 | | opelxpi 5722 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ 0 ∈ ℂ) → 〈1, 0〉 ∈ (ℂ
× ℂ)) |
| 4 | 1, 2, 3 | mp2an 692 |
. . . . . 6
⊢ 〈1,
0〉 ∈ (ℂ × ℂ) |
| 5 | | 3cn 12347 |
. . . . . . . 8
⊢ 3 ∈
ℂ |
| 6 | 5 | negcli 11577 |
. . . . . . 7
⊢ -3 ∈
ℂ |
| 7 | | 2cn 12341 |
. . . . . . 7
⊢ 2 ∈
ℂ |
| 8 | | opelxpi 5722 |
. . . . . . 7
⊢ ((-3
∈ ℂ ∧ 2 ∈ ℂ) → 〈-3, 2〉 ∈ (ℂ
× ℂ)) |
| 9 | 6, 7, 8 | mp2an 692 |
. . . . . 6
⊢ 〈-3,
2〉 ∈ (ℂ × ℂ) |
| 10 | | 0ne2 12473 |
. . . . . . . 8
⊢ 0 ≠
2 |
| 11 | 10 | olci 867 |
. . . . . . 7
⊢ (1 ≠
-3 ∨ 0 ≠ 2) |
| 12 | | 1ex 11257 |
. . . . . . . 8
⊢ 1 ∈
V |
| 13 | | c0ex 11255 |
. . . . . . . 8
⊢ 0 ∈
V |
| 14 | 12, 13 | opthne 5487 |
. . . . . . 7
⊢ (〈1,
0〉 ≠ 〈-3, 2〉 ↔ (1 ≠ -3 ∨ 0 ≠
2)) |
| 15 | 11, 14 | mpbir 231 |
. . . . . 6
⊢ 〈1,
0〉 ≠ 〈-3, 2〉 |
| 16 | 4, 9, 15 | 3pm3.2i 1340 |
. . . . 5
⊢ (〈1,
0〉 ∈ (ℂ × ℂ) ∧ 〈-3, 2〉 ∈
(ℂ × ℂ) ∧ 〈1, 0〉 ≠ 〈-3,
2〉) |
| 17 | 12, 13 | op1st 8022 |
. . . . . . . 8
⊢
(1st ‘〈1, 0〉) = 1 |
| 18 | 12, 13 | op2nd 8023 |
. . . . . . . . . 10
⊢
(2nd ‘〈1, 0〉) = 0 |
| 19 | 18 | oveq1i 7441 |
. . . . . . . . 9
⊢
((2nd ‘〈1, 0〉)↑2) =
(0↑2) |
| 20 | | sq0 14231 |
. . . . . . . . 9
⊢
(0↑2) = 0 |
| 21 | 19, 20 | eqtri 2765 |
. . . . . . . 8
⊢
((2nd ‘〈1, 0〉)↑2) = 0 |
| 22 | 17, 21 | oveq12i 7443 |
. . . . . . 7
⊢
((1st ‘〈1, 0〉) + ((2nd
‘〈1, 0〉)↑2)) = (1 + 0) |
| 23 | | 1p0e1 12390 |
. . . . . . 7
⊢ (1 + 0) =
1 |
| 24 | 22, 23 | eqtri 2765 |
. . . . . 6
⊢
((1st ‘〈1, 0〉) + ((2nd
‘〈1, 0〉)↑2)) = 1 |
| 25 | | negex 11506 |
. . . . . . . . 9
⊢ -3 ∈
V |
| 26 | | 2ex 12343 |
. . . . . . . . 9
⊢ 2 ∈
V |
| 27 | 25, 26 | op1st 8022 |
. . . . . . . 8
⊢
(1st ‘〈-3, 2〉) = -3 |
| 28 | 25, 26 | op2nd 8023 |
. . . . . . . . . 10
⊢
(2nd ‘〈-3, 2〉) = 2 |
| 29 | 28 | oveq1i 7441 |
. . . . . . . . 9
⊢
((2nd ‘〈-3, 2〉)↑2) =
(2↑2) |
| 30 | | sq2 14236 |
. . . . . . . . 9
⊢
(2↑2) = 4 |
| 31 | 29, 30 | eqtri 2765 |
. . . . . . . 8
⊢
((2nd ‘〈-3, 2〉)↑2) = 4 |
| 32 | 27, 31 | oveq12i 7443 |
. . . . . . 7
⊢
((1st ‘〈-3, 2〉) + ((2nd
‘〈-3, 2〉)↑2)) = (-3 + 4) |
| 33 | | 4cn 12351 |
. . . . . . . 8
⊢ 4 ∈
ℂ |
| 34 | 33, 5 | negsubi 11587 |
. . . . . . . . 9
⊢ (4 + -3)
= (4 − 3) |
| 35 | | 3p1e4 12411 |
. . . . . . . . . 10
⊢ (3 + 1) =
4 |
| 36 | 33, 5, 1, 35 | subaddrii 11598 |
. . . . . . . . 9
⊢ (4
− 3) = 1 |
| 37 | 34, 36 | eqtri 2765 |
. . . . . . . 8
⊢ (4 + -3)
= 1 |
| 38 | 33, 6, 37 | addcomli 11453 |
. . . . . . 7
⊢ (-3 + 4)
= 1 |
| 39 | 32, 38 | eqtri 2765 |
. . . . . 6
⊢
((1st ‘〈-3, 2〉) + ((2nd
‘〈-3, 2〉)↑2)) = 1 |
| 40 | 24, 39 | pm3.2i 470 |
. . . . 5
⊢
(((1st ‘〈1, 0〉) + ((2nd
‘〈1, 0〉)↑2)) = 1 ∧ ((1st ‘〈-3,
2〉) + ((2nd ‘〈-3, 2〉)↑2)) =
1) |
| 41 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑝 = 〈1, 0〉 →
(1st ‘𝑝) =
(1st ‘〈1, 0〉)) |
| 42 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑝 = 〈1, 0〉 →
(2nd ‘𝑝) =
(2nd ‘〈1, 0〉)) |
| 43 | 42 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑝 = 〈1, 0〉 →
((2nd ‘𝑝)↑2) = ((2nd ‘〈1,
0〉)↑2)) |
| 44 | 41, 43 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑝 = 〈1, 0〉 →
((1st ‘𝑝)
+ ((2nd ‘𝑝)↑2)) = ((1st ‘〈1,
0〉) + ((2nd ‘〈1, 0〉)↑2))) |
| 45 | 44 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑝 = 〈1, 0〉 →
(((1st ‘𝑝)
+ ((2nd ‘𝑝)↑2)) = 1 ↔ ((1st
‘〈1, 0〉) + ((2nd ‘〈1, 0〉)↑2)) =
1)) |
| 46 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑝 = 〈-3, 2〉 →
(1st ‘𝑝) =
(1st ‘〈-3, 2〉)) |
| 47 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑝 = 〈-3, 2〉 →
(2nd ‘𝑝) =
(2nd ‘〈-3, 2〉)) |
| 48 | 47 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑝 = 〈-3, 2〉 →
((2nd ‘𝑝)↑2) = ((2nd ‘〈-3,
2〉)↑2)) |
| 49 | 46, 48 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑝 = 〈-3, 2〉 →
((1st ‘𝑝)
+ ((2nd ‘𝑝)↑2)) = ((1st
‘〈-3, 2〉) + ((2nd ‘〈-3,
2〉)↑2))) |
| 50 | 49 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑝 = 〈-3, 2〉 →
(((1st ‘𝑝)
+ ((2nd ‘𝑝)↑2)) = 1 ↔ ((1st
‘〈-3, 2〉) + ((2nd ‘〈-3, 2〉)↑2))
= 1)) |
| 51 | 45, 50 | 2nreu 4444 |
. . . . 5
⊢
((〈1, 0〉 ∈ (ℂ × ℂ) ∧ 〈-3,
2〉 ∈ (ℂ × ℂ) ∧ 〈1, 0〉 ≠ 〈-3,
2〉) → ((((1st ‘〈1, 0〉) + ((2nd
‘〈1, 0〉)↑2)) = 1 ∧ ((1st ‘〈-3,
2〉) + ((2nd ‘〈-3, 2〉)↑2)) = 1) →
¬ ∃!𝑝 ∈
(ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) =
1)) |
| 52 | 16, 40, 51 | mp2 9 |
. . . 4
⊢ ¬
∃!𝑝 ∈ (ℂ
× ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 1 |
| 53 | | eqeq2 2749 |
. . . . 5
⊢ (𝐶 = 1 → (((1st
‘𝑝) +
((2nd ‘𝑝)↑2)) = 𝐶 ↔ ((1st ‘𝑝) + ((2nd
‘𝑝)↑2)) =
1)) |
| 54 | 53 | reubidv 3398 |
. . . 4
⊢ (𝐶 = 1 → (∃!𝑝 ∈ (ℂ ×
ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶 ↔ ∃!𝑝 ∈ (ℂ ×
ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) =
1)) |
| 55 | 52, 54 | mtbiri 327 |
. . 3
⊢ (𝐶 = 1 → ¬ ∃!𝑝 ∈ (ℂ ×
ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶) |
| 56 | 55 | a1d 25 |
. 2
⊢ (𝐶 = 1 → (𝐶 ∈ ℂ → ¬ ∃!𝑝 ∈ (ℂ ×
ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶)) |
| 57 | | id 22 |
. . . . . . 7
⊢ (𝐶 ∈ ℂ → 𝐶 ∈
ℂ) |
| 58 | | 0cnd 11254 |
. . . . . . 7
⊢ (𝐶 ∈ ℂ → 0 ∈
ℂ) |
| 59 | 57, 58 | opelxpd 5724 |
. . . . . 6
⊢ (𝐶 ∈ ℂ →
〈𝐶, 0〉 ∈
(ℂ × ℂ)) |
| 60 | 59 | adantr 480 |
. . . . 5
⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) → 〈𝐶, 0〉 ∈ (ℂ
× ℂ)) |
| 61 | | 1cnd 11256 |
. . . . . . 7
⊢ (𝐶 ∈ ℂ → 1 ∈
ℂ) |
| 62 | | peano2cnm 11575 |
. . . . . . . 8
⊢ (𝐶 ∈ ℂ → (𝐶 − 1) ∈
ℂ) |
| 63 | 62 | sqrtcld 15476 |
. . . . . . 7
⊢ (𝐶 ∈ ℂ →
(√‘(𝐶 −
1)) ∈ ℂ) |
| 64 | 61, 63 | opelxpd 5724 |
. . . . . 6
⊢ (𝐶 ∈ ℂ → 〈1,
(√‘(𝐶 −
1))〉 ∈ (ℂ × ℂ)) |
| 65 | 64 | adantr 480 |
. . . . 5
⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) → 〈1,
(√‘(𝐶 −
1))〉 ∈ (ℂ × ℂ)) |
| 66 | | animorrl 983 |
. . . . . 6
⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) → (𝐶 ≠ 1 ∨ 0 ≠
(√‘(𝐶 −
1)))) |
| 67 | | 0cnd 11254 |
. . . . . . 7
⊢ (𝐶 ≠ 1 → 0 ∈
ℂ) |
| 68 | | opthneg 5486 |
. . . . . . 7
⊢ ((𝐶 ∈ ℂ ∧ 0 ∈
ℂ) → (〈𝐶,
0〉 ≠ 〈1, (√‘(𝐶 − 1))〉 ↔ (𝐶 ≠ 1 ∨ 0 ≠ (√‘(𝐶 − 1))))) |
| 69 | 67, 68 | sylan2 593 |
. . . . . 6
⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) → (〈𝐶, 0〉 ≠ 〈1,
(√‘(𝐶 −
1))〉 ↔ (𝐶 ≠ 1
∨ 0 ≠ (√‘(𝐶 − 1))))) |
| 70 | 66, 69 | mpbird 257 |
. . . . 5
⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) → 〈𝐶, 0〉 ≠ 〈1,
(√‘(𝐶 −
1))〉) |
| 71 | 60, 65, 70 | 3jca 1129 |
. . . 4
⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) → (〈𝐶, 0〉 ∈ (ℂ
× ℂ) ∧ 〈1, (√‘(𝐶 − 1))〉 ∈ (ℂ ×
ℂ) ∧ 〈𝐶,
0〉 ≠ 〈1, (√‘(𝐶 − 1))〉)) |
| 72 | | op1stg 8026 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℂ ∧ 0 ∈
ℂ) → (1st ‘〈𝐶, 0〉) = 𝐶) |
| 73 | 58, 72 | mpdan 687 |
. . . . . . . 8
⊢ (𝐶 ∈ ℂ →
(1st ‘〈𝐶, 0〉) = 𝐶) |
| 74 | | op2ndg 8027 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℂ ∧ 0 ∈
ℂ) → (2nd ‘〈𝐶, 0〉) = 0) |
| 75 | 58, 74 | mpdan 687 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℂ →
(2nd ‘〈𝐶, 0〉) = 0) |
| 76 | 75 | sq0id 14233 |
. . . . . . . 8
⊢ (𝐶 ∈ ℂ →
((2nd ‘〈𝐶, 0〉)↑2) = 0) |
| 77 | 73, 76 | oveq12d 7449 |
. . . . . . 7
⊢ (𝐶 ∈ ℂ →
((1st ‘〈𝐶, 0〉) + ((2nd
‘〈𝐶,
0〉)↑2)) = (𝐶 +
0)) |
| 78 | | addrid 11441 |
. . . . . . 7
⊢ (𝐶 ∈ ℂ → (𝐶 + 0) = 𝐶) |
| 79 | 77, 78 | eqtrd 2777 |
. . . . . 6
⊢ (𝐶 ∈ ℂ →
((1st ‘〈𝐶, 0〉) + ((2nd
‘〈𝐶,
0〉)↑2)) = 𝐶) |
| 80 | | op1stg 8026 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ (√‘(𝐶 − 1)) ∈ ℂ) →
(1st ‘〈1, (√‘(𝐶 − 1))〉) = 1) |
| 81 | 61, 63, 80 | syl2anc 584 |
. . . . . . . 8
⊢ (𝐶 ∈ ℂ →
(1st ‘〈1, (√‘(𝐶 − 1))〉) = 1) |
| 82 | | op2ndg 8027 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ (√‘(𝐶 − 1)) ∈ ℂ) →
(2nd ‘〈1, (√‘(𝐶 − 1))〉) = (√‘(𝐶 − 1))) |
| 83 | 61, 63, 82 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ℂ →
(2nd ‘〈1, (√‘(𝐶 − 1))〉) = (√‘(𝐶 − 1))) |
| 84 | 83 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℂ →
((2nd ‘〈1, (√‘(𝐶 − 1))〉)↑2) =
((√‘(𝐶 −
1))↑2)) |
| 85 | 62 | sqsqrtd 15478 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℂ →
((√‘(𝐶 −
1))↑2) = (𝐶 −
1)) |
| 86 | 84, 85 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝐶 ∈ ℂ →
((2nd ‘〈1, (√‘(𝐶 − 1))〉)↑2) = (𝐶 − 1)) |
| 87 | 81, 86 | oveq12d 7449 |
. . . . . . 7
⊢ (𝐶 ∈ ℂ →
((1st ‘〈1, (√‘(𝐶 − 1))〉) + ((2nd
‘〈1, (√‘(𝐶 − 1))〉)↑2)) = (1 + (𝐶 − 1))) |
| 88 | 61, 57 | pncan3d 11623 |
. . . . . . 7
⊢ (𝐶 ∈ ℂ → (1 +
(𝐶 − 1)) = 𝐶) |
| 89 | 87, 88 | eqtrd 2777 |
. . . . . 6
⊢ (𝐶 ∈ ℂ →
((1st ‘〈1, (√‘(𝐶 − 1))〉) + ((2nd
‘〈1, (√‘(𝐶 − 1))〉)↑2)) = 𝐶) |
| 90 | 79, 89 | jca 511 |
. . . . 5
⊢ (𝐶 ∈ ℂ →
(((1st ‘〈𝐶, 0〉) + ((2nd
‘〈𝐶,
0〉)↑2)) = 𝐶 ∧
((1st ‘〈1, (√‘(𝐶 − 1))〉) + ((2nd
‘〈1, (√‘(𝐶 − 1))〉)↑2)) = 𝐶)) |
| 91 | 90 | adantr 480 |
. . . 4
⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) →
(((1st ‘〈𝐶, 0〉) + ((2nd
‘〈𝐶,
0〉)↑2)) = 𝐶 ∧
((1st ‘〈1, (√‘(𝐶 − 1))〉) + ((2nd
‘〈1, (√‘(𝐶 − 1))〉)↑2)) = 𝐶)) |
| 92 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑝 = 〈𝐶, 0〉 → (1st
‘𝑝) = (1st
‘〈𝐶,
0〉)) |
| 93 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑝 = 〈𝐶, 0〉 → (2nd
‘𝑝) = (2nd
‘〈𝐶,
0〉)) |
| 94 | 93 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑝 = 〈𝐶, 0〉 → ((2nd
‘𝑝)↑2) =
((2nd ‘〈𝐶, 0〉)↑2)) |
| 95 | 92, 94 | oveq12d 7449 |
. . . . . 6
⊢ (𝑝 = 〈𝐶, 0〉 → ((1st
‘𝑝) +
((2nd ‘𝑝)↑2)) = ((1st
‘〈𝐶, 0〉) +
((2nd ‘〈𝐶, 0〉)↑2))) |
| 96 | 95 | eqeq1d 2739 |
. . . . 5
⊢ (𝑝 = 〈𝐶, 0〉 → (((1st
‘𝑝) +
((2nd ‘𝑝)↑2)) = 𝐶 ↔ ((1st ‘〈𝐶, 0〉) + ((2nd
‘〈𝐶,
0〉)↑2)) = 𝐶)) |
| 97 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑝 = 〈1,
(√‘(𝐶 −
1))〉 → (1st ‘𝑝) = (1st ‘〈1,
(√‘(𝐶 −
1))〉)) |
| 98 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑝 = 〈1,
(√‘(𝐶 −
1))〉 → (2nd ‘𝑝) = (2nd ‘〈1,
(√‘(𝐶 −
1))〉)) |
| 99 | 98 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑝 = 〈1,
(√‘(𝐶 −
1))〉 → ((2nd ‘𝑝)↑2) = ((2nd ‘〈1,
(√‘(𝐶 −
1))〉)↑2)) |
| 100 | 97, 99 | oveq12d 7449 |
. . . . . 6
⊢ (𝑝 = 〈1,
(√‘(𝐶 −
1))〉 → ((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = ((1st
‘〈1, (√‘(𝐶 − 1))〉) + ((2nd
‘〈1, (√‘(𝐶 −
1))〉)↑2))) |
| 101 | 100 | eqeq1d 2739 |
. . . . 5
⊢ (𝑝 = 〈1,
(√‘(𝐶 −
1))〉 → (((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶 ↔ ((1st ‘〈1,
(√‘(𝐶 −
1))〉) + ((2nd ‘〈1, (√‘(𝐶 − 1))〉)↑2)) = 𝐶)) |
| 102 | 96, 101 | 2nreu 4444 |
. . . 4
⊢
((〈𝐶, 0〉
∈ (ℂ × ℂ) ∧ 〈1, (√‘(𝐶 − 1))〉 ∈
(ℂ × ℂ) ∧ 〈𝐶, 0〉 ≠ 〈1,
(√‘(𝐶 −
1))〉) → ((((1st ‘〈𝐶, 0〉) + ((2nd
‘〈𝐶,
0〉)↑2)) = 𝐶 ∧
((1st ‘〈1, (√‘(𝐶 − 1))〉) + ((2nd
‘〈1, (√‘(𝐶 − 1))〉)↑2)) = 𝐶) → ¬ ∃!𝑝 ∈ (ℂ ×
ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶)) |
| 103 | 71, 91, 102 | sylc 65 |
. . 3
⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) → ¬
∃!𝑝 ∈ (ℂ
× ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶) |
| 104 | 103 | expcom 413 |
. 2
⊢ (𝐶 ≠ 1 → (𝐶 ∈ ℂ → ¬
∃!𝑝 ∈ (ℂ
× ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶)) |
| 105 | 56, 104 | pm2.61ine 3025 |
1
⊢ (𝐶 ∈ ℂ → ¬
∃!𝑝 ∈ (ℂ
× ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶) |