MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2sqreunnlem1 Structured version   Visualization version   GIF version

Theorem 2sqreunnlem1 27298
Description: Lemma 1 for 2sqreunn 27306. (Contributed by AV, 11-Jun-2023.)
Assertion
Ref Expression
2sqreunnlem1 ((𝑃 ∈ β„™ ∧ (𝑃 mod 4) = 1) β†’ βˆƒ!π‘Ž ∈ β„• βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃))
Distinct variable group:   𝑃,π‘Ž,𝑏

Proof of Theorem 2sqreunnlem1
Dummy variables 𝑐 π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2sqnn 27288 . . 3 ((𝑃 ∈ β„™ ∧ (𝑃 mod 4) = 1) β†’ βˆƒπ‘₯ ∈ β„• βˆƒπ‘¦ ∈ β„• 𝑃 = ((π‘₯↑2) + (𝑦↑2)))
2 simpll 764 . . . . . . . . 9 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2))) β†’ π‘₯ ∈ β„•)
32adantl 481 . . . . . . . 8 ((π‘₯ ≀ 𝑦 ∧ ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2)))) β†’ π‘₯ ∈ β„•)
4 breq1 5141 . . . . . . . . . . 11 (π‘Ž = π‘₯ β†’ (π‘Ž ≀ 𝑏 ↔ π‘₯ ≀ 𝑏))
5 oveq1 7408 . . . . . . . . . . . . 13 (π‘Ž = π‘₯ β†’ (π‘Žβ†‘2) = (π‘₯↑2))
65oveq1d 7416 . . . . . . . . . . . 12 (π‘Ž = π‘₯ β†’ ((π‘Žβ†‘2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑏↑2)))
76eqeq1d 2726 . . . . . . . . . . 11 (π‘Ž = π‘₯ β†’ (((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃 ↔ ((π‘₯↑2) + (𝑏↑2)) = 𝑃))
84, 7anbi12d 630 . . . . . . . . . 10 (π‘Ž = π‘₯ β†’ ((π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) ↔ (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = 𝑃)))
98reubidv 3386 . . . . . . . . 9 (π‘Ž = π‘₯ β†’ (βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) ↔ βˆƒ!𝑏 ∈ β„• (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = 𝑃)))
109adantl 481 . . . . . . . 8 (((π‘₯ ≀ 𝑦 ∧ ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2)))) ∧ π‘Ž = π‘₯) β†’ (βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) ↔ βˆƒ!𝑏 ∈ β„• (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = 𝑃)))
11 simpr 484 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ 𝑦 ∈ β„•)
1211adantr 480 . . . . . . . . . . . . . 14 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) β†’ 𝑦 ∈ β„•)
13 breq2 5142 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑦 β†’ (π‘₯ ≀ 𝑏 ↔ π‘₯ ≀ 𝑦))
14 oveq1 7408 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑦 β†’ (𝑏↑2) = (𝑦↑2))
1514oveq2d 7417 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑦 β†’ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)))
1615eqeq1d 2726 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑦 β†’ (((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)) ↔ ((π‘₯↑2) + (𝑦↑2)) = ((π‘₯↑2) + (𝑦↑2))))
1713, 16anbi12d 630 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑦 β†’ ((π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))) ↔ (π‘₯ ≀ 𝑦 ∧ ((π‘₯↑2) + (𝑦↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
18 equequ1 2020 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑦 β†’ (𝑏 = 𝑐 ↔ 𝑦 = 𝑐))
1918imbi2d 340 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑦 β†’ (((π‘₯ ≀ 𝑐 ∧ ((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑏 = 𝑐) ↔ ((π‘₯ ≀ 𝑐 ∧ ((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑦 = 𝑐)))
2019ralbidv 3169 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑦 β†’ (βˆ€π‘ ∈ β„• ((π‘₯ ≀ 𝑐 ∧ ((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑏 = 𝑐) ↔ βˆ€π‘ ∈ β„• ((π‘₯ ≀ 𝑐 ∧ ((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑦 = 𝑐)))
2117, 20anbi12d 630 . . . . . . . . . . . . . . 15 (𝑏 = 𝑦 β†’ (((π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))) ∧ βˆ€π‘ ∈ β„• ((π‘₯ ≀ 𝑐 ∧ ((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑏 = 𝑐)) ↔ ((π‘₯ ≀ 𝑦 ∧ ((π‘₯↑2) + (𝑦↑2)) = ((π‘₯↑2) + (𝑦↑2))) ∧ βˆ€π‘ ∈ β„• ((π‘₯ ≀ 𝑐 ∧ ((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑦 = 𝑐))))
2221adantl 481 . . . . . . . . . . . . . 14 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) ∧ 𝑏 = 𝑦) β†’ (((π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))) ∧ βˆ€π‘ ∈ β„• ((π‘₯ ≀ 𝑐 ∧ ((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑏 = 𝑐)) ↔ ((π‘₯ ≀ 𝑦 ∧ ((π‘₯↑2) + (𝑦↑2)) = ((π‘₯↑2) + (𝑦↑2))) ∧ βˆ€π‘ ∈ β„• ((π‘₯ ≀ 𝑐 ∧ ((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑦 = 𝑐))))
23 simpr 484 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) β†’ π‘₯ ≀ 𝑦)
24 eqidd 2725 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) β†’ ((π‘₯↑2) + (𝑦↑2)) = ((π‘₯↑2) + (𝑦↑2)))
25 nnre 12216 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 ∈ β„• β†’ 𝑐 ∈ ℝ)
2625resqcld 14087 . . . . . . . . . . . . . . . . . . . 20 (𝑐 ∈ β„• β†’ (𝑐↑2) ∈ ℝ)
2726adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) ∧ 𝑐 ∈ β„•) β†’ (𝑐↑2) ∈ ℝ)
28 nnre 12216 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ β„• β†’ 𝑦 ∈ ℝ)
2928resqcld 14087 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ β„• β†’ (𝑦↑2) ∈ ℝ)
3029adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ (𝑦↑2) ∈ ℝ)
3130ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) ∧ 𝑐 ∈ β„•) β†’ (𝑦↑2) ∈ ℝ)
32 nnre 12216 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ β„• β†’ π‘₯ ∈ ℝ)
3332resqcld 14087 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ β„• β†’ (π‘₯↑2) ∈ ℝ)
3433adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ (π‘₯↑2) ∈ ℝ)
3534ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) ∧ 𝑐 ∈ β„•) β†’ (π‘₯↑2) ∈ ℝ)
36 readdcan 11385 . . . . . . . . . . . . . . . . . . 19 (((𝑐↑2) ∈ ℝ ∧ (𝑦↑2) ∈ ℝ ∧ (π‘₯↑2) ∈ ℝ) β†’ (((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2)) ↔ (𝑐↑2) = (𝑦↑2)))
3727, 31, 35, 36syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) ∧ 𝑐 ∈ β„•) β†’ (((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2)) ↔ (𝑐↑2) = (𝑦↑2)))
3828ad4antlr 730 . . . . . . . . . . . . . . . . . . . 20 (((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) ∧ 𝑐 ∈ β„•) ∧ (𝑐↑2) = (𝑦↑2)) β†’ 𝑦 ∈ ℝ)
3925ad2antlr 724 . . . . . . . . . . . . . . . . . . . 20 (((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) ∧ 𝑐 ∈ β„•) ∧ (𝑐↑2) = (𝑦↑2)) β†’ 𝑐 ∈ ℝ)
40 nnnn0 12476 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ β„• β†’ 𝑦 ∈ β„•0)
4140nn0ge0d 12532 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ β„• β†’ 0 ≀ 𝑦)
4241ad4antlr 730 . . . . . . . . . . . . . . . . . . . 20 (((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) ∧ 𝑐 ∈ β„•) ∧ (𝑐↑2) = (𝑦↑2)) β†’ 0 ≀ 𝑦)
43 nnnn0 12476 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 ∈ β„• β†’ 𝑐 ∈ β„•0)
4443nn0ge0d 12532 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 ∈ β„• β†’ 0 ≀ 𝑐)
4544ad2antlr 724 . . . . . . . . . . . . . . . . . . . 20 (((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) ∧ 𝑐 ∈ β„•) ∧ (𝑐↑2) = (𝑦↑2)) β†’ 0 ≀ 𝑐)
46 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 (((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) ∧ 𝑐 ∈ β„•) ∧ (𝑐↑2) = (𝑦↑2)) β†’ (𝑐↑2) = (𝑦↑2))
4746eqcomd 2730 . . . . . . . . . . . . . . . . . . . 20 (((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) ∧ 𝑐 ∈ β„•) ∧ (𝑐↑2) = (𝑦↑2)) β†’ (𝑦↑2) = (𝑐↑2))
4838, 39, 42, 45, 47sq11d 14218 . . . . . . . . . . . . . . . . . . 19 (((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) ∧ 𝑐 ∈ β„•) ∧ (𝑐↑2) = (𝑦↑2)) β†’ 𝑦 = 𝑐)
4948ex 412 . . . . . . . . . . . . . . . . . 18 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) ∧ 𝑐 ∈ β„•) β†’ ((𝑐↑2) = (𝑦↑2) β†’ 𝑦 = 𝑐))
5037, 49sylbid 239 . . . . . . . . . . . . . . . . 17 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) ∧ 𝑐 ∈ β„•) β†’ (((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2)) β†’ 𝑦 = 𝑐))
5150adantld 490 . . . . . . . . . . . . . . . 16 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) ∧ 𝑐 ∈ β„•) β†’ ((π‘₯ ≀ 𝑐 ∧ ((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑦 = 𝑐))
5251ralrimiva 3138 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) β†’ βˆ€π‘ ∈ β„• ((π‘₯ ≀ 𝑐 ∧ ((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑦 = 𝑐))
5323, 24, 52jca31 514 . . . . . . . . . . . . . 14 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) β†’ ((π‘₯ ≀ 𝑦 ∧ ((π‘₯↑2) + (𝑦↑2)) = ((π‘₯↑2) + (𝑦↑2))) ∧ βˆ€π‘ ∈ β„• ((π‘₯ ≀ 𝑐 ∧ ((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑦 = 𝑐)))
5412, 22, 53rspcedvd 3606 . . . . . . . . . . . . 13 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) β†’ βˆƒπ‘ ∈ β„• ((π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))) ∧ βˆ€π‘ ∈ β„• ((π‘₯ ≀ 𝑐 ∧ ((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑏 = 𝑐)))
55 breq2 5142 . . . . . . . . . . . . . . 15 (𝑏 = 𝑐 β†’ (π‘₯ ≀ 𝑏 ↔ π‘₯ ≀ 𝑐))
56 oveq1 7408 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑐 β†’ (𝑏↑2) = (𝑐↑2))
5756oveq2d 7417 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑐 β†’ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑐↑2)))
5857eqeq1d 2726 . . . . . . . . . . . . . . 15 (𝑏 = 𝑐 β†’ (((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)) ↔ ((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))))
5955, 58anbi12d 630 . . . . . . . . . . . . . 14 (𝑏 = 𝑐 β†’ ((π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))) ↔ (π‘₯ ≀ 𝑐 ∧ ((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
6059reu8 3721 . . . . . . . . . . . . 13 (βˆƒ!𝑏 ∈ β„• (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))) ↔ βˆƒπ‘ ∈ β„• ((π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))) ∧ βˆ€π‘ ∈ β„• ((π‘₯ ≀ 𝑐 ∧ ((π‘₯↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑏 = 𝑐)))
6154, 60sylibr 233 . . . . . . . . . . . 12 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ π‘₯ ≀ 𝑦) β†’ βˆƒ!𝑏 ∈ β„• (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))))
6261ex 412 . . . . . . . . . . 11 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ (π‘₯ ≀ 𝑦 β†’ βˆƒ!𝑏 ∈ β„• (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
6362adantr 480 . . . . . . . . . 10 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2))) β†’ (π‘₯ ≀ 𝑦 β†’ βˆƒ!𝑏 ∈ β„• (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
6463impcom 407 . . . . . . . . 9 ((π‘₯ ≀ 𝑦 ∧ ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2)))) β†’ βˆƒ!𝑏 ∈ β„• (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))))
65 eqeq2 2736 . . . . . . . . . . . . 13 (𝑃 = ((π‘₯↑2) + (𝑦↑2)) β†’ (((π‘₯↑2) + (𝑏↑2)) = 𝑃 ↔ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))))
6665anbi2d 628 . . . . . . . . . . . 12 (𝑃 = ((π‘₯↑2) + (𝑦↑2)) β†’ ((π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = 𝑃) ↔ (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
6766reubidv 3386 . . . . . . . . . . 11 (𝑃 = ((π‘₯↑2) + (𝑦↑2)) β†’ (βˆƒ!𝑏 ∈ β„• (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = 𝑃) ↔ βˆƒ!𝑏 ∈ β„• (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
6867adantl 481 . . . . . . . . . 10 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2))) β†’ (βˆƒ!𝑏 ∈ β„• (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = 𝑃) ↔ βˆƒ!𝑏 ∈ β„• (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
6968adantl 481 . . . . . . . . 9 ((π‘₯ ≀ 𝑦 ∧ ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2)))) β†’ (βˆƒ!𝑏 ∈ β„• (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = 𝑃) ↔ βˆƒ!𝑏 ∈ β„• (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
7064, 69mpbird 257 . . . . . . . 8 ((π‘₯ ≀ 𝑦 ∧ ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2)))) β†’ βˆƒ!𝑏 ∈ β„• (π‘₯ ≀ 𝑏 ∧ ((π‘₯↑2) + (𝑏↑2)) = 𝑃))
713, 10, 70rspcedvd 3606 . . . . . . 7 ((π‘₯ ≀ 𝑦 ∧ ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2)))) β†’ βˆƒπ‘Ž ∈ β„• βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃))
7211adantr 480 . . . . . . . . 9 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑦 ∈ β„•)
7372adantl 481 . . . . . . . 8 ((Β¬ π‘₯ ≀ 𝑦 ∧ ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2)))) β†’ 𝑦 ∈ β„•)
74 breq1 5141 . . . . . . . . . . 11 (π‘Ž = 𝑦 β†’ (π‘Ž ≀ 𝑏 ↔ 𝑦 ≀ 𝑏))
75 oveq1 7408 . . . . . . . . . . . . 13 (π‘Ž = 𝑦 β†’ (π‘Žβ†‘2) = (𝑦↑2))
7675oveq1d 7416 . . . . . . . . . . . 12 (π‘Ž = 𝑦 β†’ ((π‘Žβ†‘2) + (𝑏↑2)) = ((𝑦↑2) + (𝑏↑2)))
7776eqeq1d 2726 . . . . . . . . . . 11 (π‘Ž = 𝑦 β†’ (((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃 ↔ ((𝑦↑2) + (𝑏↑2)) = 𝑃))
7874, 77anbi12d 630 . . . . . . . . . 10 (π‘Ž = 𝑦 β†’ ((π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) ↔ (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃)))
7978reubidv 3386 . . . . . . . . 9 (π‘Ž = 𝑦 β†’ (βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) ↔ βˆƒ!𝑏 ∈ β„• (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃)))
8079adantl 481 . . . . . . . 8 (((Β¬ π‘₯ ≀ 𝑦 ∧ ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2)))) ∧ π‘Ž = 𝑦) β†’ (βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) ↔ βˆƒ!𝑏 ∈ β„• (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃)))
81 simpll 764 . . . . . . . . . . . . . 14 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ Β¬ π‘₯ ≀ 𝑦) β†’ π‘₯ ∈ β„•)
82 breq2 5142 . . . . . . . . . . . . . . . . 17 (𝑏 = π‘₯ β†’ (𝑦 ≀ 𝑏 ↔ 𝑦 ≀ π‘₯))
83 oveq1 7408 . . . . . . . . . . . . . . . . . . 19 (𝑏 = π‘₯ β†’ (𝑏↑2) = (π‘₯↑2))
8483oveq2d 7417 . . . . . . . . . . . . . . . . . 18 (𝑏 = π‘₯ β†’ ((𝑦↑2) + (𝑏↑2)) = ((𝑦↑2) + (π‘₯↑2)))
8584eqeq1d 2726 . . . . . . . . . . . . . . . . 17 (𝑏 = π‘₯ β†’ (((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)) ↔ ((𝑦↑2) + (π‘₯↑2)) = ((π‘₯↑2) + (𝑦↑2))))
8682, 85anbi12d 630 . . . . . . . . . . . . . . . 16 (𝑏 = π‘₯ β†’ ((𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))) ↔ (𝑦 ≀ π‘₯ ∧ ((𝑦↑2) + (π‘₯↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
87 equequ1 2020 . . . . . . . . . . . . . . . . . 18 (𝑏 = π‘₯ β†’ (𝑏 = 𝑐 ↔ π‘₯ = 𝑐))
8887imbi2d 340 . . . . . . . . . . . . . . . . 17 (𝑏 = π‘₯ β†’ (((𝑦 ≀ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑏 = 𝑐) ↔ ((𝑦 ≀ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ π‘₯ = 𝑐)))
8988ralbidv 3169 . . . . . . . . . . . . . . . 16 (𝑏 = π‘₯ β†’ (βˆ€π‘ ∈ β„• ((𝑦 ≀ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑏 = 𝑐) ↔ βˆ€π‘ ∈ β„• ((𝑦 ≀ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ π‘₯ = 𝑐)))
9086, 89anbi12d 630 . . . . . . . . . . . . . . 15 (𝑏 = π‘₯ β†’ (((𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))) ∧ βˆ€π‘ ∈ β„• ((𝑦 ≀ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑏 = 𝑐)) ↔ ((𝑦 ≀ π‘₯ ∧ ((𝑦↑2) + (π‘₯↑2)) = ((π‘₯↑2) + (𝑦↑2))) ∧ βˆ€π‘ ∈ β„• ((𝑦 ≀ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ π‘₯ = 𝑐))))
9190adantl 481 . . . . . . . . . . . . . 14 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ Β¬ π‘₯ ≀ 𝑦) ∧ 𝑏 = π‘₯) β†’ (((𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))) ∧ βˆ€π‘ ∈ β„• ((𝑦 ≀ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑏 = 𝑐)) ↔ ((𝑦 ≀ π‘₯ ∧ ((𝑦↑2) + (π‘₯↑2)) = ((π‘₯↑2) + (𝑦↑2))) ∧ βˆ€π‘ ∈ β„• ((𝑦 ≀ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ π‘₯ = 𝑐))))
92 ltnle 11290 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℝ ∧ π‘₯ ∈ ℝ) β†’ (𝑦 < π‘₯ ↔ Β¬ π‘₯ ≀ 𝑦))
9328, 32, 92syl2anr 596 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ (𝑦 < π‘₯ ↔ Β¬ π‘₯ ≀ 𝑦))
9428ad2antlr 724 . . . . . . . . . . . . . . . . . . 19 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑦 < π‘₯) β†’ 𝑦 ∈ ℝ)
9532ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑦 < π‘₯) β†’ π‘₯ ∈ ℝ)
96 simpr 484 . . . . . . . . . . . . . . . . . . 19 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑦 < π‘₯) β†’ 𝑦 < π‘₯)
9794, 95, 96ltled 11359 . . . . . . . . . . . . . . . . . 18 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑦 < π‘₯) β†’ 𝑦 ≀ π‘₯)
9897ex 412 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ (𝑦 < π‘₯ β†’ 𝑦 ≀ π‘₯))
9993, 98sylbird 260 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ (Β¬ π‘₯ ≀ 𝑦 β†’ 𝑦 ≀ π‘₯))
10099imp 406 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ Β¬ π‘₯ ≀ 𝑦) β†’ 𝑦 ≀ π‘₯)
10129recnd 11239 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ β„• β†’ (𝑦↑2) ∈ β„‚)
102101adantl 481 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ (𝑦↑2) ∈ β„‚)
10333recnd 11239 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ β„• β†’ (π‘₯↑2) ∈ β„‚)
104103adantr 480 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ (π‘₯↑2) ∈ β„‚)
105102, 104addcomd 11413 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ ((𝑦↑2) + (π‘₯↑2)) = ((π‘₯↑2) + (𝑦↑2)))
106105adantr 480 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ Β¬ π‘₯ ≀ 𝑦) β†’ ((𝑦↑2) + (π‘₯↑2)) = ((π‘₯↑2) + (𝑦↑2)))
10734recnd 11239 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ (π‘₯↑2) ∈ β„‚)
108107adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) β†’ (π‘₯↑2) ∈ β„‚)
10930recnd 11239 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ (𝑦↑2) ∈ β„‚)
110109adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) β†’ (𝑦↑2) ∈ β„‚)
111108, 110addcomd 11413 . . . . . . . . . . . . . . . . . . . . 21 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) β†’ ((π‘₯↑2) + (𝑦↑2)) = ((𝑦↑2) + (π‘₯↑2)))
112111eqeq2d 2735 . . . . . . . . . . . . . . . . . . . 20 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) β†’ (((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2)) ↔ ((𝑦↑2) + (𝑐↑2)) = ((𝑦↑2) + (π‘₯↑2))))
11326adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) β†’ (𝑐↑2) ∈ ℝ)
11433ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) β†’ (π‘₯↑2) ∈ ℝ)
11529ad2antlr 724 . . . . . . . . . . . . . . . . . . . . 21 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) β†’ (𝑦↑2) ∈ ℝ)
116 readdcan 11385 . . . . . . . . . . . . . . . . . . . . 21 (((𝑐↑2) ∈ ℝ ∧ (π‘₯↑2) ∈ ℝ ∧ (𝑦↑2) ∈ ℝ) β†’ (((𝑦↑2) + (𝑐↑2)) = ((𝑦↑2) + (π‘₯↑2)) ↔ (𝑐↑2) = (π‘₯↑2)))
117113, 114, 115, 116syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) β†’ (((𝑦↑2) + (𝑐↑2)) = ((𝑦↑2) + (π‘₯↑2)) ↔ (𝑐↑2) = (π‘₯↑2)))
118112, 117bitrd 279 . . . . . . . . . . . . . . . . . . 19 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) β†’ (((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2)) ↔ (𝑐↑2) = (π‘₯↑2)))
11925ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . 22 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) ∧ (𝑐↑2) = (π‘₯↑2)) β†’ 𝑐 ∈ ℝ)
12032adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ π‘₯ ∈ ℝ)
121120ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) ∧ (𝑐↑2) = (π‘₯↑2)) β†’ π‘₯ ∈ ℝ)
12244ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . 22 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) ∧ (𝑐↑2) = (π‘₯↑2)) β†’ 0 ≀ 𝑐)
123 nnnn0 12476 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ ∈ β„• β†’ π‘₯ ∈ β„•0)
124123nn0ge0d 12532 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ ∈ β„• β†’ 0 ≀ π‘₯)
125124adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ 0 ≀ π‘₯)
126125ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) ∧ (𝑐↑2) = (π‘₯↑2)) β†’ 0 ≀ π‘₯)
127 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) ∧ (𝑐↑2) = (π‘₯↑2)) β†’ (𝑐↑2) = (π‘₯↑2))
128119, 121, 122, 126, 127sq11d 14218 . . . . . . . . . . . . . . . . . . . . 21 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) ∧ (𝑐↑2) = (π‘₯↑2)) β†’ 𝑐 = π‘₯)
129128eqcomd 2730 . . . . . . . . . . . . . . . . . . . 20 ((((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) ∧ (𝑐↑2) = (π‘₯↑2)) β†’ π‘₯ = 𝑐)
130129ex 412 . . . . . . . . . . . . . . . . . . 19 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) β†’ ((𝑐↑2) = (π‘₯↑2) β†’ π‘₯ = 𝑐))
131118, 130sylbid 239 . . . . . . . . . . . . . . . . . 18 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) β†’ (((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2)) β†’ π‘₯ = 𝑐))
132131adantld 490 . . . . . . . . . . . . . . . . 17 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑐 ∈ β„•) β†’ ((𝑦 ≀ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ π‘₯ = 𝑐))
133132ralrimiva 3138 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ βˆ€π‘ ∈ β„• ((𝑦 ≀ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ π‘₯ = 𝑐))
134133adantr 480 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ Β¬ π‘₯ ≀ 𝑦) β†’ βˆ€π‘ ∈ β„• ((𝑦 ≀ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ π‘₯ = 𝑐))
135100, 106, 134jca31 514 . . . . . . . . . . . . . 14 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ Β¬ π‘₯ ≀ 𝑦) β†’ ((𝑦 ≀ π‘₯ ∧ ((𝑦↑2) + (π‘₯↑2)) = ((π‘₯↑2) + (𝑦↑2))) ∧ βˆ€π‘ ∈ β„• ((𝑦 ≀ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ π‘₯ = 𝑐)))
13681, 91, 135rspcedvd 3606 . . . . . . . . . . . . 13 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ Β¬ π‘₯ ≀ 𝑦) β†’ βˆƒπ‘ ∈ β„• ((𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))) ∧ βˆ€π‘ ∈ β„• ((𝑦 ≀ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑏 = 𝑐)))
137 breq2 5142 . . . . . . . . . . . . . . 15 (𝑏 = 𝑐 β†’ (𝑦 ≀ 𝑏 ↔ 𝑦 ≀ 𝑐))
13856oveq2d 7417 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑐 β†’ ((𝑦↑2) + (𝑏↑2)) = ((𝑦↑2) + (𝑐↑2)))
139138eqeq1d 2726 . . . . . . . . . . . . . . 15 (𝑏 = 𝑐 β†’ (((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)) ↔ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))))
140137, 139anbi12d 630 . . . . . . . . . . . . . 14 (𝑏 = 𝑐 β†’ ((𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))) ↔ (𝑦 ≀ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
141140reu8 3721 . . . . . . . . . . . . 13 (βˆƒ!𝑏 ∈ β„• (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))) ↔ βˆƒπ‘ ∈ β„• ((𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))) ∧ βˆ€π‘ ∈ β„• ((𝑦 ≀ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((π‘₯↑2) + (𝑦↑2))) β†’ 𝑏 = 𝑐)))
142136, 141sylibr 233 . . . . . . . . . . . 12 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ Β¬ π‘₯ ≀ 𝑦) β†’ βˆƒ!𝑏 ∈ β„• (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))))
143142ex 412 . . . . . . . . . . 11 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ (Β¬ π‘₯ ≀ 𝑦 β†’ βˆƒ!𝑏 ∈ β„• (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
144143adantr 480 . . . . . . . . . 10 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2))) β†’ (Β¬ π‘₯ ≀ 𝑦 β†’ βˆƒ!𝑏 ∈ β„• (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
145144impcom 407 . . . . . . . . 9 ((Β¬ π‘₯ ≀ 𝑦 ∧ ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2)))) β†’ βˆƒ!𝑏 ∈ β„• (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))))
146 eqeq2 2736 . . . . . . . . . . . . 13 (𝑃 = ((π‘₯↑2) + (𝑦↑2)) β†’ (((𝑦↑2) + (𝑏↑2)) = 𝑃 ↔ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2))))
147146anbi2d 628 . . . . . . . . . . . 12 (𝑃 = ((π‘₯↑2) + (𝑦↑2)) β†’ ((𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃) ↔ (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
148147reubidv 3386 . . . . . . . . . . 11 (𝑃 = ((π‘₯↑2) + (𝑦↑2)) β†’ (βˆƒ!𝑏 ∈ β„• (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃) ↔ βˆƒ!𝑏 ∈ β„• (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
149148adantl 481 . . . . . . . . . 10 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2))) β†’ (βˆƒ!𝑏 ∈ β„• (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃) ↔ βˆƒ!𝑏 ∈ β„• (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
150149adantl 481 . . . . . . . . 9 ((Β¬ π‘₯ ≀ 𝑦 ∧ ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2)))) β†’ (βˆƒ!𝑏 ∈ β„• (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃) ↔ βˆƒ!𝑏 ∈ β„• (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((π‘₯↑2) + (𝑦↑2)))))
151145, 150mpbird 257 . . . . . . . 8 ((Β¬ π‘₯ ≀ 𝑦 ∧ ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2)))) β†’ βˆƒ!𝑏 ∈ β„• (𝑦 ≀ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃))
15273, 80, 151rspcedvd 3606 . . . . . . 7 ((Β¬ π‘₯ ≀ 𝑦 ∧ ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2)))) β†’ βˆƒπ‘Ž ∈ β„• βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃))
15371, 152pm2.61ian 809 . . . . . 6 (((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) ∧ 𝑃 = ((π‘₯↑2) + (𝑦↑2))) β†’ βˆƒπ‘Ž ∈ β„• βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃))
154153ex 412 . . . . 5 ((π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•) β†’ (𝑃 = ((π‘₯↑2) + (𝑦↑2)) β†’ βˆƒπ‘Ž ∈ β„• βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃)))
155154adantl 481 . . . 4 (((𝑃 ∈ β„™ ∧ (𝑃 mod 4) = 1) ∧ (π‘₯ ∈ β„• ∧ 𝑦 ∈ β„•)) β†’ (𝑃 = ((π‘₯↑2) + (𝑦↑2)) β†’ βˆƒπ‘Ž ∈ β„• βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃)))
156155rexlimdvva 3203 . . 3 ((𝑃 ∈ β„™ ∧ (𝑃 mod 4) = 1) β†’ (βˆƒπ‘₯ ∈ β„• βˆƒπ‘¦ ∈ β„• 𝑃 = ((π‘₯↑2) + (𝑦↑2)) β†’ βˆƒπ‘Ž ∈ β„• βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃)))
1571, 156mpd 15 . 2 ((𝑃 ∈ β„™ ∧ (𝑃 mod 4) = 1) β†’ βˆƒπ‘Ž ∈ β„• βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃))
158 reurex 3372 . . . . 5 (βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) β†’ βˆƒπ‘ ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃))
159158a1i 11 . . . 4 (((𝑃 ∈ β„™ ∧ (𝑃 mod 4) = 1) ∧ π‘Ž ∈ β„•) β†’ (βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) β†’ βˆƒπ‘ ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃)))
160159ralrimiva 3138 . . 3 ((𝑃 ∈ β„™ ∧ (𝑃 mod 4) = 1) β†’ βˆ€π‘Ž ∈ β„• (βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) β†’ βˆƒπ‘ ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃)))
161 2sqmo 27286 . . . . 5 (𝑃 ∈ β„™ β†’ βˆƒ*π‘Ž ∈ β„•0 βˆƒπ‘ ∈ β„•0 (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃))
162 nnssnn0 12472 . . . . . 6 β„• βŠ† β„•0
163 nfcv 2895 . . . . . . 7 β„²π‘Žβ„•
164 nfcv 2895 . . . . . . 7 β„²π‘Žβ„•0
165163, 164ssrmof 4041 . . . . . 6 (β„• βŠ† β„•0 β†’ (βˆƒ*π‘Ž ∈ β„•0 βˆƒπ‘ ∈ β„•0 (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) β†’ βˆƒ*π‘Ž ∈ β„• βˆƒπ‘ ∈ β„•0 (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃)))
166162, 165ax-mp 5 . . . . 5 (βˆƒ*π‘Ž ∈ β„•0 βˆƒπ‘ ∈ β„•0 (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) β†’ βˆƒ*π‘Ž ∈ β„• βˆƒπ‘ ∈ β„•0 (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃))
167 ssrexv 4043 . . . . . . 7 (β„• βŠ† β„•0 β†’ (βˆƒπ‘ ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) β†’ βˆƒπ‘ ∈ β„•0 (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃)))
168162, 167ax-mp 5 . . . . . 6 (βˆƒπ‘ ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) β†’ βˆƒπ‘ ∈ β„•0 (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃))
169168rmoimi 3730 . . . . 5 (βˆƒ*π‘Ž ∈ β„• βˆƒπ‘ ∈ β„•0 (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) β†’ βˆƒ*π‘Ž ∈ β„• βˆƒπ‘ ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃))
170161, 166, 1693syl 18 . . . 4 (𝑃 ∈ β„™ β†’ βˆƒ*π‘Ž ∈ β„• βˆƒπ‘ ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃))
171170adantr 480 . . 3 ((𝑃 ∈ β„™ ∧ (𝑃 mod 4) = 1) β†’ βˆƒ*π‘Ž ∈ β„• βˆƒπ‘ ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃))
172 rmoim 3728 . . 3 (βˆ€π‘Ž ∈ β„• (βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) β†’ βˆƒπ‘ ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃)) β†’ (βˆƒ*π‘Ž ∈ β„• βˆƒπ‘ ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) β†’ βˆƒ*π‘Ž ∈ β„• βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃)))
173160, 171, 172sylc 65 . 2 ((𝑃 ∈ β„™ ∧ (𝑃 mod 4) = 1) β†’ βˆƒ*π‘Ž ∈ β„• βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃))
174 reu5 3370 . 2 (βˆƒ!π‘Ž ∈ β„• βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) ↔ (βˆƒπ‘Ž ∈ β„• βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃) ∧ βˆƒ*π‘Ž ∈ β„• βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃)))
175157, 173, 174sylanbrc 582 1 ((𝑃 ∈ β„™ ∧ (𝑃 mod 4) = 1) β†’ βˆƒ!π‘Ž ∈ β„• βˆƒ!𝑏 ∈ β„• (π‘Ž ≀ 𝑏 ∧ ((π‘Žβ†‘2) + (𝑏↑2)) = 𝑃))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098  βˆ€wral 3053  βˆƒwrex 3062  βˆƒ!wreu 3366  βˆƒ*wrmo 3367   βŠ† wss 3940   class class class wbr 5138  (class class class)co 7401  β„‚cc 11104  β„cr 11105  0cc0 11106  1c1 11107   + caddc 11109   < clt 11245   ≀ cle 11246  β„•cn 12209  2c2 12264  4c4 12266  β„•0cn0 12469   mod cmo 13831  β†‘cexp 14024  β„™cprime 16605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-ofr 7664  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-tpos 8206  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-oadd 8465  df-er 8699  df-ec 8701  df-qs 8705  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-xnn0 12542  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-dvds 16195  df-gcd 16433  df-prm 16606  df-phi 16698  df-pc 16769  df-gz 16862  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-0g 17386  df-gsum 17387  df-prds 17392  df-pws 17394  df-imas 17453  df-qus 17454  df-mre 17529  df-mrc 17530  df-acs 17532  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-mhm 18703  df-submnd 18704  df-grp 18856  df-minusg 18857  df-sbg 18858  df-mulg 18986  df-subg 19040  df-nsg 19041  df-eqg 19042  df-ghm 19129  df-cntz 19223  df-cmn 19692  df-abl 19693  df-mgp 20030  df-rng 20048  df-ur 20077  df-srg 20082  df-ring 20130  df-cring 20131  df-oppr 20226  df-dvdsr 20249  df-unit 20250  df-invr 20280  df-dvr 20293  df-rhm 20364  df-nzr 20405  df-subrng 20436  df-subrg 20461  df-drng 20579  df-field 20580  df-lmod 20698  df-lss 20769  df-lsp 20809  df-sra 21011  df-rgmod 21012  df-lidl 21057  df-rsp 21058  df-2idl 21097  df-rlreg 21183  df-domn 21184  df-idom 21185  df-cnfld 21229  df-zring 21302  df-zrh 21358  df-zn 21361  df-assa 21716  df-asp 21717  df-ascl 21718  df-psr 21771  df-mvr 21772  df-mpl 21773  df-opsr 21775  df-evls 21945  df-evl 21946  df-psr1 22022  df-vr1 22023  df-ply1 22024  df-coe1 22025  df-evl1 22157  df-mdeg 25910  df-deg1 25911  df-mon1 25988  df-uc1p 25989  df-q1p 25990  df-r1p 25991  df-lgs 27144
This theorem is referenced by:  2sqreunnltlem  27299  2sqreunn  27306
  Copyright terms: Public domain W3C validator