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 ⊢ φ → A ∈ ℕ
fltabcoprm.b ⊢ φ → B ∈ ℕ
fltabcoprm.c ⊢ φ → C ∈ ℕ
fltabcoprm.2 ⊢ φ → A gcd C = 1
fltabcoprm.3 ⊢ φ → A 2 + B 2 = C 2
Assertion fltabcoprm ⊢ φ → A gcd B = 1

Proof

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