Metamath Proof Explorer

Theorem 2sqreunnltlem

Description: Lemma for 2sqreunnlt . (Contributed by AV, 4-Jun-2023) Specialization to different integers, proposed by GL. (Revised by AV, 11-Jun-2023)

Ref Expression
Assertion 2sqreunnltlem ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ∃! 𝑎 ∈ ℕ ∃! 𝑏 ∈ ℕ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )

Proof

Step Hyp Ref Expression
1 2sqreunnlem1 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ∃! 𝑎 ∈ ℕ ∃! 𝑏 ∈ ℕ ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
2 oveq1 ⊢ ( 𝑏 = 𝑎 → ( 𝑏 ↑ 2 ) = ( 𝑎 ↑ 2 ) )
3 2 oveq2d ⊢ ( 𝑏 = 𝑎 → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( ( 𝑎 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) )
4 3 adantr ⊢ ( ( 𝑏 = 𝑎 ∧ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( ( 𝑎 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) )
5 nncn ⊢ ( 𝑎 ∈ ℕ → 𝑎 ∈ ℂ )
6 5 sqcld ⊢ ( 𝑎 ∈ ℕ → ( 𝑎 ↑ 2 ) ∈ ℂ )
7 2times ⊢ ( ( 𝑎 ↑ 2 ) ∈ ℂ → ( 2 · ( 𝑎 ↑ 2 ) ) = ( ( 𝑎 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) )
8 7 eqcomd ⊢ ( ( 𝑎 ↑ 2 ) ∈ ℂ → ( ( 𝑎 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 2 · ( 𝑎 ↑ 2 ) ) )
9 6 8 syl ⊢ ( 𝑎 ∈ ℕ → ( ( 𝑎 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 2 · ( 𝑎 ↑ 2 ) ) )
10 9 adantl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) → ( ( 𝑎 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 2 · ( 𝑎 ↑ 2 ) ) )
11 10 ad2antrl ⊢ ( ( 𝑏 = 𝑎 ∧ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) ) → ( ( 𝑎 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 2 · ( 𝑎 ↑ 2 ) ) )
12 4 11 eqtrd ⊢ ( ( 𝑏 = 𝑎 ∧ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 2 · ( 𝑎 ↑ 2 ) ) )
13 12 eqeq1d ⊢ ( ( 𝑏 = 𝑎 ∧ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) ) → ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ↔ ( 2 · ( 𝑎 ↑ 2 ) ) = 𝑃 ) )
14 oveq1 ⊢ ( 𝑃 = ( 2 · ( 𝑎 ↑ 2 ) ) → ( 𝑃 mod 4 ) = ( ( 2 · ( 𝑎 ↑ 2 ) ) mod 4 ) )
15 14 eqeq1d ⊢ ( 𝑃 = ( 2 · ( 𝑎 ↑ 2 ) ) → ( ( 𝑃 mod 4 ) = 1 ↔ ( ( 2 · ( 𝑎 ↑ 2 ) ) mod 4 ) = 1 ) )
16 eleq1 ⊢ ( 𝑃 = ( 2 · ( 𝑎 ↑ 2 ) ) → ( 𝑃 ∈ ℙ ↔ ( 2 · ( 𝑎 ↑ 2 ) ) ∈ ℙ ) )
17 15 16 anbi12d ⊢ ( 𝑃 = ( 2 · ( 𝑎 ↑ 2 ) ) → ( ( ( 𝑃 mod 4 ) = 1 ∧ 𝑃 ∈ ℙ ) ↔ ( ( ( 2 · ( 𝑎 ↑ 2 ) ) mod 4 ) = 1 ∧ ( 2 · ( 𝑎 ↑ 2 ) ) ∈ ℙ ) ) )
18 nnz ⊢ ( 𝑎 ∈ ℕ → 𝑎 ∈ ℤ )
19 2nn0 ⊢ 2 ∈ ℕ0
20 zexpcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 2 ∈ ℕ0 ) → ( 𝑎 ↑ 2 ) ∈ ℤ )
21 18 19 20 sylancl ⊢ ( 𝑎 ∈ ℕ → ( 𝑎 ↑ 2 ) ∈ ℤ )
22 2mulprm ⊢ ( ( 𝑎 ↑ 2 ) ∈ ℤ → ( ( 2 · ( 𝑎 ↑ 2 ) ) ∈ ℙ ↔ ( 𝑎 ↑ 2 ) = 1 ) )
23 21 22 syl ⊢ ( 𝑎 ∈ ℕ → ( ( 2 · ( 𝑎 ↑ 2 ) ) ∈ ℙ ↔ ( 𝑎 ↑ 2 ) = 1 ) )
24 oveq2 ⊢ ( ( 𝑎 ↑ 2 ) = 1 → ( 2 · ( 𝑎 ↑ 2 ) ) = ( 2 · 1 ) )
25 2t1e2 ⊢ ( 2 · 1 ) = 2
26 24 25 eqtrdi ⊢ ( ( 𝑎 ↑ 2 ) = 1 → ( 2 · ( 𝑎 ↑ 2 ) ) = 2 )
27 26 oveq1d ⊢ ( ( 𝑎 ↑ 2 ) = 1 → ( ( 2 · ( 𝑎 ↑ 2 ) ) mod 4 ) = ( 2 mod 4 ) )
28 2re ⊢ 2 ∈ ℝ
29 4nn ⊢ 4 ∈ ℕ
30 nnrp ⊢ ( 4 ∈ ℕ → 4 ∈ ℝ+ )
31 29 30 ax-mp ⊢ 4 ∈ ℝ+
32 0le2 ⊢ 0 ≤ 2
33 2lt4 ⊢ 2 < 4
34 modid ⊢ ( ( ( 2 ∈ ℝ ∧ 4 ∈ ℝ+ ) ∧ ( 0 ≤ 2 ∧ 2 < 4 ) ) → ( 2 mod 4 ) = 2 )
35 28 31 32 33 34 mp4an ⊢ ( 2 mod 4 ) = 2
36 27 35 eqtrdi ⊢ ( ( 𝑎 ↑ 2 ) = 1 → ( ( 2 · ( 𝑎 ↑ 2 ) ) mod 4 ) = 2 )
37 36 eqeq1d ⊢ ( ( 𝑎 ↑ 2 ) = 1 → ( ( ( 2 · ( 𝑎 ↑ 2 ) ) mod 4 ) = 1 ↔ 2 = 1 ) )
38 1ne2 ⊢ 1 ≠ 2
39 eqcom ⊢ ( 2 = 1 ↔ 1 = 2 )
40 eqneqall ⊢ ( 1 = 2 → ( 1 ≠ 2 → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) )
41 40 com12 ⊢ ( 1 ≠ 2 → ( 1 = 2 → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) )
42 39 41 syl5bi ⊢ ( 1 ≠ 2 → ( 2 = 1 → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) )
43 38 42 ax-mp ⊢ ( 2 = 1 → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) )
44 37 43 syl6bi ⊢ ( ( 𝑎 ↑ 2 ) = 1 → ( ( ( 2 · ( 𝑎 ↑ 2 ) ) mod 4 ) = 1 → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) )
45 23 44 syl6bi ⊢ ( 𝑎 ∈ ℕ → ( ( 2 · ( 𝑎 ↑ 2 ) ) ∈ ℙ → ( ( ( 2 · ( 𝑎 ↑ 2 ) ) mod 4 ) = 1 → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) ) )
46 45 impcomd ⊢ ( 𝑎 ∈ ℕ → ( ( ( ( 2 · ( 𝑎 ↑ 2 ) ) mod 4 ) = 1 ∧ ( 2 · ( 𝑎 ↑ 2 ) ) ∈ ℙ ) → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) )
47 46 com12 ⊢ ( ( ( ( 2 · ( 𝑎 ↑ 2 ) ) mod 4 ) = 1 ∧ ( 2 · ( 𝑎 ↑ 2 ) ) ∈ ℙ ) → ( 𝑎 ∈ ℕ → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) )
48 17 47 syl6bi ⊢ ( 𝑃 = ( 2 · ( 𝑎 ↑ 2 ) ) → ( ( ( 𝑃 mod 4 ) = 1 ∧ 𝑃 ∈ ℙ ) → ( 𝑎 ∈ ℕ → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) ) )
49 48 expd ⊢ ( 𝑃 = ( 2 · ( 𝑎 ↑ 2 ) ) → ( ( 𝑃 mod 4 ) = 1 → ( 𝑃 ∈ ℙ → ( 𝑎 ∈ ℕ → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) ) ) )
50 49 com34 ⊢ ( 𝑃 = ( 2 · ( 𝑎 ↑ 2 ) ) → ( ( 𝑃 mod 4 ) = 1 → ( 𝑎 ∈ ℕ → ( 𝑃 ∈ ℙ → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) ) ) )
51 50 eqcoms ⊢ ( ( 2 · ( 𝑎 ↑ 2 ) ) = 𝑃 → ( ( 𝑃 mod 4 ) = 1 → ( 𝑎 ∈ ℕ → ( 𝑃 ∈ ℙ → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) ) ) )
52 51 com14 ⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 mod 4 ) = 1 → ( 𝑎 ∈ ℕ → ( ( 2 · ( 𝑎 ↑ 2 ) ) = 𝑃 → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) ) ) )
53 52 imp31 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) → ( ( 2 · ( 𝑎 ↑ 2 ) ) = 𝑃 → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) )
54 53 ad2antrl ⊢ ( ( 𝑏 = 𝑎 ∧ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) ) → ( ( 2 · ( 𝑎 ↑ 2 ) ) = 𝑃 → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) )
55 13 54 sylbid ⊢ ( ( 𝑏 = 𝑎 ∧ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) ) → ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) )
56 55 expimpd ⊢ ( 𝑏 = 𝑎 → ( ( ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) )
57 2a1 ⊢ ( 𝑏 ≠ 𝑎 → ( ( ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) ) )
58 56 57 pm2.61ine ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎 ) )
59 58 pm4.71d ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑎 ≤ 𝑏 ↔ ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≠ 𝑎 ) ) )
60 nnre ⊢ ( 𝑎 ∈ ℕ → 𝑎 ∈ ℝ )
61 60 adantl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) → 𝑎 ∈ ℝ )
62 nnre ⊢ ( 𝑏 ∈ ℕ → 𝑏 ∈ ℝ )
63 ltlen ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑎 < 𝑏 ↔ ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≠ 𝑎 ) ) )
64 61 62 63 syl2an ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) → ( 𝑎 < 𝑏 ↔ ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≠ 𝑎 ) ) )
65 64 bibi2d ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) → ( ( 𝑎 ≤ 𝑏 ↔ 𝑎 < 𝑏 ) ↔ ( 𝑎 ≤ 𝑏 ↔ ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≠ 𝑎 ) ) ) )
66 65 adantr ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( ( 𝑎 ≤ 𝑏 ↔ 𝑎 < 𝑏 ) ↔ ( 𝑎 ≤ 𝑏 ↔ ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≠ 𝑎 ) ) ) )
67 59 66 mpbird ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑎 ≤ 𝑏 ↔ 𝑎 < 𝑏 ) )
68 67 ex ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) → ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 → ( 𝑎 ≤ 𝑏 ↔ 𝑎 < 𝑏 ) ) )
69 68 pm5.32rd ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ℕ ) → ( ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) )
70 69 reubidva ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ 𝑎 ∈ ℕ ) → ( ∃! 𝑏 ∈ ℕ ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ∃! 𝑏 ∈ ℕ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) )
71 70 reubidva ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ( ∃! 𝑎 ∈ ℕ ∃! 𝑏 ∈ ℕ ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ∃! 𝑎 ∈ ℕ ∃! 𝑏 ∈ ℕ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) )
72 1 71 mpbid ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ∃! 𝑎 ∈ ℕ ∃! 𝑏 ∈ ℕ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )