dvnmptdivc

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

	Ref	Expression
Hypotheses	dvnmptdivc.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvnmptdivc.x	$⊢ φ \to X \subseteq S$
	dvnmptdivc.a	$⊢ (φ \land x \in X) \to A \in ℂ$
	dvnmptdivc.b	$⊢ (φ \land x \in X \land n \in (0 \dots M)) \to B \in ℂ$
	dvnmptdivc.dvn	$⊢ (φ \land n \in (0 \dots M)) \to (S D^{n} (x \in X ⟼ A)) (n) = (x \in X ⟼ B)$
	dvnmptdivc.c	$⊢ φ \to C \in ℂ$
	dvnmptdivc.cne0	$⊢ φ \to C \neq 0$
	dvnmptdivc.8	$⊢ φ \to M \in ℕ_{0}$
Assertion	dvnmptdivc	$⊢ (φ \land n \in (0 \dots M)) \to (S D^{n} (x \in X ⟼ \frac{A}{C})) (n) = (x \in X ⟼ \frac{B}{C})$

Proof

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

Metamath Proof Explorer

Theorem dvnmptdivc

Proof