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	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
	ruc.2	⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) )
	ruc.4	⊢ 𝐶 = ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 )
	ruc.5	⊢ 𝐺 = seq 0 ( 𝐷 , 𝐶 )
	ruclem10.6	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
	ruclem10.7	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	ruclem10	⊢ ( 𝜑 → ( 1st ‘ ( 𝐺 ‘ 𝑀 ) ) < ( 2nd ‘ ( 𝐺 ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ruc.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
2		ruc.2	⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) )
3		ruc.4	⊢ 𝐶 = ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 )
4		ruc.5	⊢ 𝐺 = seq 0 ( 𝐷 , 𝐶 )
5		ruclem10.6	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
6		ruclem10.7	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7	1 2 3 4	ruclem6	⊢ ( 𝜑 → 𝐺 : ℕ0 ⟶ ( ℝ × ℝ ) )
8	7 5	ffvelrnd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑀 ) ∈ ( ℝ × ℝ ) )
9		xp1st	⊢ ( ( 𝐺 ‘ 𝑀 ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝐺 ‘ 𝑀 ) ) ∈ ℝ )
10	8 9	syl	⊢ ( 𝜑 → ( 1st ‘ ( 𝐺 ‘ 𝑀 ) ) ∈ ℝ )
11	6 5	ifcld	⊢ ( 𝜑 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℕ0 )
12	7 11	ffvelrnd	⊢ ( 𝜑 → ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∈ ( ℝ × ℝ ) )
13		xp1st	⊢ ( ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) ∈ ℝ )
14	12 13	syl	⊢ ( 𝜑 → ( 1st ‘ ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) ∈ ℝ )
15	7 6	ffvelrnd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑁 ) ∈ ( ℝ × ℝ ) )
16		xp2nd	⊢ ( ( 𝐺 ‘ 𝑁 ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐺 ‘ 𝑁 ) ) ∈ ℝ )
17	15 16	syl	⊢ ( 𝜑 → ( 2nd ‘ ( 𝐺 ‘ 𝑁 ) ) ∈ ℝ )
18	5	nn0red	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
19	6	nn0red	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
20		max1	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
21	18 19 20	syl2anc	⊢ ( 𝜑 → 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
22	5	nn0zd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
23	11	nn0zd	⊢ ( 𝜑 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℤ )
24		eluz	⊢ ( ( 𝑀 ∈ ℤ ∧ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℤ ) → ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
25	22 23 24	syl2anc	⊢ ( 𝜑 → ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
26	21 25	mpbird	⊢ ( 𝜑 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
27	1 2 3 4 5 26	ruclem9	⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1st ‘ ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) ∧ ( 2nd ‘ ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) )
28	27	simpld	⊢ ( 𝜑 → ( 1st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1st ‘ ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) )
29		xp2nd	⊢ ( ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) ∈ ℝ )
30	12 29	syl	⊢ ( 𝜑 → ( 2nd ‘ ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) ∈ ℝ )
31	1 2 3 4	ruclem8	⊢ ( ( 𝜑 ∧ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℕ0 ) → ( 1st ‘ ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) < ( 2nd ‘ ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) )
32	11 31	mpdan	⊢ ( 𝜑 → ( 1st ‘ ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) < ( 2nd ‘ ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) )
33		max2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
34	18 19 33	syl2anc	⊢ ( 𝜑 → 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
35	6	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
36		eluz	⊢ ( ( 𝑁 ∈ ℤ ∧ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℤ ) → ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑁 ) ↔ 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
37	35 23 36	syl2anc	⊢ ( 𝜑 → ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑁 ) ↔ 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
38	34 37	mpbird	⊢ ( 𝜑 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
39	1 2 3 4 6 38	ruclem9	⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐺 ‘ 𝑁 ) ) ≤ ( 1st ‘ ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) ∧ ( 2nd ‘ ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑁 ) ) ) )
40	39	simprd	⊢ ( 𝜑 → ( 2nd ‘ ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑁 ) ) )
41	14 30 17 32 40	ltletrd	⊢ ( 𝜑 → ( 1st ‘ ( 𝐺 ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) < ( 2nd ‘ ( 𝐺 ‘ 𝑁 ) ) )
42	10 14 17 28 41	lelttrd	⊢ ( 𝜑 → ( 1st ‘ ( 𝐺 ‘ 𝑀 ) ) < ( 2nd ‘ ( 𝐺 ‘ 𝑁 ) ) )