This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvnmptdivc

Description: Function-builder for iterated derivative, division rule for constant divisor. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvnmptdivc.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvnmptdivc.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
dvnmptdivc.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
dvnmptdivc.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → 𝐵 ∈ ℂ )
dvnmptdivc.dvn ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
dvnmptdivc.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
dvnmptdivc.cne0 ⊢ ( 𝜑 → 𝐶 ≠ 0 )
dvnmptdivc.8 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
Assertion dvnmptdivc ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 / 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 dvnmptdivc.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvnmptdivc.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
3 dvnmptdivc.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
4 dvnmptdivc.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → 𝐵 ∈ ℂ )
5 dvnmptdivc.dvn ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
6 dvnmptdivc.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
7 dvnmptdivc.cne0 ⊢ ( 𝜑 → 𝐶 ≠ 0 )
8 dvnmptdivc.8 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → 𝑛 ∈ ( 0 ... 𝑀 ) )
10 simpl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → 𝜑 )
11 fveq2 ⊢ ( 𝑘 = 0 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 0 ) )
12 csbeq1 ⊢ ( 𝑘 = 0 → ⦋ 𝑘 / 𝑛 ⦌ 𝐵 = ⦋ 0 / 𝑛 ⦌ 𝐵 )
13 12 oveq1d ⊢ ( 𝑘 = 0 → ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) = ( ⦋ 0 / 𝑛 ⦌ 𝐵 / 𝐶 ) )
14 13 mpteq2dv ⊢ ( 𝑘 = 0 → ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 0 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) )
15 11 14 eqeq12d ⊢ ( 𝑘 = 0 → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ↔ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 0 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) )
16 15 imbi2d ⊢ ( 𝑘 = 0 → ( ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) ↔ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 0 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) ) )
17 fveq2 ⊢ ( 𝑘 = 𝑗 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) )
18 csbeq1 ⊢ ( 𝑘 = 𝑗 → ⦋ 𝑘 / 𝑛 ⦌ 𝐵 = ⦋ 𝑗 / 𝑛 ⦌ 𝐵 )
19 18 oveq1d ⊢ ( 𝑘 = 𝑗 → ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) = ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) )
20 19 mpteq2dv ⊢ ( 𝑘 = 𝑗 → ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) )
21 17 20 eqeq12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ↔ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) )
22 21 imbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) ↔ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) ) )
23 fveq2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ ( 𝑗 + 1 ) ) )
24 csbeq1 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ⦋ 𝑘 / 𝑛 ⦌ 𝐵 = ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 )
25 24 oveq1d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) = ( ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 / 𝐶 ) )
26 25 mpteq2dv ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 / 𝐶 ) ) )
27 23 26 eqeq12d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ↔ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) )
28 27 imbi2d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) ↔ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) ) )
29 fveq2 ⊢ ( 𝑘 = 𝑛 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑛 ) )
30 csbeq1a ⊢ ( 𝑛 = 𝑘 → 𝐵 = ⦋ 𝑘 / 𝑛 ⦌ 𝐵 )
31 30 equcoms ⊢ ( 𝑘 = 𝑛 → 𝐵 = ⦋ 𝑘 / 𝑛 ⦌ 𝐵 )
32 31 eqcomd ⊢ ( 𝑘 = 𝑛 → ⦋ 𝑘 / 𝑛 ⦌ 𝐵 = 𝐵 )
33 32 oveq1d ⊢ ( 𝑘 = 𝑛 → ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) = ( 𝐵 / 𝐶 ) )
34 33 mpteq2dv ⊢ ( 𝑘 = 𝑛 → ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 / 𝐶 ) ) )
35 29 34 eqeq12d ⊢ ( 𝑘 = 𝑛 → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ↔ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 / 𝐶 ) ) ) )
36 35 imbi2d ⊢ ( 𝑘 = 𝑛 → ( ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑘 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) ↔ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 / 𝐶 ) ) ) ) )
37 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
38 1 37 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
39 cnex ⊢ ℂ ∈ V
40 39 a1i ⊢ ( 𝜑 → ℂ ∈ V )
41 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
42 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ≠ 0 )
43 3 41 42 divcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 / 𝐶 ) ∈ ℂ )
44 43 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) : 𝑋 ⟶ ℂ )
45 elpm2r ⊢ ( ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ 𝑆 ) ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ∈ ( ℂ ↑pm 𝑆 ) )
46 40 1 44 2 45 syl22anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ∈ ( ℂ ↑pm 𝑆 ) )
47 dvn0 ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) )
48 38 46 47 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) )
49 id ⊢ ( 𝜑 → 𝜑 )
50 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
51 8 50 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
52 eluzfz1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) )
53 51 52 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
54 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 0 ∈ ( 0 ... 𝑀 ) )
55 nfcv ⊢ Ⅎ 𝑛 ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 0 )
56 nfcv ⊢ Ⅎ 𝑛 𝑋
57 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ 0 / 𝑛 ⦌ 𝐵
58 56 57 nfmpt ⊢ Ⅎ 𝑛 ( 𝑥 ∈ 𝑋 ↦ ⦋ 0 / 𝑛 ⦌ 𝐵 )
59 55 58 nfeq ⊢ Ⅎ 𝑛 ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 0 / 𝑛 ⦌ 𝐵 )
60 54 59 nfim ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 0 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 0 / 𝑛 ⦌ 𝐵 ) )
61 c0ex ⊢ 0 ∈ V
62 eleq1 ⊢ ( 𝑛 = 0 → ( 𝑛 ∈ ( 0 ... 𝑀 ) ↔ 0 ∈ ( 0 ... 𝑀 ) ) )
63 62 anbi2d ⊢ ( 𝑛 = 0 → ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) ↔ ( 𝜑 ∧ 0 ∈ ( 0 ... 𝑀 ) ) ) )
64 fveq2 ⊢ ( 𝑛 = 0 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 0 ) )
65 csbeq1a ⊢ ( 𝑛 = 0 → 𝐵 = ⦋ 0 / 𝑛 ⦌ 𝐵 )
66 65 mpteq2dv ⊢ ( 𝑛 = 0 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 0 / 𝑛 ⦌ 𝐵 ) )
67 64 66 eqeq12d ⊢ ( 𝑛 = 0 → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↔ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 0 / 𝑛 ⦌ 𝐵 ) ) )
68 63 67 imbi12d ⊢ ( 𝑛 = 0 → ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ) ↔ ( ( 𝜑 ∧ 0 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 0 / 𝑛 ⦌ 𝐵 ) ) ) )
69 60 61 68 5 vtoclf ⊢ ( ( 𝜑 ∧ 0 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 0 / 𝑛 ⦌ 𝐵 ) )
70 49 53 69 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 0 / 𝑛 ⦌ 𝐵 ) )
71 70 fveq1d ⊢ ( 𝜑 → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 0 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ ⦋ 0 / 𝑛 ⦌ 𝐵 ) ‘ 𝑥 ) )
72 71 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 0 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ ⦋ 0 / 𝑛 ⦌ 𝐵 ) ‘ 𝑥 ) )
73 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
74 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝜑 )
75 53 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ∈ ( 0 ... 𝑀 ) )
76 0re ⊢ 0 ∈ ℝ
77 nfcv ⊢ Ⅎ 𝑛 0
78 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ ( 0 ... 𝑀 ) )
79 nfcv ⊢ Ⅎ 𝑛 ℂ
80 57 79 nfel ⊢ Ⅎ 𝑛 ⦋ 0 / 𝑛 ⦌ 𝐵 ∈ ℂ
81 78 80 nfim ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ ( 0 ... 𝑀 ) ) → ⦋ 0 / 𝑛 ⦌ 𝐵 ∈ ℂ )
82 62 3anbi3d ⊢ ( 𝑛 = 0 → ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) ↔ ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ ( 0 ... 𝑀 ) ) ) )
83 65 eleq1d ⊢ ( 𝑛 = 0 → ( 𝐵 ∈ ℂ ↔ ⦋ 0 / 𝑛 ⦌ 𝐵 ∈ ℂ ) )
84 82 83 imbi12d ⊢ ( 𝑛 = 0 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ ( 0 ... 𝑀 ) ) → ⦋ 0 / 𝑛 ⦌ 𝐵 ∈ ℂ ) ) )
85 77 81 84 4 vtoclgf ⊢ ( 0 ∈ ℝ → ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ ( 0 ... 𝑀 ) ) → ⦋ 0 / 𝑛 ⦌ 𝐵 ∈ ℂ ) )
86 76 85 ax-mp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ ( 0 ... 𝑀 ) ) → ⦋ 0 / 𝑛 ⦌ 𝐵 ∈ ℂ )
87 74 73 75 86 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⦋ 0 / 𝑛 ⦌ 𝐵 ∈ ℂ )
88 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ ⦋ 0 / 𝑛 ⦌ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 0 / 𝑛 ⦌ 𝐵 )
89 88 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ⦋ 0 / 𝑛 ⦌ 𝐵 ∈ ℂ ) → ( ( 𝑥 ∈ 𝑋 ↦ ⦋ 0 / 𝑛 ⦌ 𝐵 ) ‘ 𝑥 ) = ⦋ 0 / 𝑛 ⦌ 𝐵 )
90 73 87 89 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ ⦋ 0 / 𝑛 ⦌ 𝐵 ) ‘ 𝑥 ) = ⦋ 0 / 𝑛 ⦌ 𝐵 )
91 72 90 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⦋ 0 / 𝑛 ⦌ 𝐵 = ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 0 ) ‘ 𝑥 ) )
92 3 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
93 elpm2r ⊢ ( ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ 𝑆 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ℂ ↑pm 𝑆 ) )
94 40 1 92 2 93 syl22anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ℂ ↑pm 𝑆 ) )
95 dvn0 ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
96 38 94 95 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
97 96 fveq1d ⊢ ( 𝜑 → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 0 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) )
98 97 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 0 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) )
99 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 )
100 99 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ ℂ ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
101 73 3 100 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
102 91 98 101 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 = ⦋ 0 / 𝑛 ⦌ 𝐵 )
103 102 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 / 𝐶 ) = ( ⦋ 0 / 𝑛 ⦌ 𝐵 / 𝐶 ) )
104 103 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 0 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) )
105 48 104 eqtrd ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 0 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) )
106 105 a1i ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 0 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) )
107 simp3 ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) ∧ 𝜑 ) → 𝜑 )
108 simp1 ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) ∧ 𝜑 ) → 𝑗 ∈ ( 0 ..^ 𝑀 ) )
109 simpr ⊢ ( ( ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) ∧ 𝜑 ) → 𝜑 )
110 simpl ⊢ ( ( ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) ∧ 𝜑 ) → ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) )
111 109 110 mpd ⊢ ( ( ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) ∧ 𝜑 ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) )
112 111 3adant1 ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) ∧ 𝜑 ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) )
113 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) → 𝑆 ⊆ ℂ )
114 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ∈ ( ℂ ↑pm 𝑆 ) )
115 elfzofz ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
116 elfznn0 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℕ0 )
117 116 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) → 𝑗 ∈ ℕ0 )
118 115 117 sylanl2 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) → 𝑗 ∈ ℕ0 )
119 dvnp1 ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) ) )
120 113 114 118 119 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) ) )
121 oveq2 ⊢ ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) → ( 𝑆 D ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) )
122 121 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) → ( 𝑆 D ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) )
123 38 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝑆 ⊆ ℂ )
124 46 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ∈ ( ℂ ↑pm 𝑆 ) )
125 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
126 125 116 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ℕ0 )
127 115 126 sylan2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝑗 ∈ ℕ0 )
128 123 124 127 119 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) ) )
129 128 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) ) )
130 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝑆 ∈ { ℝ , ℂ } )
131 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
132 49 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝜑 )
133 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
134 132 133 131 3jca ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) )
135 nfcv ⊢ Ⅎ 𝑛 𝑗
136 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) )
137 135 nfcsb1 ⊢ Ⅎ 𝑛 ⦋ 𝑗 / 𝑛 ⦌ 𝐵
138 137 79 nfel ⊢ Ⅎ 𝑛 ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ∈ ℂ
139 136 138 nfim ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ∈ ℂ )
140 eleq1 ⊢ ( 𝑛 = 𝑗 → ( 𝑛 ∈ ( 0 ... 𝑀 ) ↔ 𝑗 ∈ ( 0 ... 𝑀 ) ) )
141 140 3anbi3d ⊢ ( 𝑛 = 𝑗 → ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) ↔ ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ) )
142 csbeq1a ⊢ ( 𝑛 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑛 ⦌ 𝐵 )
143 142 eleq1d ⊢ ( 𝑛 = 𝑗 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ∈ ℂ ) )
144 141 143 imbi12d ⊢ ( 𝑛 = 𝑗 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ∈ ℂ ) ) )
145 135 139 144 4 vtoclgf ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ∈ ℂ ) )
146 131 134 145 sylc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ∈ ℂ )
147 115 146 sylanl2 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ∈ ℂ )
148 fzofzp1 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) )
149 148 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) )
150 115 132 sylanl2 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝜑 )
151 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
152 150 151 149 3jca ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) ) )
153 nfcv ⊢ Ⅎ 𝑛 ( 𝑗 + 1 )
154 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) )
155 153 nfcsb1 ⊢ Ⅎ 𝑛 ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵
156 155 79 nfel ⊢ Ⅎ 𝑛 ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 ∈ ℂ
157 154 156 nfim ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) ) → ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 ∈ ℂ )
158 eleq1 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( 𝑛 ∈ ( 0 ... 𝑀 ) ↔ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) ) )
159 158 3anbi3d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) ↔ ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) ) ) )
160 csbeq1a ⊢ ( 𝑛 = ( 𝑗 + 1 ) → 𝐵 = ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 )
161 160 eleq1d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( 𝐵 ∈ ℂ ↔ ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 ∈ ℂ ) )
162 159 161 imbi12d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) ) → ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 ∈ ℂ ) ) )
163 153 157 162 4 vtoclgf ⊢ ( ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) ) → ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 ∈ ℂ ) )
164 149 152 163 sylc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ 𝑋 ) → ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 ∈ ℂ )
165 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝜑 )
166 115 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
167 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) )
168 nfcv ⊢ Ⅎ 𝑛 ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑗 )
169 56 137 nfmpt ⊢ Ⅎ 𝑛 ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑛 ⦌ 𝐵 )
170 168 169 nfeq ⊢ Ⅎ 𝑛 ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑛 ⦌ 𝐵 )
171 167 170 nfim ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ) )
172 140 anbi2d ⊢ ( 𝑛 = 𝑗 → ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) ↔ ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ) )
173 fveq2 ⊢ ( 𝑛 = 𝑗 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑗 ) )
174 142 mpteq2dv ⊢ ( 𝑛 = 𝑗 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ) )
175 173 174 eqeq12d ⊢ ( 𝑛 = 𝑗 → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↔ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ) ) )
176 172 175 imbi12d ⊢ ( 𝑛 = 𝑗 → ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ) ) ) )
177 171 176 5 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ) )
178 165 166 177 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ) )
179 178 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑗 ) )
180 179 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑗 ) ) )
181 165 94 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ℂ ↑pm 𝑆 ) )
182 dvnp1 ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑗 ) ) )
183 123 181 127 182 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑗 ) ) )
184 183 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 D ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑗 ) ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑗 + 1 ) ) )
185 148 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) )
186 165 185 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) ) )
187 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) )
188 nfcv ⊢ Ⅎ 𝑛 ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑗 + 1 ) )
189 56 155 nfmpt ⊢ Ⅎ 𝑛 ( 𝑥 ∈ 𝑋 ↦ ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 )
190 188 189 nfeq ⊢ Ⅎ 𝑛 ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 )
191 187 190 nfim ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 ) )
192 158 anbi2d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) ↔ ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) ) ) )
193 fveq2 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑗 + 1 ) ) )
194 160 mpteq2dv ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 ) )
195 193 194 eqeq12d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↔ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 ) ) )
196 192 195 imbi12d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ) ↔ ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 ) ) ) )
197 153 191 196 5 vtoclgf ⊢ ( ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) → ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 ) ) )
198 185 186 197 sylc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 ) )
199 180 184 198 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑛 ⦌ 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 ) )
200 6 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝐶 ∈ ℂ )
201 7 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝐶 ≠ 0 )
202 130 147 164 199 200 201 dvmptdivc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 / 𝐶 ) ) )
203 202 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 / 𝐶 ) ) )
204 129 122 203 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 / 𝐶 ) ) )
205 204 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ ( ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 / 𝐶 ) ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ ( 𝑗 + 1 ) ) )
206 205 120 122 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 / 𝐶 ) ) )
207 120 122 206 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 / 𝐶 ) ) )
208 107 108 112 207 syl21anc ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) ∧ 𝜑 ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 / 𝐶 ) ) )
209 208 3exp ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ 𝑗 / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) → ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ ( 𝑗 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ⦋ ( 𝑗 + 1 ) / 𝑛 ⦌ 𝐵 / 𝐶 ) ) ) ) )
210 16 22 28 36 106 209 fzind2 ⊢ ( 𝑛 ∈ ( 0 ... 𝑀 ) → ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 / 𝐶 ) ) ) )
211 9 10 210 sylc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 / 𝐶 ) ) )