Metamath Proof Explorer

Theorem pythagtriplem7

Description: Lemma for pythagtrip . Calculate ( sqrt( C + B ) ) . (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion pythagtriplem7 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C + B = C + B gcd A

Proof

Step Hyp Ref Expression
1 simp3 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C ∈ ℕ
2 1 nnzd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C ∈ ℤ
3 simp2 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → B ∈ ℕ
4 3 nnzd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → B ∈ ℤ
5 2 4 zsubcld ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C − B ∈ ℤ
6 5 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C − B ∈ ℤ
7 1 3 nnaddcld ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C + B ∈ ℕ
8 7 nnnn0d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C + B ∈ ℕ 0
9 8 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C + B ∈ ℕ 0
10 nnnn0 ⊢ A ∈ ℕ → A ∈ ℕ 0
11 10 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A ∈ ℕ 0
12 11 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → A ∈ ℕ 0
13 6 9 12 3jca ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C − B ∈ ℤ ∧ C + B ∈ ℕ 0 ∧ A ∈ ℕ 0
14 pythagtriplem4 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C − B gcd C + B = 1
15 14 oveq1d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C − B gcd C + B gcd A = 1 gcd A
16 nnz ⊢ A ∈ ℕ → A ∈ ℤ
17 16 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A ∈ ℤ
18 17 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → A ∈ ℤ
19 1gcd ⊢ A ∈ ℤ → 1 gcd A = 1
20 18 19 syl ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → 1 gcd A = 1
21 15 20 eqtrd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C − B gcd C + B gcd A = 1
22 13 21 jca ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C − B ∈ ℤ ∧ C + B ∈ ℕ 0 ∧ A ∈ ℕ 0 ∧ C − B gcd C + B gcd A = 1
23 oveq1 ⊢ A 2 + B 2 = C 2 → A 2 + B 2 - B 2 = C 2 − B 2
24 23 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
25 nncn ⊢ A ∈ ℕ → A ∈ ℂ
26 25 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A ∈ ℂ
27 26 sqcld ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A 2 ∈ ℂ
28 3 nncnd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → B ∈ ℂ
29 28 sqcld ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → B 2 ∈ ℂ
30 27 29 pncand ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A 2 + B 2 - B 2 = A 2
31 30 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → A 2 + B 2 - B 2 = A 2
32 1 nncnd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C ∈ ℂ
33 subsq ⊢ C ∈ ℂ ∧ B ∈ ℂ → C 2 − B 2 = C + B ⁢ C − B
34 32 28 33 syl2anc ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C 2 − B 2 = C + B ⁢ C − B
35 7 nncnd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C + B ∈ ℂ
36 5 zcnd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C − B ∈ ℂ
37 35 36 mulcomd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C + B ⁢ C − B = C − B ⁢ C + B
38 34 37 eqtrd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C 2 − B 2 = C − B ⁢ C + B
39 38 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C 2 − B 2 = C − B ⁢ C + B
40 24 31 39 3eqtr3d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → A 2 = C − B ⁢ C + B
41 coprimeprodsq2 ⊢ C − B ∈ ℤ ∧ C + B ∈ ℕ 0 ∧ A ∈ ℕ 0 ∧ C − B gcd C + B gcd A = 1 → A 2 = C − B ⁢ C + B → C + B = C + B gcd A 2
42 22 40 41 sylc ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C + B = C + B gcd A 2
43 42 fveq2d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C + B = C + B gcd A 2
44 7 nnzd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C + B ∈ ℤ
45 44 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C + B ∈ ℤ
46 45 18 gcdcld ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C + B gcd A ∈ ℕ 0
47 46 nn0red ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C + B gcd A ∈ ℝ
48 46 nn0ge0d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → 0 ≤ C + B gcd A
49 47 48 sqrtsqd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C + B gcd A 2 = C + B gcd A
50 43 49 eqtrd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C + B = C + B gcd A