Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2sqreuop | Structured version Visualization version GIF version |
Description: There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two nonnegative integers. Ordered pair variant of 2sqreu 26614. (Contributed by AV, 2-Jul-2023.) |
Ref | Expression |
---|---|
2sqreuop | ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) ≤ (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biid 260 | . . 3 ⊢ ((𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | |
2 | 1 | 2sqreu 26614 | . 2 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃!𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ∧ ∃!𝑏 ∈ ℕ0 ∃𝑎 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))) |
3 | fveq2 6766 | . . . . . 6 ⊢ (𝑝 = 〈𝑎, 𝑏〉 → (1st ‘𝑝) = (1st ‘〈𝑎, 𝑏〉)) | |
4 | fveq2 6766 | . . . . . 6 ⊢ (𝑝 = 〈𝑎, 𝑏〉 → (2nd ‘𝑝) = (2nd ‘〈𝑎, 𝑏〉)) | |
5 | 3, 4 | breq12d 5086 | . . . . 5 ⊢ (𝑝 = 〈𝑎, 𝑏〉 → ((1st ‘𝑝) ≤ (2nd ‘𝑝) ↔ (1st ‘〈𝑎, 𝑏〉) ≤ (2nd ‘〈𝑎, 𝑏〉))) |
6 | vex 3433 | . . . . . . 7 ⊢ 𝑎 ∈ V | |
7 | vex 3433 | . . . . . . 7 ⊢ 𝑏 ∈ V | |
8 | 6, 7 | op1st 7828 | . . . . . 6 ⊢ (1st ‘〈𝑎, 𝑏〉) = 𝑎 |
9 | 6, 7 | op2nd 7829 | . . . . . 6 ⊢ (2nd ‘〈𝑎, 𝑏〉) = 𝑏 |
10 | 8, 9 | breq12i 5082 | . . . . 5 ⊢ ((1st ‘〈𝑎, 𝑏〉) ≤ (2nd ‘〈𝑎, 𝑏〉) ↔ 𝑎 ≤ 𝑏) |
11 | 5, 10 | bitrdi 287 | . . . 4 ⊢ (𝑝 = 〈𝑎, 𝑏〉 → ((1st ‘𝑝) ≤ (2nd ‘𝑝) ↔ 𝑎 ≤ 𝑏)) |
12 | 6, 7 | op1std 7830 | . . . . . . 7 ⊢ (𝑝 = 〈𝑎, 𝑏〉 → (1st ‘𝑝) = 𝑎) |
13 | 12 | oveq1d 7282 | . . . . . 6 ⊢ (𝑝 = 〈𝑎, 𝑏〉 → ((1st ‘𝑝)↑2) = (𝑎↑2)) |
14 | 6, 7 | op2ndd 7831 | . . . . . . 7 ⊢ (𝑝 = 〈𝑎, 𝑏〉 → (2nd ‘𝑝) = 𝑏) |
15 | 14 | oveq1d 7282 | . . . . . 6 ⊢ (𝑝 = 〈𝑎, 𝑏〉 → ((2nd ‘𝑝)↑2) = (𝑏↑2)) |
16 | 13, 15 | oveq12d 7285 | . . . . 5 ⊢ (𝑝 = 〈𝑎, 𝑏〉 → (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = ((𝑎↑2) + (𝑏↑2))) |
17 | 16 | eqeq1d 2740 | . . . 4 ⊢ (𝑝 = 〈𝑎, 𝑏〉 → ((((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃 ↔ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) |
18 | 11, 17 | anbi12d 631 | . . 3 ⊢ (𝑝 = 〈𝑎, 𝑏〉 → (((1st ‘𝑝) ≤ (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃) ↔ (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))) |
19 | 18 | opreu2reurex 6190 | . 2 ⊢ (∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) ≤ (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃) ↔ (∃!𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ∧ ∃!𝑏 ∈ ℕ0 ∃𝑎 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))) |
20 | 2, 19 | sylibr 233 | 1 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) ≤ (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1539 ∈ wcel 2106 ∃wrex 3065 ∃!wreu 3066 〈cop 4567 class class class wbr 5073 × cxp 5582 ‘cfv 6426 (class class class)co 7267 1st c1st 7818 2nd c2nd 7819 1c1 10882 + caddc 10884 ≤ cle 11020 2c2 12038 4c4 12040 ℕ0cn0 12243 mod cmo 13599 ↑cexp 13792 ℙcprime 16386 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5208 ax-sep 5221 ax-nul 5228 ax-pow 5286 ax-pr 5350 ax-un 7578 ax-cnex 10937 ax-resscn 10938 ax-1cn 10939 ax-icn 10940 ax-addcl 10941 ax-addrcl 10942 ax-mulcl 10943 ax-mulrcl 10944 ax-mulcom 10945 ax-addass 10946 ax-mulass 10947 ax-distr 10948 ax-i2m1 10949 ax-1ne0 10950 ax-1rid 10951 ax-rnegex 10952 ax-rrecex 10953 ax-cnre 10954 ax-pre-lttri 10955 ax-pre-lttrn 10956 ax-pre-ltadd 10957 ax-pre-mulgt0 10958 ax-pre-sup 10959 ax-addf 10960 ax-mulf 10961 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3431 df-sbc 3716 df-csb 3832 df-dif 3889 df-un 3891 df-in 3893 df-ss 3903 df-pss 3905 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-iin 4927 df-br 5074 df-opab 5136 df-mpt 5157 df-tr 5191 df-id 5484 df-eprel 5490 df-po 5498 df-so 5499 df-fr 5539 df-se 5540 df-we 5541 df-xp 5590 df-rel 5591 df-cnv 5592 df-co 5593 df-dm 5594 df-rn 5595 df-res 5596 df-ima 5597 df-pred 6195 df-ord 6262 df-on 6263 df-lim 6264 df-suc 6265 df-iota 6384 df-fun 6428 df-fn 6429 df-f 6430 df-f1 6431 df-fo 6432 df-f1o 6433 df-fv 6434 df-isom 6435 df-riota 7224 df-ov 7270 df-oprab 7271 df-mpo 7272 df-of 7523 df-ofr 7524 df-om 7703 df-1st 7820 df-2nd 7821 df-supp 7965 df-tpos 8029 df-frecs 8084 df-wrecs 8115 df-recs 8189 df-rdg 8228 df-1o 8284 df-2o 8285 df-oadd 8288 df-er 8485 df-ec 8487 df-qs 8491 df-map 8604 df-pm 8605 df-ixp 8673 df-en 8721 df-dom 8722 df-sdom 8723 df-fin 8724 df-fsupp 9116 df-sup 9188 df-inf 9189 df-oi 9256 df-dju 9669 df-card 9707 df-pnf 11021 df-mnf 11022 df-xr 11023 df-ltxr 11024 df-le 11025 df-sub 11217 df-neg 11218 df-div 11643 df-nn 11984 df-2 12046 df-3 12047 df-4 12048 df-5 12049 df-6 12050 df-7 12051 df-8 12052 df-9 12053 df-n0 12244 df-xnn0 12316 df-z 12330 df-dec 12448 df-uz 12593 df-q 12699 df-rp 12741 df-fz 13250 df-fzo 13393 df-fl 13522 df-mod 13600 df-seq 13732 df-exp 13793 df-hash 14055 df-cj 14820 df-re 14821 df-im 14822 df-sqrt 14956 df-abs 14957 df-dvds 15974 df-gcd 16212 df-prm 16387 df-phi 16477 df-pc 16548 df-gz 16641 df-struct 16858 df-sets 16875 df-slot 16893 df-ndx 16905 df-base 16923 df-ress 16952 df-plusg 16985 df-mulr 16986 df-starv 16987 df-sca 16988 df-vsca 16989 df-ip 16990 df-tset 16991 df-ple 16992 df-ds 16994 df-unif 16995 df-hom 16996 df-cco 16997 df-0g 17162 df-gsum 17163 df-prds 17168 df-pws 17170 df-imas 17229 df-qus 17230 df-mre 17305 df-mrc 17306 df-acs 17308 df-mgm 18336 df-sgrp 18385 df-mnd 18396 df-mhm 18440 df-submnd 18441 df-grp 18590 df-minusg 18591 df-sbg 18592 df-mulg 18711 df-subg 18762 df-nsg 18763 df-eqg 18764 df-ghm 18842 df-cntz 18933 df-cmn 19398 df-abl 19399 df-mgp 19731 df-ur 19748 df-srg 19752 df-ring 19795 df-cring 19796 df-oppr 19872 df-dvdsr 19893 df-unit 19894 df-invr 19924 df-dvr 19935 df-rnghom 19969 df-drng 20003 df-field 20004 df-subrg 20032 df-lmod 20135 df-lss 20204 df-lsp 20244 df-sra 20444 df-rgmod 20445 df-lidl 20446 df-rsp 20447 df-2idl 20513 df-nzr 20539 df-rlreg 20564 df-domn 20565 df-idom 20566 df-cnfld 20608 df-zring 20681 df-zrh 20715 df-zn 20718 df-assa 21070 df-asp 21071 df-ascl 21072 df-psr 21122 df-mvr 21123 df-mpl 21124 df-opsr 21126 df-evls 21292 df-evl 21293 df-psr1 21361 df-vr1 21362 df-ply1 21363 df-coe1 21364 df-evl1 21492 df-mdeg 25227 df-deg1 25228 df-mon1 25305 df-uc1p 25306 df-q1p 25307 df-r1p 25308 df-lgs 26453 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |