cau3lem

	Ref	Expression
Hypotheses	cau3lem.1	$⊢ Z \subseteq ℤ$
	cau3lem.2	$⊢ τ \to ψ$
	cau3lem.3	$⊢ F (k) = F (j) \to (ψ \leftrightarrow χ)$
	cau3lem.4	$⊢ F (k) = F (m) \to (ψ \leftrightarrow θ)$
	cau3lem.5	$⊢ (φ \land χ \land ψ) \to G (F (j) D F (k)) = G (F (k) D F (j))$
	cau3lem.6	$⊢ (φ \land θ \land χ) \to G (F (m) D F (j)) = G (F (j) D F (m))$
	cau3lem.7	$⊢ (φ \land (ψ \land θ) \land (χ \land x \in ℝ)) \to ((G (F (k) D F (j)) < \frac{x}{2} \land G (F (j) D F (m)) < \frac{x}{2}) \to G (F (k) D F (m)) < x)$
Assertion	cau3lem	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x))$

Proof

Step	Hyp	Ref	Expression
1		cau3lem.1	$⊢ Z \subseteq ℤ$
2		cau3lem.2	$⊢ τ \to ψ$
3		cau3lem.3	$⊢ F (k) = F (j) \to (ψ \leftrightarrow χ)$
4		cau3lem.4	$⊢ F (k) = F (m) \to (ψ \leftrightarrow θ)$
5		cau3lem.5	$⊢ (φ \land χ \land ψ) \to G (F (j) D F (k)) = G (F (k) D F (j))$
6		cau3lem.6	$⊢ (φ \land θ \land χ) \to G (F (m) D F (j)) = G (F (j) D F (m))$
7		cau3lem.7	$⊢ (φ \land (ψ \land θ) \land (χ \land x \in ℝ)) \to ((G (F (k) D F (j)) < \frac{x}{2} \land G (F (j) D F (m)) < \frac{x}{2}) \to G (F (k) D F (m)) < x)$
8		breq2	$⊢ x = z \to (G (F (k) D F (j)) < x \leftrightarrow G (F (k) D F (j)) < z)$
9	8	anbi2d	$⊢ x = z \to ((τ \land G (F (k) D F (j)) < x) \leftrightarrow (τ \land G (F (k) D F (j)) < z))$
10	9	rexralbidv	$⊢ x = z \to (\exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < x) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < z))$
11	10	cbvralvw	$⊢ \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < x) \leftrightarrow \forall z \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < z)$
12		rphalfcl	$⊢ x \in ℝ^{+} \to \frac{x}{2} \in ℝ^{+}$
13		breq2	$⊢ z = \frac{x}{2} \to (G (F (k) D F (j)) < z \leftrightarrow G (F (k) D F (j)) < \frac{x}{2})$
14	13	anbi2d	$⊢ z = \frac{x}{2} \to ((τ \land G (F (k) D F (j)) < z) \leftrightarrow (τ \land G (F (k) D F (j)) < \frac{x}{2}))$
15	14	rexralbidv	$⊢ z = \frac{x}{2} \to (\exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < z) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < \frac{x}{2}))$
16	15	rspcv	$⊢ \frac{x}{2} \in ℝ^{+} \to (\forall z \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < z) \to \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < \frac{x}{2}))$
17	12 16	syl	$⊢ x \in ℝ^{+} \to (\forall z \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < z) \to \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < \frac{x}{2}))$
18	17	adantl	$⊢ (φ \land x \in ℝ^{+}) \to (\forall z \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < z) \to \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < \frac{x}{2}))$
19	2	ralimi	$⊢ \forall k \in ℤ_{\geq j} τ \to \forall k \in ℤ_{\geq j} ψ$
20		r19.26	$⊢ \forall k \in ℤ_{\geq j} (ψ \land G (F (k) D F (j)) < \frac{x}{2}) \leftrightarrow (\forall k \in ℤ_{\geq j} ψ \land \forall k \in ℤ_{\geq j} G (F (k) D F (j)) < \frac{x}{2})$
21		fveq2	$⊢ k = m \to F (k) = F (m)$
22	21 4	syl	$⊢ k = m \to (ψ \leftrightarrow θ)$
23	21	fvoveq1d	$⊢ k = m \to G (F (k) D F (j)) = G (F (m) D F (j))$
24	23	breq1d	$⊢ k = m \to (G (F (k) D F (j)) < \frac{x}{2} \leftrightarrow G (F (m) D F (j)) < \frac{x}{2})$
25	22 24	anbi12d	$⊢ k = m \to ((ψ \land G (F (k) D F (j)) < \frac{x}{2}) \leftrightarrow (θ \land G (F (m) D F (j)) < \frac{x}{2}))$
26	25	cbvralvw	$⊢ \forall k \in ℤ_{\geq j} (ψ \land G (F (k) D F (j)) < \frac{x}{2}) \leftrightarrow \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2})$
27	26	biimpi	$⊢ \forall k \in ℤ_{\geq j} (ψ \land G (F (k) D F (j)) < \frac{x}{2}) \to \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2})$
28	27	a1i	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} (ψ \land G (F (k) D F (j)) < \frac{x}{2}) \to \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2}))$
29	20 28	biimtrrid	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to ((\forall k \in ℤ_{\geq j} ψ \land \forall k \in ℤ_{\geq j} G (F (k) D F (j)) < \frac{x}{2}) \to \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2}))$
30	29	expdimp	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land \forall k \in ℤ_{\geq j} ψ) \to (\forall k \in ℤ_{\geq j} G (F (k) D F (j)) < \frac{x}{2} \to \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2}))$
31	1	sseli	$⊢ j \in Z \to j \in ℤ$
32		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
33	31 32	syl	$⊢ j \in Z \to j \in ℤ_{\geq j}$
34		fveq2	$⊢ k = j \to F (k) = F (j)$
35	34 3	syl	$⊢ k = j \to (ψ \leftrightarrow χ)$
36	35	rspcva	$⊢ (j \in ℤ_{\geq j} \land \forall k \in ℤ_{\geq j} ψ) \to χ$
37	33 36	sylan	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} ψ) \to χ$
38	37	adantll	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land \forall k \in ℤ_{\geq j} ψ) \to χ$
39	30 38	jctild	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land \forall k \in ℤ_{\geq j} ψ) \to (\forall k \in ℤ_{\geq j} G (F (k) D F (j)) < \frac{x}{2} \to (χ \land \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2})))$
40		simplll	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land θ)) \land ψ) \to φ$
41		simplrr	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land θ)) \land ψ) \to θ$
42		simplrl	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land θ)) \land ψ) \to χ$
43	40 41 42 6	syl3anc	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land θ)) \land ψ) \to G (F (m) D F (j)) = G (F (j) D F (m))$
44	43	breq1d	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land θ)) \land ψ) \to (G (F (m) D F (j)) < \frac{x}{2} \leftrightarrow G (F (j) D F (m)) < \frac{x}{2})$
45	44	anbi2d	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land θ)) \land ψ) \to ((G (F (k) D F (j)) < \frac{x}{2} \land G (F (m) D F (j)) < \frac{x}{2}) \leftrightarrow (G (F (k) D F (j)) < \frac{x}{2} \land G (F (j) D F (m)) < \frac{x}{2}))$
46		simpr	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land θ)) \land ψ) \to ψ$
47		simpllr	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land θ)) \land ψ) \to x \in ℝ^{+}$
48	47	rpred	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land θ)) \land ψ) \to x \in ℝ$
49	40 46 41 42 48 7	syl122anc	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land θ)) \land ψ) \to ((G (F (k) D F (j)) < \frac{x}{2} \land G (F (j) D F (m)) < \frac{x}{2}) \to G (F (k) D F (m)) < x)$
50	45 49	sylbid	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land θ)) \land ψ) \to ((G (F (k) D F (j)) < \frac{x}{2} \land G (F (m) D F (j)) < \frac{x}{2}) \to G (F (k) D F (m)) < x)$
51	50	expd	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land θ)) \land ψ) \to (G (F (k) D F (j)) < \frac{x}{2} \to (G (F (m) D F (j)) < \frac{x}{2} \to G (F (k) D F (m)) < x))$
52	51	impr	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land θ)) \land (ψ \land G (F (k) D F (j)) < \frac{x}{2})) \to (G (F (m) D F (j)) < \frac{x}{2} \to G (F (k) D F (m)) < x)$
53	52	an32s	$⊢ (((φ \land x \in ℝ^{+}) \land (ψ \land G (F (k) D F (j)) < \frac{x}{2})) \land (χ \land θ)) \to (G (F (m) D F (j)) < \frac{x}{2} \to G (F (k) D F (m)) < x)$
54	53	anassrs	$⊢ ((((φ \land x \in ℝ^{+}) \land (ψ \land G (F (k) D F (j)) < \frac{x}{2})) \land χ) \land θ) \to (G (F (m) D F (j)) < \frac{x}{2} \to G (F (k) D F (m)) < x)$
55	54	expimpd	$⊢ (((φ \land x \in ℝ^{+}) \land (ψ \land G (F (k) D F (j)) < \frac{x}{2})) \land χ) \to ((θ \land G (F (m) D F (j)) < \frac{x}{2}) \to G (F (k) D F (m)) < x)$
56	55	ralimdv	$⊢ (((φ \land x \in ℝ^{+}) \land (ψ \land G (F (k) D F (j)) < \frac{x}{2})) \land χ) \to (\forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2}) \to \forall m \in ℤ_{\geq j} G (F (k) D F (m)) < x)$
57	56	impr	$⊢ (((φ \land x \in ℝ^{+}) \land (ψ \land G (F (k) D F (j)) < \frac{x}{2})) \land (χ \land \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2}))) \to \forall m \in ℤ_{\geq j} G (F (k) D F (m)) < x$
58	57	an32s	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2}))) \land (ψ \land G (F (k) D F (j)) < \frac{x}{2})) \to \forall m \in ℤ_{\geq j} G (F (k) D F (m)) < x$
59	58	expr	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2}))) \land ψ) \to (G (F (k) D F (j)) < \frac{x}{2} \to \forall m \in ℤ_{\geq j} G (F (k) D F (m)) < x)$
60		uzss	$⊢ k \in ℤ_{\geq j} \to ℤ_{\geq k} \subseteq ℤ_{\geq j}$
61		ssralv	$⊢ ℤ_{\geq k} \subseteq ℤ_{\geq j} \to (\forall m \in ℤ_{\geq j} G (F (k) D F (m)) < x \to \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x)$
62	60 61	syl	$⊢ k \in ℤ_{\geq j} \to (\forall m \in ℤ_{\geq j} G (F (k) D F (m)) < x \to \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x)$
63	59 62	sylan9	$⊢ ((((φ \land x \in ℝ^{+}) \land (χ \land \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2}))) \land ψ) \land k \in ℤ_{\geq j}) \to (G (F (k) D F (j)) < \frac{x}{2} \to \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x)$
64	63	an32s	$⊢ ((((φ \land x \in ℝ^{+}) \land (χ \land \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2}))) \land k \in ℤ_{\geq j}) \land ψ) \to (G (F (k) D F (j)) < \frac{x}{2} \to \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x)$
65	64	expimpd	$⊢ (((φ \land x \in ℝ^{+}) \land (χ \land \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2}))) \land k \in ℤ_{\geq j}) \to ((ψ \land G (F (k) D F (j)) < \frac{x}{2}) \to \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x)$
66	65	ralimdva	$⊢ ((φ \land x \in ℝ^{+}) \land (χ \land \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2}))) \to (\forall k \in ℤ_{\geq j} (ψ \land G (F (k) D F (j)) < \frac{x}{2}) \to \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x)$
67	66	ex	$⊢ (φ \land x \in ℝ^{+}) \to ((χ \land \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2})) \to (\forall k \in ℤ_{\geq j} (ψ \land G (F (k) D F (j)) < \frac{x}{2}) \to \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x))$
68	67	com23	$⊢ (φ \land x \in ℝ^{+}) \to (\forall k \in ℤ_{\geq j} (ψ \land G (F (k) D F (j)) < \frac{x}{2}) \to ((χ \land \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2})) \to \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x))$
69	68	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} (ψ \land G (F (k) D F (j)) < \frac{x}{2}) \to ((χ \land \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2})) \to \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x))$
70	20 69	biimtrrid	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to ((\forall k \in ℤ_{\geq j} ψ \land \forall k \in ℤ_{\geq j} G (F (k) D F (j)) < \frac{x}{2}) \to ((χ \land \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2})) \to \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x))$
71	70	expdimp	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land \forall k \in ℤ_{\geq j} ψ) \to (\forall k \in ℤ_{\geq j} G (F (k) D F (j)) < \frac{x}{2} \to ((χ \land \forall m \in ℤ_{\geq j} (θ \land G (F (m) D F (j)) < \frac{x}{2})) \to \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x))$
72	39 71	mpdd	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land \forall k \in ℤ_{\geq j} ψ) \to (\forall k \in ℤ_{\geq j} G (F (k) D F (j)) < \frac{x}{2} \to \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x)$
73	19 72	sylan2	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land \forall k \in ℤ_{\geq j} τ) \to (\forall k \in ℤ_{\geq j} G (F (k) D F (j)) < \frac{x}{2} \to \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x)$
74	73	imdistanda	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to ((\forall k \in ℤ_{\geq j} τ \land \forall k \in ℤ_{\geq j} G (F (k) D F (j)) < \frac{x}{2}) \to (\forall k \in ℤ_{\geq j} τ \land \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x))$
75		r19.26	$⊢ \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < \frac{x}{2}) \leftrightarrow (\forall k \in ℤ_{\geq j} τ \land \forall k \in ℤ_{\geq j} G (F (k) D F (j)) < \frac{x}{2})$
76		r19.26	$⊢ \forall k \in ℤ_{\geq j} (τ \land \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x) \leftrightarrow (\forall k \in ℤ_{\geq j} τ \land \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x)$
77	74 75 76	3imtr4g	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < \frac{x}{2}) \to \forall k \in ℤ_{\geq j} (τ \land \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x))$
78	77	reximdva	$⊢ (φ \land x \in ℝ^{+}) \to (\exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < \frac{x}{2}) \to \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x))$
79	18 78	syld	$⊢ (φ \land x \in ℝ^{+}) \to (\forall z \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < z) \to \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x))$
80	79	ralrimdva	$⊢ φ \to (\forall z \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < z) \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x))$
81	11 80	biimtrid	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < x) \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x))$
82		fveq2	$⊢ k = j \to ℤ_{\geq k} = ℤ_{\geq j}$
83	34	fvoveq1d	$⊢ k = j \to G (F (k) D F (m)) = G (F (j) D F (m))$
84	83	breq1d	$⊢ k = j \to (G (F (k) D F (m)) < x \leftrightarrow G (F (j) D F (m)) < x)$
85	82 84	raleqbidv	$⊢ k = j \to (\forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x \leftrightarrow \forall m \in ℤ_{\geq j} G (F (j) D F (m)) < x)$
86	85	rspcv	$⊢ j \in ℤ_{\geq j} \to (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x \to \forall m \in ℤ_{\geq j} G (F (j) D F (m)) < x)$
87	86	ad2antlr	$⊢ ((φ \land j \in ℤ_{\geq j}) \land \forall k \in ℤ_{\geq j} ψ) \to (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x \to \forall m \in ℤ_{\geq j} G (F (j) D F (m)) < x)$
88		fveq2	$⊢ m = k \to F (m) = F (k)$
89	88	oveq2d	$⊢ m = k \to F (j) D F (m) = F (j) D F (k)$
90	89	fveq2d	$⊢ m = k \to G (F (j) D F (m)) = G (F (j) D F (k))$
91	90	breq1d	$⊢ m = k \to (G (F (j) D F (m)) < x \leftrightarrow G (F (j) D F (k)) < x)$
92	91	cbvralvw	$⊢ \forall m \in ℤ_{\geq j} G (F (j) D F (m)) < x \leftrightarrow \forall k \in ℤ_{\geq j} G (F (j) D F (k)) < x$
93	36	anim2i	$⊢ (φ \land (j \in ℤ_{\geq j} \land \forall k \in ℤ_{\geq j} ψ)) \to (φ \land χ)$
94	93	anassrs	$⊢ ((φ \land j \in ℤ_{\geq j}) \land \forall k \in ℤ_{\geq j} ψ) \to (φ \land χ)$
95		simpr	$⊢ ((φ \land j \in ℤ_{\geq j}) \land \forall k \in ℤ_{\geq j} ψ) \to \forall k \in ℤ_{\geq j} ψ$
96	5	breq1d	$⊢ (φ \land χ \land ψ) \to (G (F (j) D F (k)) < x \leftrightarrow G (F (k) D F (j)) < x)$
97	96	3expia	$⊢ (φ \land χ) \to (ψ \to (G (F (j) D F (k)) < x \leftrightarrow G (F (k) D F (j)) < x))$
98	97	ralimdv	$⊢ (φ \land χ) \to (\forall k \in ℤ_{\geq j} ψ \to \forall k \in ℤ_{\geq j} (G (F (j) D F (k)) < x \leftrightarrow G (F (k) D F (j)) < x))$
99	94 95 98	sylc	$⊢ ((φ \land j \in ℤ_{\geq j}) \land \forall k \in ℤ_{\geq j} ψ) \to \forall k \in ℤ_{\geq j} (G (F (j) D F (k)) < x \leftrightarrow G (F (k) D F (j)) < x)$
100		ralbi	$⊢ \forall k \in ℤ_{\geq j} (G (F (j) D F (k)) < x \leftrightarrow G (F (k) D F (j)) < x) \to (\forall k \in ℤ_{\geq j} G (F (j) D F (k)) < x \leftrightarrow \forall k \in ℤ_{\geq j} G (F (k) D F (j)) < x)$
101	99 100	syl	$⊢ ((φ \land j \in ℤ_{\geq j}) \land \forall k \in ℤ_{\geq j} ψ) \to (\forall k \in ℤ_{\geq j} G (F (j) D F (k)) < x \leftrightarrow \forall k \in ℤ_{\geq j} G (F (k) D F (j)) < x)$
102	92 101	bitrid	$⊢ ((φ \land j \in ℤ_{\geq j}) \land \forall k \in ℤ_{\geq j} ψ) \to (\forall m \in ℤ_{\geq j} G (F (j) D F (m)) < x \leftrightarrow \forall k \in ℤ_{\geq j} G (F (k) D F (j)) < x)$
103	87 102	sylibd	$⊢ ((φ \land j \in ℤ_{\geq j}) \land \forall k \in ℤ_{\geq j} ψ) \to (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x \to \forall k \in ℤ_{\geq j} G (F (k) D F (j)) < x)$
104	19 103	sylan2	$⊢ ((φ \land j \in ℤ_{\geq j}) \land \forall k \in ℤ_{\geq j} τ) \to (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x \to \forall k \in ℤ_{\geq j} G (F (k) D F (j)) < x)$
105	104	imdistanda	$⊢ (φ \land j \in ℤ_{\geq j}) \to ((\forall k \in ℤ_{\geq j} τ \land \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x) \to (\forall k \in ℤ_{\geq j} τ \land \forall k \in ℤ_{\geq j} G (F (k) D F (j)) < x))$
106	33 105	sylan2	$⊢ (φ \land j \in Z) \to ((\forall k \in ℤ_{\geq j} τ \land \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x) \to (\forall k \in ℤ_{\geq j} τ \land \forall k \in ℤ_{\geq j} G (F (k) D F (j)) < x))$
107		r19.26	$⊢ \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < x) \leftrightarrow (\forall k \in ℤ_{\geq j} τ \land \forall k \in ℤ_{\geq j} G (F (k) D F (j)) < x)$
108	106 76 107	3imtr4g	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} (τ \land \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x) \to \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < x))$
109	108	reximdva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (τ \land \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x) \to \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < x))$
110	109	ralimdv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x) \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < x))$
111	81 110	impbid	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land G (F (k) D F (j)) < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (τ \land \forall m \in ℤ_{\geq k} G (F (k) D F (m)) < x))$

Metamath Proof Explorer

Theorem cau3lem

Proof