Metamath Proof Explorer

Theorem 2sqmo

Description: There exists at most one decomposition of a prime as a sum of two squares. See 2sqb for the existence of such a decomposition. (Contributed by Thierry Arnoux, 2-Feb-2020)

Ref Expression
Assertion 2sqmo ( 𝑃 ∈ ℙ → ∃* 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑏 ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 )
2 nfre1 ⊢ Ⅎ 𝑏 ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 )
3 1 2 nfan ⊢ Ⅎ 𝑏 ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
4 nfv ⊢ Ⅎ 𝑏 𝑑 ∈ ℕ0
5 3 4 nfan ⊢ Ⅎ 𝑏 ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) ∧ 𝑑 ∈ ℕ0 )
6 nfv ⊢ Ⅎ 𝑏 𝑐 ≤ 𝑑
7 5 6 nfan ⊢ Ⅎ 𝑏 ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 )
8 nfv ⊢ Ⅎ 𝑏 ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃
9 7 8 nfan ⊢ Ⅎ 𝑏 ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 )
10 simp-8l ⊢ ( ( ( ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑎 ≤ 𝑏 ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → 𝑃 ∈ ℙ )
11 simp-8r ⊢ ( ( ( ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑎 ≤ 𝑏 ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → 𝑎 ∈ ℕ0 )
12 simpllr ⊢ ( ( ( ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑎 ≤ 𝑏 ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → 𝑏 ∈ ℕ0 )
13 simp-7r ⊢ ( ( ( ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑎 ≤ 𝑏 ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → 𝑐 ∈ ℕ0 )
14 simp-6r ⊢ ( ( ( ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑎 ≤ 𝑏 ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → 𝑑 ∈ ℕ0 )
15 simplr ⊢ ( ( ( ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑎 ≤ 𝑏 ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → 𝑎 ≤ 𝑏 )
16 simp-5r ⊢ ( ( ( ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑎 ≤ 𝑏 ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → 𝑐 ≤ 𝑑 )
17 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑎 ≤ 𝑏 ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 )
18 simp-4r ⊢ ( ( ( ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑎 ≤ 𝑏 ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 )
19 10 11 12 13 14 15 16 17 18 2sqmod ⊢ ( ( ( ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑎 ≤ 𝑏 ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) )
20 19 simpld ⊢ ( ( ( ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑎 ≤ 𝑏 ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → 𝑎 = 𝑐 )
21 20 anasss ⊢ ( ( ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) → 𝑎 = 𝑐 )
22 21 adantl5r ⊢ ( ( ( ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) → 𝑎 = 𝑐 )
23 simp-4r ⊢ ( ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) → ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
24 9 22 23 r19.29af ⊢ ( ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑐 ≤ 𝑑 ) ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) → 𝑎 = 𝑐 )
25 24 anasss ⊢ ( ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑐 ≤ 𝑑 ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ) → 𝑎 = 𝑐 )
26 25 r19.29an ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) ∧ ∃ 𝑑 ∈ ℕ0 ( 𝑐 ≤ 𝑑 ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ) → 𝑎 = 𝑐 )
27 26 expl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) → ( ( ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ∧ ∃ 𝑑 ∈ ℕ0 ( 𝑐 ≤ 𝑑 ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ) → 𝑎 = 𝑐 ) )
28 27 ralrimiva ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) → ∀ 𝑐 ∈ ℕ0 ( ( ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ∧ ∃ 𝑑 ∈ ℕ0 ( 𝑐 ≤ 𝑑 ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ) → 𝑎 = 𝑐 ) )
29 28 ralrimiva ⊢ ( 𝑃 ∈ ℙ → ∀ 𝑎 ∈ ℕ0 ∀ 𝑐 ∈ ℕ0 ( ( ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ∧ ∃ 𝑑 ∈ ℕ0 ( 𝑐 ≤ 𝑑 ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ) → 𝑎 = 𝑐 ) )
30 breq12 ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑎 ≤ 𝑏 ↔ 𝑐 ≤ 𝑑 ) )
31 simpl ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → 𝑎 = 𝑐 )
32 31 oveq1d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑎 ↑ 2 ) = ( 𝑐 ↑ 2 ) )
33 simpr ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → 𝑏 = 𝑑 )
34 33 oveq1d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑏 ↑ 2 ) = ( 𝑑 ↑ 2 ) )
35 32 34 oveq12d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) )
36 35 eqeq1d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ↔ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) )
37 30 36 anbi12d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ( 𝑐 ≤ 𝑑 ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ) )
38 37 cbvrexdva ⊢ ( 𝑎 = 𝑐 → ( ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ∃ 𝑑 ∈ ℕ0 ( 𝑐 ≤ 𝑑 ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ) )
39 38 rmo4 ⊢ ( ∃* 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ∀ 𝑎 ∈ ℕ0 ∀ 𝑐 ∈ ℕ0 ( ( ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ∧ ∃ 𝑑 ∈ ℕ0 ( 𝑐 ≤ 𝑑 ∧ ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = 𝑃 ) ) → 𝑎 = 𝑐 ) )
40 29 39 sylibr ⊢ ( 𝑃 ∈ ℙ → ∃* 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )