This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pythagtriplem3

Description: Lemma for pythagtrip . Show that C and B are relatively prime under some conditions. (Contributed by Scott Fenton, 8-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion pythagtriplem3 ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐵 gcd 𝐶 ) = 1 )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) → ( ( 𝐵 ↑ 2 ) gcd ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) = ( ( 𝐵 ↑ 2 ) gcd ( 𝐶 ↑ 2 ) ) )
2 1 adantl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ( 𝐵 ↑ 2 ) gcd ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) = ( ( 𝐵 ↑ 2 ) gcd ( 𝐶 ↑ 2 ) ) )
3 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
4 zsqcl ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 ↑ 2 ) ∈ ℤ )
5 3 4 syl ⊢ ( 𝐵 ∈ ℕ → ( 𝐵 ↑ 2 ) ∈ ℤ )
6 5 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐵 ↑ 2 ) ∈ ℤ )
7 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
8 zsqcl ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )
9 7 8 syl ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ↑ 2 ) ∈ ℤ )
10 9 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 ↑ 2 ) ∈ ℤ )
11 gcdadd ⊢ ( ( ( 𝐵 ↑ 2 ) ∈ ℤ ∧ ( 𝐴 ↑ 2 ) ∈ ℤ ) → ( ( 𝐵 ↑ 2 ) gcd ( 𝐴 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) gcd ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
12 6 10 11 syl2anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐵 ↑ 2 ) gcd ( 𝐴 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) gcd ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
13 6 10 gcdcomd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐵 ↑ 2 ) gcd ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )
14 12 13 eqtr3d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐵 ↑ 2 ) gcd ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )
15 14 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ( 𝐵 ↑ 2 ) gcd ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )
16 2 15 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ( 𝐵 ↑ 2 ) gcd ( 𝐶 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )
17 simpl2 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → 𝐵 ∈ ℕ )
18 simpl3 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → 𝐶 ∈ ℕ )
19 sqgcd ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐵 gcd 𝐶 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) gcd ( 𝐶 ↑ 2 ) ) )
20 17 18 19 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ( 𝐵 gcd 𝐶 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) gcd ( 𝐶 ↑ 2 ) ) )
21 simpl1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → 𝐴 ∈ ℕ )
22 sqgcd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )
23 21 17 22 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )
24 16 20 23 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ( 𝐵 gcd 𝐶 ) ↑ 2 ) = ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) )
25 24 3adant3 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐵 gcd 𝐶 ) ↑ 2 ) = ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) )
26 simp3l ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐴 gcd 𝐵 ) = 1 )
27 26 oveq1d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( 1 ↑ 2 ) )
28 25 27 eqtrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐵 gcd 𝐶 ) ↑ 2 ) = ( 1 ↑ 2 ) )
29 3 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐵 ∈ ℤ )
30 nnz ⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℤ )
31 30 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℤ )
32 29 31 gcdcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐵 gcd 𝐶 ) ∈ ℕ0 )
33 32 nn0red ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐵 gcd 𝐶 ) ∈ ℝ )
34 33 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐵 gcd 𝐶 ) ∈ ℝ )
35 32 nn0ge0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 ≤ ( 𝐵 gcd 𝐶 ) )
36 35 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 ≤ ( 𝐵 gcd 𝐶 ) )
37 1re ⊢ 1 ∈ ℝ
38 0le1 ⊢ 0 ≤ 1
39 sq11 ⊢ ( ( ( ( 𝐵 gcd 𝐶 ) ∈ ℝ ∧ 0 ≤ ( 𝐵 gcd 𝐶 ) ) ∧ ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ) → ( ( ( 𝐵 gcd 𝐶 ) ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( 𝐵 gcd 𝐶 ) = 1 ) )
40 37 38 39 mpanr12 ⊢ ( ( ( 𝐵 gcd 𝐶 ) ∈ ℝ ∧ 0 ≤ ( 𝐵 gcd 𝐶 ) ) → ( ( ( 𝐵 gcd 𝐶 ) ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( 𝐵 gcd 𝐶 ) = 1 ) )
41 34 36 40 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐵 gcd 𝐶 ) ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( 𝐵 gcd 𝐶 ) = 1 ) )
42 28 41 mpbid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐵 gcd 𝐶 ) = 1 )