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 )