Metamath Proof Explorer

Theorem flt4lem6

Description: Remove shared factors in a solution to A ^ 4 + B ^ 4 = C ^ 2 . (Contributed by SN, 24-Jul-2024)

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

Proof

Step Hyp Ref Expression
1 flt4lem6.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 flt4lem6.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 flt4lem6.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4 flt4lem6.1 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( 𝐶 ↑ 2 ) )
5 2 nnzd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
6 divgcdnn ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ )
7 1 5 6 syl2anc ⊢ ( 𝜑 → ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ )
8 1 nnzd ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
9 divgcdnnr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℤ ) → ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ )
10 2 8 9 syl2anc ⊢ ( 𝜑 → ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ )
11 gcdnncl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
12 1 2 11 syl2anc ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
13 12 nncnd ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ ℂ )
14 13 flt4lem ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ↑ 4 ) = ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ↑ 2 ) )
15 4 14 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) / ( ( 𝐴 gcd 𝐵 ) ↑ 4 ) ) = ( ( 𝐶 ↑ 2 ) / ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ↑ 2 ) ) )
16 1 nncnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
17 12 nnne0d ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ≠ 0 )
18 4nn0 ⊢ 4 ∈ ℕ0
19 18 a1i ⊢ ( 𝜑 → 4 ∈ ℕ0 )
20 16 13 17 19 expdivd ⊢ ( 𝜑 → ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) = ( ( 𝐴 ↑ 4 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 4 ) ) )
21 2 nncnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
22 21 13 17 19 expdivd ⊢ ( 𝜑 → ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) = ( ( 𝐵 ↑ 4 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 4 ) ) )
23 20 22 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) + ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) ) = ( ( ( 𝐴 ↑ 4 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 4 ) ) + ( ( 𝐵 ↑ 4 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 4 ) ) ) )
24 16 19 expcld ⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) ∈ ℂ )
25 21 19 expcld ⊢ ( 𝜑 → ( 𝐵 ↑ 4 ) ∈ ℂ )
26 13 19 expcld ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ↑ 4 ) ∈ ℂ )
27 12 19 nnexpcld ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ↑ 4 ) ∈ ℕ )
28 27 nnne0d ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ↑ 4 ) ≠ 0 )
29 24 25 26 28 divdird ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) / ( ( 𝐴 gcd 𝐵 ) ↑ 4 ) ) = ( ( ( 𝐴 ↑ 4 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 4 ) ) + ( ( 𝐵 ↑ 4 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 4 ) ) ) )
30 23 29 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) + ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) ) = ( ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) / ( ( 𝐴 gcd 𝐵 ) ↑ 4 ) ) )
31 3 nncnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
32 12 nnsqcld ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℕ )
33 32 nncnd ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℂ )
34 32 nnne0d ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ≠ 0 )
35 31 33 34 sqdivd ⊢ ( 𝜑 → ( ( 𝐶 / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) ↑ 2 ) = ( ( 𝐶 ↑ 2 ) / ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ↑ 2 ) ) )
36 15 30 35 3eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) + ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) ) = ( ( 𝐶 / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) ↑ 2 ) )
37 7 19 nnexpcld ⊢ ( 𝜑 → ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) ∈ ℕ )
38 10 19 nnexpcld ⊢ ( 𝜑 → ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) ∈ ℕ )
39 37 38 nnaddcld ⊢ ( 𝜑 → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) + ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) ) ∈ ℕ )
40 39 nnzd ⊢ ( 𝜑 → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) + ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) ) ∈ ℤ )
41 36 40 eqeltrrd ⊢ ( 𝜑 → ( ( 𝐶 / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) ↑ 2 ) ∈ ℤ )
42 3 nnzd ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
43 znq ⊢ ( ( 𝐶 ∈ ℤ ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℕ ) → ( 𝐶 / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) ∈ ℚ )
44 42 32 43 syl2anc ⊢ ( 𝜑 → ( 𝐶 / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) ∈ ℚ )
45 3 nnred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
46 32 nnred ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℝ )
47 3 nngt0d ⊢ ( 𝜑 → 0 < 𝐶 )
48 32 nngt0d ⊢ ( 𝜑 → 0 < ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) )
49 45 46 47 48 divgt0d ⊢ ( 𝜑 → 0 < ( 𝐶 / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) )
50 41 44 49 posqsqznn ⊢ ( 𝜑 → ( 𝐶 / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) ∈ ℕ )
51 7 10 50 3jca ⊢ ( 𝜑 → ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ ∧ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ ∧ ( 𝐶 / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) ∈ ℕ ) )
52 51 36 jca ⊢ ( 𝜑 → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ ∧ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ ∧ ( 𝐶 / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) ∈ ℕ ) ∧ ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) + ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 4 ) ) = ( ( 𝐶 / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) ↑ 2 ) ) )