Theorem limsup10exlem

Description: The range of the given function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	limsup10exlem.1	$$⊢F=\left(n\in \mathbb{N}⟼if\left(2\parallel n,0,1\right)\right)$$
	limsup10exlem.2	$$⊢\phi \to K\in ℝ$$
Assertion	limsup10exlem	$$⊢\phi \to F\left[\left[K,\mathrm{+\infty }\right)\right]=\left\{0,1\right\}$$

Proof

Step	Hyp	Ref	Expression
1		limsup10exlem.1	$$⊢F=\left(n\in \mathbb{N}⟼if\left(2\parallel n,0,1\right)\right)$$
2		limsup10exlem.2	$$⊢\phi \to K\in ℝ$$
3		c0ex	$$⊢0\in \mathrm{V}$$
4	3	prid1	$$⊢0\in \left\{0,1\right\}$$
5		1re	$$⊢1\in ℝ$$
6	5	elexi	$$⊢1\in \mathrm{V}$$
7	6	prid2	$$⊢1\in \left\{0,1\right\}$$
8	4 7	ifcli	$$⊢if\left(2\parallel n,0,1\right)\in \left\{0,1\right\}$$
9	8	a1i	$$⊢\left(\phi \wedge n\in \left(\mathbb{N}\cap \left[K,\mathrm{+\infty }\right)\right)\right)\to if\left(2\parallel n,0,1\right)\in \left\{0,1\right\}$$
10	9	ralrimiva	$$⊢\phi \to \forall n\in \left(\mathbb{N}\cap \left[K,\mathrm{+\infty }\right)\right)if\left(2\parallel n,0,1\right)\in \left\{0,1\right\}$$
11		nfv	$$⊢Ⅎn\phi$$
12	3 6	ifex	$$⊢if\left(2\parallel n,0,1\right)\in \mathrm{V}$$
13	12	a1i	$$⊢\left(\phi \wedge n\in \left(\mathbb{N}\cap \left[K,\mathrm{+\infty }\right)\right)\right)\to if\left(2\parallel n,0,1\right)\in \mathrm{V}$$
14	11 13 1	imassmpt	$$⊢\phi \to \left(F\left[\left[K,\mathrm{+\infty }\right)\right]\subseteq \left\{0,1\right\}\leftrightarrow \forall n\in \left(\mathbb{N}\cap \left[K,\mathrm{+\infty }\right)\right)if\left(2\parallel n,0,1\right)\in \left\{0,1\right\}\right)$$
15	10 14	mpbird	$$⊢\phi \to F\left[\left[K,\mathrm{+\infty }\right)\right]\subseteq \left\{0,1\right\}$$
16	2	ceilcld	$$⊢\phi \to ⌈K⌉\in \mathbb{Z}$$
17		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
18	16 17	ifcld	$$⊢\phi \to if\left(1\le K,⌈K⌉,1\right)\in \mathbb{Z}$$
19	18	adantr	$$⊢\left(\phi \wedge n=2if\left(1\le K,⌈K⌉,1\right)\right)\to if\left(1\le K,⌈K⌉,1\right)\in \mathbb{Z}$$
20		simpr	$$⊢\left(\phi \wedge n=2if\left(1\le K,⌈K⌉,1\right)\right)\to n=2if\left(1\le K,⌈K⌉,1\right)$$
21		2teven	$$⊢\left(if\left(1\le K,⌈K⌉,1\right)\in \mathbb{Z}\wedge n=2if\left(1\le K,⌈K⌉,1\right)\right)\to 2\parallel n$$
22	19 20 21	syl2anc	$$⊢\left(\phi \wedge n=2if\left(1\le K,⌈K⌉,1\right)\right)\to 2\parallel n$$
23	22	iftrued	$$⊢\left(\phi \wedge n=2if\left(1\le K,⌈K⌉,1\right)\right)\to if\left(2\parallel n,0,1\right)=0$$
24		2nn	$$⊢2\in \mathbb{N}$$
25	24	a1i	$$⊢\phi \to 2\in \mathbb{N}$$
26		eqid	$$⊢{\mathbb{Z}}_{\ge 1}={\mathbb{Z}}_{\ge 1}$$
27	5	a1i	$$⊢\left(\phi \wedge 1\le K\right)\to 1\in ℝ$$
28	2	adantr	$$⊢\left(\phi \wedge 1\le K\right)\to K\in ℝ$$
29	16	zred	$$⊢\phi \to ⌈K⌉\in ℝ$$
30	29	adantr	$$⊢\left(\phi \wedge 1\le K\right)\to ⌈K⌉\in ℝ$$
31		simpr	$$⊢\left(\phi \wedge 1\le K\right)\to 1\le K$$
32	2	ceilged	$$⊢\phi \to K\le ⌈K⌉$$
33	32	adantr	$$⊢\left(\phi \wedge 1\le K\right)\to K\le ⌈K⌉$$
34	27 28 30 31 33	letrd	$$⊢\left(\phi \wedge 1\le K\right)\to 1\le ⌈K⌉$$
35		iftrue	$$⊢1\le K\to if\left(1\le K,⌈K⌉,1\right)=⌈K⌉$$
36	35	adantl	$$⊢\left(\phi \wedge 1\le K\right)\to if\left(1\le K,⌈K⌉,1\right)=⌈K⌉$$
37	34 36	breqtrrd	$$⊢\left(\phi \wedge 1\le K\right)\to 1\le if\left(1\le K,⌈K⌉,1\right)$$
38	5	leidi	$$⊢1\le 1$$
39	38	a1i	$$⊢\left(\phi \wedge \neg 1\le K\right)\to 1\le 1$$
40		iffalse	$$⊢\neg 1\le K\to if\left(1\le K,⌈K⌉,1\right)=1$$
41	40	adantl	$$⊢\left(\phi \wedge \neg 1\le K\right)\to if\left(1\le K,⌈K⌉,1\right)=1$$
42	39 41	breqtrrd	$$⊢\left(\phi \wedge \neg 1\le K\right)\to 1\le if\left(1\le K,⌈K⌉,1\right)$$
43	37 42	pm2.61dan	$$⊢\phi \to 1\le if\left(1\le K,⌈K⌉,1\right)$$
44	26 17 18 43	eluzd	$$⊢\phi \to if\left(1\le K,⌈K⌉,1\right)\in {\mathbb{Z}}_{\ge 1}$$
45		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
46	44 45	eleqtrrdi	$$⊢\phi \to if\left(1\le K,⌈K⌉,1\right)\in \mathbb{N}$$
47	25 46	nnmulcld	$$⊢\phi \to 2if\left(1\le K,⌈K⌉,1\right)\in \mathbb{N}$$
48	3	a1i	$$⊢\phi \to 0\in \mathrm{V}$$
49	1 23 47 48	fvmptd2	$$⊢\phi \to F\left(2if\left(1\le K,⌈K⌉,1\right)\right)=0$$
50	12 1	fnmpti	$$⊢FFn\mathbb{N}$$
51	50	a1i	$$⊢\phi \to FFn\mathbb{N}$$
52	2	rexrd	$$⊢\phi \to K\in {ℝ}^{*}$$
53		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
54	53	a1i	$$⊢\phi \to \mathrm{+\infty }\in {ℝ}^{*}$$
55	47	nnxrd	$$⊢\phi \to 2if\left(1\le K,⌈K⌉,1\right)\in {ℝ}^{*}$$
56	47	nnred	$$⊢\phi \to 2if\left(1\le K,⌈K⌉,1\right)\in ℝ$$
57	46	nnred	$$⊢\phi \to if\left(1\le K,⌈K⌉,1\right)\in ℝ$$
58	33 36	breqtrrd	$$⊢\left(\phi \wedge 1\le K\right)\to K\le if\left(1\le K,⌈K⌉,1\right)$$
59	2	adantr	$$⊢\left(\phi \wedge \neg 1\le K\right)\to K\in ℝ$$
60	5	a1i	$$⊢\left(\phi \wedge \neg 1\le K\right)\to 1\in ℝ$$
61		simpr	$$⊢\left(\phi \wedge \neg 1\le K\right)\to \neg 1\le K$$
62	59 60 61	nleltd	$$⊢\left(\phi \wedge \neg 1\le K\right)\to K<1$$
63	59 60 62	ltled	$$⊢\left(\phi \wedge \neg 1\le K\right)\to K\le 1$$
64	41	eqcomd	$$⊢\left(\phi \wedge \neg 1\le K\right)\to 1=if\left(1\le K,⌈K⌉,1\right)$$
65	63 64	breqtrd	$$⊢\left(\phi \wedge \neg 1\le K\right)\to K\le if\left(1\le K,⌈K⌉,1\right)$$
66	58 65	pm2.61dan	$$⊢\phi \to K\le if\left(1\le K,⌈K⌉,1\right)$$
67	46	nnrpd	$$⊢\phi \to if\left(1\le K,⌈K⌉,1\right)\in {ℝ}^{+}$$
68		2timesgt	$$⊢if\left(1\le K,⌈K⌉,1\right)\in {ℝ}^{+}\to if\left(1\le K,⌈K⌉,1\right)<2if\left(1\le K,⌈K⌉,1\right)$$
69	67 68	syl	$$⊢\phi \to if\left(1\le K,⌈K⌉,1\right)<2if\left(1\le K,⌈K⌉,1\right)$$
70	2 57 56 66 69	lelttrd	$$⊢\phi \to K<2if\left(1\le K,⌈K⌉,1\right)$$
71	2 56 70	ltled	$$⊢\phi \to K\le 2if\left(1\le K,⌈K⌉,1\right)$$
72	56	ltpnfd	$$⊢\phi \to 2if\left(1\le K,⌈K⌉,1\right)<\mathrm{+\infty }$$
73	52 54 55 71 72	elicod	$$⊢\phi \to 2if\left(1\le K,⌈K⌉,1\right)\in \left[K,\mathrm{+\infty }\right)$$
74	51 47 73	fnfvimad	$$⊢\phi \to F\left(2if\left(1\le K,⌈K⌉,1\right)\right)\in F\left[\left[K,\mathrm{+\infty }\right)\right]$$
75	49 74	eqeltrrd	$$⊢\phi \to 0\in F\left[\left[K,\mathrm{+\infty }\right)\right]$$
76	18	adantr	$$⊢\left(\phi \wedge n=2if\left(1\le K,⌈K⌉,1\right)+1\right)\to if\left(1\le K,⌈K⌉,1\right)\in \mathbb{Z}$$
77		simpr	$$⊢\left(\phi \wedge n=2if\left(1\le K,⌈K⌉,1\right)+1\right)\to n=2if\left(1\le K,⌈K⌉,1\right)+1$$
78		2tp1odd	$$⊢\left(if\left(1\le K,⌈K⌉,1\right)\in \mathbb{Z}\wedge n=2if\left(1\le K,⌈K⌉,1\right)+1\right)\to \neg 2\parallel n$$
79	76 77 78	syl2anc	$$⊢\left(\phi \wedge n=2if\left(1\le K,⌈K⌉,1\right)+1\right)\to \neg 2\parallel n$$
80	79	iffalsed	$$⊢\left(\phi \wedge n=2if\left(1\le K,⌈K⌉,1\right)+1\right)\to if\left(2\parallel n,0,1\right)=1$$
81	47	peano2nnd	$$⊢\phi \to 2if\left(1\le K,⌈K⌉,1\right)+1\in \mathbb{N}$$
82		1xr	$$⊢1\in {ℝ}^{*}$$
83	82	a1i	$$⊢\phi \to 1\in {ℝ}^{*}$$
84	1 80 81 83	fvmptd2	$$⊢\phi \to F\left(2if\left(1\le K,⌈K⌉,1\right)+1\right)=1$$
85	81	nnxrd	$$⊢\phi \to 2if\left(1\le K,⌈K⌉,1\right)+1\in {ℝ}^{*}$$
86	81	nnred	$$⊢\phi \to 2if\left(1\le K,⌈K⌉,1\right)+1\in ℝ$$
87	56	ltp1d	$$⊢\phi \to 2if\left(1\le K,⌈K⌉,1\right)<2if\left(1\le K,⌈K⌉,1\right)+1$$
88	2 56 86 70 87	lttrd	$$⊢\phi \to K<2if\left(1\le K,⌈K⌉,1\right)+1$$
89	2 86 88	ltled	$$⊢\phi \to K\le 2if\left(1\le K,⌈K⌉,1\right)+1$$
90	86	ltpnfd	$$⊢\phi \to 2if\left(1\le K,⌈K⌉,1\right)+1<\mathrm{+\infty }$$
91	52 54 85 89 90	elicod	$$⊢\phi \to 2if\left(1\le K,⌈K⌉,1\right)+1\in \left[K,\mathrm{+\infty }\right)$$
92	51 81 91	fnfvimad	$$⊢\phi \to F\left(2if\left(1\le K,⌈K⌉,1\right)+1\right)\in F\left[\left[K,\mathrm{+\infty }\right)\right]$$
93	84 92	eqeltrrd	$$⊢\phi \to 1\in F\left[\left[K,\mathrm{+\infty }\right)\right]$$
94	75 93	prssd	$$⊢\phi \to \left\{0,1\right\}\subseteq F\left[\left[K,\mathrm{+\infty }\right)\right]$$
95	15 94	eqssd	$$⊢\phi \to F\left[\left[K,\mathrm{+\infty }\right)\right]=\left\{0,1\right\}$$