Description: For each complex number C , there does not exist a unique complex number b , squared and added to a unique another complex number a resulting in the given complex number C . Actually, for each complex number b , a = ( C - ( b ^ 2 ) ) is unique.
Remark: This, together with addsq2reu , shows that commutation of two unique quantifications need not be equivalent, and provides an evident justification of the fact that considering the pair of variables is necessary to obtain what we intuitively understand as "double unique existence". (Proposed by GL, 23-Jun-2023.). (Contributed by AV, 23-Jun-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | addsqn2reu | ⊢ ( 𝐶 ∈ ℂ → ¬ ∃! 𝑏 ∈ ℂ ∃! 𝑎 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-1cn | ⊢ 1 ∈ ℂ | |
| 2 | neg1cn | ⊢ - 1 ∈ ℂ | |
| 3 | 1nn | ⊢ 1 ∈ ℕ | |
| 4 | nnneneg | ⊢ ( 1 ∈ ℕ → 1 ≠ - 1 ) | |
| 5 | 3 4 | ax-mp | ⊢ 1 ≠ - 1 |
| 6 | 1 2 5 | 3pm3.2i | ⊢ ( 1 ∈ ℂ ∧ - 1 ∈ ℂ ∧ 1 ≠ - 1 ) |
| 7 | 1cnd | ⊢ ( 𝐶 ∈ ℂ → 1 ∈ ℂ ) | |
| 8 | negeu | ⊢ ( ( 1 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ∃! 𝑎 ∈ ℂ ( 1 + 𝑎 ) = 𝐶 ) | |
| 9 | 7 8 | mpancom | ⊢ ( 𝐶 ∈ ℂ → ∃! 𝑎 ∈ ℂ ( 1 + 𝑎 ) = 𝐶 ) |
| 10 | sq1 | ⊢ ( 1 ↑ 2 ) = 1 | |
| 11 | 10 | a1i | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( 1 ↑ 2 ) = 1 ) |
| 12 | 11 | oveq2d | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( 𝑎 + ( 1 ↑ 2 ) ) = ( 𝑎 + 1 ) ) |
| 13 | id | ⊢ ( 𝑎 ∈ ℂ → 𝑎 ∈ ℂ ) | |
| 14 | 1cnd | ⊢ ( 𝑎 ∈ ℂ → 1 ∈ ℂ ) | |
| 15 | 13 14 | addcomd | ⊢ ( 𝑎 ∈ ℂ → ( 𝑎 + 1 ) = ( 1 + 𝑎 ) ) |
| 16 | 15 | adantl | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( 𝑎 + 1 ) = ( 1 + 𝑎 ) ) |
| 17 | 12 16 | eqtrd | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( 𝑎 + ( 1 ↑ 2 ) ) = ( 1 + 𝑎 ) ) |
| 18 | 17 | eqeq1d | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( ( 𝑎 + ( 1 ↑ 2 ) ) = 𝐶 ↔ ( 1 + 𝑎 ) = 𝐶 ) ) |
| 19 | 18 | reubidva | ⊢ ( 𝐶 ∈ ℂ → ( ∃! 𝑎 ∈ ℂ ( 𝑎 + ( 1 ↑ 2 ) ) = 𝐶 ↔ ∃! 𝑎 ∈ ℂ ( 1 + 𝑎 ) = 𝐶 ) ) |
| 20 | 9 19 | mpbird | ⊢ ( 𝐶 ∈ ℂ → ∃! 𝑎 ∈ ℂ ( 𝑎 + ( 1 ↑ 2 ) ) = 𝐶 ) |
| 21 | neg1sqe1 | ⊢ ( - 1 ↑ 2 ) = 1 | |
| 22 | 21 | a1i | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( - 1 ↑ 2 ) = 1 ) |
| 23 | 22 | oveq2d | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( 𝑎 + ( - 1 ↑ 2 ) ) = ( 𝑎 + 1 ) ) |
| 24 | 23 16 | eqtrd | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( 𝑎 + ( - 1 ↑ 2 ) ) = ( 1 + 𝑎 ) ) |
| 25 | 24 | eqeq1d | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( ( 𝑎 + ( - 1 ↑ 2 ) ) = 𝐶 ↔ ( 1 + 𝑎 ) = 𝐶 ) ) |
| 26 | 25 | reubidva | ⊢ ( 𝐶 ∈ ℂ → ( ∃! 𝑎 ∈ ℂ ( 𝑎 + ( - 1 ↑ 2 ) ) = 𝐶 ↔ ∃! 𝑎 ∈ ℂ ( 1 + 𝑎 ) = 𝐶 ) ) |
| 27 | 9 26 | mpbird | ⊢ ( 𝐶 ∈ ℂ → ∃! 𝑎 ∈ ℂ ( 𝑎 + ( - 1 ↑ 2 ) ) = 𝐶 ) |
| 28 | 20 27 | jca | ⊢ ( 𝐶 ∈ ℂ → ( ∃! 𝑎 ∈ ℂ ( 𝑎 + ( 1 ↑ 2 ) ) = 𝐶 ∧ ∃! 𝑎 ∈ ℂ ( 𝑎 + ( - 1 ↑ 2 ) ) = 𝐶 ) ) |
| 29 | oveq1 | ⊢ ( 𝑏 = 1 → ( 𝑏 ↑ 2 ) = ( 1 ↑ 2 ) ) | |
| 30 | 29 | oveq2d | ⊢ ( 𝑏 = 1 → ( 𝑎 + ( 𝑏 ↑ 2 ) ) = ( 𝑎 + ( 1 ↑ 2 ) ) ) |
| 31 | 30 | eqeq1d | ⊢ ( 𝑏 = 1 → ( ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ( 𝑎 + ( 1 ↑ 2 ) ) = 𝐶 ) ) |
| 32 | 31 | reubidv | ⊢ ( 𝑏 = 1 → ( ∃! 𝑎 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ∃! 𝑎 ∈ ℂ ( 𝑎 + ( 1 ↑ 2 ) ) = 𝐶 ) ) |
| 33 | oveq1 | ⊢ ( 𝑏 = - 1 → ( 𝑏 ↑ 2 ) = ( - 1 ↑ 2 ) ) | |
| 34 | 33 | oveq2d | ⊢ ( 𝑏 = - 1 → ( 𝑎 + ( 𝑏 ↑ 2 ) ) = ( 𝑎 + ( - 1 ↑ 2 ) ) ) |
| 35 | 34 | eqeq1d | ⊢ ( 𝑏 = - 1 → ( ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ( 𝑎 + ( - 1 ↑ 2 ) ) = 𝐶 ) ) |
| 36 | 35 | reubidv | ⊢ ( 𝑏 = - 1 → ( ∃! 𝑎 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ∃! 𝑎 ∈ ℂ ( 𝑎 + ( - 1 ↑ 2 ) ) = 𝐶 ) ) |
| 37 | 32 36 | 2nreu | ⊢ ( ( 1 ∈ ℂ ∧ - 1 ∈ ℂ ∧ 1 ≠ - 1 ) → ( ( ∃! 𝑎 ∈ ℂ ( 𝑎 + ( 1 ↑ 2 ) ) = 𝐶 ∧ ∃! 𝑎 ∈ ℂ ( 𝑎 + ( - 1 ↑ 2 ) ) = 𝐶 ) → ¬ ∃! 𝑏 ∈ ℂ ∃! 𝑎 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) ) |
| 38 | 6 28 37 | mpsyl | ⊢ ( 𝐶 ∈ ℂ → ¬ ∃! 𝑏 ∈ ℂ ∃! 𝑎 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) |