Step | Hyp | Ref
| Expression |
1 | | elfz1end 12242 |
. . . . 5
⊢ (𝐵 ∈ ℕ ↔ 𝐵 ∈ (1...𝐵)) |
2 | 1 | biimpi 205 |
. . . 4
⊢ (𝐵 ∈ ℕ → 𝐵 ∈ (1...𝐵)) |
3 | | oveq2 6557 |
. . . . . 6
⊢ (𝑚 = 1 → (1...𝑚) = (1...1)) |
4 | 3 | raleqdv 3121 |
. . . . 5
⊢ (𝑚 = 1 → (∀𝑏 ∈ (1...𝑚)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ ∀𝑏 ∈ (1...1)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))) |
5 | | oveq2 6557 |
. . . . . 6
⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛)) |
6 | 5 | raleqdv 3121 |
. . . . 5
⊢ (𝑚 = 𝑛 → (∀𝑏 ∈ (1...𝑚)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ ∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))) |
7 | | oveq2 6557 |
. . . . . 6
⊢ (𝑚 = (𝑛 + 1) → (1...𝑚) = (1...(𝑛 + 1))) |
8 | 7 | raleqdv 3121 |
. . . . 5
⊢ (𝑚 = (𝑛 + 1) → (∀𝑏 ∈ (1...𝑚)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ ∀𝑏 ∈ (1...(𝑛 + 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))) |
9 | | oveq2 6557 |
. . . . . 6
⊢ (𝑚 = 𝐵 → (1...𝑚) = (1...𝐵)) |
10 | 9 | raleqdv 3121 |
. . . . 5
⊢ (𝑚 = 𝐵 → (∀𝑏 ∈ (1...𝑚)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ ∀𝑏 ∈ (1...𝐵)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))) |
11 | | elfz1eq 12223 |
. . . . . . . . 9
⊢ (𝑏 ∈ (1...1) → 𝑏 = 1) |
12 | | 1z 11284 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
13 | | zgz 15475 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → 1 ∈ ℤ[i]) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . 11
⊢ 1 ∈
ℤ[i] |
15 | | sq1 12820 |
. . . . . . . . . . . 12
⊢
(1↑2) = 1 |
16 | 15 | eqcomi 2619 |
. . . . . . . . . . 11
⊢ 1 =
(1↑2) |
17 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 1 → (abs‘𝑥) =
(abs‘1)) |
18 | | abs1 13885 |
. . . . . . . . . . . . . . 15
⊢
(abs‘1) = 1 |
19 | 17, 18 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (abs‘𝑥) = 1) |
20 | 19 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → ((abs‘𝑥)↑2) =
(1↑2)) |
21 | 20 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → (1 =
((abs‘𝑥)↑2)
↔ 1 = (1↑2))) |
22 | 21 | rspcev 3282 |
. . . . . . . . . . 11
⊢ ((1
∈ ℤ[i] ∧ 1 = (1↑2)) → ∃𝑥 ∈ ℤ[i] 1 = ((abs‘𝑥)↑2)) |
23 | 14, 16, 22 | mp2an 704 |
. . . . . . . . . 10
⊢
∃𝑥 ∈
ℤ[i] 1 = ((abs‘𝑥)↑2) |
24 | | 2sq.1 |
. . . . . . . . . . 11
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) |
25 | 24 | 2sqlem1 24942 |
. . . . . . . . . 10
⊢ (1 ∈
𝑆 ↔ ∃𝑥 ∈ ℤ[i] 1 =
((abs‘𝑥)↑2)) |
26 | 23, 25 | mpbir 220 |
. . . . . . . . 9
⊢ 1 ∈
𝑆 |
27 | 11, 26 | syl6eqel 2696 |
. . . . . . . 8
⊢ (𝑏 ∈ (1...1) → 𝑏 ∈ 𝑆) |
28 | 27 | a1d 25 |
. . . . . . 7
⊢ (𝑏 ∈ (1...1) → (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) |
29 | 28 | ralrimivw 2950 |
. . . . . 6
⊢ (𝑏 ∈ (1...1) →
∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) |
30 | 29 | rgen 2906 |
. . . . 5
⊢
∀𝑏 ∈
(1...1)∀𝑎 ∈
𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) |
31 | | 2sqlem7.2 |
. . . . . . . . . . . . 13
⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} |
32 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ ∧
∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) ∧ (𝑚 ∈ 𝑌 ∧ (𝑛 + 1) ∥ 𝑚)) → ∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) |
33 | | nncn 10905 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
34 | 33 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℕ ∧
∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) ∧ (𝑚 ∈ 𝑌 ∧ (𝑛 + 1) ∥ 𝑚)) → 𝑛 ∈ ℂ) |
35 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
36 | | pncan 10166 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
37 | 34, 35, 36 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℕ ∧
∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) ∧ (𝑚 ∈ 𝑌 ∧ (𝑛 + 1) ∥ 𝑚)) → ((𝑛 + 1) − 1) = 𝑛) |
38 | 37 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ ∧
∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) ∧ (𝑚 ∈ 𝑌 ∧ (𝑛 + 1) ∥ 𝑚)) → (1...((𝑛 + 1) − 1)) = (1...𝑛)) |
39 | 38 | raleqdv 3121 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ ∧
∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) ∧ (𝑚 ∈ 𝑌 ∧ (𝑛 + 1) ∥ 𝑚)) → (∀𝑏 ∈ (1...((𝑛 + 1) − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ ∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))) |
40 | 32, 39 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ ∧
∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) ∧ (𝑚 ∈ 𝑌 ∧ (𝑛 + 1) ∥ 𝑚)) → ∀𝑏 ∈ (1...((𝑛 + 1) − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) |
41 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ ∧
∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) ∧ (𝑚 ∈ 𝑌 ∧ (𝑛 + 1) ∥ 𝑚)) → (𝑛 + 1) ∥ 𝑚) |
42 | | peano2nn 10909 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
43 | 42 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ ∧
∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) ∧ (𝑚 ∈ 𝑌 ∧ (𝑛 + 1) ∥ 𝑚)) → (𝑛 + 1) ∈ ℕ) |
44 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ ∧
∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) ∧ (𝑚 ∈ 𝑌 ∧ (𝑛 + 1) ∥ 𝑚)) → 𝑚 ∈ 𝑌) |
45 | 24, 31, 40, 41, 43, 44 | 2sqlem9 24952 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ ∧
∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) ∧ (𝑚 ∈ 𝑌 ∧ (𝑛 + 1) ∥ 𝑚)) → (𝑛 + 1) ∈ 𝑆) |
46 | 45 | expr 641 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ ∧
∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) ∧ 𝑚 ∈ 𝑌) → ((𝑛 + 1) ∥ 𝑚 → (𝑛 + 1) ∈ 𝑆)) |
47 | 46 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧
∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) → ∀𝑚 ∈ 𝑌 ((𝑛 + 1) ∥ 𝑚 → (𝑛 + 1) ∈ 𝑆)) |
48 | 47 | ex 449 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(∀𝑏 ∈
(1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) → ∀𝑚 ∈ 𝑌 ((𝑛 + 1) ∥ 𝑚 → (𝑛 + 1) ∈ 𝑆))) |
49 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑚 → ((𝑛 + 1) ∥ 𝑎 ↔ (𝑛 + 1) ∥ 𝑚)) |
50 | 49 | imbi1d 330 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑚 → (((𝑛 + 1) ∥ 𝑎 → (𝑛 + 1) ∈ 𝑆) ↔ ((𝑛 + 1) ∥ 𝑚 → (𝑛 + 1) ∈ 𝑆))) |
51 | 50 | cbvralv 3147 |
. . . . . . . . 9
⊢
(∀𝑎 ∈
𝑌 ((𝑛 + 1) ∥ 𝑎 → (𝑛 + 1) ∈ 𝑆) ↔ ∀𝑚 ∈ 𝑌 ((𝑛 + 1) ∥ 𝑚 → (𝑛 + 1) ∈ 𝑆)) |
52 | 48, 51 | syl6ibr 241 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(∀𝑏 ∈
(1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) → ∀𝑎 ∈ 𝑌 ((𝑛 + 1) ∥ 𝑎 → (𝑛 + 1) ∈ 𝑆))) |
53 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑛 + 1) ∈ V |
54 | | breq1 4586 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑛 + 1) → (𝑏 ∥ 𝑎 ↔ (𝑛 + 1) ∥ 𝑎)) |
55 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑛 + 1) → (𝑏 ∈ 𝑆 ↔ (𝑛 + 1) ∈ 𝑆)) |
56 | 54, 55 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑏 = (𝑛 + 1) → ((𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ ((𝑛 + 1) ∥ 𝑎 → (𝑛 + 1) ∈ 𝑆))) |
57 | 56 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑏 = (𝑛 + 1) → (∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ ∀𝑎 ∈ 𝑌 ((𝑛 + 1) ∥ 𝑎 → (𝑛 + 1) ∈ 𝑆))) |
58 | 53, 57 | ralsn 4169 |
. . . . . . . 8
⊢
(∀𝑏 ∈
{(𝑛 + 1)}∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ ∀𝑎 ∈ 𝑌 ((𝑛 + 1) ∥ 𝑎 → (𝑛 + 1) ∈ 𝑆)) |
59 | 52, 58 | syl6ibr 241 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
(∀𝑏 ∈
(1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) → ∀𝑏 ∈ {(𝑛 + 1)}∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))) |
60 | 59 | ancld 574 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(∀𝑏 ∈
(1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) → (∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ∧ ∀𝑏 ∈ {(𝑛 + 1)}∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)))) |
61 | | elnnuz 11600 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) |
62 | | fzsuc 12258 |
. . . . . . . . 9
⊢ (𝑛 ∈
(ℤ≥‘1) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)})) |
63 | 61, 62 | sylbi 206 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)})) |
64 | 63 | raleqdv 3121 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
(∀𝑏 ∈
(1...(𝑛 + 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ ∀𝑏 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))) |
65 | | ralunb 3756 |
. . . . . . 7
⊢
(∀𝑏 ∈
((1...𝑛) ∪ {(𝑛 + 1)})∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ (∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ∧ ∀𝑏 ∈ {(𝑛 + 1)}∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))) |
66 | 64, 65 | syl6bb 275 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(∀𝑏 ∈
(1...(𝑛 + 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ (∀𝑏 ∈ (1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ∧ ∀𝑏 ∈ {(𝑛 + 1)}∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)))) |
67 | 60, 66 | sylibrd 248 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
(∀𝑏 ∈
(1...𝑛)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) → ∀𝑏 ∈ (1...(𝑛 + 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))) |
68 | 4, 6, 8, 10, 30, 67 | nnind 10915 |
. . . 4
⊢ (𝐵 ∈ ℕ →
∀𝑏 ∈ (1...𝐵)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) |
69 | | breq1 4586 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (𝑏 ∥ 𝑎 ↔ 𝐵 ∥ 𝑎)) |
70 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (𝑏 ∈ 𝑆 ↔ 𝐵 ∈ 𝑆)) |
71 | 69, 70 | imbi12d 333 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ((𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ (𝐵 ∥ 𝑎 → 𝐵 ∈ 𝑆))) |
72 | 71 | ralbidv 2969 |
. . . . 5
⊢ (𝑏 = 𝐵 → (∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ ∀𝑎 ∈ 𝑌 (𝐵 ∥ 𝑎 → 𝐵 ∈ 𝑆))) |
73 | 72 | rspcv 3278 |
. . . 4
⊢ (𝐵 ∈ (1...𝐵) → (∀𝑏 ∈ (1...𝐵)∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) → ∀𝑎 ∈ 𝑌 (𝐵 ∥ 𝑎 → 𝐵 ∈ 𝑆))) |
74 | 2, 68, 73 | sylc 63 |
. . 3
⊢ (𝐵 ∈ ℕ →
∀𝑎 ∈ 𝑌 (𝐵 ∥ 𝑎 → 𝐵 ∈ 𝑆)) |
75 | | breq2 4587 |
. . . . 5
⊢ (𝑎 = 𝐴 → (𝐵 ∥ 𝑎 ↔ 𝐵 ∥ 𝐴)) |
76 | 75 | imbi1d 330 |
. . . 4
⊢ (𝑎 = 𝐴 → ((𝐵 ∥ 𝑎 → 𝐵 ∈ 𝑆) ↔ (𝐵 ∥ 𝐴 → 𝐵 ∈ 𝑆))) |
77 | 76 | rspcv 3278 |
. . 3
⊢ (𝐴 ∈ 𝑌 → (∀𝑎 ∈ 𝑌 (𝐵 ∥ 𝑎 → 𝐵 ∈ 𝑆) → (𝐵 ∥ 𝐴 → 𝐵 ∈ 𝑆))) |
78 | 74, 77 | syl5 33 |
. 2
⊢ (𝐴 ∈ 𝑌 → (𝐵 ∈ ℕ → (𝐵 ∥ 𝐴 → 𝐵 ∈ 𝑆))) |
79 | 78 | 3imp 1249 |
1
⊢ ((𝐴 ∈ 𝑌 ∧ 𝐵 ∈ ℕ ∧ 𝐵 ∥ 𝐴) → 𝐵 ∈ 𝑆) |