rexuzre

Description: Convert an upper real quantifier to an upper integer quantifier. (Contributed by Mario Carneiro, 7-May-2016)

		Ref	Expression
	Hypothesis	rexuz3.1	$⊢ Z = ℤ_{\geq M}$
	Assertion	rexuzre	$⊢ M \in ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} φ \leftrightarrow \exists j \in ℝ \forall k \in Z (j \leq k \to φ))$

Proof

Step	Hyp	Ref	Expression
1		rexuz3.1	$⊢ Z = ℤ_{\geq M}$
2		eluzelre	$⊢ j \in ℤ_{\geq M} \to j \in ℝ$
3	2 1	eleq2s	$⊢ j \in Z \to j \in ℝ$
4	3	adantr	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} φ) \to j \in ℝ$
5		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
6	5 1	eleq2s	$⊢ j \in Z \to j \in ℤ$
7		eluzelz	$⊢ k \in ℤ_{\geq M} \to k \in ℤ$
8	7 1	eleq2s	$⊢ k \in Z \to k \in ℤ$
9		eluz	$⊢ (j \in ℤ \land k \in ℤ) \to (k \in ℤ_{\geq j} \leftrightarrow j \leq k)$
10	6 8 9	syl2an	$⊢ (j \in Z \land k \in Z) \to (k \in ℤ_{\geq j} \leftrightarrow j \leq k)$
11	10	biimprd	$⊢ (j \in Z \land k \in Z) \to (j \leq k \to k \in ℤ_{\geq j})$
12	11	expimpd	$⊢ j \in Z \to ((k \in Z \land j \leq k) \to k \in ℤ_{\geq j})$
13	12	imim1d	$⊢ j \in Z \to ((k \in ℤ_{\geq j} \to φ) \to ((k \in Z \land j \leq k) \to φ))$
14	13	exp4a	$⊢ j \in Z \to ((k \in ℤ_{\geq j} \to φ) \to (k \in Z \to (j \leq k \to φ)))$
15	14	ralimdv2	$⊢ j \in Z \to (\forall k \in ℤ_{\geq j} φ \to \forall k \in Z (j \leq k \to φ))$
16	15	imp	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} φ) \to \forall k \in Z (j \leq k \to φ)$
17	4 16	jca	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} φ) \to (j \in ℝ \land \forall k \in Z (j \leq k \to φ))$
18	17	reximi2	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} φ \to \exists j \in ℝ \forall k \in Z (j \leq k \to φ)$
19		simpl	$⊢ (M \in ℤ \land j \in ℝ) \to M \in ℤ$
20		flcl	$⊢ j \in ℝ \to ⌊j⌋ \in ℤ$
21	20	adantl	$⊢ (M \in ℤ \land j \in ℝ) \to ⌊j⌋ \in ℤ$
22	21	peano2zd	$⊢ (M \in ℤ \land j \in ℝ) \to ⌊j⌋ + 1 \in ℤ$
23	22 19	ifcld	$⊢ (M \in ℤ \land j \in ℝ) \to if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M) \in ℤ$
24		zre	$⊢ M \in ℤ \to M \in ℝ$
25		reflcl	$⊢ j \in ℝ \to ⌊j⌋ \in ℝ$
26		peano2re	$⊢ ⌊j⌋ \in ℝ \to ⌊j⌋ + 1 \in ℝ$
27	25 26	syl	$⊢ j \in ℝ \to ⌊j⌋ + 1 \in ℝ$
28		max1	$⊢ (M \in ℝ \land ⌊j⌋ + 1 \in ℝ) \to M \leq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)$
29	24 27 28	syl2an	$⊢ (M \in ℤ \land j \in ℝ) \to M \leq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)$
30		eluz2	$⊢ if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M) \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M) \in ℤ \land M \leq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M))$
31	19 23 29 30	syl3anbrc	$⊢ (M \in ℤ \land j \in ℝ) \to if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M) \in ℤ_{\geq M}$
32	31 1	eleqtrrdi	$⊢ (M \in ℤ \land j \in ℝ) \to if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M) \in Z$
33		impexp	$⊢ ((k \in Z \land j \leq k) \to φ) \leftrightarrow (k \in Z \to (j \leq k \to φ))$
34		uzss	$⊢ if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M) \in ℤ_{\geq M} \to ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)} \subseteq ℤ_{\geq M}$
35	31 34	syl	$⊢ (M \in ℤ \land j \in ℝ) \to ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)} \subseteq ℤ_{\geq M}$
36	35 1	sseqtrrdi	$⊢ (M \in ℤ \land j \in ℝ) \to ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)} \subseteq Z$
37	36	sselda	$⊢ ((M \in ℤ \land j \in ℝ) \land k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)}) \to k \in Z$
38		simplr	$⊢ ((M \in ℤ \land j \in ℝ) \land k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)}) \to j \in ℝ$
39	23	adantr	$⊢ ((M \in ℤ \land j \in ℝ) \land k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)}) \to if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M) \in ℤ$
40	39	zred	$⊢ ((M \in ℤ \land j \in ℝ) \land k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)}) \to if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M) \in ℝ$
41		eluzelre	$⊢ k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)} \to k \in ℝ$
42	41	adantl	$⊢ ((M \in ℤ \land j \in ℝ) \land k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)}) \to k \in ℝ$
43		simpr	$⊢ (M \in ℤ \land j \in ℝ) \to j \in ℝ$
44	27	adantl	$⊢ (M \in ℤ \land j \in ℝ) \to ⌊j⌋ + 1 \in ℝ$
45	23	zred	$⊢ (M \in ℤ \land j \in ℝ) \to if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M) \in ℝ$
46		fllep1	$⊢ j \in ℝ \to j \leq ⌊j⌋ + 1$
47	46	adantl	$⊢ (M \in ℤ \land j \in ℝ) \to j \leq ⌊j⌋ + 1$
48		max2	$⊢ (M \in ℝ \land ⌊j⌋ + 1 \in ℝ) \to ⌊j⌋ + 1 \leq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)$
49	24 27 48	syl2an	$⊢ (M \in ℤ \land j \in ℝ) \to ⌊j⌋ + 1 \leq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)$
50	43 44 45 47 49	letrd	$⊢ (M \in ℤ \land j \in ℝ) \to j \leq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)$
51	50	adantr	$⊢ ((M \in ℤ \land j \in ℝ) \land k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)}) \to j \leq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)$
52		eluzle	$⊢ k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)} \to if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M) \leq k$
53	52	adantl	$⊢ ((M \in ℤ \land j \in ℝ) \land k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)}) \to if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M) \leq k$
54	38 40 42 51 53	letrd	$⊢ ((M \in ℤ \land j \in ℝ) \land k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)}) \to j \leq k$
55	37 54	jca	$⊢ ((M \in ℤ \land j \in ℝ) \land k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)}) \to (k \in Z \land j \leq k)$
56	55	ex	$⊢ (M \in ℤ \land j \in ℝ) \to (k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)} \to (k \in Z \land j \leq k))$
57	56	imim1d	$⊢ (M \in ℤ \land j \in ℝ) \to (((k \in Z \land j \leq k) \to φ) \to (k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)} \to φ))$
58	33 57	biimtrrid	$⊢ (M \in ℤ \land j \in ℝ) \to ((k \in Z \to (j \leq k \to φ)) \to (k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)} \to φ))$
59	58	ralimdv2	$⊢ (M \in ℤ \land j \in ℝ) \to (\forall k \in Z (j \leq k \to φ) \to \forall k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)} φ)$
60		fveq2	$⊢ m = if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M) \to ℤ_{\geq m} = ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)}$
61	60	raleqdv	$⊢ m = if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M) \to (\forall k \in ℤ_{\geq m} φ \leftrightarrow \forall k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)} φ)$
62	61	rspcev	$⊢ (if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M) \in Z \land \forall k \in ℤ_{\geq if (M \leq ⌊j⌋ + 1, ⌊j⌋ + 1, M)} φ) \to \exists m \in Z \forall k \in ℤ_{\geq m} φ$
63	32 59 62	syl6an	$⊢ (M \in ℤ \land j \in ℝ) \to (\forall k \in Z (j \leq k \to φ) \to \exists m \in Z \forall k \in ℤ_{\geq m} φ)$
64	63	rexlimdva	$⊢ M \in ℤ \to (\exists j \in ℝ \forall k \in Z (j \leq k \to φ) \to \exists m \in Z \forall k \in ℤ_{\geq m} φ)$
65		fveq2	$⊢ m = j \to ℤ_{\geq m} = ℤ_{\geq j}$
66	65	raleqdv	$⊢ m = j \to (\forall k \in ℤ_{\geq m} φ \leftrightarrow \forall k \in ℤ_{\geq j} φ)$
67	66	cbvrexvw	$⊢ \exists m \in Z \forall k \in ℤ_{\geq m} φ \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} φ$
68	64 67	imbitrdi	$⊢ M \in ℤ \to (\exists j \in ℝ \forall k \in Z (j \leq k \to φ) \to \exists j \in Z \forall k \in ℤ_{\geq j} φ)$
69	18 68	impbid2	$⊢ M \in ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} φ \leftrightarrow \exists j \in ℝ \forall k \in Z (j \leq k \to φ))$

Metamath Proof Explorer

Theorem rexuzre

Proof