Step | Hyp | Ref
| Expression |
1 | | breq1 5077 |
. . . 4
⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (𝑙 < 𝐶 ↔ ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶)) |
2 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (𝑙↑2) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2)) |
3 | 2 | eqeq2d 2749 |
. . . . . 6
⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (((𝑚↑4) + (𝑛↑4)) = (𝑙↑2) ↔ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))) |
4 | 3 | anbi2d 629 |
. . . . 5
⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) ↔ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2)))) |
5 | 4 | 2rexbidv 3229 |
. . . 4
⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) ↔ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2)))) |
6 | 1, 5 | anbi12d 631 |
. . 3
⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → ((𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ↔ (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))))) |
7 | | eqid 2738 |
. . . . . . 7
⊢
(((√‘(𝐶
+ (𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2) =
(((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) /
2) |
8 | | eqid 2738 |
. . . . . . 7
⊢
(((√‘(𝐶
+ (𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2) =
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) /
2) |
9 | | eqid 2738 |
. . . . . . 7
⊢
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
= (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) /
2) |
10 | | eqid 2738 |
. . . . . . 7
⊢
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
= (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) /
2) |
11 | | flt4lem7.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℕ) |
12 | | flt4lem7.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℕ) |
13 | | flt4lem7.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℕ) |
14 | | flt4lem7.1 |
. . . . . . 7
⊢ (𝜑 → ¬ 2 ∥ 𝐴) |
15 | 11 | nnsqcld 13959 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴↑2) ∈ ℕ) |
16 | 12 | nnsqcld 13959 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵↑2) ∈ ℕ) |
17 | | 2nn0 12250 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℕ0) |
19 | 11 | nncnd 11989 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
20 | 19 | flt4lem 40482 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴↑4) = ((𝐴↑2)↑2)) |
21 | 12 | nncnd 11989 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℂ) |
22 | 21 | flt4lem 40482 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵↑4) = ((𝐵↑2)↑2)) |
23 | 20, 22 | oveq12d 7293 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (((𝐴↑2)↑2) + ((𝐵↑2)↑2))) |
24 | | flt4lem7.3 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) |
25 | 23, 24 | eqtr3d 2780 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴↑2)↑2) + ((𝐵↑2)↑2)) = (𝐶↑2)) |
26 | | flt4lem7.2 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) |
27 | | 2nn 12046 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
28 | 27 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℕ) |
29 | | rppwr 16269 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 2 ∈
ℕ) → ((𝐴 gcd
𝐵) = 1 → ((𝐴↑2) gcd (𝐵↑2)) = 1)) |
30 | 11, 12, 28, 29 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑2) gcd (𝐵↑2)) = 1)) |
31 | 26, 30 | mpd 15 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴↑2) gcd (𝐵↑2)) = 1) |
32 | 15, 16, 13, 18, 25, 31 | fltaccoprm 40477 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴↑2) gcd 𝐶) = 1) |
33 | 11 | nnzd 12425 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℤ) |
34 | 13 | nnzd 12425 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℤ) |
35 | | rpexp 16427 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 2 ∈
ℕ) → (((𝐴↑2) gcd 𝐶) = 1 ↔ (𝐴 gcd 𝐶) = 1)) |
36 | 33, 34, 28, 35 | syl3anc 1370 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴↑2) gcd 𝐶) = 1 ↔ (𝐴 gcd 𝐶) = 1)) |
37 | 32, 36 | mpbid 231 |
. . . . . . 7
⊢ (𝜑 → (𝐴 gcd 𝐶) = 1) |
38 | 7, 8, 9, 10, 11, 12, 13, 14, 37, 24 | flt4lem5e 40493 |
. . . . . 6
⊢ (𝜑 →
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2))
= 1 ∧ ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2)) = 1
∧ ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2)) = 1)
∧ ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
∈ ℕ ∧ (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
∈ ℕ ∧ (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈ ℕ) ∧
(((((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2) ·
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
· (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) /
2))) = ((𝐵 / 2)↑2)
∧ (𝐵 / 2) ∈
ℕ))) |
39 | 38 | simp2d 1142 |
. . . . 5
⊢ (𝜑 →
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
∈ ℕ ∧ (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
∈ ℕ ∧ (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈
ℕ)) |
40 | 39 | simp3d 1143 |
. . . 4
⊢ (𝜑 → (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈
ℕ) |
41 | 38 | simp3d 1143 |
. . . . 5
⊢ (𝜑 → (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ·
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
· (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) /
2))) = ((𝐵 / 2)↑2)
∧ (𝐵 / 2) ∈
ℕ)) |
42 | 41 | simprd 496 |
. . . 4
⊢ (𝜑 → (𝐵 / 2) ∈ ℕ) |
43 | | gcdnncl 16214 |
. . . 4
⊢
(((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈ ℕ ∧ (𝐵 / 2) ∈ ℕ) →
((((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2) gcd
(𝐵 / 2)) ∈
ℕ) |
44 | 40, 42, 43 | syl2anc 584 |
. . 3
⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ) |
45 | 44 | nnred 11988 |
. . . . 5
⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ∈ ℝ) |
46 | 42 | nnred 11988 |
. . . . 5
⊢ (𝜑 → (𝐵 / 2) ∈ ℝ) |
47 | 13 | nnred 11988 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℝ) |
48 | 40 | nnzd 12425 |
. . . . . 6
⊢ (𝜑 → (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈
ℤ) |
49 | 48, 42 | gcdle2d 40331 |
. . . . 5
⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ≤ (𝐵 / 2)) |
50 | 12 | nnred 11988 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
51 | 12 | nnrpd 12770 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
52 | | rphalflt 12759 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ+
→ (𝐵 / 2) < 𝐵) |
53 | 51, 52 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐵 / 2) < 𝐵) |
54 | 16 | nnred 11988 |
. . . . . . . 8
⊢ (𝜑 → (𝐵↑2) ∈ ℝ) |
55 | | 4nn0 12252 |
. . . . . . . . . . 11
⊢ 4 ∈
ℕ0 |
56 | 55 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 4 ∈
ℕ0) |
57 | 12, 56 | nnexpcld 13960 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵↑4) ∈ ℕ) |
58 | 57 | nnred 11988 |
. . . . . . . 8
⊢ (𝜑 → (𝐵↑4) ∈ ℝ) |
59 | 13 | nnsqcld 13959 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶↑2) ∈ ℕ) |
60 | 59 | nnred 11988 |
. . . . . . . 8
⊢ (𝜑 → (𝐶↑2) ∈ ℝ) |
61 | | 2lt4 12148 |
. . . . . . . . 9
⊢ 2 <
4 |
62 | | 2z 12352 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
63 | 62 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℤ) |
64 | | 4z 12354 |
. . . . . . . . . . 11
⊢ 4 ∈
ℤ |
65 | 64 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 4 ∈
ℤ) |
66 | | 1red 10976 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℝ) |
67 | | 2re 12047 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
68 | 67 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℝ) |
69 | | 1lt2 12144 |
. . . . . . . . . . . 12
⊢ 1 <
2 |
70 | 69 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 < 2) |
71 | | 2t1e2 12136 |
. . . . . . . . . . . 12
⊢ (2
· 1) = 2 |
72 | 42 | nnge1d 12021 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ≤ (𝐵 / 2)) |
73 | | 2rp 12735 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ+ |
74 | 73 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℝ+) |
75 | 66, 50, 74 | lemuldiv2d 12822 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 1) ≤ 𝐵 ↔ 1 ≤ (𝐵 / 2))) |
76 | 72, 75 | mpbird 256 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 · 1) ≤ 𝐵) |
77 | 71, 76 | eqbrtrrid 5110 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ≤ 𝐵) |
78 | 66, 68, 50, 70, 77 | ltletrd 11135 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < 𝐵) |
79 | 50, 63, 65, 78 | ltexp2d 13968 |
. . . . . . . . 9
⊢ (𝜑 → (2 < 4 ↔ (𝐵↑2) < (𝐵↑4))) |
80 | 61, 79 | mpbii 232 |
. . . . . . . 8
⊢ (𝜑 → (𝐵↑2) < (𝐵↑4)) |
81 | 11, 56 | nnexpcld 13960 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴↑4) ∈ ℕ) |
82 | 81 | nngt0d 12022 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < (𝐴↑4)) |
83 | 81 | nnred 11988 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴↑4) ∈ ℝ) |
84 | 83, 58 | ltaddpos2d 11560 |
. . . . . . . . . 10
⊢ (𝜑 → (0 < (𝐴↑4) ↔ (𝐵↑4) < ((𝐴↑4) + (𝐵↑4)))) |
85 | 82, 84 | mpbid 231 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵↑4) < ((𝐴↑4) + (𝐵↑4))) |
86 | 85, 24 | breqtrd 5100 |
. . . . . . . 8
⊢ (𝜑 → (𝐵↑4) < (𝐶↑2)) |
87 | 54, 58, 60, 80, 86 | lttrd 11136 |
. . . . . . 7
⊢ (𝜑 → (𝐵↑2) < (𝐶↑2)) |
88 | 13 | nnrpd 12770 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
89 | 51, 88, 28 | ltexp1d 40322 |
. . . . . . 7
⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐵↑2) < (𝐶↑2))) |
90 | 87, 89 | mpbird 256 |
. . . . . 6
⊢ (𝜑 → 𝐵 < 𝐶) |
91 | 46, 50, 47, 53, 90 | lttrd 11136 |
. . . . 5
⊢ (𝜑 → (𝐵 / 2) < 𝐶) |
92 | 45, 46, 47, 49, 91 | lelttrd 11133 |
. . . 4
⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶) |
93 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑚 =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) → (𝑚 gcd 𝑛) =
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) gcd 𝑛)) |
94 | 93 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑚 =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) → ((𝑚 gcd 𝑛) = 1 ↔
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) gcd 𝑛) = 1)) |
95 | | oveq1 7282 |
. . . . . . . 8
⊢ (𝑚 =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) → (𝑚↑4) =
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 /
2))↑4)) |
96 | 95 | oveq1d 7290 |
. . . . . . 7
⊢ (𝑚 =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) → ((𝑚↑4) + (𝑛↑4)) =
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4) +
(𝑛↑4))) |
97 | 96 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑚 =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) →
(((𝑚↑4) + (𝑛↑4)) =
(((((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2) gcd
(𝐵 / 2))↑2) ↔
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4) +
(𝑛↑4)) =
(((((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2) gcd
(𝐵 /
2))↑2))) |
98 | 94, 97 | anbi12d 631 |
. . . . 5
⊢ (𝑚 =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) →
(((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2)) ↔
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) gcd 𝑛) = 1 ∧
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4) +
(𝑛↑4)) =
(((((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2) gcd
(𝐵 /
2))↑2)))) |
99 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑛 =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) →
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) gcd 𝑛) =
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) gcd
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 /
2)))) |
100 | 99 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑛 =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) →
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) gcd 𝑛) = 1 ↔
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) gcd
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))) =
1)) |
101 | | oveq1 7282 |
. . . . . . . 8
⊢ (𝑛 =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) → (𝑛↑4) =
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 /
2))↑4)) |
102 | 101 | oveq2d 7291 |
. . . . . . 7
⊢ (𝑛 =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) →
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4) +
(𝑛↑4)) =
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4) +
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 /
2))↑4))) |
103 | 102 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑛 =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) →
(((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4) +
(𝑛↑4)) =
(((((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2) gcd
(𝐵 / 2))↑2) ↔
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4) +
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4)) =
(((((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2) gcd
(𝐵 /
2))↑2))) |
104 | 100, 103 | anbi12d 631 |
. . . . 5
⊢ (𝑛 =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) →
(((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) gcd 𝑛) = 1 ∧
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4) +
(𝑛↑4)) =
(((((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2) gcd
(𝐵 / 2))↑2)) ↔
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) gcd
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))) = 1 ∧
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4) +
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4)) =
(((((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2) gcd
(𝐵 /
2))↑2)))) |
105 | 39 | simp1d 1141 |
. . . . . 6
⊢ (𝜑 →
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
∈ ℕ) |
106 | | gcdnncl 16214 |
. . . . . 6
⊢
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
∈ ℕ ∧ (𝐵 /
2) ∈ ℕ) → ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) ∈
ℕ) |
107 | 105, 42, 106 | syl2anc 584 |
. . . . 5
⊢ (𝜑 →
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) ∈
ℕ) |
108 | 39 | simp2d 1142 |
. . . . . 6
⊢ (𝜑 →
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
∈ ℕ) |
109 | | gcdnncl 16214 |
. . . . . 6
⊢
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
∈ ℕ ∧ (𝐵 /
2) ∈ ℕ) → ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) ∈
ℕ) |
110 | 108, 42, 109 | syl2anc 584 |
. . . . 5
⊢ (𝜑 →
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) ∈
ℕ) |
111 | 105 | nnzd 12425 |
. . . . . . . 8
⊢ (𝜑 →
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
∈ ℤ) |
112 | 42 | nnzd 12425 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 / 2) ∈ ℤ) |
113 | 110 | nnzd 12425 |
. . . . . . . 8
⊢ (𝜑 →
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) ∈
ℤ) |
114 | | gcdass 16255 |
. . . . . . . 8
⊢
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
∈ ℤ ∧ (𝐵 /
2) ∈ ℤ ∧ ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) ∈
ℤ) → (((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) gcd
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))) =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd ((𝐵 / 2) gcd
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 /
2))))) |
115 | 111, 112,
113, 114 | syl3anc 1370 |
. . . . . . 7
⊢ (𝜑 →
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) gcd
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))) =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd ((𝐵 / 2) gcd
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 /
2))))) |
116 | 108 | nnzd 12425 |
. . . . . . . . . 10
⊢ (𝜑 →
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
∈ ℤ) |
117 | | gcdass 16255 |
. . . . . . . . . 10
⊢ (((𝐵 / 2) ∈ ℤ ∧
(𝐵 / 2) ∈ ℤ
∧ (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
∈ ℤ) → (((𝐵
/ 2) gcd (𝐵 / 2)) gcd
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2))
= ((𝐵 / 2) gcd ((𝐵 / 2) gcd
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) /
2)))) |
118 | 112, 112,
116, 117 | syl3anc 1370 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐵 / 2) gcd (𝐵 / 2)) gcd
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2))
= ((𝐵 / 2) gcd ((𝐵 / 2) gcd
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) /
2)))) |
119 | 42 | nnnn0d 12293 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 / 2) ∈
ℕ0) |
120 | | gcdnn0id 40329 |
. . . . . . . . . . . 12
⊢ ((𝐵 / 2) ∈ ℕ0
→ ((𝐵 / 2) gcd (𝐵 / 2)) = (𝐵 / 2)) |
121 | 119, 120 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 / 2) gcd (𝐵 / 2)) = (𝐵 / 2)) |
122 | 121 | oveq1d 7290 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐵 / 2) gcd (𝐵 / 2)) gcd
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2))
= ((𝐵 / 2) gcd
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) /
2))) |
123 | 112, 116 | gcdcomd 16221 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵 / 2) gcd
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2))
= ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 /
2))) |
124 | 122, 123 | eqtr2d 2779 |
. . . . . . . . 9
⊢ (𝜑 →
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) = (((𝐵 / 2) gcd (𝐵 / 2)) gcd
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) /
2))) |
125 | 116, 112 | gcdcomd 16221 |
. . . . . . . . . 10
⊢ (𝜑 →
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) = ((𝐵 / 2) gcd
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) /
2))) |
126 | 125 | oveq2d 7291 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 / 2) gcd
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))) = ((𝐵 / 2) gcd ((𝐵 / 2) gcd
(((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) /
2)))) |
127 | 118, 124,
126 | 3eqtr4rd 2789 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 / 2) gcd
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))) =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 /
2))) |
128 | 127 | oveq2d 7291 |
. . . . . . 7
⊢ (𝜑 →
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd ((𝐵 / 2) gcd
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)))) =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 /
2)))) |
129 | 38 | simp1d 1141 |
. . . . . . . . . 10
⊢ (𝜑 →
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2))
= 1 ∧ ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2)) = 1
∧ ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2)) =
1)) |
130 | 129 | simp1d 1141 |
. . . . . . . . 9
⊢ (𝜑 →
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2))
= 1) |
131 | 130 | oveq1d 7290 |
. . . . . . . 8
⊢ (𝜑 →
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2))
gcd (𝐵 / 2)) = (1 gcd
(𝐵 / 2))) |
132 | | gcdass 16255 |
. . . . . . . . 9
⊢
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
∈ ℤ ∧ (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
∈ ℤ ∧ (𝐵 /
2) ∈ ℤ) → (((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2))
gcd (𝐵 / 2)) =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 /
2)))) |
133 | 111, 116,
112, 132 | syl3anc 1370 |
. . . . . . . 8
⊢ (𝜑 →
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2))
gcd (𝐵 / 2)) =
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 /
2)))) |
134 | | 1gcd 16241 |
. . . . . . . . 9
⊢ ((𝐵 / 2) ∈ ℤ → (1
gcd (𝐵 / 2)) =
1) |
135 | 112, 134 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1 gcd (𝐵 / 2)) = 1) |
136 | 131, 133,
135 | 3eqtr3d 2786 |
. . . . . . 7
⊢ (𝜑 →
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))) =
1) |
137 | 115, 128,
136 | 3eqtrd 2782 |
. . . . . 6
⊢ (𝜑 →
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) gcd
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))) =
1) |
138 | 7, 8, 9, 10, 11, 12, 13, 14, 37, 24 | flt4lem5f 40494 |
. . . . . . 7
⊢ (𝜑 → (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2) =
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4) +
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 /
2))↑4))) |
139 | 138 | eqcomd 2744 |
. . . . . 6
⊢ (𝜑 →
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4) +
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4)) =
(((((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2) gcd
(𝐵 /
2))↑2)) |
140 | 137, 139 | jca 512 |
. . . . 5
⊢ (𝜑 →
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2)) gcd
((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))) = 1 ∧
((((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) +
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4) +
(((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) −
(√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) −
(((√‘(𝐶 +
(𝐵↑2))) −
(√‘(𝐶 −
(𝐵↑2)))) / 2)))) / 2)
gcd (𝐵 / 2))↑4)) =
(((((√‘(𝐶 +
(𝐵↑2))) +
(√‘(𝐶 −
(𝐵↑2)))) / 2) gcd
(𝐵 /
2))↑2))) |
141 | 98, 104, 107, 110, 140 | 2rspcedvdw 40180 |
. . . 4
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))) |
142 | 92, 141 | jca 512 |
. . 3
⊢ (𝜑 → (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2)))) |
143 | 6, 44, 142 | rspcedvdw 40179 |
. 2
⊢ (𝜑 → ∃𝑙 ∈ ℕ (𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)))) |
144 | | breq2 5078 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑚 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑚)) |
145 | 144 | notbid 318 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑚 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑚)) |
146 | | oveq1 7282 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑚 → (𝑔 gcd ℎ) = (𝑚 gcd ℎ)) |
147 | 146 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑚 → ((𝑔 gcd ℎ) = 1 ↔ (𝑚 gcd ℎ) = 1)) |
148 | | oveq1 7282 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑚 → (𝑔↑4) = (𝑚↑4)) |
149 | 148 | oveq1d 7290 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑚 → ((𝑔↑4) + (ℎ↑4)) = ((𝑚↑4) + (ℎ↑4))) |
150 | 149 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑚 → (((𝑔↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2))) |
151 | 147, 150 | anbi12d 631 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑚 → (((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2)))) |
152 | 145, 151 | anbi12d 631 |
. . . . . . . . 9
⊢ (𝑔 = 𝑚 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2))))) |
153 | | oveq2 7283 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑛 → (𝑚 gcd ℎ) = (𝑚 gcd 𝑛)) |
154 | 153 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑛 → ((𝑚 gcd ℎ) = 1 ↔ (𝑚 gcd 𝑛) = 1)) |
155 | | oveq1 7282 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝑛 → (ℎ↑4) = (𝑛↑4)) |
156 | 155 | oveq2d 7291 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑛 → ((𝑚↑4) + (ℎ↑4)) = ((𝑚↑4) + (𝑛↑4))) |
157 | 156 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑛 → (((𝑚↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) |
158 | 154, 157 | anbi12d 631 |
. . . . . . . . . 10
⊢ (ℎ = 𝑛 → (((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)))) |
159 | 158 | anbi2d 629 |
. . . . . . . . 9
⊢ (ℎ = 𝑛 → ((¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))))) |
160 | | simplrl 774 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → 𝑚 ∈ ℕ) |
161 | 160 | adantr 481 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → 𝑚 ∈ ℕ) |
162 | | simprr 770 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑛 ∈ ℕ) |
163 | 162 | ad2antrr 723 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → 𝑛 ∈ ℕ) |
164 | | simpr 485 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → ¬ 2 ∥ 𝑚) |
165 | | simplr 766 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) |
166 | 164, 165 | jca 512 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → (¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)))) |
167 | 152, 159,
161, 163, 166 | 2rspcedvdw 40180 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → ∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥
𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2)))) |
168 | | simp-4r 781 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → 𝑙 < 𝐶) |
169 | 167, 168 | jca 512 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥
𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)) |
170 | | breq2 5078 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑛 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑛)) |
171 | 170 | notbid 318 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑛 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑛)) |
172 | | oveq1 7282 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑛 → (𝑔 gcd ℎ) = (𝑛 gcd ℎ)) |
173 | 172 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑛 → ((𝑔 gcd ℎ) = 1 ↔ (𝑛 gcd ℎ) = 1)) |
174 | | oveq1 7282 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑛 → (𝑔↑4) = (𝑛↑4)) |
175 | 174 | oveq1d 7290 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑛 → ((𝑔↑4) + (ℎ↑4)) = ((𝑛↑4) + (ℎ↑4))) |
176 | 175 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑛 → (((𝑔↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2))) |
177 | 173, 176 | anbi12d 631 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑛 → (((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2)))) |
178 | 171, 177 | anbi12d 631 |
. . . . . . . . 9
⊢ (𝑔 = 𝑛 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2))))) |
179 | | oveq2 7283 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑚 → (𝑛 gcd ℎ) = (𝑛 gcd 𝑚)) |
180 | 179 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑚 → ((𝑛 gcd ℎ) = 1 ↔ (𝑛 gcd 𝑚) = 1)) |
181 | | oveq1 7282 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝑚 → (ℎ↑4) = (𝑚↑4)) |
182 | 181 | oveq2d 7291 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑚 → ((𝑛↑4) + (ℎ↑4)) = ((𝑛↑4) + (𝑚↑4))) |
183 | 182 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑚 → (((𝑛↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2))) |
184 | 180, 183 | anbi12d 631 |
. . . . . . . . . 10
⊢ (ℎ = 𝑚 → (((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑛 gcd 𝑚) = 1 ∧ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2)))) |
185 | 184 | anbi2d 629 |
. . . . . . . . 9
⊢ (ℎ = 𝑚 → ((¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd 𝑚) = 1 ∧ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2))))) |
186 | 162 | ad2antrr 723 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑛 ∈ ℕ) |
187 | 160 | adantr 481 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑚 ∈ ℕ) |
188 | | simpr 485 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ¬ 2 ∥ 𝑛) |
189 | 186 | nnzd 12425 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑛 ∈ ℤ) |
190 | 187 | nnzd 12425 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑚 ∈ ℤ) |
191 | 189, 190 | gcdcomd 16221 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛 gcd 𝑚) = (𝑚 gcd 𝑛)) |
192 | | simplrl 774 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑚 gcd 𝑛) = 1) |
193 | 191, 192 | eqtrd 2778 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛 gcd 𝑚) = 1) |
194 | 55 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 4 ∈
ℕ0) |
195 | 186, 194 | nnexpcld 13960 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛↑4) ∈ ℕ) |
196 | 195 | nncnd 11989 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛↑4) ∈ ℂ) |
197 | 187, 194 | nnexpcld 13960 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑚↑4) ∈ ℕ) |
198 | 197 | nncnd 11989 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑚↑4) ∈ ℂ) |
199 | 196, 198 | addcomd 11177 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ((𝑛↑4) + (𝑚↑4)) = ((𝑚↑4) + (𝑛↑4))) |
200 | | simplrr 775 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) |
201 | 199, 200 | eqtrd 2778 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2)) |
202 | 188, 193,
201 | jca32 516 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd 𝑚) = 1 ∧ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2)))) |
203 | 178, 185,
186, 187, 202 | 2rspcedvdw 40180 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥
𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2)))) |
204 | | simp-4r 781 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑙 < 𝐶) |
205 | 203, 204 | jca 512 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥
𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)) |
206 | | simprl 768 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑚 ∈ ℕ) |
207 | 206 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑚 ∈ ℕ) |
208 | 207 | nnsqcld 13959 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑚↑2) ∈ ℕ) |
209 | 162 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑛 ∈ ℕ) |
210 | 209 | nnsqcld 13959 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑛↑2) ∈ ℕ) |
211 | | simp-5r 783 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑙 ∈ ℕ) |
212 | 160 | nnzd 12425 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → 𝑚 ∈ ℤ) |
213 | 27 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → 2 ∈
ℕ) |
214 | | dvdsexp2im 16036 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℤ ∧ 𝑚
∈ ℤ ∧ 2 ∈ ℕ) → (2 ∥ 𝑚 → 2 ∥ (𝑚↑2))) |
215 | 62, 212, 213, 214 | mp3an2i 1465 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (2 ∥ 𝑚 → 2 ∥ (𝑚↑2))) |
216 | 215 | imp 407 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 2 ∥ (𝑚↑2)) |
217 | 17 | a1i 11 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 2 ∈
ℕ0) |
218 | 207 | nncnd 11989 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑚 ∈ ℂ) |
219 | 218 | flt4lem 40482 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑚↑4) = ((𝑚↑2)↑2)) |
220 | 209 | nncnd 11989 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑛 ∈ ℂ) |
221 | 220 | flt4lem 40482 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑛↑4) = ((𝑛↑2)↑2)) |
222 | 219, 221 | oveq12d 7293 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑4) + (𝑛↑4)) = (((𝑚↑2)↑2) + ((𝑛↑2)↑2))) |
223 | | simplrr 775 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) |
224 | 222, 223 | eqtr3d 2780 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (((𝑚↑2)↑2) + ((𝑛↑2)↑2)) = (𝑙↑2)) |
225 | | simplrl 774 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑚 gcd 𝑛) = 1) |
226 | 27 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 2 ∈ ℕ) |
227 | | rppwr 16269 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ∧ 2 ∈
ℕ) → ((𝑚 gcd
𝑛) = 1 → ((𝑚↑2) gcd (𝑛↑2)) = 1)) |
228 | 207, 209,
226, 227 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚 gcd 𝑛) = 1 → ((𝑚↑2) gcd (𝑛↑2)) = 1)) |
229 | 225, 228 | mpd 15 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑2) gcd (𝑛↑2)) = 1) |
230 | 208, 210,
211, 217, 224, 229 | fltaccoprm 40477 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑2) gcd 𝑙) = 1) |
231 | 208, 210,
211, 216, 230, 224 | flt4lem2 40484 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ¬ 2 ∥ (𝑛↑2)) |
232 | 209 | nnzd 12425 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑛 ∈ ℤ) |
233 | | dvdsexp2im 16036 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 𝑛
∈ ℤ ∧ 2 ∈ ℕ) → (2 ∥ 𝑛 → 2 ∥ (𝑛↑2))) |
234 | 62, 232, 226, 233 | mp3an2i 1465 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (2 ∥ 𝑛 → 2 ∥ (𝑛↑2))) |
235 | 231, 234 | mtod 197 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ¬ 2 ∥ 𝑛) |
236 | 235 | ex 413 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (2 ∥ 𝑚 → ¬ 2 ∥ 𝑛)) |
237 | | imor 850 |
. . . . . . . 8
⊢ ((2
∥ 𝑚 → ¬ 2
∥ 𝑛) ↔ (¬ 2
∥ 𝑚 ∨ ¬ 2
∥ 𝑛)) |
238 | 236, 237 | sylib 217 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (¬ 2 ∥ 𝑚 ∨ ¬ 2 ∥ 𝑛)) |
239 | 169, 205,
238 | mpjaodan 956 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)) |
240 | 239 | ex 413 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))) |
241 | 240 | rexlimdvva 3223 |
. . . 4
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) → (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))) |
242 | 241 | expimpd 454 |
. . 3
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))) |
243 | 242 | reximdva 3203 |
. 2
⊢ (𝜑 → (∃𝑙 ∈ ℕ (𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))) |
244 | 143, 243 | mpd 15 |
1
⊢ (𝜑 → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)) |