Metamath Proof Explorer

Theorem fltaccoprm

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

Ref Expression
Hypotheses fltabcoprmex.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
fltabcoprmex.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
fltabcoprmex.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
fltabcoprmex.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
fltabcoprmex.1 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
fltaccoprm.1 ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
Assertion fltaccoprm ( 𝜑 → ( 𝐴 gcd 𝐶 ) = 1 )

Proof

Step Hyp Ref Expression
1 fltabcoprmex.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 fltabcoprmex.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 fltabcoprmex.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4 fltabcoprmex.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 fltabcoprmex.1 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
6 fltaccoprm.1 ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
7 coprmgcdb ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ↔ ( 𝐴 gcd 𝐵 ) = 1 ) )
8 1 2 7 syl2anc ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ↔ ( 𝐴 gcd 𝐵 ) = 1 ) )
9 6 8 mpbird ⊢ ( 𝜑 → ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) )
10 simprl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) → 𝑖 ∥ 𝐴 )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ )
12 11 nnzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℤ )
13 3 nnzd ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝐶 ∈ ℤ )
15 4 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
16 dvdsexpim ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑖 ∥ 𝐶 → ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐶 ↑ 𝑁 ) ) )
17 12 14 15 16 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝑖 ∥ 𝐶 → ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐶 ↑ 𝑁 ) ) )
18 1 nnzd ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝐴 ∈ ℤ )
20 dvdsexpim ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑖 ∥ 𝐴 → ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐴 ↑ 𝑁 ) ) )
21 12 19 15 20 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝑖 ∥ 𝐴 → ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐴 ↑ 𝑁 ) ) )
22 17 21 anim12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( 𝑖 ∥ 𝐶 ∧ 𝑖 ∥ 𝐴 ) → ( ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐶 ↑ 𝑁 ) ∧ ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐴 ↑ 𝑁 ) ) ) )
23 22 ancomsd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) → ( ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐶 ↑ 𝑁 ) ∧ ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐴 ↑ 𝑁 ) ) ) )
24 23 imp ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) → ( ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐶 ↑ 𝑁 ) ∧ ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐴 ↑ 𝑁 ) ) )
25 11 15 nnexpcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝑖 ↑ 𝑁 ) ∈ ℕ )
26 25 nnzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝑖 ↑ 𝑁 ) ∈ ℤ )
27 26 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) → ( 𝑖 ↑ 𝑁 ) ∈ ℤ )
28 3 4 nnexpcld ⊢ ( 𝜑 → ( 𝐶 ↑ 𝑁 ) ∈ ℕ )
29 28 nnzd ⊢ ( 𝜑 → ( 𝐶 ↑ 𝑁 ) ∈ ℤ )
30 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) → ( 𝐶 ↑ 𝑁 ) ∈ ℤ )
31 1 4 nnexpcld ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℕ )
32 31 nnzd ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℤ )
33 32 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) → ( 𝐴 ↑ 𝑁 ) ∈ ℤ )
34 dvds2sub ⊢ ( ( ( 𝑖 ↑ 𝑁 ) ∈ ℤ ∧ ( 𝐶 ↑ 𝑁 ) ∈ ℤ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) → ( ( ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐶 ↑ 𝑁 ) ∧ ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐴 ↑ 𝑁 ) ) → ( 𝑖 ↑ 𝑁 ) ∥ ( ( 𝐶 ↑ 𝑁 ) − ( 𝐴 ↑ 𝑁 ) ) ) )
35 27 30 33 34 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) → ( ( ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐶 ↑ 𝑁 ) ∧ ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐴 ↑ 𝑁 ) ) → ( 𝑖 ↑ 𝑁 ) ∥ ( ( 𝐶 ↑ 𝑁 ) − ( 𝐴 ↑ 𝑁 ) ) ) )
36 24 35 mpd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) → ( 𝑖 ↑ 𝑁 ) ∥ ( ( 𝐶 ↑ 𝑁 ) − ( 𝐴 ↑ 𝑁 ) ) )
37 1 nncnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
38 37 4 expcld ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
39 2 nncnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
40 39 4 expcld ⊢ ( 𝜑 → ( 𝐵 ↑ 𝑁 ) ∈ ℂ )
41 38 40 5 laddrotrd ⊢ ( 𝜑 → ( ( 𝐶 ↑ 𝑁 ) − ( 𝐴 ↑ 𝑁 ) ) = ( 𝐵 ↑ 𝑁 ) )
42 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) → ( ( 𝐶 ↑ 𝑁 ) − ( 𝐴 ↑ 𝑁 ) ) = ( 𝐵 ↑ 𝑁 ) )
43 36 42 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) → ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) )
44 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) → 𝑖 ∈ ℕ )
45 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) → 𝐵 ∈ ℕ )
46 3 nncnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
47 37 39 46 4 5 flt0 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
48 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) → 𝑁 ∈ ℕ )
49 dvdsexpnn ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑖 ∥ 𝐵 ↔ ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )
50 44 45 48 49 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) → ( 𝑖 ∥ 𝐵 ↔ ( 𝑖 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )
51 43 50 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) → 𝑖 ∥ 𝐵 )
52 10 51 jca ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ) → ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) )
53 52 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) → ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) )
54 53 imim1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) → ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) → 𝑖 = 1 ) ) )
55 54 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) → ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) → 𝑖 = 1 ) ) )
56 9 55 mpd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) → 𝑖 = 1 ) )
57 coprmgcdb ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) → 𝑖 = 1 ) ↔ ( 𝐴 gcd 𝐶 ) = 1 ) )
58 1 3 57 syl2anc ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) → 𝑖 = 1 ) ↔ ( 𝐴 gcd 𝐶 ) = 1 ) )
59 56 58 mpbid ⊢ ( 𝜑 → ( 𝐴 gcd 𝐶 ) = 1 )