Metamath Proof Explorer

Theorem pythagtriplem16

Description: Lemma for pythagtrip . Show the relationship between M , N , and B . (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses pythagtriplem15.1 ⊢M=C+B+C−B2
pythagtriplem15.2 ⊢N=C+B−C−B2
Assertion pythagtriplem16 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→B=2⁢ M⋅ N

Proof

Step Hyp Ref Expression
1 pythagtriplem15.1 ⊢M=C+B+C−B2
2 pythagtriplem15.2 ⊢N=C+B−C−B2
3 1 2 oveq12i ⊢ M⋅ N=C+B+C−B2⁢C+B−C−B2
4 nncn ⊢C∈ℕ→C∈ℂ
5 nncn ⊢B∈ℕ→B∈ℂ
6 addcl ⊢C∈ℂ∧B∈ℂ→C+B∈ℂ
7 4 5 6 syl2anr ⊢B∈ℕ∧C∈ℕ→C+B∈ℂ
8 7 sqrtcld ⊢B∈ℕ∧C∈ℕ→C+B∈ℂ
9 subcl ⊢C∈ℂ∧B∈ℂ→C−B∈ℂ
10 4 5 9 syl2anr ⊢B∈ℕ∧C∈ℕ→C−B∈ℂ
11 10 sqrtcld ⊢B∈ℕ∧C∈ℕ→C−B∈ℂ
12 addcl ⊢C+B∈ℂ∧C−B∈ℂ→C+B+C−B∈ℂ
13 8 11 12 syl2anc ⊢B∈ℕ∧C∈ℕ→C+B+C−B∈ℂ
14 13 3adant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→C+B+C−B∈ℂ
15 14 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B+C−B∈ℂ
16 subcl ⊢C+B∈ℂ∧C−B∈ℂ→C+B−C−B∈ℂ
17 8 11 16 syl2anc ⊢B∈ℕ∧C∈ℕ→C+B−C−B∈ℂ
18 17 3adant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→C+B−C−B∈ℂ
19 18 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B−C−B∈ℂ
20 2cnne0 ⊢2∈ℂ∧2≠0
21 divmuldiv ⊢C+B+C−B∈ℂ∧C+B−C−B∈ℂ∧2∈ℂ∧2≠0∧2∈ℂ∧2≠0→C+B+C−B2⁢C+B−C−B2=C+B+C−B⁢C+B−C−B2⋅2
22 20 20 21 mpanr12 ⊢C+B+C−B∈ℂ∧C+B−C−B∈ℂ→C+B+C−B2⁢C+B−C−B2=C+B+C−B⁢C+B−C−B2⋅2
23 15 19 22 syl2anc ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B+C−B2⁢C+B−C−B2=C+B+C−B⁢C+B−C−B2⋅2
24 13 17 mulcld ⊢B∈ℕ∧C∈ℕ→C+B+C−B⁢C+B−C−B∈ℂ
25 24 3adant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→C+B+C−B⁢C+B−C−B∈ℂ
26 25 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B+C−B⁢C+B−C−B∈ℂ
27 divdiv1 ⊢C+B+C−B⁢C+B−C−B∈ℂ∧2∈ℂ∧2≠0∧2∈ℂ∧2≠0→C+B+C−B⁢C+B−C−B22=C+B+C−B⁢C+B−C−B2⋅2
28 20 20 27 mp3an23 ⊢C+B+C−B⁢C+B−C−B∈ℂ→C+B+C−B⁢C+B−C−B22=C+B+C−B⁢C+B−C−B2⋅2
29 26 28 syl ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B+C−B⁢C+B−C−B22=C+B+C−B⁢C+B−C−B2⋅2
30 23 29 eqtr4d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B+C−B2⁢C+B−C−B2=C+B+C−B⁢C+B−C−B22
31 nnre ⊢C∈ℕ→C∈ℝ
32 nnre ⊢B∈ℕ→B∈ℝ
33 readdcl ⊢C∈ℝ∧B∈ℝ→C+B∈ℝ
34 31 32 33 syl2anr ⊢B∈ℕ∧C∈ℕ→C+B∈ℝ
35 34 3adant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→C+B∈ℝ
36 35 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B∈ℝ
37 31 adantl ⊢B∈ℕ∧C∈ℕ→C∈ℝ
38 32 adantr ⊢B∈ℕ∧C∈ℕ→B∈ℝ
39 nngt0 ⊢C∈ℕ→0<C
40 39 adantl ⊢B∈ℕ∧C∈ℕ→0<C
41 nngt0 ⊢B∈ℕ→0<B
42 41 adantr ⊢B∈ℕ∧C∈ℕ→0<B
43 37 38 40 42 addgt0d ⊢B∈ℕ∧C∈ℕ→0<C+B
44 0re ⊢0∈ℝ
45 ltle ⊢0∈ℝ∧C+B∈ℝ→0<C+B→0≤C+B
46 44 45 mpan ⊢C+B∈ℝ→0<C+B→0≤C+B
47 34 43 46 sylc ⊢B∈ℕ∧C∈ℕ→0≤C+B
48 47 3adant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→0≤C+B
49 48 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→0≤C+B
50 resqrtth ⊢C+B∈ℝ∧0≤C+B→C+B2=C+B
51 36 49 50 syl2anc ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B2=C+B
52 resubcl ⊢C∈ℝ∧B∈ℝ→C−B∈ℝ
53 31 32 52 syl2anr ⊢B∈ℕ∧C∈ℕ→C−B∈ℝ
54 53 3adant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→C−B∈ℝ
55 54 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C−B∈ℝ
56 pythagtriplem10 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2→0<C−B
57 56 3adant3 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→0<C−B
58 ltle ⊢0∈ℝ∧C−B∈ℝ→0<C−B→0≤C−B
59 44 58 mpan ⊢C−B∈ℝ→0<C−B→0≤C−B
60 55 57 59 sylc ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→0≤C−B
61 resqrtth ⊢C−B∈ℝ∧0≤C−B→C−B2=C−B
62 55 60 61 syl2anc ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C−B2=C−B
63 51 62 oveq12d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B2−C−B2=C+B-C−B
64 63 oveq1d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B2−C−B22=C+B-C−B2
65 simp12 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→B∈ℕ
66 simp13 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C∈ℕ
67 65 66 8 syl2anc ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B∈ℂ
68 65 66 11 syl2anc ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C−B∈ℂ
69 subsq ⊢C+B∈ℂ∧C−B∈ℂ→C+B2−C−B2=C+B+C−B⁢C+B−C−B
70 67 68 69 syl2anc ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B2−C−B2=C+B+C−B⁢C+B−C−B
71 70 oveq1d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B2−C−B22=C+B+C−B⁢C+B−C−B2
72 pnncan ⊢C∈ℂ∧B∈ℂ∧B∈ℂ→C+B-C−B=B+B
73 72 3anidm23 ⊢C∈ℂ∧B∈ℂ→C+B-C−B=B+B
74 2times ⊢B∈ℂ→2⁢B=B+B
75 74 adantl ⊢C∈ℂ∧B∈ℂ→2⁢B=B+B
76 73 75 eqtr4d ⊢C∈ℂ∧B∈ℂ→C+B-C−B=2⁢B
77 4 5 76 syl2anr ⊢B∈ℕ∧C∈ℕ→C+B-C−B=2⁢B
78 77 3adant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→C+B-C−B=2⁢B
79 78 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B-C−B=2⁢B
80 79 oveq1d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B-C−B2=2⁢B2
81 2cn ⊢2∈ℂ
82 2ne0 ⊢2≠0
83 divcan3 ⊢B∈ℂ∧2∈ℂ∧2≠0→2⁢B2=B
84 81 82 83 mp3an23 ⊢B∈ℂ→2⁢B2=B
85 65 5 84 3syl ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→2⁢B2=B
86 80 85 eqtrd ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B-C−B2=B
87 64 71 86 3eqtr3d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B+C−B⁢C+B−C−B2=B
88 87 oveq1d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B+C−B⁢C+B−C−B22=B2
89 30 88 eqtrd ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B+C−B2⁢C+B−C−B2=B2
90 3 89 eqtrid ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→ M⋅ N=B2
91 90 oveq2d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→2⁢ M⋅ N=2⁢B2
92 divcan2 ⊢B∈ℂ∧2∈ℂ∧2≠0→2⁢B2=B
93 81 82 92 mp3an23 ⊢B∈ℂ→2⁢B2=B
94 5 93 syl ⊢B∈ℕ→2⁢B2=B
95 94 3ad2ant2 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→2⁢B2=B
96 95 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→2⁢B2=B
97 91 96 eqtr2d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→B=2⁢ M⋅ N