Proof of Theorem 2sqreultlem
| Step | Hyp | Ref
| Expression |
| 1 | | 2sqreulem1 27490 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) →
∃!𝑎 ∈
ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) |
| 2 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑎 → (𝑏↑2) = (𝑎↑2)) |
| 3 | 2 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑎 → ((𝑎↑2) + (𝑏↑2)) = ((𝑎↑2) + (𝑎↑2))) |
| 4 | 3 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0))
→ ((𝑎↑2) + (𝑏↑2)) = ((𝑎↑2) + (𝑎↑2))) |
| 5 | | nn0cn 12536 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
ℂ) |
| 6 | 5 | sqcld 14184 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ ℕ0
→ (𝑎↑2) ∈
ℂ) |
| 7 | | 2times 12402 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎↑2) ∈ ℂ →
(2 · (𝑎↑2)) =
((𝑎↑2) + (𝑎↑2))) |
| 8 | 7 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎↑2) ∈ ℂ →
((𝑎↑2) + (𝑎↑2)) = (2 · (𝑎↑2))) |
| 9 | 6, 8 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℕ0
→ ((𝑎↑2) + (𝑎↑2)) = (2 · (𝑎↑2))) |
| 10 | 9 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0)
→ ((𝑎↑2) + (𝑎↑2)) = (2 · (𝑎↑2))) |
| 11 | 10 | ad2antrl 728 |
. . . . . . . . . . . . 13
⊢ ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0))
→ ((𝑎↑2) + (𝑎↑2)) = (2 · (𝑎↑2))) |
| 12 | 4, 11 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0))
→ ((𝑎↑2) + (𝑏↑2)) = (2 · (𝑎↑2))) |
| 13 | 12 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0))
→ (((𝑎↑2) +
(𝑏↑2)) = 𝑃 ↔ (2 · (𝑎↑2)) = 𝑃)) |
| 14 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 = (2 · (𝑎↑2)) → (𝑃 mod 4) = ((2 · (𝑎↑2)) mod
4)) |
| 15 | 14 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 = (2 · (𝑎↑2)) → ((𝑃 mod 4) = 1 ↔ ((2 ·
(𝑎↑2)) mod 4) =
1)) |
| 16 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 = (2 · (𝑎↑2)) → (𝑃 ∈ ℙ ↔ (2
· (𝑎↑2)) ∈
ℙ)) |
| 17 | 15, 16 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 = (2 · (𝑎↑2)) → (((𝑃 mod 4) = 1 ∧ 𝑃 ∈ ℙ) ↔ (((2
· (𝑎↑2)) mod 4)
= 1 ∧ (2 · (𝑎↑2)) ∈ ℙ))) |
| 18 | | nn0z 12638 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
ℤ) |
| 19 | | 2nn0 12543 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℕ0 |
| 20 | | zexpcl 14117 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ ℤ ∧ 2 ∈
ℕ0) → (𝑎↑2) ∈ ℤ) |
| 21 | 18, 19, 20 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 ∈ ℕ0
→ (𝑎↑2) ∈
ℤ) |
| 22 | | 2mulprm 16730 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎↑2) ∈ ℤ →
((2 · (𝑎↑2))
∈ ℙ ↔ (𝑎↑2) = 1)) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ℕ0
→ ((2 · (𝑎↑2)) ∈ ℙ ↔ (𝑎↑2) = 1)) |
| 24 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎↑2) = 1 → (2 ·
(𝑎↑2)) = (2 ·
1)) |
| 25 | | 2t1e2 12429 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (2
· 1) = 2 |
| 26 | 24, 25 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎↑2) = 1 → (2 ·
(𝑎↑2)) =
2) |
| 27 | 26 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎↑2) = 1 → ((2 ·
(𝑎↑2)) mod 4) = (2 mod
4)) |
| 28 | | 2re 12340 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℝ |
| 29 | | 4nn 12349 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 4 ∈
ℕ |
| 30 | | nnrp 13046 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
| 31 | 29, 30 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 4 ∈
ℝ+ |
| 32 | | 0le2 12368 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ≤
2 |
| 33 | | 2lt4 12441 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 <
4 |
| 34 | | modid 13936 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((2
∈ ℝ ∧ 4 ∈ ℝ+) ∧ (0 ≤ 2 ∧ 2 <
4)) → (2 mod 4) = 2) |
| 35 | 28, 31, 32, 33, 34 | mp4an 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 mod 4)
= 2 |
| 36 | 27, 35 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎↑2) = 1 → ((2 ·
(𝑎↑2)) mod 4) =
2) |
| 37 | 36 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎↑2) = 1 → (((2
· (𝑎↑2)) mod 4)
= 1 ↔ 2 = 1)) |
| 38 | | 1ne2 12474 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ≠
2 |
| 39 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 = 1
↔ 1 = 2) |
| 40 | | eqneqall 2951 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (1 = 2
→ (1 ≠ 2 → (𝑎
≤ 𝑏 → 𝑏 ≠ 𝑎))) |
| 41 | 40 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 ≠ 2
→ (1 = 2 → (𝑎
≤ 𝑏 → 𝑏 ≠ 𝑎))) |
| 42 | 39, 41 | biimtrid 242 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 ≠ 2
→ (2 = 1 → (𝑎
≤ 𝑏 → 𝑏 ≠ 𝑎))) |
| 43 | 38, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 = 1
→ (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)) |
| 44 | 37, 43 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎↑2) = 1 → (((2
· (𝑎↑2)) mod 4)
= 1 → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))) |
| 45 | 23, 44 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ ℕ0
→ ((2 · (𝑎↑2)) ∈ ℙ → (((2 ·
(𝑎↑2)) mod 4) = 1
→ (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))) |
| 46 | 45 | impcomd 411 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ ℕ0
→ ((((2 · (𝑎↑2)) mod 4) = 1 ∧ (2 · (𝑎↑2)) ∈ ℙ) →
(𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))) |
| 47 | 46 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((2
· (𝑎↑2)) mod 4)
= 1 ∧ (2 · (𝑎↑2)) ∈ ℙ) → (𝑎 ∈ ℕ0
→ (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))) |
| 48 | 17, 47 | biimtrdi 253 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 = (2 · (𝑎↑2)) → (((𝑃 mod 4) = 1 ∧ 𝑃 ∈ ℙ) → (𝑎 ∈ ℕ0
→ (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))) |
| 49 | 48 | expd 415 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 = (2 · (𝑎↑2)) → ((𝑃 mod 4) = 1 → (𝑃 ∈ ℙ → (𝑎 ∈ ℕ0
→ (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))))) |
| 50 | 49 | com34 91 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 = (2 · (𝑎↑2)) → ((𝑃 mod 4) = 1 → (𝑎 ∈ ℕ0
→ (𝑃 ∈ ℙ
→ (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))))) |
| 51 | 50 | eqcoms 2745 |
. . . . . . . . . . . . . 14
⊢ ((2
· (𝑎↑2)) =
𝑃 → ((𝑃 mod 4) = 1 → (𝑎 ∈ ℕ0
→ (𝑃 ∈ ℙ
→ (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))))) |
| 52 | 51 | com14 96 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 → (𝑎 ∈ ℕ0
→ ((2 · (𝑎↑2)) = 𝑃 → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))))) |
| 53 | 52 | imp31 417 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0)
→ ((2 · (𝑎↑2)) = 𝑃 → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))) |
| 54 | 53 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0))
→ ((2 · (𝑎↑2)) = 𝑃 → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))) |
| 55 | 13, 54 | sylbid 240 |
. . . . . . . . . 10
⊢ ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0))
→ (((𝑎↑2) +
(𝑏↑2)) = 𝑃 → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))) |
| 56 | 55 | expimpd 453 |
. . . . . . . . 9
⊢ (𝑏 = 𝑎 → (((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0)
∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))) |
| 57 | | 2a1 28 |
. . . . . . . . 9
⊢ (𝑏 ≠ 𝑎 → (((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0)
∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))) |
| 58 | 56, 57 | pm2.61ine 3025 |
. . . . . . . 8
⊢
(((((𝑃 ∈
ℙ ∧ (𝑃 mod 4) =
1) ∧ 𝑎 ∈
ℕ0) ∧ 𝑏 ∈ ℕ0) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)) |
| 59 | 58 | pm4.71d 561 |
. . . . . . 7
⊢
(((((𝑃 ∈
ℙ ∧ (𝑃 mod 4) =
1) ∧ 𝑎 ∈
ℕ0) ∧ 𝑏 ∈ ℕ0) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → (𝑎 ≤ 𝑏 ↔ (𝑎 ≤ 𝑏 ∧ 𝑏 ≠ 𝑎))) |
| 60 | | nn0re 12535 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
ℝ) |
| 61 | 60 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0)
→ 𝑎 ∈
ℝ) |
| 62 | | nn0re 12535 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ℕ0
→ 𝑏 ∈
ℝ) |
| 63 | | ltlen 11362 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 < 𝑏 ↔ (𝑎 ≤ 𝑏 ∧ 𝑏 ≠ 𝑎))) |
| 64 | 61, 62, 63 | syl2an 596 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0)
∧ 𝑏 ∈
ℕ0) → (𝑎 < 𝑏 ↔ (𝑎 ≤ 𝑏 ∧ 𝑏 ≠ 𝑎))) |
| 65 | 64 | bibi2d 342 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0)
∧ 𝑏 ∈
ℕ0) → ((𝑎 ≤ 𝑏 ↔ 𝑎 < 𝑏) ↔ (𝑎 ≤ 𝑏 ↔ (𝑎 ≤ 𝑏 ∧ 𝑏 ≠ 𝑎)))) |
| 66 | 65 | adantr 480 |
. . . . . . 7
⊢
(((((𝑃 ∈
ℙ ∧ (𝑃 mod 4) =
1) ∧ 𝑎 ∈
ℕ0) ∧ 𝑏 ∈ ℕ0) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → ((𝑎 ≤ 𝑏 ↔ 𝑎 < 𝑏) ↔ (𝑎 ≤ 𝑏 ↔ (𝑎 ≤ 𝑏 ∧ 𝑏 ≠ 𝑎)))) |
| 67 | 59, 66 | mpbird 257 |
. . . . . 6
⊢
(((((𝑃 ∈
ℙ ∧ (𝑃 mod 4) =
1) ∧ 𝑎 ∈
ℕ0) ∧ 𝑏 ∈ ℕ0) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → (𝑎 ≤ 𝑏 ↔ 𝑎 < 𝑏)) |
| 68 | 67 | ex 412 |
. . . . 5
⊢ ((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0)
∧ 𝑏 ∈
ℕ0) → (((𝑎↑2) + (𝑏↑2)) = 𝑃 → (𝑎 ≤ 𝑏 ↔ 𝑎 < 𝑏))) |
| 69 | 68 | pm5.32rd 578 |
. . . 4
⊢ ((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0)
∧ 𝑏 ∈
ℕ0) → ((𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))) |
| 70 | 69 | reubidva 3396 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0)
→ (∃!𝑏 ∈
ℕ0 (𝑎 ≤
𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))) |
| 71 | 70 | reubidva 3396 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) →
(∃!𝑎 ∈
ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0
(𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))) |
| 72 | 1, 71 | mpbid 232 |
1
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) →
∃!𝑎 ∈
ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) |