ruclem8

Description: Lemma for ruc . The intervals of the G sequence are all nonempty. (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 ( 𝐷 , 𝐶 )
Assertion	ruclem8	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ₀ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑁 ) ) < ( 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		2fveq3	⊢ ( 𝑘 = 0 → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 1^st ‘ ( 𝐺 ‘ 0 ) ) )
6		2fveq3	⊢ ( 𝑘 = 0 → ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐺 ‘ 0 ) ) )
7	5 6	breq12d	⊢ ( 𝑘 = 0 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ↔ ( 1^st ‘ ( 𝐺 ‘ 0 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 0 ) ) ) )
8	7	imbi2d	⊢ ( 𝑘 = 0 → ( ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ) ↔ ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ 0 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 0 ) ) ) ) )
9		2fveq3	⊢ ( 𝑘 = 𝑛 → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) )
10		2fveq3	⊢ ( 𝑘 = 𝑛 → ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
11	9 10	breq12d	⊢ ( 𝑘 = 𝑛 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ↔ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
12	11	imbi2d	⊢ ( 𝑘 = 𝑛 → ( ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ) ↔ ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
13		2fveq3	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
14		2fveq3	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
15	13 14	breq12d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ↔ ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) < ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
16	15	imbi2d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ) ↔ ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) < ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) ) )
17		2fveq3	⊢ ( 𝑘 = 𝑁 → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 1^st ‘ ( 𝐺 ‘ 𝑁 ) ) )
18		2fveq3	⊢ ( 𝑘 = 𝑁 → ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐺 ‘ 𝑁 ) ) )
19	17 18	breq12d	⊢ ( 𝑘 = 𝑁 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ↔ ( 1^st ‘ ( 𝐺 ‘ 𝑁 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑁 ) ) ) )
20	19	imbi2d	⊢ ( 𝑘 = 𝑁 → ( ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ) ↔ ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ 𝑁 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑁 ) ) ) ) )
21		0lt1	⊢ 0 < 1
22	21	a1i	⊢ ( 𝜑 → 0 < 1 )
23	1 2 3 4	ruclem4	⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = ⟨ 0 , 1 ⟩ )
24	23	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ 0 ) ) = ( 1^st ‘ ⟨ 0 , 1 ⟩ ) )
25		c0ex	⊢ 0 ∈ V
26		1ex	⊢ 1 ∈ V
27	25 26	op1st	⊢ ( 1^st ‘ ⟨ 0 , 1 ⟩ ) = 0
28	24 27	eqtrdi	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ 0 ) ) = 0 )
29	23	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐺 ‘ 0 ) ) = ( 2^nd ‘ ⟨ 0 , 1 ⟩ ) )
30	25 26	op2nd	⊢ ( 2^nd ‘ ⟨ 0 , 1 ⟩ ) = 1
31	29 30	eqtrdi	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐺 ‘ 0 ) ) = 1 )
32	22 28 31	3brtr4d	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ 0 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 0 ) ) )
33	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → 𝐹 : ℕ ⟶ ℝ )
34	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1^st ‘ 𝑥 ) + ( 2^nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1^st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2^nd ‘ 𝑥 ) ) / 2 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) ) )
35	1 2 3 4	ruclem6	⊢ ( 𝜑 → 𝐺 : ℕ₀ ⟶ ( ℝ × ℝ ) )
36	35	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) )
37	36	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) )
38		xp1st	⊢ ( ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
39	37 38	syl	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
40		xp2nd	⊢ ( ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
41	37 40	syl	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
42		nn0p1nn	⊢ ( 𝑛 ∈ ℕ₀ → ( 𝑛 + 1 ) ∈ ℕ )
43		ffvelrn	⊢ ( ( 𝐹 : ℕ ⟶ ℝ ∧ ( 𝑛 + 1 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
44	1 42 43	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
45	44	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
46		eqid	⊢ ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) = ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
47		eqid	⊢ ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) = ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
48		simprr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
49	33 34 39 41 45 46 47 48	ruclem2	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → ( ( 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 ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
50	49	simp2d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) < ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
51	1 2 3 4	ruclem7	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → ( 𝐺 ‘ ( 𝑛 + 1 ) ) = ( ( 𝐺 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
52	51	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → ( 𝐺 ‘ ( 𝑛 + 1 ) ) = ( ( 𝐺 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
53		1st2nd2	⊢ ( ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 𝐺 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ )
54	37 53	syl	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → ( 𝐺 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ )
55	54	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → ( ( 𝐺 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
56	52 55	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → ( 𝐺 ‘ ( 𝑛 + 1 ) ) = ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
57	56	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) = ( 1^st ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
58	56	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) = ( 2^nd ‘ ( ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
59	50 57 58	3brtr4d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) < ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
60	59	expr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ₀ ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) → ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) < ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
61	60	expcom	⊢ ( 𝑛 ∈ ℕ₀ → ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) → ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) < ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) ) )
62	61	a2d	⊢ ( 𝑛 ∈ ℕ₀ → ( ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) < ( 2^nd ‘ ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) ) )
63	8 12 16 20 32 62	nn0ind	⊢ ( 𝑁 ∈ ℕ₀ → ( 𝜑 → ( 1^st ‘ ( 𝐺 ‘ 𝑁 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑁 ) ) ) )
64	63	impcom	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ₀ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑁 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑁 ) ) )

Metamath Proof Explorer

Theorem ruclem8

Proof