ruclem9

Description: Lemma for ruc . The first components of the G sequence are increasing, and the second components are decreasing. (Contributed by Mario Carneiro, 28-May-2014)

	Ref	Expression
Hypotheses	ruc.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
	ruc.2	⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1^st ‘ 𝑥 ) + ( 2^nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1^st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2^nd ‘ 𝑥 ) ) / 2 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) ) )
	ruc.4	⊢ 𝐶 = ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 )
	ruc.5	⊢ 𝐺 = seq 0 ( 𝐷 , 𝐶 )
	ruclem9.6	⊢ ( 𝜑 → 𝑀 ∈ ℕ₀ )
	ruclem9.7	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) )
Assertion	ruclem9	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ruc.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
2		ruc.2	⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1^st ‘ 𝑥 ) + ( 2^nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1^st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2^nd ‘ 𝑥 ) ) / 2 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) ) )
3		ruc.4	⊢ 𝐶 = ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 )
4		ruc.5	⊢ 𝐺 = seq 0 ( 𝐷 , 𝐶 )
5		ruclem9.6	⊢ ( 𝜑 → 𝑀 ∈ ℕ₀ )
6		ruclem9.7	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) )
7		2fveq3	⊢ ( 𝑘 = 𝑀 → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) )
8	7	breq2d	⊢ ( 𝑘 = 𝑀 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ↔ ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ) )
9		2fveq3	⊢ ( 𝑘 = 𝑀 → ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) )
10	9	breq1d	⊢ ( 𝑘 = 𝑀 → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ↔ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) )
11	8 10	anbi12d	⊢ ( 𝑘 = 𝑀 → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ↔ ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) )
12	11	imbi2d	⊢ ( 𝑘 = 𝑀 → ( ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) ↔ ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) ) )
13		2fveq3	⊢ ( 𝑘 = 𝑛 → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) )
14	13	breq2d	⊢ ( 𝑘 = 𝑛 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ↔ ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
15		2fveq3	⊢ ( 𝑘 = 𝑛 → ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
16	15	breq1d	⊢ ( 𝑘 = 𝑛 → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ↔ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) )
17	14 16	anbi12d	⊢ ( 𝑘 = 𝑛 → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ↔ ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) )
18	17	imbi2d	⊢ ( 𝑘 = 𝑛 → ( ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) ↔ ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) ) )
19		2fveq3	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
20	19	breq2d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ↔ ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
21		2fveq3	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
22	21	breq1d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ↔ ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) )
23	20 22	anbi12d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ↔ ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) )
24	23	imbi2d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) ↔ ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) ) )
25		2fveq3	⊢ ( 𝑘 = 𝑁 → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 1^st ‘ ( 𝐺 ‘ 𝑁 ) ) )
26	25	breq2d	⊢ ( 𝑘 = 𝑁 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ↔ ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑁 ) ) ) )
27		2fveq3	⊢ ( 𝑘 = 𝑁 → ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐺 ‘ 𝑁 ) ) )
28	27	breq1d	⊢ ( 𝑘 = 𝑁 → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ↔ ( 2^nd ‘ ( 𝐺 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) )
29	26 28	anbi12d	⊢ ( 𝑘 = 𝑁 → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ↔ ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) )
30	29	imbi2d	⊢ ( 𝑘 = 𝑁 → ( ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) ↔ ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) ) )
31	1 2 3 4	ruclem6	⊢ ( 𝜑 → 𝐺 : ℕ₀ ⟶ ( ℝ × ℝ ) )
32	31 5	ffvelrnd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑀 ) ∈ ( ℝ × ℝ ) )
33		xp1st	⊢ ( ( 𝐺 ‘ 𝑀 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ∈ ℝ )
34	32 33	syl	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ∈ ℝ )
35	34	leidd	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) )
36		xp2nd	⊢ ( ( 𝐺 ‘ 𝑀 ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ∈ ℝ )
37	32 36	syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ∈ ℝ )
38	37	leidd	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) )
39	35 38	jca	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) )
40	1	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → 𝐹 : ℕ ⟶ ℝ )
41	2	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1^st ‘ 𝑥 ) + ( 2^nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1^st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2^nd ‘ 𝑥 ) ) / 2 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) ) )
42	31	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → 𝐺 : ℕ₀ ⟶ ( ℝ × ℝ ) )
43		eluznn0	⊢ ( ( 𝑀 ∈ ℕ₀ ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → 𝑛 ∈ ℕ₀ )
44	5 43	sylan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → 𝑛 ∈ ℕ₀ )
45	42 44	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) )
46		xp1st	⊢ ( ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
47	45 46	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
48		xp2nd	⊢ ( ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
49	45 48	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
50		nn0p1nn	⊢ ( 𝑛 ∈ ℕ₀ → ( 𝑛 + 1 ) ∈ ℕ )
51	44 50	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 𝑛 + 1 ) ∈ ℕ )
52	40 51	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
53		eqid	⊢ ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) = ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
54		eqid	⊢ ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) = ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
55	1 2 3 4	ruclem8	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
56	44 55	syldan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
57	40 41 47 49 52 53 54 56	ruclem2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ∧ ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) < ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ∧ ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
58	57	simp1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
59	1 2 3 4	ruclem7	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → ( 𝐺 ‘ ( 𝑛 + 1 ) ) = ( ( 𝐺 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
60	44 59	syldan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 𝐺 ‘ ( 𝑛 + 1 ) ) = ( ( 𝐺 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
61		1st2nd2	⊢ ( ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 𝐺 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ )
62	45 61	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 𝐺 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ )
63	62	oveq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( ( 𝐺 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
64	60 63	eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 𝐺 ‘ ( 𝑛 + 1 ) ) = ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
65	64	fveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) = ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
66	58 65	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
67	34	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ∈ ℝ )
68		peano2nn0	⊢ ( 𝑛 ∈ ℕ₀ → ( 𝑛 + 1 ) ∈ ℕ₀ )
69	44 68	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 𝑛 + 1 ) ∈ ℕ₀ )
70	42 69	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 𝐺 ‘ ( 𝑛 + 1 ) ) ∈ ( ℝ × ℝ ) )
71		xp1st	⊢ ( ( 𝐺 ‘ ( 𝑛 + 1 ) ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ )
72	70 71	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ )
73		letr	⊢ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) → ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
74	67 47 72 73	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) → ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
75	66 74	mpan2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) → ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
76	64	fveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) = ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
77	57	simp3d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
78	76 77	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
79		xp2nd	⊢ ( ( 𝐺 ‘ ( 𝑛 + 1 ) ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ )
80	70 79	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ )
81	37	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ∈ ℝ )
82		letr	⊢ ( ( ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ∈ ℝ ) → ( ( ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) → ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) )
83	80 49 81 82	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( ( ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) → ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) )
84	78 83	mpand	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) → ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) )
85	75 84	anim12d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) )
86	85	expcom	⊢ ( 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) → ( 𝜑 → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) ) )
87	86	a2d	⊢ ( 𝑛 ∈ ( ℤ_≥ ‘ 𝑀 ) → ( ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) → ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) ) )
88	12 18 24 30 39 87	uzind4i	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) → ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) ) )
89	6 88	mpcom	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑀 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑀 ) ) ) )

Metamath Proof Explorer

Theorem ruclem9

Proof