Proof of Theorem pythagtriplem1
Step | Hyp | Ref
| Expression |
1 | | nncn 10905 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
2 | | nncn 10905 |
. . . . . 6
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
3 | | nncn 10905 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
4 | | sqcl 12787 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℂ → (𝑚↑2) ∈
ℂ) |
5 | 4 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝑚↑2) ∈
ℂ) |
6 | 5 | sqcld 12868 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((𝑚↑2)↑2) ∈
ℂ) |
7 | | 2cn 10968 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
8 | | sqcl 12787 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → (𝑛↑2) ∈
ℂ) |
9 | | mulcl 9899 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚↑2) ∈ ℂ ∧
(𝑛↑2) ∈ ℂ)
→ ((𝑚↑2) ·
(𝑛↑2)) ∈
ℂ) |
10 | 4, 8, 9 | syl2anr 494 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((𝑚↑2) · (𝑛↑2)) ∈
ℂ) |
11 | | mulcl 9899 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℂ ∧ ((𝑚↑2) · (𝑛↑2)) ∈ ℂ) → (2 ·
((𝑚↑2) · (𝑛↑2))) ∈
ℂ) |
12 | 7, 10, 11 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (2
· ((𝑚↑2)
· (𝑛↑2)))
∈ ℂ) |
13 | 6, 12 | subcld 10271 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((𝑚↑2)↑2) − (2
· ((𝑚↑2)
· (𝑛↑2))))
∈ ℂ) |
14 | 8 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝑛↑2) ∈
ℂ) |
15 | 14 | sqcld 12868 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((𝑛↑2)↑2) ∈
ℂ) |
16 | | mulcl 9899 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑚 · 𝑛) ∈ ℂ) |
17 | 16 | ancoms 468 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝑚 · 𝑛) ∈ ℂ) |
18 | | mulcl 9899 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℂ ∧ (𝑚
· 𝑛) ∈ ℂ)
→ (2 · (𝑚
· 𝑛)) ∈
ℂ) |
19 | 7, 17, 18 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (2
· (𝑚 · 𝑛)) ∈
ℂ) |
20 | 19 | sqcld 12868 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((2
· (𝑚 · 𝑛))↑2) ∈
ℂ) |
21 | 13, 15, 20 | add32d 10142 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
(((((𝑚↑2)↑2)
− (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2)) + ((2 · (𝑚 · 𝑛))↑2)) = (((((𝑚↑2)↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))) + ((2 ·
(𝑚 · 𝑛))↑2)) + ((𝑛↑2)↑2))) |
22 | 6, 12, 20 | subadd23d 10293 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
((((𝑚↑2)↑2)
− (2 · ((𝑚↑2) · (𝑛↑2)))) + ((2 · (𝑚 · 𝑛))↑2)) = (((𝑚↑2)↑2) + (((2 · (𝑚 · 𝑛))↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))))) |
23 | | sqmul 12788 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℂ ∧ (𝑚
· 𝑛) ∈ ℂ)
→ ((2 · (𝑚
· 𝑛))↑2) =
((2↑2) · ((𝑚
· 𝑛)↑2))) |
24 | 7, 17, 23 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((2
· (𝑚 · 𝑛))↑2) = ((2↑2)
· ((𝑚 · 𝑛)↑2))) |
25 | | sq2 12822 |
. . . . . . . . . . . . . . . . . . 19
⊢
(2↑2) = 4 |
26 | 25 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
(2↑2) = 4) |
27 | | sqmul 12788 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑚 · 𝑛)↑2) = ((𝑚↑2) · (𝑛↑2))) |
28 | 27 | ancoms 468 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((𝑚 · 𝑛)↑2) = ((𝑚↑2) · (𝑛↑2))) |
29 | 26, 28 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
((2↑2) · ((𝑚
· 𝑛)↑2)) = (4
· ((𝑚↑2)
· (𝑛↑2)))) |
30 | 24, 29 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((2
· (𝑚 · 𝑛))↑2) = (4 · ((𝑚↑2) · (𝑛↑2)))) |
31 | 30 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((2
· (𝑚 · 𝑛))↑2) − (2 ·
((𝑚↑2) · (𝑛↑2)))) = ((4 ·
((𝑚↑2) · (𝑛↑2))) − (2 ·
((𝑚↑2) · (𝑛↑2))))) |
32 | | 4cn 10975 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℂ |
33 | | 2p2e4 11021 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 + 2) =
4 |
34 | 32, 7, 7, 33 | subaddrii 10249 |
. . . . . . . . . . . . . . . . 17
⊢ (4
− 2) = 2 |
35 | 34 | oveq1i 6559 |
. . . . . . . . . . . . . . . 16
⊢ ((4
− 2) · ((𝑚↑2) · (𝑛↑2))) = (2 · ((𝑚↑2) · (𝑛↑2))) |
36 | | subdir 10343 |
. . . . . . . . . . . . . . . . . 18
⊢ ((4
∈ ℂ ∧ 2 ∈ ℂ ∧ ((𝑚↑2) · (𝑛↑2)) ∈ ℂ) → ((4 −
2) · ((𝑚↑2)
· (𝑛↑2))) = ((4
· ((𝑚↑2)
· (𝑛↑2)))
− (2 · ((𝑚↑2) · (𝑛↑2))))) |
37 | 32, 7, 36 | mp3an12 1406 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑚↑2) · (𝑛↑2)) ∈ ℂ →
((4 − 2) · ((𝑚↑2) · (𝑛↑2))) = ((4 · ((𝑚↑2) · (𝑛↑2))) − (2 ·
((𝑚↑2) · (𝑛↑2))))) |
38 | 10, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((4
− 2) · ((𝑚↑2) · (𝑛↑2))) = ((4 · ((𝑚↑2) · (𝑛↑2))) − (2 ·
((𝑚↑2) · (𝑛↑2))))) |
39 | 35, 38 | syl5reqr 2659 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((4
· ((𝑚↑2)
· (𝑛↑2)))
− (2 · ((𝑚↑2) · (𝑛↑2)))) = (2 · ((𝑚↑2) · (𝑛↑2)))) |
40 | 31, 39 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((2
· (𝑚 · 𝑛))↑2) − (2 ·
((𝑚↑2) · (𝑛↑2)))) = (2 ·
((𝑚↑2) · (𝑛↑2)))) |
41 | 40 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((𝑚↑2)↑2) + (((2 ·
(𝑚 · 𝑛))↑2) − (2 ·
((𝑚↑2) · (𝑛↑2))))) = (((𝑚↑2)↑2) + (2 ·
((𝑚↑2) · (𝑛↑2))))) |
42 | 22, 41 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
((((𝑚↑2)↑2)
− (2 · ((𝑚↑2) · (𝑛↑2)))) + ((2 · (𝑚 · 𝑛))↑2)) = (((𝑚↑2)↑2) + (2 · ((𝑚↑2) · (𝑛↑2))))) |
43 | 42 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
(((((𝑚↑2)↑2)
− (2 · ((𝑚↑2) · (𝑛↑2)))) + ((2 · (𝑚 · 𝑛))↑2)) + ((𝑛↑2)↑2)) = ((((𝑚↑2)↑2) + (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2))) |
44 | 21, 43 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
(((((𝑚↑2)↑2)
− (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2)) + ((2 · (𝑚 · 𝑛))↑2)) = ((((𝑚↑2)↑2) + (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2))) |
45 | | binom2sub 12843 |
. . . . . . . . . . . 12
⊢ (((𝑚↑2) ∈ ℂ ∧
(𝑛↑2) ∈ ℂ)
→ (((𝑚↑2) −
(𝑛↑2))↑2) =
((((𝑚↑2)↑2)
− (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2))) |
46 | 4, 8, 45 | syl2anr 494 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((𝑚↑2) − (𝑛↑2))↑2) = ((((𝑚↑2)↑2) − (2
· ((𝑚↑2)
· (𝑛↑2)))) +
((𝑛↑2)↑2))) |
47 | 46 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
((((𝑚↑2) −
(𝑛↑2))↑2) + ((2
· (𝑚 · 𝑛))↑2)) = (((((𝑚↑2)↑2) − (2
· ((𝑚↑2)
· (𝑛↑2)))) +
((𝑛↑2)↑2)) + ((2
· (𝑚 · 𝑛))↑2))) |
48 | | binom2 12841 |
. . . . . . . . . . 11
⊢ (((𝑚↑2) ∈ ℂ ∧
(𝑛↑2) ∈ ℂ)
→ (((𝑚↑2) +
(𝑛↑2))↑2) =
((((𝑚↑2)↑2) + (2
· ((𝑚↑2)
· (𝑛↑2)))) +
((𝑛↑2)↑2))) |
49 | 4, 8, 48 | syl2anr 494 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((𝑚↑2) + (𝑛↑2))↑2) = ((((𝑚↑2)↑2) + (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2))) |
50 | 44, 47, 49 | 3eqtr4d 2654 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) →
((((𝑚↑2) −
(𝑛↑2))↑2) + ((2
· (𝑚 · 𝑛))↑2)) = (((𝑚↑2) + (𝑛↑2))↑2)) |
51 | 50 | 3adant3 1074 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) →
((((𝑚↑2) −
(𝑛↑2))↑2) + ((2
· (𝑚 · 𝑛))↑2)) = (((𝑚↑2) + (𝑛↑2))↑2)) |
52 | 51 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘↑2) · ((((𝑚↑2) − (𝑛↑2))↑2) + ((2 ·
(𝑚 · 𝑛))↑2))) = ((𝑘↑2) · (((𝑚↑2) + (𝑛↑2))↑2))) |
53 | | simp3 1056 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → 𝑘 ∈
ℂ) |
54 | 4 | 3ad2ant2 1076 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑚↑2) ∈
ℂ) |
55 | 8 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑛↑2) ∈
ℂ) |
56 | 54, 55 | subcld 10271 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑚↑2) − (𝑛↑2)) ∈
ℂ) |
57 | 53, 56 | sqmuld 12882 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) = ((𝑘↑2) · (((𝑚↑2) − (𝑛↑2))↑2))) |
58 | 17 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑚 · 𝑛) ∈ ℂ) |
59 | 7, 58, 18 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2
· (𝑚 · 𝑛)) ∈
ℂ) |
60 | 53, 59 | sqmuld 12882 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘 · (2 · (𝑚 · 𝑛)))↑2) = ((𝑘↑2) · ((2 · (𝑚 · 𝑛))↑2))) |
61 | 57, 60 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) = (((𝑘↑2) · (((𝑚↑2) − (𝑛↑2))↑2)) + ((𝑘↑2) · ((2 · (𝑚 · 𝑛))↑2)))) |
62 | | sqcl 12787 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℂ → (𝑘↑2) ∈
ℂ) |
63 | 62 | 3ad2ant3 1077 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑘↑2) ∈
ℂ) |
64 | 56 | sqcld 12868 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑚↑2) − (𝑛↑2))↑2) ∈
ℂ) |
65 | 59 | sqcld 12868 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((2
· (𝑚 · 𝑛))↑2) ∈
ℂ) |
66 | 63, 64, 65 | adddid 9943 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘↑2) · ((((𝑚↑2) − (𝑛↑2))↑2) + ((2 ·
(𝑚 · 𝑛))↑2))) = (((𝑘↑2) · (((𝑚↑2) − (𝑛↑2))↑2)) + ((𝑘↑2) · ((2 ·
(𝑚 · 𝑛))↑2)))) |
67 | 61, 66 | eqtr4d 2647 |
. . . . . . 7
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) = ((𝑘↑2) · ((((𝑚↑2) − (𝑛↑2))↑2) + ((2 · (𝑚 · 𝑛))↑2)))) |
68 | 54, 55 | addcld 9938 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑚↑2) + (𝑛↑2)) ∈ ℂ) |
69 | 53, 68 | sqmuld 12882 |
. . . . . . 7
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2) = ((𝑘↑2) · (((𝑚↑2) + (𝑛↑2))↑2))) |
70 | 52, 67, 69 | 3eqtr4d 2654 |
. . . . . 6
⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) = ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2)) |
71 | 1, 2, 3, 70 | syl3an 1360 |
. . . . 5
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) = ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2)) |
72 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) → (𝐴↑2) = ((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2)) |
73 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) → (𝐵↑2) = ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) |
74 | 72, 73 | oveqan12d 6568 |
. . . . . . 7
⊢ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) → ((𝐴↑2) + (𝐵↑2)) = (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2))) |
75 | 74 | 3adant3 1074 |
. . . . . 6
⊢ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2))) |
76 | | oveq1 6556 |
. . . . . . 7
⊢ (𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))) → (𝐶↑2) = ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2)) |
77 | 76 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → (𝐶↑2) = ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2)) |
78 | 75, 77 | eqeq12d 2625 |
. . . . 5
⊢ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → (((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ↔ (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) = ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2))) |
79 | 71, 78 | syl5ibrcom 236 |
. . . 4
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))) |
80 | 79 | 3expa 1257 |
. . 3
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))) |
81 | 80 | rexlimdva 3013 |
. 2
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) →
(∃𝑘 ∈ ℕ
(𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))) |
82 | 81 | rexlimivv 3018 |
1
⊢
(∃𝑛 ∈
ℕ ∃𝑚 ∈
ℕ ∃𝑘 ∈
ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) |