Theorem ruclem1

Description: Lemma for ruc (the reals are uncountable). Substitutions for the function D . (Contributed by Mario Carneiro, 28-May-2014) (Revised by Fan Zheng, 6-Jun-2016)

	Ref	Expression
Hypotheses	ruc.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
	ruc.2	⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) )
	ruclem1.3	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ruclem1.4	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ruclem1.5	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
	ruclem1.6	⊢ 𝑋 = ( 1st ‘ ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) )
	ruclem1.7	⊢ 𝑌 = ( 2nd ‘ ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) )
Assertion	ruclem1	⊢ ( 𝜑 → ( ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) ∈ ( ℝ × ℝ ) ∧ 𝑋 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) ∧ 𝑌 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ruc.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
2		ruc.2	⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) )
3		ruclem1.3	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4		ruclem1.4	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5		ruclem1.5	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
6		ruclem1.6	⊢ 𝑋 = ( 1st ‘ ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) )
7		ruclem1.7	⊢ 𝑌 = ( 2nd ‘ ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) )
8	2	oveqd	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) = ( ⟨ 𝐴 , 𝐵 ⟩ ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) 𝑀 ) )
9	3 4	opelxpd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ℝ × ℝ ) )
10		simpr	⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = 𝑀 ) → 𝑦 = 𝑀 )
11	10	breq2d	⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = 𝑀 ) → ( 𝑚 < 𝑦 ↔ 𝑚 < 𝑀 ) )
12		simpl	⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = 𝑀 ) → 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ )
13	12	fveq2d	⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = 𝑀 ) → ( 1st ‘ 𝑥 ) = ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
14	13	opeq1d	⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = 𝑀 ) → ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ = ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ )
15	12	fveq2d	⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = 𝑀 ) → ( 2nd ‘ 𝑥 ) = ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
16	15	oveq2d	⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = 𝑀 ) → ( 𝑚 + ( 2nd ‘ 𝑥 ) ) = ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
17	16	oveq1d	⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = 𝑀 ) → ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) = ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) )
18	17 15	opeq12d	⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = 𝑀 ) → ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ = ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ )
19	11 14 18	ifbieq12d	⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = 𝑀 ) → if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) = if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) )
20	19	csbeq2dv	⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = 𝑀 ) → ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) = ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) )
21	13 15	oveq12d	⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = 𝑀 ) → ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
22	21	oveq1d	⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = 𝑀 ) → ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) = ( ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) )
23	22	csbeq1d	⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = 𝑀 ) → ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) = ⦋ ( ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) )
24	20 23	eqtrd	⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = 𝑀 ) → ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) = ⦋ ( ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) )
25		eqid	⊢ ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) )
26		opex	⊢ ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ ∈ V
27		opex	⊢ ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ∈ V
28	26 27	ifex	⊢ if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) ∈ V
29	28	csbex	⊢ ⦋ ( ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) ∈ V
30	24 25 29	ovmpoa	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ℝ × ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ⟨ 𝐴 , 𝐵 ⟩ ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) 𝑀 ) = ⦋ ( ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) )
31	9 5 30	syl2anc	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) 𝑀 ) = ⦋ ( ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) )
32	8 31	eqtrd	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) = ⦋ ( ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) )
33		op1stg	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
34	3 4 33	syl2anc	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
35		op2ndg	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
36	3 4 35	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
37	34 36	oveq12d	⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝐴 + 𝐵 ) )
38	37	oveq1d	⊢ ( 𝜑 → ( ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) = ( ( 𝐴 + 𝐵 ) / 2 ) )
39	38	csbeq1d	⊢ ( 𝜑 → ⦋ ( ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) = ⦋ ( ( 𝐴 + 𝐵 ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) )
40		ovex	⊢ ( ( 𝐴 + 𝐵 ) / 2 ) ∈ V
41		breq1	⊢ ( 𝑚 = ( ( 𝐴 + 𝐵 ) / 2 ) → ( 𝑚 < 𝑀 ↔ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 ) )
42		opeq2	⊢ ( 𝑚 = ( ( 𝐴 + 𝐵 ) / 2 ) → ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ = ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ )
43		oveq1	⊢ ( 𝑚 = ( ( 𝐴 + 𝐵 ) / 2 ) → ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
44	43	oveq1d	⊢ ( 𝑚 = ( ( 𝐴 + 𝐵 ) / 2 ) → ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) = ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) )
45	44	opeq1d	⊢ ( 𝑚 = ( ( 𝐴 + 𝐵 ) / 2 ) → ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ = ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ )
46	41 42 45	ifbieq12d	⊢ ( 𝑚 = ( ( 𝐴 + 𝐵 ) / 2 ) → if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ , ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) )
47	40 46	csbie	⊢ ⦋ ( ( 𝐴 + 𝐵 ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ , ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ )
48	34	opeq1d	⊢ ( 𝜑 → ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ = ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ )
49	36	oveq2d	⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) )
50	49	oveq1d	⊢ ( 𝜑 → ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) = ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) )
51	50 36	opeq12d	⊢ ( 𝜑 → ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ = ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ )
52	48 51	ifeq12d	⊢ ( 𝜑 → if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ , ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ , ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) )
53	47 52	syl5eq	⊢ ( 𝜑 → ⦋ ( ( 𝐴 + 𝐵 ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ , ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) )
54	39 53	eqtrd	⊢ ( 𝜑 → ⦋ ( ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑀 , ⟨ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) / 2 ) , ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⟩ ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ , ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) )
55	32 54	eqtrd	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ , ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) )
56	3 4	readdcld	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
57	56	rehalfcld	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℝ )
58	3 57	opelxpd	⊢ ( 𝜑 → ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ ∈ ( ℝ × ℝ ) )
59	57 4	readdcld	⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) ∈ ℝ )
60	59	rehalfcld	⊢ ( 𝜑 → ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ∈ ℝ )
61	60 4	opelxpd	⊢ ( 𝜑 → ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ∈ ( ℝ × ℝ ) )
62	58 61	ifcld	⊢ ( 𝜑 → if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ , ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) ∈ ( ℝ × ℝ ) )
63	55 62	eqeltrd	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) ∈ ( ℝ × ℝ ) )
64	55	fveq2d	⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) ) = ( 1st ‘ if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ , ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) ) )
65		fvif	⊢ ( 1st ‘ if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ , ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( 1st ‘ ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ ) , ( 1st ‘ ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) )
66		op1stg	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝐴 + 𝐵 ) / 2 ) ∈ V ) → ( 1st ‘ ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ ) = 𝐴 )
67	3 40 66	sylancl	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ ) = 𝐴 )
68		ovex	⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ∈ V
69		op1stg	⊢ ( ( ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ∈ V ∧ 𝐵 ∈ ℝ ) → ( 1st ‘ ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) = ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) )
70	68 4 69	sylancr	⊢ ( 𝜑 → ( 1st ‘ ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) = ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) )
71	67 70	ifeq12d	⊢ ( 𝜑 → if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( 1st ‘ ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ ) , ( 1st ‘ ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
72	65 71	syl5eq	⊢ ( 𝜑 → ( 1st ‘ if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ , ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
73	64 72	eqtrd	⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
74	6 73	syl5eq	⊢ ( 𝜑 → 𝑋 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) )
75	55	fveq2d	⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) ) = ( 2nd ‘ if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ , ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) ) )
76		fvif	⊢ ( 2nd ‘ if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ , ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( 2nd ‘ ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ ) , ( 2nd ‘ ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) )
77		op2ndg	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝐴 + 𝐵 ) / 2 ) ∈ V ) → ( 2nd ‘ ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ ) = ( ( 𝐴 + 𝐵 ) / 2 ) )
78	3 40 77	sylancl	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ ) = ( ( 𝐴 + 𝐵 ) / 2 ) )
79		op2ndg	⊢ ( ( ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ∈ V ∧ 𝐵 ∈ ℝ ) → ( 2nd ‘ ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) = 𝐵 )
80	68 4 79	sylancr	⊢ ( 𝜑 → ( 2nd ‘ ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) = 𝐵 )
81	78 80	ifeq12d	⊢ ( 𝜑 → if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( 2nd ‘ ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ ) , ( 2nd ‘ ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) )
82	76 81	syl5eq	⊢ ( 𝜑 → ( 2nd ‘ if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ⟨ 𝐴 , ( ( 𝐴 + 𝐵 ) / 2 ) ⟩ , ⟨ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) , 𝐵 ⟩ ) ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) )
83	75 82	eqtrd	⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) ) = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) )
84	7 83	syl5eq	⊢ ( 𝜑 → 𝑌 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) )
85	63 74 84	3jca	⊢ ( 𝜑 → ( ( ⟨ 𝐴 , 𝐵 ⟩ 𝐷 𝑀 ) ∈ ( ℝ × ℝ ) ∧ 𝑋 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , 𝐴 , ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + 𝐵 ) / 2 ) ) ∧ 𝑌 = if ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝑀 , ( ( 𝐴 + 𝐵 ) / 2 ) , 𝐵 ) ) )