# Metamath Proof Explorer

## Theorem pythagtriplem14

Description: Lemma for pythagtrip . Calculate the square of N . (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypothesis pythagtriplem13.1 ${⊢}{N}=\frac{\sqrt{{C}+{B}}-\sqrt{{C}-{B}}}{2}$
Assertion pythagtriplem14 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {{N}}^{2}=\frac{{C}-{A}}{2}$

### Proof

Step Hyp Ref Expression
1 pythagtriplem13.1 ${⊢}{N}=\frac{\sqrt{{C}+{B}}-\sqrt{{C}-{B}}}{2}$
2 1 oveq1i ${⊢}{{N}}^{2}={\left(\frac{\sqrt{{C}+{B}}-\sqrt{{C}-{B}}}{2}\right)}^{2}$
3 nncn ${⊢}{C}\in ℕ\to {C}\in ℂ$
4 nncn ${⊢}{B}\in ℕ\to {B}\in ℂ$
5 addcl ${⊢}\left({C}\in ℂ\wedge {B}\in ℂ\right)\to {C}+{B}\in ℂ$
6 3 4 5 syl2anr ${⊢}\left({B}\in ℕ\wedge {C}\in ℕ\right)\to {C}+{B}\in ℂ$
7 6 sqrtcld ${⊢}\left({B}\in ℕ\wedge {C}\in ℕ\right)\to \sqrt{{C}+{B}}\in ℂ$
8 subcl ${⊢}\left({C}\in ℂ\wedge {B}\in ℂ\right)\to {C}-{B}\in ℂ$
9 3 4 8 syl2anr ${⊢}\left({B}\in ℕ\wedge {C}\in ℕ\right)\to {C}-{B}\in ℂ$
10 9 sqrtcld ${⊢}\left({B}\in ℕ\wedge {C}\in ℕ\right)\to \sqrt{{C}-{B}}\in ℂ$
11 7 10 subcld ${⊢}\left({B}\in ℕ\wedge {C}\in ℕ\right)\to \sqrt{{C}+{B}}-\sqrt{{C}-{B}}\in ℂ$
12 11 3adant1 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to \sqrt{{C}+{B}}-\sqrt{{C}-{B}}\in ℂ$
13 12 3ad2ant1 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \sqrt{{C}+{B}}-\sqrt{{C}-{B}}\in ℂ$
14 2cn ${⊢}2\in ℂ$
15 2ne0 ${⊢}2\ne 0$
16 sqdiv ${⊢}\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to {\left(\frac{\sqrt{{C}+{B}}-\sqrt{{C}-{B}}}{2}\right)}^{2}=\frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{{2}^{2}}$
17 14 15 16 mp3an23 ${⊢}\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\in ℂ\to {\left(\frac{\sqrt{{C}+{B}}-\sqrt{{C}-{B}}}{2}\right)}^{2}=\frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{{2}^{2}}$
18 13 17 syl ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {\left(\frac{\sqrt{{C}+{B}}-\sqrt{{C}-{B}}}{2}\right)}^{2}=\frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{{2}^{2}}$
19 14 sqvali ${⊢}{2}^{2}=2\cdot 2$
20 19 oveq2i ${⊢}\frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{{2}^{2}}=\frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{2\cdot 2}$
21 13 sqcld ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}\in ℂ$
22 2cnne0 ${⊢}\left(2\in ℂ\wedge 2\ne 0\right)$
23 divdiv1 ${⊢}\left({\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{\frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{2}}{2}=\frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{2\cdot 2}$
24 22 22 23 mp3an23 ${⊢}{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}\in ℂ\to \frac{\frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{2}}{2}=\frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{2\cdot 2}$
25 21 24 syl ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \frac{\frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{2}}{2}=\frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{2\cdot 2}$
26 simp12 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {B}\in ℕ$
27 simp13 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {C}\in ℕ$
28 26 27 7 syl2anc ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \sqrt{{C}+{B}}\in ℂ$
29 26 27 10 syl2anc ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \sqrt{{C}-{B}}\in ℂ$
30 binom2sub ${⊢}\left(\sqrt{{C}+{B}}\in ℂ\wedge \sqrt{{C}-{B}}\in ℂ\right)\to {\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}={\sqrt{{C}+{B}}}^{2}-2\sqrt{{C}+{B}}\sqrt{{C}-{B}}+{\sqrt{{C}-{B}}}^{2}$
31 28 29 30 syl2anc ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}={\sqrt{{C}+{B}}}^{2}-2\sqrt{{C}+{B}}\sqrt{{C}-{B}}+{\sqrt{{C}-{B}}}^{2}$
32 nnre ${⊢}{C}\in ℕ\to {C}\in ℝ$
33 nnre ${⊢}{B}\in ℕ\to {B}\in ℝ$
34 readdcl ${⊢}\left({C}\in ℝ\wedge {B}\in ℝ\right)\to {C}+{B}\in ℝ$
35 32 33 34 syl2anr ${⊢}\left({B}\in ℕ\wedge {C}\in ℕ\right)\to {C}+{B}\in ℝ$
36 35 3adant1 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to {C}+{B}\in ℝ$
37 36 3ad2ant1 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {C}+{B}\in ℝ$
38 37 recnd ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {C}+{B}\in ℂ$
39 resubcl ${⊢}\left({C}\in ℝ\wedge {B}\in ℝ\right)\to {C}-{B}\in ℝ$
40 32 33 39 syl2anr ${⊢}\left({B}\in ℕ\wedge {C}\in ℕ\right)\to {C}-{B}\in ℝ$
41 40 3adant1 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to {C}-{B}\in ℝ$
42 41 3ad2ant1 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {C}-{B}\in ℝ$
43 42 recnd ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {C}-{B}\in ℂ$
44 7 3adant1 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to \sqrt{{C}+{B}}\in ℂ$
45 10 3adant1 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to \sqrt{{C}-{B}}\in ℂ$
46 44 45 mulcld ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to \sqrt{{C}+{B}}\sqrt{{C}-{B}}\in ℂ$
47 mulcl ${⊢}\left(2\in ℂ\wedge \sqrt{{C}+{B}}\sqrt{{C}-{B}}\in ℂ\right)\to 2\sqrt{{C}+{B}}\sqrt{{C}-{B}}\in ℂ$
48 14 46 47 sylancr ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to 2\sqrt{{C}+{B}}\sqrt{{C}-{B}}\in ℂ$
49 48 3ad2ant1 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to 2\sqrt{{C}+{B}}\sqrt{{C}-{B}}\in ℂ$
50 38 43 49 addsubd ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \left({C}+{B}\right)+\left({C}-{B}\right)-2\sqrt{{C}+{B}}\sqrt{{C}-{B}}=\left({C}+{B}-2\sqrt{{C}+{B}}\sqrt{{C}-{B}}\right)+{C}-{B}$
51 27 nncnd ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {C}\in ℂ$
52 simp11 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {A}\in ℕ$
53 52 nncnd ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {A}\in ℂ$
54 subdi ${⊢}\left(2\in ℂ\wedge {C}\in ℂ\wedge {A}\in ℂ\right)\to 2\left({C}-{A}\right)=2{C}-2{A}$
55 14 51 53 54 mp3an2i ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to 2\left({C}-{A}\right)=2{C}-2{A}$
56 ppncan ${⊢}\left({C}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {C}+{B}+\left({C}-{B}\right)={C}+{C}$
57 56 3anidm13 ${⊢}\left({C}\in ℂ\wedge {B}\in ℂ\right)\to {C}+{B}+\left({C}-{B}\right)={C}+{C}$
58 2times ${⊢}{C}\in ℂ\to 2{C}={C}+{C}$
59 58 adantr ${⊢}\left({C}\in ℂ\wedge {B}\in ℂ\right)\to 2{C}={C}+{C}$
60 57 59 eqtr4d ${⊢}\left({C}\in ℂ\wedge {B}\in ℂ\right)\to {C}+{B}+\left({C}-{B}\right)=2{C}$
61 3 4 60 syl2anr ${⊢}\left({B}\in ℕ\wedge {C}\in ℕ\right)\to {C}+{B}+\left({C}-{B}\right)=2{C}$
62 61 3adant1 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to {C}+{B}+\left({C}-{B}\right)=2{C}$
63 62 3ad2ant1 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {C}+{B}+\left({C}-{B}\right)=2{C}$
64 26 nncnd ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {B}\in ℂ$
65 subsq ${⊢}\left({C}\in ℂ\wedge {B}\in ℂ\right)\to {{C}}^{2}-{{B}}^{2}=\left({C}+{B}\right)\left({C}-{B}\right)$
66 51 64 65 syl2anc ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {{C}}^{2}-{{B}}^{2}=\left({C}+{B}\right)\left({C}-{B}\right)$
67 oveq1 ${⊢}{{A}}^{2}+{{B}}^{2}={{C}}^{2}\to {{A}}^{2}+{{B}}^{2}-{{B}}^{2}={{C}}^{2}-{{B}}^{2}$
68 67 3ad2ant2 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {{A}}^{2}+{{B}}^{2}-{{B}}^{2}={{C}}^{2}-{{B}}^{2}$
69 nncn ${⊢}{A}\in ℕ\to {A}\in ℂ$
70 69 sqcld ${⊢}{A}\in ℕ\to {{A}}^{2}\in ℂ$
71 70 3ad2ant1 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to {{A}}^{2}\in ℂ$
72 4 sqcld ${⊢}{B}\in ℕ\to {{B}}^{2}\in ℂ$
73 72 3ad2ant2 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to {{B}}^{2}\in ℂ$
74 71 73 pncand ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to {{A}}^{2}+{{B}}^{2}-{{B}}^{2}={{A}}^{2}$
75 74 3ad2ant1 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {{A}}^{2}+{{B}}^{2}-{{B}}^{2}={{A}}^{2}$
76 68 75 eqtr3d ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {{C}}^{2}-{{B}}^{2}={{A}}^{2}$
77 66 76 eqtr3d ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \left({C}+{B}\right)\left({C}-{B}\right)={{A}}^{2}$
78 77 fveq2d ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \sqrt{\left({C}+{B}\right)\left({C}-{B}\right)}=\sqrt{{{A}}^{2}}$
79 32 adantl ${⊢}\left({B}\in ℕ\wedge {C}\in ℕ\right)\to {C}\in ℝ$
80 33 adantr ${⊢}\left({B}\in ℕ\wedge {C}\in ℕ\right)\to {B}\in ℝ$
81 nngt0 ${⊢}{C}\in ℕ\to 0<{C}$
82 81 adantl ${⊢}\left({B}\in ℕ\wedge {C}\in ℕ\right)\to 0<{C}$
83 nngt0 ${⊢}{B}\in ℕ\to 0<{B}$
84 83 adantr ${⊢}\left({B}\in ℕ\wedge {C}\in ℕ\right)\to 0<{B}$
85 79 80 82 84 addgt0d ${⊢}\left({B}\in ℕ\wedge {C}\in ℕ\right)\to 0<{C}+{B}$
86 0re ${⊢}0\in ℝ$
87 ltle ${⊢}\left(0\in ℝ\wedge {C}+{B}\in ℝ\right)\to \left(0<{C}+{B}\to 0\le {C}+{B}\right)$
88 86 87 mpan ${⊢}{C}+{B}\in ℝ\to \left(0<{C}+{B}\to 0\le {C}+{B}\right)$
89 35 85 88 sylc ${⊢}\left({B}\in ℕ\wedge {C}\in ℕ\right)\to 0\le {C}+{B}$
90 89 3adant1 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to 0\le {C}+{B}$
91 90 3ad2ant1 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to 0\le {C}+{B}$
92 pythagtriplem10 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\right)\to 0<{C}-{B}$
93 92 3adant3 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to 0<{C}-{B}$
94 ltle ${⊢}\left(0\in ℝ\wedge {C}-{B}\in ℝ\right)\to \left(0<{C}-{B}\to 0\le {C}-{B}\right)$
95 86 94 mpan ${⊢}{C}-{B}\in ℝ\to \left(0<{C}-{B}\to 0\le {C}-{B}\right)$
96 42 93 95 sylc ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to 0\le {C}-{B}$
97 37 91 42 96 sqrtmuld ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \sqrt{\left({C}+{B}\right)\left({C}-{B}\right)}=\sqrt{{C}+{B}}\sqrt{{C}-{B}}$
98 78 97 eqtr3d ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \sqrt{{{A}}^{2}}=\sqrt{{C}+{B}}\sqrt{{C}-{B}}$
99 nnre ${⊢}{A}\in ℕ\to {A}\in ℝ$
100 99 3ad2ant1 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to {A}\in ℝ$
101 100 3ad2ant1 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {A}\in ℝ$
102 nnnn0 ${⊢}{A}\in ℕ\to {A}\in {ℕ}_{0}$
103 102 nn0ge0d ${⊢}{A}\in ℕ\to 0\le {A}$
104 103 3ad2ant1 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to 0\le {A}$
105 104 3ad2ant1 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to 0\le {A}$
106 101 105 sqrtsqd ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \sqrt{{{A}}^{2}}={A}$
107 98 106 eqtr3d ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \sqrt{{C}+{B}}\sqrt{{C}-{B}}={A}$
108 107 oveq2d ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to 2\sqrt{{C}+{B}}\sqrt{{C}-{B}}=2{A}$
109 63 108 oveq12d ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \left({C}+{B}\right)+\left({C}-{B}\right)-2\sqrt{{C}+{B}}\sqrt{{C}-{B}}=2{C}-2{A}$
110 55 109 eqtr4d ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to 2\left({C}-{A}\right)=\left({C}+{B}\right)+\left({C}-{B}\right)-2\sqrt{{C}+{B}}\sqrt{{C}-{B}}$
111 resqrtth ${⊢}\left({C}+{B}\in ℝ\wedge 0\le {C}+{B}\right)\to {\sqrt{{C}+{B}}}^{2}={C}+{B}$
112 37 91 111 syl2anc ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {\sqrt{{C}+{B}}}^{2}={C}+{B}$
113 112 oveq1d ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {\sqrt{{C}+{B}}}^{2}-2\sqrt{{C}+{B}}\sqrt{{C}-{B}}={C}+{B}-2\sqrt{{C}+{B}}\sqrt{{C}-{B}}$
114 resqrtth ${⊢}\left({C}-{B}\in ℝ\wedge 0\le {C}-{B}\right)\to {\sqrt{{C}-{B}}}^{2}={C}-{B}$
115 42 96 114 syl2anc ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {\sqrt{{C}-{B}}}^{2}={C}-{B}$
116 113 115 oveq12d ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {\sqrt{{C}+{B}}}^{2}-2\sqrt{{C}+{B}}\sqrt{{C}-{B}}+{\sqrt{{C}-{B}}}^{2}=\left({C}+{B}-2\sqrt{{C}+{B}}\sqrt{{C}-{B}}\right)+{C}-{B}$
117 50 110 116 3eqtr4rd ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {\sqrt{{C}+{B}}}^{2}-2\sqrt{{C}+{B}}\sqrt{{C}-{B}}+{\sqrt{{C}-{B}}}^{2}=2\left({C}-{A}\right)$
118 31 117 eqtrd ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}=2\left({C}-{A}\right)$
119 118 oveq1d ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{2}=\frac{2\left({C}-{A}\right)}{2}$
120 subcl ${⊢}\left({C}\in ℂ\wedge {A}\in ℂ\right)\to {C}-{A}\in ℂ$
121 3 69 120 syl2anr ${⊢}\left({A}\in ℕ\wedge {C}\in ℕ\right)\to {C}-{A}\in ℂ$
122 121 3adant2 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to {C}-{A}\in ℂ$
123 122 3ad2ant1 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {C}-{A}\in ℂ$
124 divcan3 ${⊢}\left({C}-{A}\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to \frac{2\left({C}-{A}\right)}{2}={C}-{A}$
125 14 15 124 mp3an23 ${⊢}{C}-{A}\in ℂ\to \frac{2\left({C}-{A}\right)}{2}={C}-{A}$
126 123 125 syl ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \frac{2\left({C}-{A}\right)}{2}={C}-{A}$
127 119 126 eqtrd ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{2}={C}-{A}$
128 127 oveq1d ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \frac{\frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{2}}{2}=\frac{{C}-{A}}{2}$
129 25 128 eqtr3d ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{2\cdot 2}=\frac{{C}-{A}}{2}$
130 20 129 syl5eq ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to \frac{{\left(\sqrt{{C}+{B}}-\sqrt{{C}-{B}}\right)}^{2}}{{2}^{2}}=\frac{{C}-{A}}{2}$
131 18 130 eqtrd ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {\left(\frac{\sqrt{{C}+{B}}-\sqrt{{C}-{B}}}{2}\right)}^{2}=\frac{{C}-{A}}{2}$
132 2 131 syl5eq ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge {{A}}^{2}+{{B}}^{2}={{C}}^{2}\wedge \left({A}\mathrm{gcd}{B}=1\wedge ¬2\parallel {A}\right)\right)\to {{N}}^{2}=\frac{{C}-{A}}{2}$