Proof of Theorem pythagtriplem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nncn 12275 | . . . . . 6
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) | 
| 2 |  | nncn 12275 | . . . . . 6
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) | 
| 3 |  | nncn 12275 | . . . . . 6
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) | 
| 4 |  | sqcl 14159 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℂ → (𝑚↑2) ∈
ℂ) | 
| 5 | 4 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝑚↑2) ∈
ℂ) | 
| 6 | 5 | sqcld 14185 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((𝑚↑2)↑2) ∈
ℂ) | 
| 7 |  | 2cn 12342 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ | 
| 8 |  | sqcl 14159 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → (𝑛↑2) ∈
ℂ) | 
| 9 |  | mulcl 11240 | . . . . . . . . . . . . . . 15
⊢ (((𝑚↑2) ∈ ℂ ∧
(𝑛↑2) ∈ ℂ)
→ ((𝑚↑2) ·
(𝑛↑2)) ∈
ℂ) | 
| 10 | 4, 8, 9 | syl2anr 597 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((𝑚↑2) · (𝑛↑2)) ∈
ℂ) | 
| 11 |  | mulcl 11240 | . . . . . . . . . . . . . 14
⊢ ((2
∈ ℂ ∧ ((𝑚↑2) · (𝑛↑2)) ∈ ℂ) → (2 ·
((𝑚↑2) · (𝑛↑2))) ∈
ℂ) | 
| 12 | 7, 10, 11 | sylancr 587 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (2
· ((𝑚↑2)
· (𝑛↑2)))
∈ ℂ) | 
| 13 | 6, 12 | subcld 11621 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((𝑚↑2)↑2) − (2
· ((𝑚↑2)
· (𝑛↑2))))
∈ ℂ) | 
| 14 | 8 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝑛↑2) ∈
ℂ) | 
| 15 | 14 | sqcld 14185 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((𝑛↑2)↑2) ∈
ℂ) | 
| 16 |  | mulcl 11240 | . . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑚 · 𝑛) ∈ ℂ) | 
| 17 | 16 | ancoms 458 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝑚 · 𝑛) ∈ ℂ) | 
| 18 |  | mulcl 11240 | . . . . . . . . . . . . . 14
⊢ ((2
∈ ℂ ∧ (𝑚
· 𝑛) ∈ ℂ)
→ (2 · (𝑚
· 𝑛)) ∈
ℂ) | 
| 19 | 7, 17, 18 | sylancr 587 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (2
· (𝑚 · 𝑛)) ∈
ℂ) | 
| 20 | 19 | sqcld 14185 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((2
· (𝑚 · 𝑛))↑2) ∈
ℂ) | 
| 21 | 13, 15, 20 | add32d 11490 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
(((((𝑚↑2)↑2)
− (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2)) + ((2 · (𝑚 · 𝑛))↑2)) = (((((𝑚↑2)↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))) + ((2 ·
(𝑚 · 𝑛))↑2)) + ((𝑛↑2)↑2))) | 
| 22 | 6, 12, 20 | subadd23d 11643 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
((((𝑚↑2)↑2)
− (2 · ((𝑚↑2) · (𝑛↑2)))) + ((2 · (𝑚 · 𝑛))↑2)) = (((𝑚↑2)↑2) + (((2 · (𝑚 · 𝑛))↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))))) | 
| 23 |  | sqmul 14160 | . . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℂ ∧ (𝑚
· 𝑛) ∈ ℂ)
→ ((2 · (𝑚
· 𝑛))↑2) =
((2↑2) · ((𝑚
· 𝑛)↑2))) | 
| 24 | 7, 17, 23 | sylancr 587 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((2
· (𝑚 · 𝑛))↑2) = ((2↑2)
· ((𝑚 · 𝑛)↑2))) | 
| 25 |  | sq2 14237 | . . . . . . . . . . . . . . . . . . 19
⊢
(2↑2) = 4 | 
| 26 | 25 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
(2↑2) = 4) | 
| 27 |  | sqmul 14160 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑚 · 𝑛)↑2) = ((𝑚↑2) · (𝑛↑2))) | 
| 28 | 27 | ancoms 458 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((𝑚 · 𝑛)↑2) = ((𝑚↑2) · (𝑛↑2))) | 
| 29 | 26, 28 | oveq12d 7450 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
((2↑2) · ((𝑚
· 𝑛)↑2)) = (4
· ((𝑚↑2)
· (𝑛↑2)))) | 
| 30 | 24, 29 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((2
· (𝑚 · 𝑛))↑2) = (4 · ((𝑚↑2) · (𝑛↑2)))) | 
| 31 | 30 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((2
· (𝑚 · 𝑛))↑2) − (2 ·
((𝑚↑2) · (𝑛↑2)))) = ((4 ·
((𝑚↑2) · (𝑛↑2))) − (2 ·
((𝑚↑2) · (𝑛↑2))))) | 
| 32 |  | 4cn 12352 | . . . . . . . . . . . . . . . . 17
⊢ 4 ∈
ℂ | 
| 33 |  | subdir 11698 | . . . . . . . . . . . . . . . . 17
⊢ ((4
∈ ℂ ∧ 2 ∈ ℂ ∧ ((𝑚↑2) · (𝑛↑2)) ∈ ℂ) → ((4 −
2) · ((𝑚↑2)
· (𝑛↑2))) = ((4
· ((𝑚↑2)
· (𝑛↑2)))
− (2 · ((𝑚↑2) · (𝑛↑2))))) | 
| 34 | 32, 7, 10, 33 | mp3an12i 1466 | . . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((4
− 2) · ((𝑚↑2) · (𝑛↑2))) = ((4 · ((𝑚↑2) · (𝑛↑2))) − (2 ·
((𝑚↑2) · (𝑛↑2))))) | 
| 35 |  | 2p2e4 12402 | . . . . . . . . . . . . . . . . . 18
⊢ (2 + 2) =
4 | 
| 36 | 32, 7, 7, 35 | subaddrii 11599 | . . . . . . . . . . . . . . . . 17
⊢ (4
− 2) = 2 | 
| 37 | 36 | oveq1i 7442 | . . . . . . . . . . . . . . . 16
⊢ ((4
− 2) · ((𝑚↑2) · (𝑛↑2))) = (2 · ((𝑚↑2) · (𝑛↑2))) | 
| 38 | 34, 37 | eqtr3di 2791 | . . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((4
· ((𝑚↑2)
· (𝑛↑2)))
− (2 · ((𝑚↑2) · (𝑛↑2)))) = (2 · ((𝑚↑2) · (𝑛↑2)))) | 
| 39 | 31, 38 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((2
· (𝑚 · 𝑛))↑2) − (2 ·
((𝑚↑2) · (𝑛↑2)))) = (2 ·
((𝑚↑2) · (𝑛↑2)))) | 
| 40 | 39 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((𝑚↑2)↑2) + (((2 ·
(𝑚 · 𝑛))↑2) − (2 ·
((𝑚↑2) · (𝑛↑2))))) = (((𝑚↑2)↑2) + (2 ·
((𝑚↑2) · (𝑛↑2))))) | 
| 41 | 22, 40 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
((((𝑚↑2)↑2)
− (2 · ((𝑚↑2) · (𝑛↑2)))) + ((2 · (𝑚 · 𝑛))↑2)) = (((𝑚↑2)↑2) + (2 · ((𝑚↑2) · (𝑛↑2))))) | 
| 42 | 41 | oveq1d 7447 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
(((((𝑚↑2)↑2)
− (2 · ((𝑚↑2) · (𝑛↑2)))) + ((2 · (𝑚 · 𝑛))↑2)) + ((𝑛↑2)↑2)) = ((((𝑚↑2)↑2) + (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2))) | 
| 43 | 21, 42 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
(((((𝑚↑2)↑2)
− (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2)) + ((2 · (𝑚 · 𝑛))↑2)) = ((((𝑚↑2)↑2) + (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2))) | 
| 44 |  | binom2sub 14260 | . . . . . . . . . . . 12
⊢ (((𝑚↑2) ∈ ℂ ∧
(𝑛↑2) ∈ ℂ)
→ (((𝑚↑2) −
(𝑛↑2))↑2) =
((((𝑚↑2)↑2)
− (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2))) | 
| 45 | 4, 8, 44 | syl2anr 597 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((𝑚↑2) − (𝑛↑2))↑2) = ((((𝑚↑2)↑2) − (2
· ((𝑚↑2)
· (𝑛↑2)))) +
((𝑛↑2)↑2))) | 
| 46 | 45 | oveq1d 7447 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
((((𝑚↑2) −
(𝑛↑2))↑2) + ((2
· (𝑚 · 𝑛))↑2)) = (((((𝑚↑2)↑2) − (2
· ((𝑚↑2)
· (𝑛↑2)))) +
((𝑛↑2)↑2)) + ((2
· (𝑚 · 𝑛))↑2))) | 
| 47 |  | binom2 14257 | . . . . . . . . . . 11
⊢ (((𝑚↑2) ∈ ℂ ∧
(𝑛↑2) ∈ ℂ)
→ (((𝑚↑2) +
(𝑛↑2))↑2) =
((((𝑚↑2)↑2) + (2
· ((𝑚↑2)
· (𝑛↑2)))) +
((𝑛↑2)↑2))) | 
| 48 | 4, 8, 47 | syl2anr 597 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((𝑚↑2) + (𝑛↑2))↑2) = ((((𝑚↑2)↑2) + (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2))) | 
| 49 | 43, 46, 48 | 3eqtr4d 2786 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
((((𝑚↑2) −
(𝑛↑2))↑2) + ((2
· (𝑚 · 𝑛))↑2)) = (((𝑚↑2) + (𝑛↑2))↑2)) | 
| 50 | 49 | 3adant3 1132 | . . . . . . . 8
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) →
((((𝑚↑2) −
(𝑛↑2))↑2) + ((2
· (𝑚 · 𝑛))↑2)) = (((𝑚↑2) + (𝑛↑2))↑2)) | 
| 51 | 50 | oveq2d 7448 | . . . . . . 7
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘↑2) · ((((𝑚↑2) − (𝑛↑2))↑2) + ((2 ·
(𝑚 · 𝑛))↑2))) = ((𝑘↑2) · (((𝑚↑2) + (𝑛↑2))↑2))) | 
| 52 |  | simp3 1138 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → 𝑘 ∈
ℂ) | 
| 53 | 4 | 3ad2ant2 1134 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑚↑2) ∈
ℂ) | 
| 54 | 8 | 3ad2ant1 1133 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑛↑2) ∈
ℂ) | 
| 55 | 53, 54 | subcld 11621 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑚↑2) − (𝑛↑2)) ∈
ℂ) | 
| 56 | 52, 55 | sqmuld 14199 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) = ((𝑘↑2) · (((𝑚↑2) − (𝑛↑2))↑2))) | 
| 57 | 17 | 3adant3 1132 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑚 · 𝑛) ∈ ℂ) | 
| 58 | 7, 57, 18 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2
· (𝑚 · 𝑛)) ∈
ℂ) | 
| 59 | 52, 58 | sqmuld 14199 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘 · (2 · (𝑚 · 𝑛)))↑2) = ((𝑘↑2) · ((2 · (𝑚 · 𝑛))↑2))) | 
| 60 | 56, 59 | oveq12d 7450 | . . . . . . . 8
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) = (((𝑘↑2) · (((𝑚↑2) − (𝑛↑2))↑2)) + ((𝑘↑2) · ((2 · (𝑚 · 𝑛))↑2)))) | 
| 61 |  | sqcl 14159 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℂ → (𝑘↑2) ∈
ℂ) | 
| 62 | 61 | 3ad2ant3 1135 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑘↑2) ∈
ℂ) | 
| 63 | 55 | sqcld 14185 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑚↑2) − (𝑛↑2))↑2) ∈
ℂ) | 
| 64 | 58 | sqcld 14185 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((2
· (𝑚 · 𝑛))↑2) ∈
ℂ) | 
| 65 | 62, 63, 64 | adddid 11286 | . . . . . . . 8
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘↑2) · ((((𝑚↑2) − (𝑛↑2))↑2) + ((2 ·
(𝑚 · 𝑛))↑2))) = (((𝑘↑2) · (((𝑚↑2) − (𝑛↑2))↑2)) + ((𝑘↑2) · ((2 ·
(𝑚 · 𝑛))↑2)))) | 
| 66 | 60, 65 | eqtr4d 2779 | . . . . . . 7
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) = ((𝑘↑2) · ((((𝑚↑2) − (𝑛↑2))↑2) + ((2 · (𝑚 · 𝑛))↑2)))) | 
| 67 | 53, 54 | addcld 11281 | . . . . . . . 8
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑚↑2) + (𝑛↑2)) ∈ ℂ) | 
| 68 | 52, 67 | sqmuld 14199 | . . . . . . 7
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2) = ((𝑘↑2) · (((𝑚↑2) + (𝑛↑2))↑2))) | 
| 69 | 51, 66, 68 | 3eqtr4d 2786 | . . . . . 6
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) = ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2)) | 
| 70 | 1, 2, 3, 69 | syl3an 1160 | . . . . 5
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) = ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2)) | 
| 71 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) → (𝐴↑2) = ((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2)) | 
| 72 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) → (𝐵↑2) = ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) | 
| 73 | 71, 72 | oveqan12d 7451 | . . . . . . 7
⊢ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) → ((𝐴↑2) + (𝐵↑2)) = (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2))) | 
| 74 | 73 | 3adant3 1132 | . . . . . 6
⊢ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2))) | 
| 75 |  | oveq1 7439 | . . . . . . 7
⊢ (𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))) → (𝐶↑2) = ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2)) | 
| 76 | 75 | 3ad2ant3 1135 | . . . . . 6
⊢ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → (𝐶↑2) = ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2)) | 
| 77 | 74, 76 | eqeq12d 2752 | . . . . 5
⊢ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → (((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ↔ (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) = ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2))) | 
| 78 | 70, 77 | syl5ibrcom 247 | . . . 4
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))) | 
| 79 | 78 | 3expa 1118 | . . 3
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))) | 
| 80 | 79 | rexlimdva 3154 | . 2
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) →
(∃𝑘 ∈ ℕ
(𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))) | 
| 81 | 80 | rexlimivv 3200 | 1
⊢
(∃𝑛 ∈
ℕ ∃𝑚 ∈
ℕ ∃𝑘 ∈
ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) |