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 B 2
Assertion pythagtriplem14 A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A N 2 = C A 2

Proof

Step Hyp Ref Expression
1 pythagtriplem13.1 N = C + B C B 2
2 1 oveq1i N 2 = C + B C B 2 2
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 A 2 + B 2 = C 2 A gcd B = 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 B 2 2 = C + B C B 2 2 2
17 14 15 16 mp3an23 C + B C B C + B C B 2 2 = C + B C B 2 2 2
18 13 17 syl A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B C B 2 2 = C + B C B 2 2 2
19 14 sqvali 2 2 = 2 2
20 19 oveq2i C + B C B 2 2 2 = C + B C B 2 2 2
21 13 sqcld A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B C B 2
22 2cnne0 2 2 0
23 divdiv1 C + B C B 2 2 2 0 2 2 0 C + B C B 2 2 2 = C + B C B 2 2 2
24 22 22 23 mp3an23 C + B C B 2 C + B C B 2 2 2 = C + B C B 2 2 2
25 21 24 syl A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B C B 2 2 2 = C + B C B 2 2 2
26 simp12 A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A B
27 simp13 A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C
28 26 27 7 syl2anc A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B
29 26 27 10 syl2anc A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C B
30 binom2sub C + B C B C + B C B 2 = C + B 2 - 2 C + B C B + C B 2
31 28 29 30 syl2anc A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B C B 2 = C + B 2 - 2 C + B C B + C B 2
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 A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B
38 37 recnd A B C A 2 + B 2 = C 2 A gcd B = 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 A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C B
43 42 recnd A B C A 2 + B 2 = C 2 A gcd B = 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 A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A 2 C + B C B
50 38 43 49 addsubd A B C A 2 + B 2 = C 2 A gcd B = 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 A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C
52 simp11 A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A A
53 52 nncnd A B C A 2 + B 2 = C 2 A gcd B = 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 A 2 + B 2 = C 2 A gcd B = 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 A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B + C B = 2 C
64 26 nncnd A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A B
65 subsq C B C 2 B 2 = C + B C B
66 51 64 65 syl2anc A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C 2 B 2 = C + B C B
67 oveq1 A 2 + B 2 = C 2 A 2 + B 2 - B 2 = C 2 B 2
68 67 3ad2ant2 A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A A 2 + B 2 - B 2 = C 2 B 2
69 nncn A A
70 69 sqcld A A 2
71 70 3ad2ant1 A B C A 2
72 4 sqcld B B 2
73 72 3ad2ant2 A B C B 2
74 71 73 pncand A B C A 2 + B 2 - B 2 = A 2
75 74 3ad2ant1 A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A A 2 + B 2 - B 2 = A 2
76 68 75 eqtr3d A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C 2 B 2 = A 2
77 66 76 eqtr3d A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B C B = A 2
78 77 fveq2d A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B C B = A 2
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 A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A 0 C + B
92 pythagtriplem10 A B C A 2 + B 2 = C 2 0 < C B
93 92 3adant3 A B C A 2 + B 2 = C 2 A gcd B = 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 A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A 0 C B
97 37 91 42 96 sqrtmuld A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B C B = C + B C B
98 78 97 eqtr3d A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A A 2 = C + B C B
99 nnre A A
100 99 3ad2ant1 A B C A
101 100 3ad2ant1 A B C A 2 + B 2 = C 2 A gcd B = 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 A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A 0 A
106 101 105 sqrtsqd A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A A 2 = A
107 98 106 eqtr3d A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B C B = A
108 107 oveq2d A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A 2 C + B C B = 2 A
109 63 108 oveq12d A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B + C B - 2 C + B C B = 2 C 2 A
110 55 109 eqtr4d A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A 2 C A = C + B + C B - 2 C + B C B
111 resqrtth C + B 0 C + B C + B 2 = C + B
112 37 91 111 syl2anc A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B 2 = C + B
113 112 oveq1d A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B 2 2 C + B C B = C + B - 2 C + B C B
114 resqrtth C B 0 C B C B 2 = C B
115 42 96 114 syl2anc A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C B 2 = C B
116 113 115 oveq12d A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B 2 - 2 C + B C B + C B 2 = C + B - 2 C + B C B + C - B
117 50 110 116 3eqtr4rd A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B 2 - 2 C + B C B + C B 2 = 2 C A
118 31 117 eqtrd A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B C B 2 = 2 C A
119 118 oveq1d A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B C B 2 2 = 2 C A 2
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 A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C A
124 divcan3 C A 2 2 0 2 C A 2 = C A
125 14 15 124 mp3an23 C A 2 C A 2 = C A
126 123 125 syl A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A 2 C A 2 = C A
127 119 126 eqtrd A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B C B 2 2 = C A
128 127 oveq1d A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B C B 2 2 2 = C A 2
129 25 128 eqtr3d A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B C B 2 2 2 = C A 2
130 20 129 syl5eq A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B C B 2 2 2 = C A 2
131 18 130 eqtrd A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A C + B C B 2 2 = C A 2
132 2 131 syl5eq A B C A 2 + B 2 = C 2 A gcd B = 1 ¬ 2 A N 2 = C A 2