Proof of Theorem flt4lem6
| Step | Hyp | Ref
| Expression |
| 1 | | flt4lem6.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℕ) |
| 2 | | flt4lem6.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℕ) |
| 3 | 2 | nnzd 12640 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℤ) |
| 4 | | divgcdnn 16552 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ) → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ) |
| 5 | 1, 3, 4 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ) |
| 6 | 1 | nnzd 12640 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℤ) |
| 7 | | divgcdnnr 16553 |
. . . 4
⊢ ((𝐵 ∈ ℕ ∧ 𝐴 ∈ ℤ) → (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ) |
| 8 | 2, 6, 7 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ) |
| 9 | | flt4lem6.1 |
. . . . . . 7
⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) |
| 10 | | gcdnncl 16544 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℕ) |
| 11 | 1, 2, 10 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 gcd 𝐵) ∈ ℕ) |
| 12 | 11 | nncnd 12282 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 gcd 𝐵) ∈ ℂ) |
| 13 | 12 | flt4lem 42655 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑4) = (((𝐴 gcd 𝐵)↑2)↑2)) |
| 14 | 9, 13 | oveq12d 7449 |
. . . . . 6
⊢ (𝜑 → (((𝐴↑4) + (𝐵↑4)) / ((𝐴 gcd 𝐵)↑4)) = ((𝐶↑2) / (((𝐴 gcd 𝐵)↑2)↑2))) |
| 15 | 1 | nncnd 12282 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 16 | 11 | nnne0d 12316 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 gcd 𝐵) ≠ 0) |
| 17 | | 4nn0 12545 |
. . . . . . . . . 10
⊢ 4 ∈
ℕ0 |
| 18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 4 ∈
ℕ0) |
| 19 | 15, 12, 16, 18 | expdivd 14200 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 / (𝐴 gcd 𝐵))↑4) = ((𝐴↑4) / ((𝐴 gcd 𝐵)↑4))) |
| 20 | 2 | nncnd 12282 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 21 | 20, 12, 16, 18 | expdivd 14200 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 / (𝐴 gcd 𝐵))↑4) = ((𝐵↑4) / ((𝐴 gcd 𝐵)↑4))) |
| 22 | 19, 21 | oveq12d 7449 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = (((𝐴↑4) / ((𝐴 gcd 𝐵)↑4)) + ((𝐵↑4) / ((𝐴 gcd 𝐵)↑4)))) |
| 23 | 15, 18 | expcld 14186 |
. . . . . . . 8
⊢ (𝜑 → (𝐴↑4) ∈ ℂ) |
| 24 | 20, 18 | expcld 14186 |
. . . . . . . 8
⊢ (𝜑 → (𝐵↑4) ∈ ℂ) |
| 25 | 12, 18 | expcld 14186 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑4) ∈ ℂ) |
| 26 | 11, 18 | nnexpcld 14284 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑4) ∈ ℕ) |
| 27 | 26 | nnne0d 12316 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑4) ≠ 0) |
| 28 | 23, 24, 25, 27 | divdird 12081 |
. . . . . . 7
⊢ (𝜑 → (((𝐴↑4) + (𝐵↑4)) / ((𝐴 gcd 𝐵)↑4)) = (((𝐴↑4) / ((𝐴 gcd 𝐵)↑4)) + ((𝐵↑4) / ((𝐴 gcd 𝐵)↑4)))) |
| 29 | 22, 28 | eqtr4d 2780 |
. . . . . 6
⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = (((𝐴↑4) + (𝐵↑4)) / ((𝐴 gcd 𝐵)↑4))) |
| 30 | | flt4lem6.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℕ) |
| 31 | 30 | nncnd 12282 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 32 | 11 | nnsqcld 14283 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑2) ∈ ℕ) |
| 33 | 32 | nncnd 12282 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑2) ∈ ℂ) |
| 34 | 32 | nnne0d 12316 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑2) ≠ 0) |
| 35 | 31, 33, 34 | sqdivd 14199 |
. . . . . 6
⊢ (𝜑 → ((𝐶 / ((𝐴 gcd 𝐵)↑2))↑2) = ((𝐶↑2) / (((𝐴 gcd 𝐵)↑2)↑2))) |
| 36 | 14, 29, 35 | 3eqtr4d 2787 |
. . . . 5
⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = ((𝐶 / ((𝐴 gcd 𝐵)↑2))↑2)) |
| 37 | 5, 18 | nnexpcld 14284 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 / (𝐴 gcd 𝐵))↑4) ∈ ℕ) |
| 38 | 8, 18 | nnexpcld 14284 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 / (𝐴 gcd 𝐵))↑4) ∈ ℕ) |
| 39 | 37, 38 | nnaddcld 12318 |
. . . . . 6
⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) ∈ ℕ) |
| 40 | 39 | nnzd 12640 |
. . . . 5
⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) ∈ ℤ) |
| 41 | 36, 40 | eqeltrrd 2842 |
. . . 4
⊢ (𝜑 → ((𝐶 / ((𝐴 gcd 𝐵)↑2))↑2) ∈
ℤ) |
| 42 | 30 | nnzd 12640 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℤ) |
| 43 | | znq 12994 |
. . . . 5
⊢ ((𝐶 ∈ ℤ ∧ ((𝐴 gcd 𝐵)↑2) ∈ ℕ) → (𝐶 / ((𝐴 gcd 𝐵)↑2)) ∈ ℚ) |
| 44 | 42, 32, 43 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐶 / ((𝐴 gcd 𝐵)↑2)) ∈ ℚ) |
| 45 | 30 | nnred 12281 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℝ) |
| 46 | 32 | nnred 12281 |
. . . . 5
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑2) ∈ ℝ) |
| 47 | 30 | nngt0d 12315 |
. . . . 5
⊢ (𝜑 → 0 < 𝐶) |
| 48 | 32 | nngt0d 12315 |
. . . . 5
⊢ (𝜑 → 0 < ((𝐴 gcd 𝐵)↑2)) |
| 49 | 45, 46, 47, 48 | divgt0d 12203 |
. . . 4
⊢ (𝜑 → 0 < (𝐶 / ((𝐴 gcd 𝐵)↑2))) |
| 50 | 41, 44, 49 | posqsqznn 42371 |
. . 3
⊢ (𝜑 → (𝐶 / ((𝐴 gcd 𝐵)↑2)) ∈ ℕ) |
| 51 | 5, 8, 50 | 3jca 1129 |
. 2
⊢ (𝜑 → ((𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐶 / ((𝐴 gcd 𝐵)↑2)) ∈ ℕ)) |
| 52 | 51, 36 | jca 511 |
1
⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐶 / ((𝐴 gcd 𝐵)↑2)) ∈ ℕ) ∧ (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = ((𝐶 / ((𝐴 gcd 𝐵)↑2))↑2))) |