Metamath Proof Explorer

Theorem crctcshwlkn0lem2

Description: Lemma for crctcshwlkn0 . (Contributed by AV, 12-Mar-2021)

Ref Expression
Hypotheses crctcshwlkn0lem.s ⊢φ→S∈1..^N
crctcshwlkn0lem.q ⊢Q=x∈0…N⟼ifx≤N−SP⁡x+SP⁡x+S-N
Assertion crctcshwlkn0lem2 ⊢φ∧J∈0…N−S→Q⁡J=P⁡J+S

Proof

Step Hyp Ref Expression
1 crctcshwlkn0lem.s ⊢φ→S∈1..^N
2 crctcshwlkn0lem.q ⊢Q=x∈0…N⟼ifx≤N−SP⁡x+SP⁡x+S-N
3 breq1 ⊢x=J→x≤N−S↔J≤N−S
4 fvoveq1 ⊢x=J→P⁡x+S=P⁡J+S
5 oveq1 ⊢x=J→x+S=J+S
6 5 fvoveq1d ⊢x=J→P⁡x+S-N=P⁡J+S-N
7 3 4 6 ifbieq12d ⊢x=J→ifx≤N−SP⁡x+SP⁡x+S-N=ifJ≤N−SP⁡J+SP⁡J+S-N
8 fzo0ss1 ⊢1..^N⊆0..^N
9 8 sseli ⊢S∈1..^N→S∈0..^N
10 elfzoel2 ⊢S∈0..^N→N∈ℤ
11 elfzonn0 ⊢S∈0..^N→S∈ℕ0
12 eluzmn ⊢N∈ℤ∧S∈ℕ0→N∈ℤ≥N−S
13 10 11 12 syl2anc ⊢S∈0..^N→N∈ℤ≥N−S
14 fzss2 ⊢N∈ℤ≥N−S→0…N−S⊆0…N
15 13 14 syl ⊢S∈0..^N→0…N−S⊆0…N
16 15 sseld ⊢S∈0..^N→J∈0…N−S→J∈0…N
17 1 9 16 3syl ⊢φ→J∈0…N−S→J∈0…N
18 17 imp ⊢φ∧J∈0…N−S→J∈0…N
19 fvex ⊢P⁡J+S∈V
20 fvex ⊢P⁡J+S-N∈V
21 19 20 ifex ⊢ifJ≤N−SP⁡J+SP⁡J+S-N∈V
22 21 a1i ⊢φ∧J∈0…N−S→ifJ≤N−SP⁡J+SP⁡J+S-N∈V
23 2 7 18 22 fvmptd3 ⊢φ∧J∈0…N−S→Q⁡J=ifJ≤N−SP⁡J+SP⁡J+S-N
24 elfzle2 ⊢J∈0…N−S→J≤N−S
25 24 adantl ⊢φ∧J∈0…N−S→J≤N−S
26 25 iftrued ⊢φ∧J∈0…N−S→ifJ≤N−SP⁡J+SP⁡J+S-N=P⁡J+S
27 23 26 eqtrd ⊢φ∧J∈0…N−S→Q⁡J=P⁡J+S