Theorem ruclem10

Description: Lemma for ruc . Every first component of the G sequence is less than every second component. That is, the sequences form a chain a_1 < a_2 < ... < b_2 < b_1, where a_i are the first components and b_i are the second components. (Contributed by Mario Carneiro, 28-May-2014)

	Ref	Expression
Hypotheses	ruc.1	$$⊢\phi \to F:\mathbb{N}⟶ℝ$$
	ruc.2	$$⊢\phi \to D=\left(x\in {ℝ}^2,y\in ℝ⟼⦋\left(\frac{1^{st}\left(x\right)+2^{nd}\left(x\right)}{2}\right)/m⦌if\left(m<y,⟨1^{st}\left(x\right),m⟩,⟨\frac{m+2^{nd}\left(x\right)}{2},2^{nd}\left(x\right)⟩\right)\right)$$
	ruc.4	$$⊢C=\left\{⟨0,⟨0,1⟩⟩\right\}\cup F$$
	ruc.5	$$⊢G=seq0\left(D,C\right)$$
	ruclem10.6	$$⊢\phi \to M\in {\mathbb{N}}_0$$
	ruclem10.7	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	ruclem10	$$⊢\phi \to 1^{st}\left(G\left(M\right)\right)<2^{nd}\left(G\left(N\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ruc.1	$$⊢\phi \to F:\mathbb{N}⟶ℝ$$
2		ruc.2	$$⊢\phi \to D=\left(x\in {ℝ}^2,y\in ℝ⟼⦋\left(\frac{1^{st}\left(x\right)+2^{nd}\left(x\right)}{2}\right)/m⦌if\left(m<y,⟨1^{st}\left(x\right),m⟩,⟨\frac{m+2^{nd}\left(x\right)}{2},2^{nd}\left(x\right)⟩\right)\right)$$
3		ruc.4	$$⊢C=\left\{⟨0,⟨0,1⟩⟩\right\}\cup F$$
4		ruc.5	$$⊢G=seq0\left(D,C\right)$$
5		ruclem10.6	$$⊢\phi \to M\in {\mathbb{N}}_0$$
6		ruclem10.7	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7	1 2 3 4	ruclem6	$$⊢\phi \to G:{\mathbb{N}}_0⟶{ℝ}^2$$
8	7 5	ffvelrnd	$$⊢\phi \to G\left(M\right)\in {ℝ}^2$$
9		xp1st	$$⊢G\left(M\right)\in {ℝ}^2\to 1^{st}\left(G\left(M\right)\right)\in ℝ$$
10	8 9	syl	$$⊢\phi \to 1^{st}\left(G\left(M\right)\right)\in ℝ$$
11	6 5	ifcld	$$⊢\phi \to if\left(M\le N,N,M\right)\in {\mathbb{N}}_0$$
12	7 11	ffvelrnd	$$⊢\phi \to G\left(if\left(M\le N,N,M\right)\right)\in {ℝ}^2$$
13		xp1st	$$⊢G\left(if\left(M\le N,N,M\right)\right)\in {ℝ}^2\to 1^{st}\left(G\left(if\left(M\le N,N,M\right)\right)\right)\in ℝ$$
14	12 13	syl	$$⊢\phi \to 1^{st}\left(G\left(if\left(M\le N,N,M\right)\right)\right)\in ℝ$$
15	7 6	ffvelrnd	$$⊢\phi \to G\left(N\right)\in {ℝ}^2$$
16		xp2nd	$$⊢G\left(N\right)\in {ℝ}^2\to 2^{nd}\left(G\left(N\right)\right)\in ℝ$$
17	15 16	syl	$$⊢\phi \to 2^{nd}\left(G\left(N\right)\right)\in ℝ$$
18	5	nn0red	$$⊢\phi \to M\in ℝ$$
19	6	nn0red	$$⊢\phi \to N\in ℝ$$
20		max1	$$⊢\left(M\in ℝ\wedge N\in ℝ\right)\to M\le if\left(M\le N,N,M\right)$$
21	18 19 20	syl2anc	$$⊢\phi \to M\le if\left(M\le N,N,M\right)$$
22	5	nn0zd	$$⊢\phi \to M\in \mathbb{Z}$$
23	11	nn0zd	$$⊢\phi \to if\left(M\le N,N,M\right)\in \mathbb{Z}$$
24		eluz	$$⊢\left(M\in \mathbb{Z}\wedge if\left(M\le N,N,M\right)\in \mathbb{Z}\right)\to \left(if\left(M\le N,N,M\right)\in {\mathbb{Z}}_{\ge M}\leftrightarrow M\le if\left(M\le N,N,M\right)\right)$$
25	22 23 24	syl2anc	$$⊢\phi \to \left(if\left(M\le N,N,M\right)\in {\mathbb{Z}}_{\ge M}\leftrightarrow M\le if\left(M\le N,N,M\right)\right)$$
26	21 25	mpbird	$$⊢\phi \to if\left(M\le N,N,M\right)\in {\mathbb{Z}}_{\ge M}$$
27	1 2 3 4 5 26	ruclem9	$$⊢\phi \to \left(1^{st}\left(G\left(M\right)\right)\le 1^{st}\left(G\left(if\left(M\le N,N,M\right)\right)\right)\wedge 2^{nd}\left(G\left(if\left(M\le N,N,M\right)\right)\right)\le 2^{nd}\left(G\left(M\right)\right)\right)$$
28	27	simpld	$$⊢\phi \to 1^{st}\left(G\left(M\right)\right)\le 1^{st}\left(G\left(if\left(M\le N,N,M\right)\right)\right)$$
29		xp2nd	$$⊢G\left(if\left(M\le N,N,M\right)\right)\in {ℝ}^2\to 2^{nd}\left(G\left(if\left(M\le N,N,M\right)\right)\right)\in ℝ$$
30	12 29	syl	$$⊢\phi \to 2^{nd}\left(G\left(if\left(M\le N,N,M\right)\right)\right)\in ℝ$$
31	1 2 3 4	ruclem8	$$⊢\left(\phi \wedge if\left(M\le N,N,M\right)\in {\mathbb{N}}_0\right)\to 1^{st}\left(G\left(if\left(M\le N,N,M\right)\right)\right)<2^{nd}\left(G\left(if\left(M\le N,N,M\right)\right)\right)$$
32	11 31	mpdan	$$⊢\phi \to 1^{st}\left(G\left(if\left(M\le N,N,M\right)\right)\right)<2^{nd}\left(G\left(if\left(M\le N,N,M\right)\right)\right)$$
33		max2	$$⊢\left(M\in ℝ\wedge N\in ℝ\right)\to N\le if\left(M\le N,N,M\right)$$
34	18 19 33	syl2anc	$$⊢\phi \to N\le if\left(M\le N,N,M\right)$$
35	6	nn0zd	$$⊢\phi \to N\in \mathbb{Z}$$
36		eluz	$$⊢\left(N\in \mathbb{Z}\wedge if\left(M\le N,N,M\right)\in \mathbb{Z}\right)\to \left(if\left(M\le N,N,M\right)\in {\mathbb{Z}}_{\ge N}\leftrightarrow N\le if\left(M\le N,N,M\right)\right)$$
37	35 23 36	syl2anc	$$⊢\phi \to \left(if\left(M\le N,N,M\right)\in {\mathbb{Z}}_{\ge N}\leftrightarrow N\le if\left(M\le N,N,M\right)\right)$$
38	34 37	mpbird	$$⊢\phi \to if\left(M\le N,N,M\right)\in {\mathbb{Z}}_{\ge N}$$
39	1 2 3 4 6 38	ruclem9	$$⊢\phi \to \left(1^{st}\left(G\left(N\right)\right)\le 1^{st}\left(G\left(if\left(M\le N,N,M\right)\right)\right)\wedge 2^{nd}\left(G\left(if\left(M\le N,N,M\right)\right)\right)\le 2^{nd}\left(G\left(N\right)\right)\right)$$
40	39	simprd	$$⊢\phi \to 2^{nd}\left(G\left(if\left(M\le N,N,M\right)\right)\right)\le 2^{nd}\left(G\left(N\right)\right)$$
41	14 30 17 32 40	ltletrd	$$⊢\phi \to 1^{st}\left(G\left(if\left(M\le N,N,M\right)\right)\right)<2^{nd}\left(G\left(N\right)\right)$$
42	10 14 17 28 41	lelttrd	$$⊢\phi \to 1^{st}\left(G\left(M\right)\right)<2^{nd}\left(G\left(N\right)\right)$$