Metamath Proof Explorer

Theorem pythagtriplem12

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

Ref Expression
Hypothesis pythagtriplem11.1 ⊢M=C+B+C−B2
Assertion pythagtriplem12 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→M2=C+A2

Proof

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