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=C+B−C−B2
Assertion pythagtriplem14 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→N2=C−A2

Proof

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