Users' Mathboxes Mathbox for Steven Nguyen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  flt4lem7 Structured version   Visualization version   GIF version

Theorem flt4lem7 41283
Description: Convert flt4lem5f 41281 into a convenient form for nna4b4nsq 41284. TODO-SN: The change to (𝐴 gcd 𝐵) = 1 points at some inefficiency in the lemmas. (Contributed by SN, 25-Aug-2024.)
Hypotheses
Ref Expression
flt4lem7.a (𝜑𝐴 ∈ ℕ)
flt4lem7.b (𝜑𝐵 ∈ ℕ)
flt4lem7.c (𝜑𝐶 ∈ ℕ)
flt4lem7.1 (𝜑 → ¬ 2 ∥ 𝐴)
flt4lem7.2 (𝜑 → (𝐴 gcd 𝐵) = 1)
flt4lem7.3 (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))
Assertion
Ref Expression
flt4lem7 (𝜑 → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
Distinct variable groups:   𝜑,𝑙   𝐵,𝑙   𝐶,𝑙   𝑔,,𝑙
Allowed substitution hints:   𝜑(𝑔,)   𝐴(𝑔,,𝑙)   𝐵(𝑔,)   𝐶(𝑔,)

Proof of Theorem flt4lem7
Dummy variables 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq1 5147 . . . 4 (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (𝑙 < 𝐶 ↔ ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶))
2 oveq1 7403 . . . . . . 7 (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (𝑙↑2) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))
32eqeq2d 2744 . . . . . 6 (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (((𝑚↑4) + (𝑛↑4)) = (𝑙↑2) ↔ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2)))
43anbi2d 630 . . . . 5 (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) ↔ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))))
542rexbidv 3220 . . . 4 (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) ↔ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))))
61, 5anbi12d 632 . . 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 2733 . . . . . . 7 (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)
8 eqid 2733 . . . . . . 7 (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2) = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)
9 eqid 2733 . . . . . . 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 2733 . . . . . . 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 ∥ 𝐴)
1511nnsqcld 14194 . . . . . . . . 9 (𝜑 → (𝐴↑2) ∈ ℕ)
1612nnsqcld 14194 . . . . . . . . 9 (𝜑 → (𝐵↑2) ∈ ℕ)
17 2nn0 12476 . . . . . . . . . 10 2 ∈ ℕ0
1817a1i 11 . . . . . . . . 9 (𝜑 → 2 ∈ ℕ0)
1911nncnd 12215 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
2019flt4lem 41269 . . . . . . . . . . 11 (𝜑 → (𝐴↑4) = ((𝐴↑2)↑2))
2112nncnd 12215 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℂ)
2221flt4lem 41269 . . . . . . . . . . 11 (𝜑 → (𝐵↑4) = ((𝐵↑2)↑2))
2320, 22oveq12d 7414 . . . . . . . . . 10 (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (((𝐴↑2)↑2) + ((𝐵↑2)↑2)))
24 flt4lem7.3 . . . . . . . . . 10 (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))
2523, 24eqtr3d 2775 . . . . . . . . 9 (𝜑 → (((𝐴↑2)↑2) + ((𝐵↑2)↑2)) = (𝐶↑2))
26 flt4lem7.2 . . . . . . . . . 10 (𝜑 → (𝐴 gcd 𝐵) = 1)
27 2nn 12272 . . . . . . . . . . . 12 2 ∈ ℕ
2827a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℕ)
29 rppwr 16488 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 2 ∈ ℕ) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑2) gcd (𝐵↑2)) = 1))
3011, 12, 28, 29syl3anc 1372 . . . . . . . . . 10 (𝜑 → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑2) gcd (𝐵↑2)) = 1))
3126, 30mpd 15 . . . . . . . . 9 (𝜑 → ((𝐴↑2) gcd (𝐵↑2)) = 1)
3215, 16, 13, 18, 25, 31fltaccoprm 41264 . . . . . . . 8 (𝜑 → ((𝐴↑2) gcd 𝐶) = 1)
3311nnzd 12572 . . . . . . . . 9 (𝜑𝐴 ∈ ℤ)
3413nnzd 12572 . . . . . . . . 9 (𝜑𝐶 ∈ ℤ)
35 rpexp 16646 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 2 ∈ ℕ) → (((𝐴↑2) gcd 𝐶) = 1 ↔ (𝐴 gcd 𝐶) = 1))
3633, 34, 28, 35syl3anc 1372 . . . . . . . 8 (𝜑 → (((𝐴↑2) gcd 𝐶) = 1 ↔ (𝐴 gcd 𝐶) = 1))
3732, 36mpbid 231 . . . . . . 7 (𝜑 → (𝐴 gcd 𝐶) = 1)
387, 8, 9, 10, 11, 12, 13, 14, 37, 24flt4lem5e 41280 . . . . . 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) ∈ ℕ)))
3938simp2d 1144 . . . . 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) ∈ ℕ))
4039simp3d 1145 . . . 4 (𝜑 → (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈ ℕ)
4138simp3d 1145 . . . . 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) ∈ ℕ))
4241simprd 497 . . . 4 (𝜑 → (𝐵 / 2) ∈ ℕ)
43 gcdnncl 16435 . . . 4 (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈ ℕ ∧ (𝐵 / 2) ∈ ℕ) → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
4440, 42, 43syl2anc 585 . . 3 (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
4544nnred 12214 . . . . 5 (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ∈ ℝ)
4642nnred 12214 . . . . 5 (𝜑 → (𝐵 / 2) ∈ ℝ)
4713nnred 12214 . . . . 5 (𝜑𝐶 ∈ ℝ)
4840nnzd 12572 . . . . . 6 (𝜑 → (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈ ℤ)
4948, 42gcdle2d 41103 . . . . 5 (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ≤ (𝐵 / 2))
5012nnred 12214 . . . . . 6 (𝜑𝐵 ∈ ℝ)
5112nnrpd 13001 . . . . . . 7 (𝜑𝐵 ∈ ℝ+)
52 rphalflt 12990 . . . . . . 7 (𝐵 ∈ ℝ+ → (𝐵 / 2) < 𝐵)
5351, 52syl 17 . . . . . 6 (𝜑 → (𝐵 / 2) < 𝐵)
5416nnred 12214 . . . . . . . 8 (𝜑 → (𝐵↑2) ∈ ℝ)
55 4nn0 12478 . . . . . . . . . . 11 4 ∈ ℕ0
5655a1i 11 . . . . . . . . . 10 (𝜑 → 4 ∈ ℕ0)
5712, 56nnexpcld 14195 . . . . . . . . 9 (𝜑 → (𝐵↑4) ∈ ℕ)
5857nnred 12214 . . . . . . . 8 (𝜑 → (𝐵↑4) ∈ ℝ)
5913nnsqcld 14194 . . . . . . . . 9 (𝜑 → (𝐶↑2) ∈ ℕ)
6059nnred 12214 . . . . . . . 8 (𝜑 → (𝐶↑2) ∈ ℝ)
61 2lt4 12374 . . . . . . . . 9 2 < 4
62 2z 12581 . . . . . . . . . . 11 2 ∈ ℤ
6362a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℤ)
64 4z 12583 . . . . . . . . . . 11 4 ∈ ℤ
6564a1i 11 . . . . . . . . . 10 (𝜑 → 4 ∈ ℤ)
66 1red 11202 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℝ)
67 2re 12273 . . . . . . . . . . . 12 2 ∈ ℝ
6867a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℝ)
69 1lt2 12370 . . . . . . . . . . . 12 1 < 2
7069a1i 11 . . . . . . . . . . 11 (𝜑 → 1 < 2)
71 2t1e2 12362 . . . . . . . . . . . 12 (2 · 1) = 2
7242nnge1d 12247 . . . . . . . . . . . . 13 (𝜑 → 1 ≤ (𝐵 / 2))
73 2rp 12966 . . . . . . . . . . . . . . 15 2 ∈ ℝ+
7473a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℝ+)
7566, 50, 74lemuldiv2d 13053 . . . . . . . . . . . . 13 (𝜑 → ((2 · 1) ≤ 𝐵 ↔ 1 ≤ (𝐵 / 2)))
7672, 75mpbird 257 . . . . . . . . . . . 12 (𝜑 → (2 · 1) ≤ 𝐵)
7771, 76eqbrtrrid 5180 . . . . . . . . . . 11 (𝜑 → 2 ≤ 𝐵)
7866, 68, 50, 70, 77ltletrd 11361 . . . . . . . . . 10 (𝜑 → 1 < 𝐵)
7950, 63, 65, 78ltexp2d 14201 . . . . . . . . 9 (𝜑 → (2 < 4 ↔ (𝐵↑2) < (𝐵↑4)))
8061, 79mpbii 232 . . . . . . . 8 (𝜑 → (𝐵↑2) < (𝐵↑4))
8111, 56nnexpcld 14195 . . . . . . . . . . 11 (𝜑 → (𝐴↑4) ∈ ℕ)
8281nngt0d 12248 . . . . . . . . . 10 (𝜑 → 0 < (𝐴↑4))
8381nnred 12214 . . . . . . . . . . 11 (𝜑 → (𝐴↑4) ∈ ℝ)
8483, 58ltaddpos2d 11786 . . . . . . . . . 10 (𝜑 → (0 < (𝐴↑4) ↔ (𝐵↑4) < ((𝐴↑4) + (𝐵↑4))))
8582, 84mpbid 231 . . . . . . . . 9 (𝜑 → (𝐵↑4) < ((𝐴↑4) + (𝐵↑4)))
8685, 24breqtrd 5170 . . . . . . . 8 (𝜑 → (𝐵↑4) < (𝐶↑2))
8754, 58, 60, 80, 86lttrd 11362 . . . . . . 7 (𝜑 → (𝐵↑2) < (𝐶↑2))
8813nnrpd 13001 . . . . . . . 8 (𝜑𝐶 ∈ ℝ+)
8951, 88, 28ltexp1d 41094 . . . . . . 7 (𝜑 → (𝐵 < 𝐶 ↔ (𝐵↑2) < (𝐶↑2)))
9087, 89mpbird 257 . . . . . 6 (𝜑𝐵 < 𝐶)
9146, 50, 47, 53, 90lttrd 11362 . . . . 5 (𝜑 → (𝐵 / 2) < 𝐶)
9245, 46, 47, 49, 91lelttrd 11359 . . . 4 (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶)
93 oveq1 7403 . . . . . . 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 𝑛))
9493eqeq1d 2735 . . . . . 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 7403 . . . . . . . 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))
9695oveq1d 7411 . . . . . . 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)))
9796eqeq1d 2735 . . . . . 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)))
9894, 97anbi12d 632 . . . . 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 7404 . . . . . . 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))))
10099eqeq1d 2735 . . . . . 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 7403 . . . . . . . 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))
102101oveq2d 7412 . . . . . . 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)))
103102eqeq1d 2735 . . . . . 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)))
104100, 103anbi12d 632 . . . . 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))))
10539simp1d 1143 . . . . . 6 (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) + (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℕ)
106 gcdnncl 16435 . . . . . 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)) ∈ ℕ)
107105, 42, 106syl2anc 585 . . . . 5 (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) + (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
10839simp2d 1144 . . . . . 6 (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℕ)
109 gcdnncl 16435 . . . . . 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)) ∈ ℕ)
110108, 42, 109syl2anc 585 . . . . 5 (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
111105nnzd 12572 . . . . . . . 8 (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) + (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℤ)
11242nnzd 12572 . . . . . . . 8 (𝜑 → (𝐵 / 2) ∈ ℤ)
113110nnzd 12572 . . . . . . . 8 (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) gcd (𝐵 / 2)) ∈ ℤ)
114 gcdass 16476 . . . . . . . 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)))))
115111, 112, 113, 114syl3anc 1372 . . . . . . 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)))))
116108nnzd 12572 . . . . . . . . . 10 (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℤ)
117 gcdass 16476 . . . . . . . . . 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))))
118112, 112, 116, 117syl3anc 1372 . . . . . . . . 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))))
11942nnnn0d 12519 . . . . . . . . . . . 12 (𝜑 → (𝐵 / 2) ∈ ℕ0)
120 gcdnn0id 41101 . . . . . . . . . . . 12 ((𝐵 / 2) ∈ ℕ0 → ((𝐵 / 2) gcd (𝐵 / 2)) = (𝐵 / 2))
121119, 120syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐵 / 2) gcd (𝐵 / 2)) = (𝐵 / 2))
122121oveq1d 7411 . . . . . . . . . 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)))
123112, 116gcdcomd 16442 . . . . . . . . . 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)))
124122, 123eqtr2d 2774 . . . . . . . . 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)))
125116, 112gcdcomd 16442 . . . . . . . . . 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)))
126125oveq2d 7412 . . . . . . . . 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))))
127118, 124, 1263eqtr4rd 2784 . . . . . . . 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)))
128127oveq2d 7412 . . . . . . 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))))
12938simp1d 1143 . . . . . . . . . 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))
130129simp1d 1143 . . . . . . . . 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)
131130oveq1d 7411 . . . . . . . 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 16476 . . . . . . . . 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))))
133111, 116, 112, 132syl3anc 1372 . . . . . . . 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 16462 . . . . . . . . 9 ((𝐵 / 2) ∈ ℤ → (1 gcd (𝐵 / 2)) = 1)
135112, 134syl 17 . . . . . . . 8 (𝜑 → (1 gcd (𝐵 / 2)) = 1)
136131, 133, 1353eqtr3d 2781 . . . . . . 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)
137115, 128, 1363eqtrd 2777 . . . . . 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)
1387, 8, 9, 10, 11, 12, 13, 14, 37, 24flt4lem5f 41281 . . . . . . 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)))
139138eqcomd 2739 . . . . . 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))
140137, 139jca 513 . . . . 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)))
14198, 104, 107, 110, 1402rspcedvdw 3623 . . . 4 (𝜑 → ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2)))
14292, 141jca 513 . . 3 (𝜑 → (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))))
1436, 44, 142rspcedvdw 40945 . 2 (𝜑 → ∃𝑙 ∈ ℕ (𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))))
144 breq2 5148 . . . . . . . . . . 11 (𝑔 = 𝑚 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑚))
145144notbid 318 . . . . . . . . . 10 (𝑔 = 𝑚 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑚))
146 oveq1 7403 . . . . . . . . . . . 12 (𝑔 = 𝑚 → (𝑔 gcd ) = (𝑚 gcd ))
147146eqeq1d 2735 . . . . . . . . . . 11 (𝑔 = 𝑚 → ((𝑔 gcd ) = 1 ↔ (𝑚 gcd ) = 1))
148 oveq1 7403 . . . . . . . . . . . . 13 (𝑔 = 𝑚 → (𝑔↑4) = (𝑚↑4))
149148oveq1d 7411 . . . . . . . . . . . 12 (𝑔 = 𝑚 → ((𝑔↑4) + (↑4)) = ((𝑚↑4) + (↑4)))
150149eqeq1d 2735 . . . . . . . . . . 11 (𝑔 = 𝑚 → (((𝑔↑4) + (↑4)) = (𝑙↑2) ↔ ((𝑚↑4) + (↑4)) = (𝑙↑2)))
151147, 150anbi12d 632 . . . . . . . . . 10 (𝑔 = 𝑚 → (((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2)) ↔ ((𝑚 gcd ) = 1 ∧ ((𝑚↑4) + (↑4)) = (𝑙↑2))))
152145, 151anbi12d 632 . . . . . . . . 9 (𝑔 = 𝑚 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd ) = 1 ∧ ((𝑚↑4) + (↑4)) = (𝑙↑2)))))
153 oveq2 7404 . . . . . . . . . . . 12 ( = 𝑛 → (𝑚 gcd ) = (𝑚 gcd 𝑛))
154153eqeq1d 2735 . . . . . . . . . . 11 ( = 𝑛 → ((𝑚 gcd ) = 1 ↔ (𝑚 gcd 𝑛) = 1))
155 oveq1 7403 . . . . . . . . . . . . 13 ( = 𝑛 → (↑4) = (𝑛↑4))
156155oveq2d 7412 . . . . . . . . . . . 12 ( = 𝑛 → ((𝑚↑4) + (↑4)) = ((𝑚↑4) + (𝑛↑4)))
157156eqeq1d 2735 . . . . . . . . . . 11 ( = 𝑛 → (((𝑚↑4) + (↑4)) = (𝑙↑2) ↔ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)))
158154, 157anbi12d 632 . . . . . . . . . 10 ( = 𝑛 → (((𝑚 gcd ) = 1 ∧ ((𝑚↑4) + (↑4)) = (𝑙↑2)) ↔ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))))
159158anbi2d 630 . . . . . . . . 9 ( = 𝑛 → ((¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd ) = 1 ∧ ((𝑚↑4) + (↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)))))
160 simplrl 776 . . . . . . . . . 10 (((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → 𝑚 ∈ ℕ)
161160adantr 482 . . . . . . . . 9 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → 𝑚 ∈ ℕ)
162 simprr 772 . . . . . . . . . 10 ((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑛 ∈ ℕ)
163162ad2antrr 725 . . . . . . . . 9 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → 𝑛 ∈ ℕ)
164 simpr 486 . . . . . . . . . 10 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → ¬ 2 ∥ 𝑚)
165 simplr 768 . . . . . . . . . 10 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)))
166164, 165jca 513 . . . . . . . . 9 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → (¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))))
167152, 159, 161, 163, 1662rspcedvdw 3623 . . . . . . . 8 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))))
168 simp-4r 783 . . . . . . . 8 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → 𝑙 < 𝐶)
169167, 168jca 513 . . . . . . 7 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
170 breq2 5148 . . . . . . . . . . 11 (𝑔 = 𝑛 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑛))
171170notbid 318 . . . . . . . . . 10 (𝑔 = 𝑛 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑛))
172 oveq1 7403 . . . . . . . . . . . 12 (𝑔 = 𝑛 → (𝑔 gcd ) = (𝑛 gcd ))
173172eqeq1d 2735 . . . . . . . . . . 11 (𝑔 = 𝑛 → ((𝑔 gcd ) = 1 ↔ (𝑛 gcd ) = 1))
174 oveq1 7403 . . . . . . . . . . . . 13 (𝑔 = 𝑛 → (𝑔↑4) = (𝑛↑4))
175174oveq1d 7411 . . . . . . . . . . . 12 (𝑔 = 𝑛 → ((𝑔↑4) + (↑4)) = ((𝑛↑4) + (↑4)))
176175eqeq1d 2735 . . . . . . . . . . 11 (𝑔 = 𝑛 → (((𝑔↑4) + (↑4)) = (𝑙↑2) ↔ ((𝑛↑4) + (↑4)) = (𝑙↑2)))
177173, 176anbi12d 632 . . . . . . . . . 10 (𝑔 = 𝑛 → (((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2)) ↔ ((𝑛 gcd ) = 1 ∧ ((𝑛↑4) + (↑4)) = (𝑙↑2))))
178171, 177anbi12d 632 . . . . . . . . 9 (𝑔 = 𝑛 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd ) = 1 ∧ ((𝑛↑4) + (↑4)) = (𝑙↑2)))))
179 oveq2 7404 . . . . . . . . . . . 12 ( = 𝑚 → (𝑛 gcd ) = (𝑛 gcd 𝑚))
180179eqeq1d 2735 . . . . . . . . . . 11 ( = 𝑚 → ((𝑛 gcd ) = 1 ↔ (𝑛 gcd 𝑚) = 1))
181 oveq1 7403 . . . . . . . . . . . . 13 ( = 𝑚 → (↑4) = (𝑚↑4))
182181oveq2d 7412 . . . . . . . . . . . 12 ( = 𝑚 → ((𝑛↑4) + (↑4)) = ((𝑛↑4) + (𝑚↑4)))
183182eqeq1d 2735 . . . . . . . . . . 11 ( = 𝑚 → (((𝑛↑4) + (↑4)) = (𝑙↑2) ↔ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2)))
184180, 183anbi12d 632 . . . . . . . . . 10 ( = 𝑚 → (((𝑛 gcd ) = 1 ∧ ((𝑛↑4) + (↑4)) = (𝑙↑2)) ↔ ((𝑛 gcd 𝑚) = 1 ∧ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2))))
185184anbi2d 630 . . . . . . . . 9 ( = 𝑚 → ((¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd ) = 1 ∧ ((𝑛↑4) + (↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd 𝑚) = 1 ∧ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2)))))
186162ad2antrr 725 . . . . . . . . 9 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑛 ∈ ℕ)
187160adantr 482 . . . . . . . . 9 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑚 ∈ ℕ)
188 simpr 486 . . . . . . . . . 10 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ¬ 2 ∥ 𝑛)
189186nnzd 12572 . . . . . . . . . . . 12 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑛 ∈ ℤ)
190187nnzd 12572 . . . . . . . . . . . 12 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑚 ∈ ℤ)
191189, 190gcdcomd 16442 . . . . . . . . . . 11 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛 gcd 𝑚) = (𝑚 gcd 𝑛))
192 simplrl 776 . . . . . . . . . . 11 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑚 gcd 𝑛) = 1)
193191, 192eqtrd 2773 . . . . . . . . . 10 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛 gcd 𝑚) = 1)
19455a1i 11 . . . . . . . . . . . . . 14 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 4 ∈ ℕ0)
195186, 194nnexpcld 14195 . . . . . . . . . . . . 13 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛↑4) ∈ ℕ)
196195nncnd 12215 . . . . . . . . . . . 12 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛↑4) ∈ ℂ)
197187, 194nnexpcld 14195 . . . . . . . . . . . . 13 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑚↑4) ∈ ℕ)
198197nncnd 12215 . . . . . . . . . . . 12 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑚↑4) ∈ ℂ)
199196, 198addcomd 11403 . . . . . . . . . . 11 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ((𝑛↑4) + (𝑚↑4)) = ((𝑚↑4) + (𝑛↑4)))
200 simplrr 777 . . . . . . . . . . 11 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))
201199, 200eqtrd 2773 . . . . . . . . . 10 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2))
202188, 193, 201jca32 517 . . . . . . . . 9 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd 𝑚) = 1 ∧ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2))))
203178, 185, 186, 187, 2022rspcedvdw 3623 . . . . . . . 8 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))))
204 simp-4r 783 . . . . . . . 8 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑙 < 𝐶)
205203, 204jca 513 . . . . . . 7 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
206 simprl 770 . . . . . . . . . . . . 13 ((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑚 ∈ ℕ)
207206ad2antrr 725 . . . . . . . . . . . 12 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑚 ∈ ℕ)
208207nnsqcld 14194 . . . . . . . . . . 11 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑚↑2) ∈ ℕ)
209162ad2antrr 725 . . . . . . . . . . . 12 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑛 ∈ ℕ)
210209nnsqcld 14194 . . . . . . . . . . 11 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑛↑2) ∈ ℕ)
211 simp-5r 785 . . . . . . . . . . 11 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑙 ∈ ℕ)
212160nnzd 12572 . . . . . . . . . . . . 13 (((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → 𝑚 ∈ ℤ)
21327a1i 11 . . . . . . . . . . . . 13 (((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → 2 ∈ ℕ)
214 dvdsexp2im 16257 . . . . . . . . . . . . 13 ((2 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 2 ∈ ℕ) → (2 ∥ 𝑚 → 2 ∥ (𝑚↑2)))
21562, 212, 213, 214mp3an2i 1467 . . . . . . . . . . . 12 (((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (2 ∥ 𝑚 → 2 ∥ (𝑚↑2)))
216215imp 408 . . . . . . . . . . 11 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 2 ∥ (𝑚↑2))
21717a1i 11 . . . . . . . . . . . 12 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 2 ∈ ℕ0)
218207nncnd 12215 . . . . . . . . . . . . . . 15 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑚 ∈ ℂ)
219218flt4lem 41269 . . . . . . . . . . . . . 14 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑚↑4) = ((𝑚↑2)↑2))
220209nncnd 12215 . . . . . . . . . . . . . . 15 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑛 ∈ ℂ)
221220flt4lem 41269 . . . . . . . . . . . . . 14 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑛↑4) = ((𝑛↑2)↑2))
222219, 221oveq12d 7414 . . . . . . . . . . . . 13 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑4) + (𝑛↑4)) = (((𝑚↑2)↑2) + ((𝑛↑2)↑2)))
223 simplrr 777 . . . . . . . . . . . . 13 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))
224222, 223eqtr3d 2775 . . . . . . . . . . . 12 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (((𝑚↑2)↑2) + ((𝑛↑2)↑2)) = (𝑙↑2))
225 simplrl 776 . . . . . . . . . . . . 13 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑚 gcd 𝑛) = 1)
22627a1i 11 . . . . . . . . . . . . . 14 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 2 ∈ ℕ)
227 rppwr 16488 . . . . . . . . . . . . . 14 ((𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ∧ 2 ∈ ℕ) → ((𝑚 gcd 𝑛) = 1 → ((𝑚↑2) gcd (𝑛↑2)) = 1))
228207, 209, 226, 227syl3anc 1372 . . . . . . . . . . . . 13 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚 gcd 𝑛) = 1 → ((𝑚↑2) gcd (𝑛↑2)) = 1))
229225, 228mpd 15 . . . . . . . . . . . 12 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑2) gcd (𝑛↑2)) = 1)
230208, 210, 211, 217, 224, 229fltaccoprm 41264 . . . . . . . . . . 11 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑2) gcd 𝑙) = 1)
231208, 210, 211, 216, 230, 224flt4lem2 41271 . . . . . . . . . 10 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ¬ 2 ∥ (𝑛↑2))
232209nnzd 12572 . . . . . . . . . . 11 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑛 ∈ ℤ)
233 dvdsexp2im 16257 . . . . . . . . . . 11 ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 2 ∈ ℕ) → (2 ∥ 𝑛 → 2 ∥ (𝑛↑2)))
23462, 232, 226, 233mp3an2i 1467 . . . . . . . . . 10 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (2 ∥ 𝑛 → 2 ∥ (𝑛↑2)))
235231, 234mtod 197 . . . . . . . . 9 ((((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ¬ 2 ∥ 𝑛)
236235ex 414 . . . . . . . 8 (((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (2 ∥ 𝑚 → ¬ 2 ∥ 𝑛))
237 imor 852 . . . . . . . 8 ((2 ∥ 𝑚 → ¬ 2 ∥ 𝑛) ↔ (¬ 2 ∥ 𝑚 ∨ ¬ 2 ∥ 𝑛))
238236, 237sylib 217 . . . . . . 7 (((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (¬ 2 ∥ 𝑚 ∨ ¬ 2 ∥ 𝑛))
239169, 205, 238mpjaodan 958 . . . . . 6 (((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
240239ex 414 . . . . 5 ((((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) → (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
241240rexlimdvva 3212 . . . 4 (((𝜑𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) → (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) → (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
242241expimpd 455 . . 3 ((𝜑𝑙 ∈ ℕ) → ((𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
243242reximdva 3169 . 2 (𝜑 → (∃𝑙 ∈ ℕ (𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
244143, 243mpd 15 1 (𝜑 → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846  w3a 1088   = wceq 1542  wcel 2107  wrex 3071   class class class wbr 5144  cfv 6535  (class class class)co 7396  cr 11096  0cc0 11097  1c1 11098   + caddc 11100   · cmul 11102   < clt 11235  cle 11236  cmin 11431   / cdiv 11858  cn 12199  2c2 12254  4c4 12256  0cn0 12459  cz 12545  +crp 12961  cexp 14014  csqrt 15167  cdvds 16184   gcd cgcd 16422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5295  ax-nul 5302  ax-pow 5359  ax-pr 5423  ax-un 7712  ax-cnex 11153  ax-resscn 11154  ax-1cn 11155  ax-icn 11156  ax-addcl 11157  ax-addrcl 11158  ax-mulcl 11159  ax-mulrcl 11160  ax-mulcom 11161  ax-addass 11162  ax-mulass 11163  ax-distr 11164  ax-i2m1 11165  ax-1ne0 11166  ax-1rid 11167  ax-rnegex 11168  ax-rrecex 11169  ax-cnre 11170  ax-pre-lttri 11171  ax-pre-lttrn 11172  ax-pre-ltadd 11173  ax-pre-mulgt0 11174  ax-pre-sup 11175
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4905  df-iun 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6292  df-ord 6359  df-on 6360  df-lim 6361  df-suc 6362  df-iota 6487  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-riota 7352  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7843  df-1st 7962  df-2nd 7963  df-frecs 8253  df-wrecs 8284  df-recs 8358  df-rdg 8397  df-1o 8453  df-2o 8454  df-er 8691  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-sup 9424  df-inf 9425  df-pnf 11237  df-mnf 11238  df-xr 11239  df-ltxr 11240  df-le 11241  df-sub 11433  df-neg 11434  df-div 11859  df-nn 12200  df-2 12262  df-3 12263  df-4 12264  df-n0 12460  df-z 12546  df-uz 12810  df-q 12920  df-rp 12962  df-fz 13472  df-fl 13744  df-mod 13822  df-seq 13954  df-exp 14015  df-cj 15033  df-re 15034  df-im 15035  df-sqrt 15169  df-abs 15170  df-dvds 16185  df-gcd 16423  df-prm 16596  df-numer 16658  df-denom 16659
This theorem is referenced by:  nna4b4nsq  41284
  Copyright terms: Public domain W3C validator