Metamath Proof Explorer

Theorem fltabcoprm

Description: A counterexample to FLT with A , C coprime also has A , B coprime. Converse of fltaccoprm . (Contributed by SN, 22-Aug-2024)

Ref Expression
Hypotheses fltabcoprm.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
fltabcoprm.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
fltabcoprm.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
fltabcoprm.2 ⊢ ( 𝜑 → ( 𝐴 gcd 𝐶 ) = 1 )
fltabcoprm.3 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
Assertion fltabcoprm ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )

Proof

Step Hyp Ref Expression
1 fltabcoprm.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 fltabcoprm.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 fltabcoprm.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4 fltabcoprm.2 ⊢ ( 𝜑 → ( 𝐴 gcd 𝐶 ) = 1 )
5 fltabcoprm.3 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
6 coprmgcdb ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) → 𝑖 = 1 ) ↔ ( 𝐴 gcd 𝐶 ) = 1 ) )
7 1 3 6 syl2anc ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) → 𝑖 = 1 ) ↔ ( 𝐴 gcd 𝐶 ) = 1 ) )
8 4 7 mpbird ⊢ ( 𝜑 → ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) → 𝑖 = 1 ) )
9 simprl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → 𝑖 ∥ 𝐴 )
10 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → 𝑖 ∈ ℕ )
11 10 nnsqcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝑖 ↑ 2 ) ∈ ℕ )
12 11 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝑖 ↑ 2 ) ∈ ℤ )
13 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → 𝐴 ∈ ℕ )
14 13 nnsqcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝐴 ↑ 2 ) ∈ ℕ )
15 14 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝐴 ↑ 2 ) ∈ ℤ )
16 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → 𝐵 ∈ ℕ )
17 16 nnsqcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝐵 ↑ 2 ) ∈ ℕ )
18 17 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝐵 ↑ 2 ) ∈ ℤ )
19 dvdssqlem ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( 𝑖 ∥ 𝐴 ↔ ( 𝑖 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ) )
20 10 13 19 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝑖 ∥ 𝐴 ↔ ( 𝑖 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ) )
21 9 20 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝑖 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) )
22 simprr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → 𝑖 ∥ 𝐵 )
23 dvdssqlem ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝑖 ∥ 𝐵 ↔ ( 𝑖 ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) )
24 10 16 23 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝑖 ∥ 𝐵 ↔ ( 𝑖 ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) )
25 22 24 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝑖 ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) )
26 12 15 18 21 25 dvds2addd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝑖 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
27 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
28 26 27 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝑖 ↑ 2 ) ∥ ( 𝐶 ↑ 2 ) )
29 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → 𝐶 ∈ ℕ )
30 dvdssqlem ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝑖 ∥ 𝐶 ↔ ( 𝑖 ↑ 2 ) ∥ ( 𝐶 ↑ 2 ) ) )
31 10 29 30 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝑖 ∥ 𝐶 ↔ ( 𝑖 ↑ 2 ) ∥ ( 𝐶 ↑ 2 ) ) )
32 28 31 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → 𝑖 ∥ 𝐶 )
33 9 32 jca ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) )
34 33 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) )
35 34 imim1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) → 𝑖 = 1 ) → ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ) )
36 35 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) → 𝑖 = 1 ) → ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ) )
37 8 36 mpd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) )
38 coprmgcdb ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ↔ ( 𝐴 gcd 𝐵 ) = 1 ) )
39 1 2 38 syl2anc ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ↔ ( 𝐴 gcd 𝐵 ) = 1 ) )
40 37 39 mpbid ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )