Metamath Proof Explorer

Theorem metakunt33

Description: Construction of one solution of the increment equation system. (Contributed by metakunt, 18-Jul-2024)

Ref Expression
Hypotheses metakunt33.1 ⊢φ→M∈ℕ
metakunt33.2 ⊢φ→I∈ℕ
metakunt33.3 ⊢φ→I≤M
metakunt33.4 ⊢A=x∈1…M⟼ifx=IMifx<Ixx−1
metakunt33.5 ⊢B=z∈1…M⟼ifz=MMifz<Iz+M-Iz+1-I
metakunt33.6 ⊢C=y∈1…M⟼ify=MIify<Iyy+1
metakunt33.7 ⊢D=w∈1…M⟼ifw=Iwifw<Iw+M−I+ifI≤w+M-I10w-I+ifI≤w−I10
Assertion metakunt33 ⊢φ→C∘B∘A=D

Proof

Step Hyp Ref Expression
1 metakunt33.1 ⊢φ→M∈ℕ
2 metakunt33.2 ⊢φ→I∈ℕ
3 metakunt33.3 ⊢φ→I≤M
4 metakunt33.4 ⊢A=x∈1…M⟼ifx=IMifx<Ixx−1
5 metakunt33.5 ⊢B=z∈1…M⟼ifz=MMifz<Iz+M-Iz+1-I
6 metakunt33.6 ⊢C=y∈1…M⟼ify=MIify<Iyy+1
7 metakunt33.7 ⊢D=w∈1…M⟼ifw=Iwifw<Iw+M−I+ifI≤w+M-I10w-I+ifI≤w−I10
8 1 2 3 6 metakunt2 ⊢φ→C:1…M⟶1…M
9 1 2 3 5 metakunt25 ⊢φ→B:1…M⟶1-1 onto1…M
10 f1of ⊢B:1…M⟶1-1 onto1…M→B:1…M⟶1…M
11 9 10 syl ⊢φ→B:1…M⟶1…M
12 1 2 3 4 metakunt1 ⊢φ→A:1…M⟶1…M
13 11 12 fcod ⊢φ→B∘A:1…M⟶1…M
14 8 13 fcod ⊢φ→C∘B∘A:1…M⟶1…M
15 14 ffnd ⊢φ→C∘B∘AFn1…M
16 nfv ⊢Ⅎwφ
17 elfzelz ⊢w∈1…M→w∈ℤ
18 17 adantl ⊢φ∧w∈1…M→w∈ℤ
19 1 nnzd ⊢φ→M∈ℤ
20 19 adantr ⊢φ∧w∈1…M→M∈ℤ
21 2 nnzd ⊢φ→I∈ℤ
22 21 adantr ⊢φ∧w∈1…M→I∈ℤ
23 20 22 zsubcld ⊢φ∧w∈1…M→M−I∈ℤ
24 18 23 zaddcld ⊢φ∧w∈1…M→w+M-I∈ℤ
25 1zzd ⊢φ∧w∈1…M→1∈ℤ
26 0zd ⊢φ∧w∈1…M→0∈ℤ
27 25 26 ifcld ⊢φ∧w∈1…M→ifI≤w+M-I10∈ℤ
28 24 27 zaddcld ⊢φ∧w∈1…M→w+M−I+ifI≤w+M-I10∈ℤ
29 18 22 zsubcld ⊢φ∧w∈1…M→w−I∈ℤ
30 25 26 ifcld ⊢φ∧w∈1…M→ifI≤w−I10∈ℤ
31 29 30 zaddcld ⊢φ∧w∈1…M→w-I+ifI≤w−I10∈ℤ
32 28 31 ifcld ⊢φ∧w∈1…M→ifw<Iw+M−I+ifI≤w+M-I10w-I+ifI≤w−I10∈ℤ
33 18 32 ifcld ⊢φ∧w∈1…M→ifw=Iwifw<Iw+M−I+ifI≤w+M-I10w-I+ifI≤w−I10∈ℤ
34 16 33 7 fnmptd ⊢φ→DFn1…M
35 13 adantr ⊢φ∧a∈1…M→B∘A:1…M⟶1…M
36 simpr ⊢φ∧a∈1…M→a∈1…M
37 35 36 fvco3d ⊢φ∧a∈1…M→C∘B∘A⁡a=C⁡B∘A⁡a
38 12 adantr ⊢φ∧a∈1…M→A:1…M⟶1…M
39 38 36 fvco3d ⊢φ∧a∈1…M→B∘A⁡a=B⁡A⁡a
40 39 fveq2d ⊢φ∧a∈1…M→C⁡B∘A⁡a=C⁡B⁡A⁡a
41 37 40 eqtrd ⊢φ∧a∈1…M→C∘B∘A⁡a=C⁡B⁡A⁡a
42 1 adantr ⊢φ∧a∈1…M→M∈ℕ
43 2 adantr ⊢φ∧a∈1…M→I∈ℕ
44 3 adantr ⊢φ∧a∈1…M→I≤M
45 eqid ⊢ifI≤a+M-I10=ifI≤a+M-I10
46 eqid ⊢ifI≤a−I10=ifI≤a−I10
47 eqid ⊢ifa=Iaifa<Ia+M−I+ifI≤a+M-I10a-I+ifI≤a−I10=ifa=Iaifa<Ia+M−I+ifI≤a+M-I10a-I+ifI≤a−I10
48 42 43 44 36 4 5 6 45 46 47 metakunt31 ⊢φ∧a∈1…M→C⁡B⁡A⁡a=ifa=Iaifa<Ia+M−I+ifI≤a+M-I10a-I+ifI≤a−I10
49 42 43 44 36 7 45 46 47 metakunt32 ⊢φ∧a∈1…M→D⁡a=ifa=Iaifa<Ia+M−I+ifI≤a+M-I10a-I+ifI≤a−I10
50 49 eqcomd ⊢φ∧a∈1…M→ifa=Iaifa<Ia+M−I+ifI≤a+M-I10a-I+ifI≤a−I10=D⁡a
51 48 50 eqtrd ⊢φ∧a∈1…M→C⁡B⁡A⁡a=D⁡a
52 41 51 eqtrd ⊢φ∧a∈1…M→C∘B∘A⁡a=D⁡a
53 15 34 52 eqfnfvd ⊢φ→C∘B∘A=D