2sqb - Metamath Proof Explorer

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

Theorem 2sqb 25202

Description: The converse to 2sq 25200. (Contributed by Mario Carneiro, 20-Jun-2015.)

**Assertion**
Ref	Expression
2sqb	⊢ (𝑃 ∈ ℙ → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2)) ↔ (𝑃 = 2 ∨ (𝑃 mod 4) = 1)))

Distinct variable group: 𝑥,𝑦,𝑃

Proof of Theorem 2sqb Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ne 2824	. . . 4 ⊢ (𝑃 ≠ 2 ↔ ¬ 𝑃 = 2)
2		prmz 15436	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
3	2	ad3antrrr 766	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → 𝑃 ∈ ℤ)
4		simplrr 818	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → 𝑦 ∈ ℤ)
5		bezout 15307	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑃 gcd 𝑦) = ((𝑃 · 𝑎) + (𝑦 · 𝑏)))
6	3, 4, 5	syl2anc 694	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑃 gcd 𝑦) = ((𝑃 · 𝑎) + (𝑦 · 𝑏)))
7		simplll 813	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑃 gcd 𝑦) = ((𝑃 · 𝑎) + (𝑦 · 𝑏)))) → (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))
8		simpllr 815	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑃 gcd 𝑦) = ((𝑃 · 𝑎) + (𝑦 · 𝑏)))) → (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ))
9		simplr 807	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑃 gcd 𝑦) = ((𝑃 · 𝑎) + (𝑦 · 𝑏)))) → 𝑃 = ((𝑥↑2) + (𝑦↑2)))
10		simprll 819	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑃 gcd 𝑦) = ((𝑃 · 𝑎) + (𝑦 · 𝑏)))) → 𝑎 ∈ ℤ)
11		simprlr 820	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑃 gcd 𝑦) = ((𝑃 · 𝑎) + (𝑦 · 𝑏)))) → 𝑏 ∈ ℤ)
12		simprr 811	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑃 gcd 𝑦) = ((𝑃 · 𝑎) + (𝑦 · 𝑏)))) → (𝑃 gcd 𝑦) = ((𝑃 · 𝑎) + (𝑦 · 𝑏)))
13	7, 8, 9, 10, 11, 12	2sqblem 25201	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑃 gcd 𝑦) = ((𝑃 · 𝑎) + (𝑦 · 𝑏)))) → (𝑃 mod 4) = 1)
14	13	expr 642	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑃 gcd 𝑦) = ((𝑃 · 𝑎) + (𝑦 · 𝑏)) → (𝑃 mod 4) = 1))
15	14	rexlimdvva 3067	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑃 gcd 𝑦) = ((𝑃 · 𝑎) + (𝑦 · 𝑏)) → (𝑃 mod 4) = 1))
16	6, 15	mpd 15	. . . . . . 7 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → (𝑃 mod 4) = 1)
17	16	ex 449	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑃 = ((𝑥↑2) + (𝑦↑2)) → (𝑃 mod 4) = 1))
18	17	rexlimdvva 3067	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2)) → (𝑃 mod 4) = 1))
19	18	impancom 455	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → (𝑃 ≠ 2 → (𝑃 mod 4) = 1))
20	1, 19	syl5bir 233	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → (¬ 𝑃 = 2 → (𝑃 mod 4) = 1))
21	20	orrd 392	. 2 ⊢ ((𝑃 ∈ ℙ ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → (𝑃 = 2 ∨ (𝑃 mod 4) = 1))
22		1z 11445	. . . . 5 ⊢ 1 ∈ ℤ
23		oveq1 6697	. . . . . . . . 9 ⊢ (𝑥 = 1 → (𝑥↑2) = (1↑2))
24		sq1 12998	. . . . . . . . 9 ⊢ (1↑2) = 1
25	23, 24	syl6eq 2701	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥↑2) = 1)
26	25	oveq1d 6705	. . . . . . 7 ⊢ (𝑥 = 1 → ((𝑥↑2) + (𝑦↑2)) = (1 + (𝑦↑2)))
27	26	eqeq2d 2661	. . . . . 6 ⊢ (𝑥 = 1 → (𝑃 = ((𝑥↑2) + (𝑦↑2)) ↔ 𝑃 = (1 + (𝑦↑2))))
28		oveq1 6697	. . . . . . . . . 10 ⊢ (𝑦 = 1 → (𝑦↑2) = (1↑2))
29	28, 24	syl6eq 2701	. . . . . . . . 9 ⊢ (𝑦 = 1 → (𝑦↑2) = 1)
30	29	oveq2d 6706	. . . . . . . 8 ⊢ (𝑦 = 1 → (1 + (𝑦↑2)) = (1 + 1))
31		1p1e2 11172	. . . . . . . 8 ⊢ (1 + 1) = 2
32	30, 31	syl6eq 2701	. . . . . . 7 ⊢ (𝑦 = 1 → (1 + (𝑦↑2)) = 2)
33	32	eqeq2d 2661	. . . . . 6 ⊢ (𝑦 = 1 → (𝑃 = (1 + (𝑦↑2)) ↔ 𝑃 = 2))
34	27, 33	rspc2ev 3355	. . . . 5 ⊢ ((1 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑃 = 2) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2)))
35	22, 22, 34	mp3an12 1454	. . . 4 ⊢ (𝑃 = 2 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2)))
36	35	adantl 481	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝑃 = 2) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2)))
37		2sq 25200	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2)))
38	36, 37	jaodan 843	. 2 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 = 2 ∨ (𝑃 mod 4) = 1)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2)))
39	21, 38	impbida 895	1 ⊢ (𝑃 ∈ ℙ → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2)) ↔ (𝑃 = 2 ∨ (𝑃 mod 4) = 1)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 382 ∧ wa 383 = wceq 1523 ∈ wcel 2030 ≠ wne 2823 ∃wrex 2942 (class class class)co 6690 1c1 9975 + caddc 9977 · cmul 9979 2c2 11108 4c4 11110 ℤcz 11415 mod cmo 12708 ↑cexp 12900 gcd cgcd 15263 ℙcprime 15432

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-8 2032 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-rep 4804 ax-sep 4814 ax-nul 4822 ax-pow 4873 ax-pr 4936 ax-un 6991 ax-inf2 8576 ax-cnex 10030 ax-resscn 10031 ax-1cn 10032 ax-icn 10033 ax-addcl 10034 ax-addrcl 10035 ax-mulcl 10036 ax-mulrcl 10037 ax-mulcom 10038 ax-addass 10039 ax-mulass 10040 ax-distr 10041 ax-i2m1 10042 ax-1ne0 10043 ax-1rid 10044 ax-rnegex 10045 ax-rrecex 10046 ax-cnre 10047 ax-pre-lttri 10048 ax-pre-lttrn 10049 ax-pre-ltadd 10050 ax-pre-mulgt0 10051 ax-pre-sup 10052 ax-addf 10053 ax-mulf 10054

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1055 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-nel 2927 df-ral 2946 df-rex 2947 df-reu 2948 df-rmo 2949 df-rab 2950 df-v 3233 df-sbc 3469 df-csb 3567 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-pss 3623 df-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-tp 4215 df-op 4217 df-uni 4469 df-int 4508 df-iun 4554 df-iin 4555 df-br 4686 df-opab 4746 df-mpt 4763 df-tr 4786 df-id 5053 df-eprel 5058 df-po 5064 df-so 5065 df-fr 5102 df-se 5103 df-we 5104 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-rn 5154 df-res 5155 df-ima 5156 df-pred 5718 df-ord 5764 df-on 5765 df-lim 5766 df-suc 5767 df-iota 5889 df-fun 5928 df-fn 5929 df-f 5930 df-f1 5931 df-fo 5932 df-f1o 5933 df-fv 5934 df-isom 5935 df-riota 6651 df-ov 6693 df-oprab 6694 df-mpt2 6695 df-of 6939 df-ofr 6940 df-om 7108 df-1st 7210 df-2nd 7211 df-supp 7341 df-tpos 7397 df-wrecs 7452 df-recs 7513 df-rdg 7551 df-1o 7605 df-2o 7606 df-oadd 7609 df-er 7787 df-ec 7789 df-qs 7793 df-map 7901 df-pm 7902 df-ixp 7951 df-en 7998 df-dom 7999 df-sdom 8000 df-fin 8001 df-fsupp 8317 df-sup 8389 df-inf 8390 df-oi 8456 df-card 8803 df-cda 9028 df-pnf 10114 df-mnf 10115 df-xr 10116 df-ltxr 10117 df-le 10118 df-sub 10306 df-neg 10307 df-div 10723 df-nn 11059 df-2 11117 df-3 11118 df-4 11119 df-5 11120 df-6 11121 df-7 11122 df-8 11123 df-9 11124 df-n0 11331 df-xnn0 11402 df-z 11416 df-dec 11532 df-uz 11726 df-q 11827 df-rp 11871 df-fz 12365 df-fzo 12505 df-fl 12633 df-mod 12709 df-seq 12842 df-exp 12901 df-hash 13158 df-cj 13883 df-re 13884 df-im 13885 df-sqrt 14019 df-abs 14020 df-dvds 15028 df-gcd 15264 df-prm 15433 df-phi 15518 df-pc 15589 df-gz 15681 df-struct 15906 df-ndx 15907 df-slot 15908 df-base 15910 df-sets 15911 df-ress 15912 df-plusg 16001 df-mulr 16002 df-starv 16003 df-sca 16004 df-vsca 16005 df-ip 16006 df-tset 16007 df-ple 16008 df-ds 16011 df-unif 16012 df-hom 16013 df-cco 16014 df-0g 16149 df-gsum 16150 df-prds 16155 df-pws 16157 df-imas 16215 df-qus 16216 df-mre 16293 df-mrc 16294 df-acs 16296 df-mgm 17289 df-sgrp 17331 df-mnd 17342 df-mhm 17382 df-submnd 17383 df-grp 17472 df-minusg 17473 df-sbg 17474 df-mulg 17588 df-subg 17638 df-nsg 17639 df-eqg 17640 df-ghm 17705 df-cntz 17796 df-cmn 18241 df-abl 18242 df-mgp 18536 df-ur 18548 df-srg 18552 df-ring 18595 df-cring 18596 df-oppr 18669 df-dvdsr 18687 df-unit 18688 df-invr 18718 df-dvr 18729 df-rnghom 18763 df-drng 18797 df-field 18798 df-subrg 18826 df-lmod 18913 df-lss 18981 df-lsp 19020 df-sra 19220 df-rgmod 19221 df-lidl 19222 df-rsp 19223 df-2idl 19280 df-nzr 19306 df-rlreg 19331 df-domn 19332 df-idom 19333 df-assa 19360 df-asp 19361 df-ascl 19362 df-psr 19404 df-mvr 19405 df-mpl 19406 df-opsr 19408 df-evls 19554 df-evl 19555 df-psr1 19598 df-vr1 19599 df-ply1 19600 df-coe1 19601 df-evl1 19729 df-cnfld 19795 df-zring 19867 df-zrh 19900 df-zn 19903 df-mdeg 23860 df-deg1 23861 df-mon1 23935 df-uc1p 23936 df-q1p 23937 df-r1p 23938 df-lgs 25065

This theorem is referenced by: (None)

W3C validator