Proof of Theorem nn0opth2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq1 7438 | . . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℕ0, 𝐴, 0) → (𝐴 + 𝐵) = (if(𝐴 ∈ ℕ0, 𝐴, 0) + 𝐵)) | 
| 2 | 1 | oveq1d 7446 | . . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℕ0, 𝐴, 0) → ((𝐴 + 𝐵)↑2) = ((if(𝐴 ∈ ℕ0, 𝐴, 0) + 𝐵)↑2)) | 
| 3 | 2 | oveq1d 7446 | . . . 4
⊢ (𝐴 = if(𝐴 ∈ ℕ0, 𝐴, 0) → (((𝐴 + 𝐵)↑2) + 𝐵) = (((if(𝐴 ∈ ℕ0, 𝐴, 0) + 𝐵)↑2) + 𝐵)) | 
| 4 | 3 | eqeq1d 2739 | . . 3
⊢ (𝐴 = if(𝐴 ∈ ℕ0, 𝐴, 0) → ((((𝐴 + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (((if(𝐴 ∈ ℕ0, 𝐴, 0) + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷))) | 
| 5 |  | eqeq1 2741 | . . . 4
⊢ (𝐴 = if(𝐴 ∈ ℕ0, 𝐴, 0) → (𝐴 = 𝐶 ↔ if(𝐴 ∈ ℕ0, 𝐴, 0) = 𝐶)) | 
| 6 | 5 | anbi1d 631 | . . 3
⊢ (𝐴 = if(𝐴 ∈ ℕ0, 𝐴, 0) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ↔ (if(𝐴 ∈ ℕ0, 𝐴, 0) = 𝐶 ∧ 𝐵 = 𝐷))) | 
| 7 | 4, 6 | bibi12d 345 | . 2
⊢ (𝐴 = if(𝐴 ∈ ℕ0, 𝐴, 0) → (((((𝐴 + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) ↔ ((((if(𝐴 ∈ ℕ0, 𝐴, 0) + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (if(𝐴 ∈ ℕ0, 𝐴, 0) = 𝐶 ∧ 𝐵 = 𝐷)))) | 
| 8 |  | oveq2 7439 | . . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℕ0, 𝐵, 0) → (if(𝐴 ∈ ℕ0,
𝐴, 0) + 𝐵) = (if(𝐴 ∈ ℕ0, 𝐴, 0) + if(𝐵 ∈ ℕ0, 𝐵, 0))) | 
| 9 | 8 | oveq1d 7446 | . . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℕ0, 𝐵, 0) → ((if(𝐴 ∈ ℕ0,
𝐴, 0) + 𝐵)↑2) = ((if(𝐴 ∈ ℕ0, 𝐴, 0) + if(𝐵 ∈ ℕ0, 𝐵, 0))↑2)) | 
| 10 |  | id 22 | . . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℕ0, 𝐵, 0) → 𝐵 = if(𝐵 ∈ ℕ0, 𝐵, 0)) | 
| 11 | 9, 10 | oveq12d 7449 | . . . 4
⊢ (𝐵 = if(𝐵 ∈ ℕ0, 𝐵, 0) → (((if(𝐴 ∈ ℕ0,
𝐴, 0) + 𝐵)↑2) + 𝐵) = (((if(𝐴 ∈ ℕ0, 𝐴, 0) + if(𝐵 ∈ ℕ0, 𝐵, 0))↑2) + if(𝐵 ∈ ℕ0,
𝐵, 0))) | 
| 12 | 11 | eqeq1d 2739 | . . 3
⊢ (𝐵 = if(𝐵 ∈ ℕ0, 𝐵, 0) → ((((if(𝐴 ∈ ℕ0,
𝐴, 0) + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (((if(𝐴 ∈ ℕ0, 𝐴, 0) + if(𝐵 ∈ ℕ0, 𝐵, 0))↑2) + if(𝐵 ∈ ℕ0,
𝐵, 0)) = (((𝐶 + 𝐷)↑2) + 𝐷))) | 
| 13 |  | eqeq1 2741 | . . . 4
⊢ (𝐵 = if(𝐵 ∈ ℕ0, 𝐵, 0) → (𝐵 = 𝐷 ↔ if(𝐵 ∈ ℕ0, 𝐵, 0) = 𝐷)) | 
| 14 | 13 | anbi2d 630 | . . 3
⊢ (𝐵 = if(𝐵 ∈ ℕ0, 𝐵, 0) → ((if(𝐴 ∈ ℕ0,
𝐴, 0) = 𝐶 ∧ 𝐵 = 𝐷) ↔ (if(𝐴 ∈ ℕ0, 𝐴, 0) = 𝐶 ∧ if(𝐵 ∈ ℕ0, 𝐵, 0) = 𝐷))) | 
| 15 | 12, 14 | bibi12d 345 | . 2
⊢ (𝐵 = if(𝐵 ∈ ℕ0, 𝐵, 0) → (((((if(𝐴 ∈ ℕ0,
𝐴, 0) + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (if(𝐴 ∈ ℕ0, 𝐴, 0) = 𝐶 ∧ 𝐵 = 𝐷)) ↔ ((((if(𝐴 ∈ ℕ0, 𝐴, 0) + if(𝐵 ∈ ℕ0, 𝐵, 0))↑2) + if(𝐵 ∈ ℕ0,
𝐵, 0)) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (if(𝐴 ∈ ℕ0, 𝐴, 0) = 𝐶 ∧ if(𝐵 ∈ ℕ0, 𝐵, 0) = 𝐷)))) | 
| 16 |  | oveq1 7438 | . . . . . 6
⊢ (𝐶 = if(𝐶 ∈ ℕ0, 𝐶, 0) → (𝐶 + 𝐷) = (if(𝐶 ∈ ℕ0, 𝐶, 0) + 𝐷)) | 
| 17 | 16 | oveq1d 7446 | . . . . 5
⊢ (𝐶 = if(𝐶 ∈ ℕ0, 𝐶, 0) → ((𝐶 + 𝐷)↑2) = ((if(𝐶 ∈ ℕ0, 𝐶, 0) + 𝐷)↑2)) | 
| 18 | 17 | oveq1d 7446 | . . . 4
⊢ (𝐶 = if(𝐶 ∈ ℕ0, 𝐶, 0) → (((𝐶 + 𝐷)↑2) + 𝐷) = (((if(𝐶 ∈ ℕ0, 𝐶, 0) + 𝐷)↑2) + 𝐷)) | 
| 19 | 18 | eqeq2d 2748 | . . 3
⊢ (𝐶 = if(𝐶 ∈ ℕ0, 𝐶, 0) → ((((if(𝐴 ∈ ℕ0,
𝐴, 0) + if(𝐵 ∈ ℕ0,
𝐵, 0))↑2) + if(𝐵 ∈ ℕ0,
𝐵, 0)) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (((if(𝐴 ∈ ℕ0, 𝐴, 0) + if(𝐵 ∈ ℕ0, 𝐵, 0))↑2) + if(𝐵 ∈ ℕ0,
𝐵, 0)) = (((if(𝐶 ∈ ℕ0,
𝐶, 0) + 𝐷)↑2) + 𝐷))) | 
| 20 |  | eqeq2 2749 | . . . 4
⊢ (𝐶 = if(𝐶 ∈ ℕ0, 𝐶, 0) → (if(𝐴 ∈ ℕ0,
𝐴, 0) = 𝐶 ↔ if(𝐴 ∈ ℕ0, 𝐴, 0) = if(𝐶 ∈ ℕ0, 𝐶, 0))) | 
| 21 | 20 | anbi1d 631 | . . 3
⊢ (𝐶 = if(𝐶 ∈ ℕ0, 𝐶, 0) → ((if(𝐴 ∈ ℕ0,
𝐴, 0) = 𝐶 ∧ if(𝐵 ∈ ℕ0, 𝐵, 0) = 𝐷) ↔ (if(𝐴 ∈ ℕ0, 𝐴, 0) = if(𝐶 ∈ ℕ0, 𝐶, 0) ∧ if(𝐵 ∈ ℕ0, 𝐵, 0) = 𝐷))) | 
| 22 | 19, 21 | bibi12d 345 | . 2
⊢ (𝐶 = if(𝐶 ∈ ℕ0, 𝐶, 0) → (((((if(𝐴 ∈ ℕ0,
𝐴, 0) + if(𝐵 ∈ ℕ0,
𝐵, 0))↑2) + if(𝐵 ∈ ℕ0,
𝐵, 0)) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (if(𝐴 ∈ ℕ0, 𝐴, 0) = 𝐶 ∧ if(𝐵 ∈ ℕ0, 𝐵, 0) = 𝐷)) ↔ ((((if(𝐴 ∈ ℕ0, 𝐴, 0) + if(𝐵 ∈ ℕ0, 𝐵, 0))↑2) + if(𝐵 ∈ ℕ0,
𝐵, 0)) = (((if(𝐶 ∈ ℕ0,
𝐶, 0) + 𝐷)↑2) + 𝐷) ↔ (if(𝐴 ∈ ℕ0, 𝐴, 0) = if(𝐶 ∈ ℕ0, 𝐶, 0) ∧ if(𝐵 ∈ ℕ0, 𝐵, 0) = 𝐷)))) | 
| 23 |  | oveq2 7439 | . . . . . 6
⊢ (𝐷 = if(𝐷 ∈ ℕ0, 𝐷, 0) → (if(𝐶 ∈ ℕ0,
𝐶, 0) + 𝐷) = (if(𝐶 ∈ ℕ0, 𝐶, 0) + if(𝐷 ∈ ℕ0, 𝐷, 0))) | 
| 24 | 23 | oveq1d 7446 | . . . . 5
⊢ (𝐷 = if(𝐷 ∈ ℕ0, 𝐷, 0) → ((if(𝐶 ∈ ℕ0,
𝐶, 0) + 𝐷)↑2) = ((if(𝐶 ∈ ℕ0, 𝐶, 0) + if(𝐷 ∈ ℕ0, 𝐷, 0))↑2)) | 
| 25 |  | id 22 | . . . . 5
⊢ (𝐷 = if(𝐷 ∈ ℕ0, 𝐷, 0) → 𝐷 = if(𝐷 ∈ ℕ0, 𝐷, 0)) | 
| 26 | 24, 25 | oveq12d 7449 | . . . 4
⊢ (𝐷 = if(𝐷 ∈ ℕ0, 𝐷, 0) → (((if(𝐶 ∈ ℕ0,
𝐶, 0) + 𝐷)↑2) + 𝐷) = (((if(𝐶 ∈ ℕ0, 𝐶, 0) + if(𝐷 ∈ ℕ0, 𝐷, 0))↑2) + if(𝐷 ∈ ℕ0,
𝐷, 0))) | 
| 27 | 26 | eqeq2d 2748 | . . 3
⊢ (𝐷 = if(𝐷 ∈ ℕ0, 𝐷, 0) → ((((if(𝐴 ∈ ℕ0,
𝐴, 0) + if(𝐵 ∈ ℕ0,
𝐵, 0))↑2) + if(𝐵 ∈ ℕ0,
𝐵, 0)) = (((if(𝐶 ∈ ℕ0,
𝐶, 0) + 𝐷)↑2) + 𝐷) ↔ (((if(𝐴 ∈ ℕ0, 𝐴, 0) + if(𝐵 ∈ ℕ0, 𝐵, 0))↑2) + if(𝐵 ∈ ℕ0,
𝐵, 0)) = (((if(𝐶 ∈ ℕ0,
𝐶, 0) + if(𝐷 ∈ ℕ0,
𝐷, 0))↑2) + if(𝐷 ∈ ℕ0,
𝐷, 0)))) | 
| 28 |  | eqeq2 2749 | . . . 4
⊢ (𝐷 = if(𝐷 ∈ ℕ0, 𝐷, 0) → (if(𝐵 ∈ ℕ0,
𝐵, 0) = 𝐷 ↔ if(𝐵 ∈ ℕ0, 𝐵, 0) = if(𝐷 ∈ ℕ0, 𝐷, 0))) | 
| 29 | 28 | anbi2d 630 | . . 3
⊢ (𝐷 = if(𝐷 ∈ ℕ0, 𝐷, 0) → ((if(𝐴 ∈ ℕ0,
𝐴, 0) = if(𝐶 ∈ ℕ0,
𝐶, 0) ∧ if(𝐵 ∈ ℕ0,
𝐵, 0) = 𝐷) ↔ (if(𝐴 ∈ ℕ0, 𝐴, 0) = if(𝐶 ∈ ℕ0, 𝐶, 0) ∧ if(𝐵 ∈ ℕ0, 𝐵, 0) = if(𝐷 ∈ ℕ0, 𝐷, 0)))) | 
| 30 | 27, 29 | bibi12d 345 | . 2
⊢ (𝐷 = if(𝐷 ∈ ℕ0, 𝐷, 0) → (((((if(𝐴 ∈ ℕ0,
𝐴, 0) + if(𝐵 ∈ ℕ0,
𝐵, 0))↑2) + if(𝐵 ∈ ℕ0,
𝐵, 0)) = (((if(𝐶 ∈ ℕ0,
𝐶, 0) + 𝐷)↑2) + 𝐷) ↔ (if(𝐴 ∈ ℕ0, 𝐴, 0) = if(𝐶 ∈ ℕ0, 𝐶, 0) ∧ if(𝐵 ∈ ℕ0, 𝐵, 0) = 𝐷)) ↔ ((((if(𝐴 ∈ ℕ0, 𝐴, 0) + if(𝐵 ∈ ℕ0, 𝐵, 0))↑2) + if(𝐵 ∈ ℕ0,
𝐵, 0)) = (((if(𝐶 ∈ ℕ0,
𝐶, 0) + if(𝐷 ∈ ℕ0,
𝐷, 0))↑2) + if(𝐷 ∈ ℕ0,
𝐷, 0)) ↔ (if(𝐴 ∈ ℕ0,
𝐴, 0) = if(𝐶 ∈ ℕ0,
𝐶, 0) ∧ if(𝐵 ∈ ℕ0,
𝐵, 0) = if(𝐷 ∈ ℕ0,
𝐷, 0))))) | 
| 31 |  | 0nn0 12541 | . . . 4
⊢ 0 ∈
ℕ0 | 
| 32 | 31 | elimel 4595 | . . 3
⊢ if(𝐴 ∈ ℕ0,
𝐴, 0) ∈
ℕ0 | 
| 33 | 31 | elimel 4595 | . . 3
⊢ if(𝐵 ∈ ℕ0,
𝐵, 0) ∈
ℕ0 | 
| 34 | 31 | elimel 4595 | . . 3
⊢ if(𝐶 ∈ ℕ0,
𝐶, 0) ∈
ℕ0 | 
| 35 | 31 | elimel 4595 | . . 3
⊢ if(𝐷 ∈ ℕ0,
𝐷, 0) ∈
ℕ0 | 
| 36 | 32, 33, 34, 35 | nn0opth2i 14310 | . 2
⊢
((((if(𝐴 ∈
ℕ0, 𝐴, 0)
+ if(𝐵 ∈
ℕ0, 𝐵,
0))↑2) + if(𝐵 ∈
ℕ0, 𝐵, 0))
= (((if(𝐶 ∈
ℕ0, 𝐶, 0)
+ if(𝐷 ∈
ℕ0, 𝐷,
0))↑2) + if(𝐷 ∈
ℕ0, 𝐷, 0))
↔ (if(𝐴 ∈
ℕ0, 𝐴, 0)
= if(𝐶 ∈
ℕ0, 𝐶, 0)
∧ if(𝐵 ∈
ℕ0, 𝐵, 0)
= if(𝐷 ∈
ℕ0, 𝐷,
0))) | 
| 37 | 7, 15, 22, 30, 36 | dedth4h 4587 | 1
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈
ℕ0) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0))
→ ((((𝐴 + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |