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

Metamath Proof Explorer

Theorem flt4lem5

Description: In the context of the lemmas of pythagtrip , M and N are coprime. (Contributed by SN, 23-Aug-2024)

Ref Expression
Hypotheses flt4lem5.1 ⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
flt4lem5.2 ⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
Assertion flt4lem5 ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝑀 gcd 𝑁 ) = 1 )

Proof

Step Hyp Ref Expression
1 flt4lem5.1 ⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
2 flt4lem5.2 ⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
3 simp3l ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐴 gcd 𝐵 ) = 1 )
4 simp11 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐴 ∈ ℕ )
5 simp12 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐵 ∈ ℕ )
6 coprmgcdb ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ↔ ( 𝐴 gcd 𝐵 ) = 1 ) )
7 4 5 6 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ↔ ( 𝐴 gcd 𝐵 ) = 1 ) )
8 3 7 mpbird ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) )
9 simplr ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝑖 ∈ ℕ )
10 9 nnzd ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝑖 ∈ ℤ )
11 1 pythagtriplem11 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝑀 ∈ ℕ )
12 11 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝑀 ∈ ℕ )
13 12 nnsqcld ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → ( 𝑀 ↑ 2 ) ∈ ℕ )
14 13 nnzd ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → ( 𝑀 ↑ 2 ) ∈ ℤ )
15 2 pythagtriplem13 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝑁 ∈ ℕ )
16 15 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝑁 ∈ ℕ )
17 16 nnsqcld ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → ( 𝑁 ↑ 2 ) ∈ ℕ )
18 17 nnzd ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → ( 𝑁 ↑ 2 ) ∈ ℤ )
19 simprl ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝑖 ∥ 𝑀 )
20 12 nnzd ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝑀 ∈ ℤ )
21 2nn ⊢ 2 ∈ ℕ
22 21 a1i ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 2 ∈ ℕ )
23 dvdsexp2im ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 2 ∈ ℕ ) → ( 𝑖 ∥ 𝑀 → 𝑖 ∥ ( 𝑀 ↑ 2 ) ) )
24 10 20 22 23 syl3anc ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → ( 𝑖 ∥ 𝑀 → 𝑖 ∥ ( 𝑀 ↑ 2 ) ) )
25 19 24 mpd ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝑖 ∥ ( 𝑀 ↑ 2 ) )
26 simprr ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝑖 ∥ 𝑁 )
27 16 nnzd ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝑁 ∈ ℤ )
28 dvdsexp2im ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ∈ ℕ ) → ( 𝑖 ∥ 𝑁 → 𝑖 ∥ ( 𝑁 ↑ 2 ) ) )
29 10 27 22 28 syl3anc ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → ( 𝑖 ∥ 𝑁 → 𝑖 ∥ ( 𝑁 ↑ 2 ) ) )
30 26 29 mpd ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝑖 ∥ ( 𝑁 ↑ 2 ) )
31 10 14 18 25 30 dvds2subd ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝑖 ∥ ( ( 𝑀 ↑ 2 ) − ( 𝑁 ↑ 2 ) ) )
32 1 2 pythagtriplem15 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐴 = ( ( 𝑀 ↑ 2 ) − ( 𝑁 ↑ 2 ) ) )
33 32 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝐴 = ( ( 𝑀 ↑ 2 ) − ( 𝑁 ↑ 2 ) ) )
34 31 33 breqtrrd ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝑖 ∥ 𝐴 )
35 2z ⊢ 2 ∈ ℤ
36 35 a1i ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 2 ∈ ℤ )
37 12 16 nnmulcld ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → ( 𝑀 · 𝑁 ) ∈ ℕ )
38 37 nnzd ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
39 10 20 27 26 dvdsmultr2d ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝑖 ∥ ( 𝑀 · 𝑁 ) )
40 10 36 38 39 dvdsmultr2d ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝑖 ∥ ( 2 · ( 𝑀 · 𝑁 ) ) )
41 1 2 pythagtriplem16 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐵 = ( 2 · ( 𝑀 · 𝑁 ) ) )
42 41 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝐵 = ( 2 · ( 𝑀 · 𝑁 ) ) )
43 40 42 breqtrrd ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → 𝑖 ∥ 𝐵 )
44 34 43 jca ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) ) → ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) )
45 44 ex ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) → ( ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) → ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) )
46 45 imim1d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 𝑖 ∈ ℕ ) → ( ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) → ( ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) → 𝑖 = 1 ) ) )
47 46 ralimdva ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) → ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) → 𝑖 = 1 ) ) )
48 8 47 mpd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) → 𝑖 = 1 ) )
49 coprmgcdb ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) → 𝑖 = 1 ) ↔ ( 𝑀 gcd 𝑁 ) = 1 ) )
50 11 15 49 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁 ) → 𝑖 = 1 ) ↔ ( 𝑀 gcd 𝑁 ) = 1 ) )
51 48 50 mpbid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝑀 gcd 𝑁 ) = 1 )