jensen

Description: Jensen's inequality, a finite extension of the definition of convexity (the last hypothesis). (Contributed by Mario Carneiro, 21-Jun-2015) (Proof shortened by AV, 27-Jul-2019)

	Ref	Expression
Hypotheses	jensen.1	$⊢ φ \to D \subseteq ℝ$
	jensen.2	$⊢ φ \to F : D ⟶ ℝ$
	jensen.3	$⊢ (φ \land (a \in D \land b \in D)) \to [a, b] \subseteq D$
	jensen.4	$⊢ φ \to A \in Fin$
	jensen.5	$⊢ φ \to T : A ⟶ [0, +∞)$
	jensen.6	$⊢ φ \to X : A ⟶ D$
	jensen.7	$⊢ φ \to 0 < \sum_{ℂ_{fld}} T$
	jensen.8	$⊢ (φ \land (x \in D \land y \in D \land t \in [0, 1])) \to F (t x + (1 - t) y) \leq t F (x) + (1 - t) F (y)$
Assertion	jensen	$⊢ φ \to (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T} \in D \land F (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T}) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T})$

Proof

Step	Hyp	Ref	Expression
1		jensen.1	$⊢ φ \to D \subseteq ℝ$
2		jensen.2	$⊢ φ \to F : D ⟶ ℝ$
3		jensen.3	$⊢ (φ \land (a \in D \land b \in D)) \to [a, b] \subseteq D$
4		jensen.4	$⊢ φ \to A \in Fin$
5		jensen.5	$⊢ φ \to T : A ⟶ [0, +∞)$
6		jensen.6	$⊢ φ \to X : A ⟶ D$
7		jensen.7	$⊢ φ \to 0 < \sum_{ℂ_{fld}} T$
8		jensen.8	$⊢ (φ \land (x \in D \land y \in D \land t \in [0, 1])) \to F (t x + (1 - t) y) \leq t F (x) + (1 - t) F (y)$
9	5	ffnd	$⊢ φ \to T Fn A$
10		fnresdm	$⊢ T Fn A \to {T ↾}_{A} = T$
11	9 10	syl	$⊢ φ \to {T ↾}_{A} = T$
12	11	oveq2d	$⊢ φ \to \sum_{ℂ_{fld}} ({T ↾}_{A}) = \sum_{ℂ_{fld}} T$
13	7 12	breqtrrd	$⊢ φ \to 0 < \sum_{ℂ_{fld}} ({T ↾}_{A})$
14		ssid	$⊢ A \subseteq A$
15	13 14	jctil	$⊢ φ \to (A \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{A}))$
16		sseq1	$⊢ a = \emptyset \to (a \subseteq A \leftrightarrow \emptyset \subseteq A)$
17		reseq2	$⊢ a = \emptyset \to {T ↾}_{a} = {T ↾}_{\emptyset}$
18		res0	$⊢ {T ↾}_{\emptyset} = \emptyset$
19	17 18	syl6eq	$⊢ a = \emptyset \to {T ↾}_{a} = \emptyset$
20	19	oveq2d	$⊢ a = \emptyset \to \sum_{ℂ_{fld}} ({T ↾}_{a}) = \sum_{ℂ_{fld}} \emptyset$
21		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
22	21	gsum0	$⊢ \sum_{ℂ_{fld}} \emptyset = 0$
23	20 22	syl6eq	$⊢ a = \emptyset \to \sum_{ℂ_{fld}} ({T ↾}_{a}) = 0$
24	23	breq2d	$⊢ a = \emptyset \to (0 < \sum_{ℂ_{fld}} ({T ↾}_{a}) \leftrightarrow 0 < 0)$
25	16 24	anbi12d	$⊢ a = \emptyset \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \leftrightarrow (\emptyset \subseteq A \land 0 < 0))$
26		reseq2	$⊢ a = \emptyset \to {(T \times_{f} X) ↾}_{a} = {(T \times_{f} X) ↾}_{\emptyset}$
27	26	oveq2d	$⊢ a = \emptyset \to \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})$
28	27 23	oveq12d	$⊢ a = \emptyset \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})}{0}$
29		reseq2	$⊢ a = \emptyset \to {(T \times_{f} (F \circ X)) ↾}_{a} = {(T \times_{f} (F \circ X)) ↾}_{\emptyset}$
30	29	oveq2d	$⊢ a = \emptyset \to \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})$
31	30 23	oveq12d	$⊢ a = \emptyset \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}$
32	31	breq2d	$⊢ a = \emptyset \to (F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \leftrightarrow F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0})$
33	32	rabbidv	$⊢ a = \emptyset \to \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} = \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}\}$
34	28 33	eleq12d	$⊢ a = \emptyset \to (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} \leftrightarrow \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})}{0} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}\})$
35	25 34	imbi12d	$⊢ a = \emptyset \to (((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\}) \leftrightarrow ((\emptyset \subseteq A \land 0 < 0) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})}{0} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}\}))$
36	35	imbi2d	$⊢ a = \emptyset \to ((φ \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\})) \leftrightarrow (φ \to ((\emptyset \subseteq A \land 0 < 0) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})}{0} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}\})))$
37		sseq1	$⊢ a = k \to (a \subseteq A \leftrightarrow k \subseteq A)$
38		reseq2	$⊢ a = k \to {T ↾}_{a} = {T ↾}_{k}$
39	38	oveq2d	$⊢ a = k \to \sum_{ℂ_{fld}} ({T ↾}_{a}) = \sum_{ℂ_{fld}} ({T ↾}_{k})$
40	39	breq2d	$⊢ a = k \to (0 < \sum_{ℂ_{fld}} ({T ↾}_{a}) \leftrightarrow 0 < \sum_{ℂ_{fld}} ({T ↾}_{k}))$
41	37 40	anbi12d	$⊢ a = k \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \leftrightarrow (k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})))$
42		reseq2	$⊢ a = k \to {(T \times_{f} X) ↾}_{a} = {(T \times_{f} X) ↾}_{k}$
43	42	oveq2d	$⊢ a = k \to \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})$
44	43 39	oveq12d	$⊢ a = k \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}$
45		reseq2	$⊢ a = k \to {(T \times_{f} (F \circ X)) ↾}_{a} = {(T \times_{f} (F \circ X)) ↾}_{k}$
46	45	oveq2d	$⊢ a = k \to \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})$
47	46 39	oveq12d	$⊢ a = k \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}$
48	47	breq2d	$⊢ a = k \to (F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \leftrightarrow F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})})$
49	48	rabbidv	$⊢ a = k \to \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} = \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}$
50	44 49	eleq12d	$⊢ a = k \to (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} \leftrightarrow \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})$
51	41 50	imbi12d	$⊢ a = k \to (((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\}) \leftrightarrow ((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}))$
52	51	imbi2d	$⊢ a = k \to ((φ \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\})) \leftrightarrow (φ \to ((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})))$
53		sseq1	$⊢ a = k \cup \{c\} \to (a \subseteq A \leftrightarrow k \cup \{c\} \subseteq A)$
54		reseq2	$⊢ a = k \cup \{c\} \to {T ↾}_{a} = {T ↾}_{(k \cup \{c\})}$
55	54	oveq2d	$⊢ a = k \cup \{c\} \to \sum_{ℂ_{fld}} ({T ↾}_{a}) = \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})$
56	55	breq2d	$⊢ a = k \cup \{c\} \to (0 < \sum_{ℂ_{fld}} ({T ↾}_{a}) \leftrightarrow 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))$
57	53 56	anbi12d	$⊢ a = k \cup \{c\} \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \leftrightarrow (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})))$
58		reseq2	$⊢ a = k \cup \{c\} \to {(T \times_{f} X) ↾}_{a} = {(T \times_{f} X) ↾}_{(k \cup \{c\})}$
59	58	oveq2d	$⊢ a = k \cup \{c\} \to \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})$
60	59 55	oveq12d	$⊢ a = k \cup \{c\} \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}$
61		reseq2	$⊢ a = k \cup \{c\} \to {(T \times_{f} (F \circ X)) ↾}_{a} = {(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}$
62	61	oveq2d	$⊢ a = k \cup \{c\} \to \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})$
63	62 55	oveq12d	$⊢ a = k \cup \{c\} \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}$
64	63	breq2d	$⊢ a = k \cup \{c\} \to (F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \leftrightarrow F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})})$
65	64	rabbidv	$⊢ a = k \cup \{c\} \to \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} = \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\}$
66	60 65	eleq12d	$⊢ a = k \cup \{c\} \to (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} \leftrightarrow \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})$
67	57 66	imbi12d	$⊢ a = k \cup \{c\} \to (((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\}) \leftrightarrow ((k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\}))$
68	67	imbi2d	$⊢ a = k \cup \{c\} \to ((φ \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\})) \leftrightarrow (φ \to ((k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})))$
69		sseq1	$⊢ a = A \to (a \subseteq A \leftrightarrow A \subseteq A)$
70		reseq2	$⊢ a = A \to {T ↾}_{a} = {T ↾}_{A}$
71	70	oveq2d	$⊢ a = A \to \sum_{ℂ_{fld}} ({T ↾}_{a}) = \sum_{ℂ_{fld}} ({T ↾}_{A})$
72	71	breq2d	$⊢ a = A \to (0 < \sum_{ℂ_{fld}} ({T ↾}_{a}) \leftrightarrow 0 < \sum_{ℂ_{fld}} ({T ↾}_{A}))$
73	69 72	anbi12d	$⊢ a = A \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \leftrightarrow (A \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{A})))$
74		reseq2	$⊢ a = A \to {(T \times_{f} X) ↾}_{a} = {(T \times_{f} X) ↾}_{A}$
75	74	oveq2d	$⊢ a = A \to \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})$
76	75 71	oveq12d	$⊢ a = A \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}$
77		reseq2	$⊢ a = A \to {(T \times_{f} (F \circ X)) ↾}_{a} = {(T \times_{f} (F \circ X)) ↾}_{A}$
78	77	oveq2d	$⊢ a = A \to \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})$
79	78 71	oveq12d	$⊢ a = A \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}$
80	79	breq2d	$⊢ a = A \to (F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \leftrightarrow F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})})$
81	80	rabbidv	$⊢ a = A \to \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} = \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\}$
82	76 81	eleq12d	$⊢ a = A \to (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} \leftrightarrow \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\})$
83	73 82	imbi12d	$⊢ a = A \to (((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\}) \leftrightarrow ((A \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{A})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\}))$
84	83	imbi2d	$⊢ a = A \to ((φ \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\})) \leftrightarrow (φ \to ((A \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{A})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\})))$
85		0re	$⊢ 0 \in ℝ$
86	85	ltnri	$⊢ \neg 0 < 0$
87	86	pm2.21i	$⊢ 0 < 0 \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})}{0} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}\}$
88	87	adantl	$⊢ (\emptyset \subseteq A \land 0 < 0) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})}{0} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}\}$
89	88	a1i	$⊢ φ \to ((\emptyset \subseteq A \land 0 < 0) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})}{0} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}\})$
90		impexp	$⊢ ((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \leftrightarrow (k \subseteq A \to (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}))$
91		simprl	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to k \cup \{c\} \subseteq A$
92	91	unssad	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to k \subseteq A$
93		simpr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})$
94	1	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to D \subseteq ℝ$
95	2	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to F : D ⟶ ℝ$
96		simplll	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to φ$
97	96 3	sylan	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \land (a \in D \land b \in D)) \to [a, b] \subseteq D$
98	96 4	syl	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to A \in Fin$
99	96 5	syl	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to T : A ⟶ [0, +∞)$
100	96 6	syl	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to X : A ⟶ D$
101	7	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to 0 < \sum_{ℂ_{fld}} T$
102	96 8	sylan	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \land (x \in D \land y \in D \land t \in [0, 1])) \to F (t x + (1 - t) y) \leq t F (x) + (1 - t) F (y)$
103		simpllr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to \neg c \in k$
104	91	adantr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to k \cup \{c\} \subseteq A$
105		eqid	$⊢ \sum_{ℂ_{fld}} ({T ↾}_{k}) = \sum_{ℂ_{fld}} ({T ↾}_{k})$
106		eqid	$⊢ \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}) = \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})$
107		cnring	$⊢ ℂ_{fld} \in Ring$
108		ringcmn	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in CMnd$
109	107 108	mp1i	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to ℂ_{fld} \in CMnd$
110	4	ad2antrr	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to A \in Fin$
111	110 92	ssfid	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to k \in Fin$
112		rege0subm	$⊢ [0, +∞) \in SubMnd (ℂ_{fld})$
113	112	a1i	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to [0, +∞) \in SubMnd (ℂ_{fld})$
114	5	ad2antrr	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to T : A ⟶ [0, +∞)$
115	114 92	fssresd	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to ({T ↾}_{k}) : k ⟶ [0, +∞)$
116		c0ex	$⊢ 0 \in V$
117	116	a1i	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to 0 \in V$
118	115 111 117	fdmfifsupp	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to {finSupp}_{0} (({T ↾}_{k}))$
119	21 109 111 113 115 118	gsumsubmcl	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to \sum_{ℂ_{fld}} ({T ↾}_{k}) \in [0, +∞)$
120		elrege0	$⊢ \sum_{ℂ_{fld}} ({T ↾}_{k}) \in [0, +∞) \leftrightarrow (\sum_{ℂ_{fld}} ({T ↾}_{k}) \in ℝ \land 0 \leq \sum_{ℂ_{fld}} ({T ↾}_{k}))$
121	120	simplbi	$⊢ \sum_{ℂ_{fld}} ({T ↾}_{k}) \in [0, +∞) \to \sum_{ℂ_{fld}} ({T ↾}_{k}) \in ℝ$
122	119 121	syl	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to \sum_{ℂ_{fld}} ({T ↾}_{k}) \in ℝ$
123	122	adantr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to \sum_{ℂ_{fld}} ({T ↾}_{k}) \in ℝ$
124		simprl	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})$
125	123 124	elrpd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to \sum_{ℂ_{fld}} ({T ↾}_{k}) \in ℝ^{+}$
126		simprr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}$
127		fveq2	$⊢ w = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \to F (w) = F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})})$
128	127	breq1d	$⊢ w = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \to (F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \leftrightarrow F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})})$
129	128	elrab	$⊢ \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\} \leftrightarrow (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in D \land F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})})$
130	126 129	sylib	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in D \land F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})})$
131	130	simpld	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in D$
132	130	simprd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}$
133	94 95 97 98 99 100 101 102 103 104 105 106 125 131 132	jensenlem2	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in D \land F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})})$
134		fveq2	$⊢ w = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \to F (w) = F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})})$
135	134	breq1d	$⊢ w = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \to (F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \leftrightarrow F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})})$
136	135	elrab	$⊢ \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\} \leftrightarrow (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in D \land F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})})$
137	133 136	sylibr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\}$
138	137	expr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\} \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})$
139	93 138	embantd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ((0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})$
140		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
141		ringmnd	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in Mnd$
142	107 141	mp1i	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ℂ_{fld} \in Mnd$
143	110 91	ssfid	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to k \cup \{c\} \in Fin$
144	143	adantr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to k \cup \{c\} \in Fin$
145		ssun2	$⊢ \{c\} \subseteq k \cup \{c\}$
146		vsnid	$⊢ c \in \{c\}$
147	145 146	sselii	$⊢ c \in (k \cup \{c\})$
148	147	a1i	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to c \in (k \cup \{c\})$
149		remulcl	$⊢ (x \in ℝ \land y \in ℝ) \to x y \in ℝ$
150	149	adantl	$⊢ (φ \land (x \in ℝ \land y \in ℝ)) \to x y \in ℝ$
151		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
152		fss	$⊢ (T : A ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to T : A ⟶ ℝ$
153	5 151 152	sylancl	$⊢ φ \to T : A ⟶ ℝ$
154	6 1	fssd	$⊢ φ \to X : A ⟶ ℝ$
155		inidm	$⊢ A \cap A = A$
156	150 153 154 4 4 155	off	$⊢ φ \to (T \times_{f} X) : A ⟶ ℝ$
157		ax-resscn	$⊢ ℝ \subseteq ℂ$
158		fss	$⊢ ((T \times_{f} X) : A ⟶ ℝ \land ℝ \subseteq ℂ) \to (T \times_{f} X) : A ⟶ ℂ$
159	156 157 158	sylancl	$⊢ φ \to (T \times_{f} X) : A ⟶ ℂ$
160	159	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (T \times_{f} X) : A ⟶ ℂ$
161	91	adantr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to k \cup \{c\} \subseteq A$
162	160 161	fssresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} X) ↾}_{(k \cup \{c\})}) : k \cup \{c\} ⟶ ℂ$
163	5	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to T : A ⟶ [0, +∞)$
164	110	adantr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to A \in Fin$
165		fex	$⊢ (T : A ⟶ [0, +∞) \land A \in Fin) \to T \in V$
166	163 164 165	syl2anc	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to T \in V$
167	6	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to X : A ⟶ D$
168		fex	$⊢ (X : A ⟶ D \land A \in Fin) \to X \in V$
169	167 164 168	syl2anc	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to X \in V$
170		offres	$⊢ (T \in V \land X \in V) \to {(T \times_{f} X) ↾}_{(k \cup \{c\})} = ({T ↾}_{(k \cup \{c\})}) \times_{f} ({X ↾}_{(k \cup \{c\})})$
171	166 169 170	syl2anc	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to {(T \times_{f} X) ↾}_{(k \cup \{c\})} = ({T ↾}_{(k \cup \{c\})}) \times_{f} ({X ↾}_{(k \cup \{c\})})$
172	171	oveq1d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} X) ↾}_{(k \cup \{c\})}) supp 0 = (({T ↾}_{(k \cup \{c\})}) \times_{f} ({X ↾}_{(k \cup \{c\})})) supp 0$
173	151 157	sstri	$⊢ [0, +∞) \subseteq ℂ$
174		fss	$⊢ (T : A ⟶ [0, +∞) \land [0, +∞) \subseteq ℂ) \to T : A ⟶ ℂ$
175	163 173 174	sylancl	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to T : A ⟶ ℂ$
176	175 161	fssresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({T ↾}_{(k \cup \{c\})}) : k \cup \{c\} ⟶ ℂ$
177		eldifi	$⊢ x \in ((k \cup \{c\}) ∖ \{c\}) \to x \in (k \cup \{c\})$
178	177	adantl	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in ((k \cup \{c\}) ∖ \{c\})) \to x \in (k \cup \{c\})$
179	178	fvresd	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in ((k \cup \{c\}) ∖ \{c\})) \to ({T ↾}_{(k \cup \{c\})}) (x) = T (x)$
180		difun2	$⊢ (k \cup \{c\}) ∖ \{c\} = k ∖ \{c\}$
181		difss	$⊢ k ∖ \{c\} \subseteq k$
182	180 181	eqsstri	$⊢ (k \cup \{c\}) ∖ \{c\} \subseteq k$
183	182	sseli	$⊢ x \in ((k \cup \{c\}) ∖ \{c\}) \to x \in k$
184		simpr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})$
185	92	adantr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to k \subseteq A$
186	163 185	feqresmpt	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to {T ↾}_{k} = (x \in k ⟼ T (x))$
187	186	oveq2d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{ℂ_{fld}} ({T ↾}_{k}) = \underset{x \in k}{\sum_{ℂ_{fld}}} T (x)$
188	111	adantr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to k \in Fin$
189	185	sselda	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in k) \to x \in A$
190	163	ffvelrnda	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in A) \to T (x) \in [0, +∞)$
191	189 190	syldan	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in k) \to T (x) \in [0, +∞)$
192	173 191	sseldi	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in k) \to T (x) \in ℂ$
193	188 192	gsumfsum	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \underset{x \in k}{\sum_{ℂ_{fld}}} T (x) = \sum_{x \in k} T (x)$
194	184 187 193	3eqtrrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{x \in k} T (x) = 0$
195		elrege0	$⊢ T (x) \in [0, +∞) \leftrightarrow (T (x) \in ℝ \land 0 \leq T (x))$
196	191 195	sylib	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in k) \to (T (x) \in ℝ \land 0 \leq T (x))$
197	196	simpld	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in k) \to T (x) \in ℝ$
198	196	simprd	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in k) \to 0 \leq T (x)$
199	188 197 198	fsum00	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (\sum_{x \in k} T (x) = 0 \leftrightarrow \forall x \in k T (x) = 0)$
200	194 199	mpbid	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \forall x \in k T (x) = 0$
201	200	r19.21bi	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in k) \to T (x) = 0$
202	183 201	sylan2	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in ((k \cup \{c\}) ∖ \{c\})) \to T (x) = 0$
203	179 202	eqtrd	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in ((k \cup \{c\}) ∖ \{c\})) \to ({T ↾}_{(k \cup \{c\})}) (x) = 0$
204	176 203	suppss	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({T ↾}_{(k \cup \{c\})}) supp 0 \subseteq \{c\}$
205		mul02	$⊢ x \in ℂ \to 0 \cdot x = 0$
206	205	adantl	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in ℂ) \to 0 \cdot x = 0$
207	1	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to D \subseteq ℝ$
208	207 157	sstrdi	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to D \subseteq ℂ$
209	167 208	fssd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to X : A ⟶ ℂ$
210	209 161	fssresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({X ↾}_{(k \cup \{c\})}) : k \cup \{c\} ⟶ ℂ$
211	116	a1i	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to 0 \in V$
212	204 206 176 210 144 211	suppssof1	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (({T ↾}_{(k \cup \{c\})}) \times_{f} ({X ↾}_{(k \cup \{c\})})) supp 0 \subseteq \{c\}$
213	172 212	eqsstrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} X) ↾}_{(k \cup \{c\})}) supp 0 \subseteq \{c\}$
214	140 21 142 144 148 162 213	gsumpt	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})}) = ({(T \times_{f} X) ↾}_{(k \cup \{c\})}) (c)$
215	148	fvresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} X) ↾}_{(k \cup \{c\})}) (c) = (T \times_{f} X) (c)$
216	163	ffnd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to T Fn A$
217	167	ffnd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to X Fn A$
218	161 148	sseldd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to c \in A$
219		fnfvof	$⊢ ((T Fn A \land X Fn A) \land (A \in Fin \land c \in A)) \to (T \times_{f} X) (c) = T (c) X (c)$
220	216 217 164 218 219	syl22anc	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (T \times_{f} X) (c) = T (c) X (c)$
221	214 215 220	3eqtrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})}) = T (c) X (c)$
222	140 21 142 144 148 176 204	gsumpt	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}) = ({T ↾}_{(k \cup \{c\})}) (c)$
223	148	fvresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({T ↾}_{(k \cup \{c\})}) (c) = T (c)$
224	222 223	eqtrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}) = T (c)$
225	221 224	oveq12d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} = \frac{T (c) X (c)}{T (c)}$
226	209 218	ffvelrnd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to X (c) \in ℂ$
227	175 218	ffvelrnd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to T (c) \in ℂ$
228		simplrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})$
229	228 224	breqtrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to 0 < T (c)$
230	229	gt0ne0d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to T (c) \neq 0$
231	226 227 230	divcan3d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{T (c) X (c)}{T (c)} = X (c)$
232	225 231	eqtrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} = X (c)$
233	167 218	ffvelrnd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to X (c) \in D$
234	232 233	eqeltrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in D$
235	2	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to F : D ⟶ ℝ$
236	235 233	ffvelrnd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to F (X (c)) \in ℝ$
237	236	leidd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to F (X (c)) \leq F (X (c))$
238	232	fveq2d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}) = F (X (c))$
239		fco	$⊢ (F : D ⟶ ℝ \land X : A ⟶ D) \to (F \circ X) : A ⟶ ℝ$
240	2 6 239	syl2anc	$⊢ φ \to (F \circ X) : A ⟶ ℝ$
241	150 153 240 4 4 155	off	$⊢ φ \to (T \times_{f} (F \circ X)) : A ⟶ ℝ$
242		fss	$⊢ ((T \times_{f} (F \circ X)) : A ⟶ ℝ \land ℝ \subseteq ℂ) \to (T \times_{f} (F \circ X)) : A ⟶ ℂ$
243	241 157 242	sylancl	$⊢ φ \to (T \times_{f} (F \circ X)) : A ⟶ ℂ$
244	243	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (T \times_{f} (F \circ X)) : A ⟶ ℂ$
245	244 161	fssresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}) : k \cup \{c\} ⟶ ℂ$
246	240	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (F \circ X) : A ⟶ ℝ$
247		fex	$⊢ ((F \circ X) : A ⟶ ℝ \land A \in Fin) \to F \circ X \in V$
248	246 164 247	syl2anc	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to F \circ X \in V$
249		offres	$⊢ (T \in V \land F \circ X \in V) \to {(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})} = ({T ↾}_{(k \cup \{c\})}) \times_{f} ({(F \circ X) ↾}_{(k \cup \{c\})})$
250	166 248 249	syl2anc	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to {(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})} = ({T ↾}_{(k \cup \{c\})}) \times_{f} ({(F \circ X) ↾}_{(k \cup \{c\})})$
251	250	oveq1d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}) supp 0 = (({T ↾}_{(k \cup \{c\})}) \times_{f} ({(F \circ X) ↾}_{(k \cup \{c\})})) supp 0$
252		fss	$⊢ ((F \circ X) : A ⟶ ℝ \land ℝ \subseteq ℂ) \to (F \circ X) : A ⟶ ℂ$
253	246 157 252	sylancl	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (F \circ X) : A ⟶ ℂ$
254	253 161	fssresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(F \circ X) ↾}_{(k \cup \{c\})}) : k \cup \{c\} ⟶ ℂ$
255	204 206 176 254 144 211	suppssof1	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (({T ↾}_{(k \cup \{c\})}) \times_{f} ({(F \circ X) ↾}_{(k \cup \{c\})})) supp 0 \subseteq \{c\}$
256	251 255	eqsstrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}) supp 0 \subseteq \{c\}$
257	140 21 142 144 148 245 256	gsumpt	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}) = ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}) (c)$
258	148	fvresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}) (c) = (T \times_{f} (F \circ X)) (c)$
259	2	ffnd	$⊢ φ \to F Fn D$
260		fnfco	$⊢ (F Fn D \land X : A ⟶ D) \to (F \circ X) Fn A$
261	259 6 260	syl2anc	$⊢ φ \to (F \circ X) Fn A$
262	261	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (F \circ X) Fn A$
263		fnfvof	$⊢ ((T Fn A \land (F \circ X) Fn A) \land (A \in Fin \land c \in A)) \to (T \times_{f} (F \circ X)) (c) = T (c) (F \circ X) (c)$
264	216 262 164 218 263	syl22anc	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (T \times_{f} (F \circ X)) (c) = T (c) (F \circ X) (c)$
265		fvco3	$⊢ (X : A ⟶ D \land c \in A) \to (F \circ X) (c) = F (X (c))$
266	167 218 265	syl2anc	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (F \circ X) (c) = F (X (c))$
267	266	oveq2d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to T (c) (F \circ X) (c) = T (c) F (X (c))$
268	264 267	eqtrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (T \times_{f} (F \circ X)) (c) = T (c) F (X (c))$
269	257 258 268	3eqtrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}) = T (c) F (X (c))$
270	269 224	oveq12d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} = \frac{T (c) F (X (c))}{T (c)}$
271	236	recnd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to F (X (c)) \in ℂ$
272	271 227 230	divcan3d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{T (c) F (X (c))}{T (c)} = F (X (c))$
273	270 272	eqtrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} = F (X (c))$
274	237 238 273	3brtr4d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}$
275	135 234 274	elrabd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\}$
276	275	a1d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ((0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})$
277	120	simprbi	$⊢ \sum_{ℂ_{fld}} ({T ↾}_{k}) \in [0, +∞) \to 0 \leq \sum_{ℂ_{fld}} ({T ↾}_{k})$
278	119 277	syl	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to 0 \leq \sum_{ℂ_{fld}} ({T ↾}_{k})$
279		leloe	$⊢ (0 \in ℝ \land \sum_{ℂ_{fld}} ({T ↾}_{k}) \in ℝ) \to (0 \leq \sum_{ℂ_{fld}} ({T ↾}_{k}) \leftrightarrow (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \lor 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})))$
280	85 122 279	sylancr	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to (0 \leq \sum_{ℂ_{fld}} ({T ↾}_{k}) \leftrightarrow (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \lor 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})))$
281	278 280	mpbid	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \lor 0 = \sum_{ℂ_{fld}} ({T ↾}_{k}))$
282	139 276 281	mpjaodan	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to ((0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})$
283	92 282	embantd	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to ((k \subseteq A \to (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})$
284	90 283	syl5bi	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to (((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})$
285	284	ex	$⊢ (φ \land \neg c \in k) \to ((k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})) \to (((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\}))$
286	285	com23	$⊢ (φ \land \neg c \in k) \to (((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to ((k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\}))$
287	286	expcom	$⊢ \neg c \in k \to (φ \to (((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to ((k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})))$
288	287	adantl	$⊢ (k \in Fin \land \neg c \in k) \to (φ \to (((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to ((k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})))$
289	288	a2d	$⊢ (k \in Fin \land \neg c \in k) \to ((φ \to ((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to (φ \to ((k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})))$
290	36 52 68 84 89 289	findcard2s	$⊢ A \in Fin \to (φ \to ((A \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{A})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\}))$
291	4 290	mpcom	$⊢ φ \to ((A \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{A})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\})$
292	15 291	mpd	$⊢ φ \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\}$
293	156	ffnd	$⊢ φ \to (T \times_{f} X) Fn A$
294		fnresdm	$⊢ (T \times_{f} X) Fn A \to {(T \times_{f} X) ↾}_{A} = T \times_{f} X$
295	293 294	syl	$⊢ φ \to {(T \times_{f} X) ↾}_{A} = T \times_{f} X$
296	295	oveq2d	$⊢ φ \to \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A}) = \sum_{ℂ_{fld}} (T \times_{f} X)$
297	296 12	oveq12d	$⊢ φ \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} = \frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T}$
298	9 261 4 4 155	offn	$⊢ φ \to (T \times_{f} (F \circ X)) Fn A$
299		fnresdm	$⊢ (T \times_{f} (F \circ X)) Fn A \to {(T \times_{f} (F \circ X)) ↾}_{A} = T \times_{f} (F \circ X)$
300	298 299	syl	$⊢ φ \to {(T \times_{f} (F \circ X)) ↾}_{A} = T \times_{f} (F \circ X)$
301	300	oveq2d	$⊢ φ \to \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A}) = \sum_{ℂ_{fld}} (T \times_{f} (F \circ X))$
302	301 12	oveq12d	$⊢ φ \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} = \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T}$
303	302	breq2d	$⊢ φ \to (F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} \leftrightarrow F (w) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T})$
304	303	rabbidv	$⊢ φ \to \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\} = \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T}\}$
305	292 297 304	3eltr3d	$⊢ φ \to \frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T}\}$
306		fveq2	$⊢ w = \frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T} \to F (w) = F (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T})$
307	306	breq1d	$⊢ w = \frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T} \to (F (w) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T} \leftrightarrow F (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T}) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T})$
308	307	elrab	$⊢ \frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T}\} \leftrightarrow (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T} \in D \land F (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T}) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T})$
309	305 308	sylib	$⊢ φ \to (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T} \in D \land F (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T}) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T})$

Metamath Proof Explorer

Theorem jensen

Proof