| Step | Hyp | Ref
| Expression |
| 1 | | simprl 529 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ (ℤ≥‘𝑀)) |
| 2 | | simprr 531 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶) |
| 3 | | seqovcd.pl |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶) |
| 4 | 3 | ralrimivva 2579 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶) |
| 5 | | oveq1 5929 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → (𝑥 + 𝑦) = (𝑎 + 𝑦)) |
| 6 | 5 | eleq1d 2265 |
. . . . . . 7
⊢ (𝑥 = 𝑎 → ((𝑥 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑦) ∈ 𝐶)) |
| 7 | | oveq2 5930 |
. . . . . . . 8
⊢ (𝑦 = 𝑏 → (𝑎 + 𝑦) = (𝑎 + 𝑏)) |
| 8 | 7 | eleq1d 2265 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → ((𝑎 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑏) ∈ 𝐶)) |
| 9 | 6, 8 | cbvral2v 2742 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 ↔ ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶) |
| 10 | 4, 9 | sylib 122 |
. . . . 5
⊢ (𝜑 → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶) |
| 11 | 10 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶) |
| 12 | | fveq2 5558 |
. . . . . . 7
⊢ (𝑎 = (𝑥 + 1) → (𝐹‘𝑎) = (𝐹‘(𝑥 + 1))) |
| 13 | 12 | eleq1d 2265 |
. . . . . 6
⊢ (𝑎 = (𝑥 + 1) → ((𝐹‘𝑎) ∈ 𝐷 ↔ (𝐹‘(𝑥 + 1)) ∈ 𝐷)) |
| 14 | | seqovcd.f |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷) |
| 15 | 14 | ralrimiva 2570 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷) |
| 16 | | fveq2 5558 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎)) |
| 17 | 16 | eleq1d 2265 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → ((𝐹‘𝑥) ∈ 𝐷 ↔ (𝐹‘𝑎) ∈ 𝐷)) |
| 18 | 17 | cbvralv 2729 |
. . . . . . . 8
⊢
(∀𝑥 ∈
(ℤ≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷 ↔ ∀𝑎 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷) |
| 19 | 15, 18 | sylib 122 |
. . . . . . 7
⊢ (𝜑 → ∀𝑎 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷) |
| 20 | 19 | adantr 276 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷) |
| 21 | | eluzp1p1 9627 |
. . . . . . 7
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (𝑥 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
| 22 | 1, 21 | syl 14 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
| 23 | 13, 20, 22 | rspcdva 2873 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝐹‘(𝑥 + 1)) ∈ 𝐷) |
| 24 | | oveq12 5931 |
. . . . . . 7
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → (𝑎 + 𝑏) = (𝑦 + (𝐹‘(𝑥 + 1)))) |
| 25 | 24 | eleq1d 2265 |
. . . . . 6
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → ((𝑎 + 𝑏) ∈ 𝐶 ↔ (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶)) |
| 26 | 25 | rspc2gv 2880 |
. . . . 5
⊢ ((𝑦 ∈ 𝐶 ∧ (𝐹‘(𝑥 + 1)) ∈ 𝐷) → (∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶 → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶)) |
| 27 | 2, 23, 26 | syl2anc 411 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶 → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶)) |
| 28 | 11, 27 | mpd 13 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶) |
| 29 | | fvoveq1 5945 |
. . . . 5
⊢ (𝑧 = 𝑥 → (𝐹‘(𝑧 + 1)) = (𝐹‘(𝑥 + 1))) |
| 30 | 29 | oveq2d 5938 |
. . . 4
⊢ (𝑧 = 𝑥 → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘(𝑥 + 1)))) |
| 31 | | oveq1 5929 |
. . . 4
⊢ (𝑤 = 𝑦 → (𝑤 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘(𝑥 + 1)))) |
| 32 | | eqid 2196 |
. . . 4
⊢ (𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) |
| 33 | 30, 31, 32 | ovmpog 6057 |
. . 3
⊢ ((𝑥 ∈
(ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶 ∧ (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = (𝑦 + (𝐹‘(𝑥 + 1)))) |
| 34 | 1, 2, 28, 33 | syl3anc 1249 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = (𝑦 + (𝐹‘(𝑥 + 1)))) |
| 35 | 34, 28 | eqeltrd 2273 |
1
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) ∈ 𝐶) |