MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ruclem1 Structured version   Visualization version   GIF version

Theorem ruclem1 16174
Description: Lemma for ruc 16186 (the reals are uncountable). Substitutions for the function 𝐷. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Fan Zheng, 6-Jun-2016.)
Hypotheses
Ref Expression
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
Ref Expression
ruclem1 (πœ‘ β†’ ((⟨𝐴, π΅βŸ©π·π‘€) ∈ (ℝ Γ— ℝ) ∧ 𝑋 = if(((𝐴 + 𝐡) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐡) / 2) + 𝐡) / 2)) ∧ π‘Œ = if(((𝐴 + 𝐡) / 2) < 𝑀, ((𝐴 + 𝐡) / 2), 𝐡)))
Distinct variable groups:   π‘₯,π‘š,𝑦,𝐴   𝐡,π‘š,π‘₯,𝑦   π‘š,𝐹,π‘₯,𝑦   π‘š,𝑀,π‘₯,𝑦
Allowed substitution hints:   πœ‘(π‘₯,𝑦,π‘š)   𝐷(π‘₯,𝑦,π‘š)   𝑋(π‘₯,𝑦,π‘š)   π‘Œ(π‘₯,𝑦,π‘š)

Proof of Theorem ruclem1
StepHypRef Expression
1 ruc.2 . . . . . 6 (πœ‘ β†’ 𝐷 = (π‘₯ ∈ (ℝ Γ— ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st β€˜π‘₯) + (2nd β€˜π‘₯)) / 2) / π‘šβ¦Œif(π‘š < 𝑦, ⟨(1st β€˜π‘₯), π‘šβŸ©, ⟨((π‘š + (2nd β€˜π‘₯)) / 2), (2nd β€˜π‘₯)⟩)))
21oveqd 7426 . . . . 5 (πœ‘ β†’ (⟨𝐴, π΅βŸ©π·π‘€) = (⟨𝐴, 𝐡⟩(π‘₯ ∈ (ℝ Γ— ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st β€˜π‘₯) + (2nd β€˜π‘₯)) / 2) / π‘šβ¦Œif(π‘š < 𝑦, ⟨(1st β€˜π‘₯), π‘šβŸ©, ⟨((π‘š + (2nd β€˜π‘₯)) / 2), (2nd β€˜π‘₯)⟩))𝑀))
3 ruclem1.3 . . . . . . 7 (πœ‘ β†’ 𝐴 ∈ ℝ)
4 ruclem1.4 . . . . . . 7 (πœ‘ β†’ 𝐡 ∈ ℝ)
53, 4opelxpd 5716 . . . . . 6 (πœ‘ β†’ ⟨𝐴, 𝐡⟩ ∈ (ℝ Γ— ℝ))
6 ruclem1.5 . . . . . 6 (πœ‘ β†’ 𝑀 ∈ ℝ)
7 simpr 486 . . . . . . . . . . 11 ((π‘₯ = ⟨𝐴, 𝐡⟩ ∧ 𝑦 = 𝑀) β†’ 𝑦 = 𝑀)
87breq2d 5161 . . . . . . . . . 10 ((π‘₯ = ⟨𝐴, 𝐡⟩ ∧ 𝑦 = 𝑀) β†’ (π‘š < 𝑦 ↔ π‘š < 𝑀))
9 simpl 484 . . . . . . . . . . . 12 ((π‘₯ = ⟨𝐴, 𝐡⟩ ∧ 𝑦 = 𝑀) β†’ π‘₯ = ⟨𝐴, 𝐡⟩)
109fveq2d 6896 . . . . . . . . . . 11 ((π‘₯ = ⟨𝐴, 𝐡⟩ ∧ 𝑦 = 𝑀) β†’ (1st β€˜π‘₯) = (1st β€˜βŸ¨π΄, 𝐡⟩))
1110opeq1d 4880 . . . . . . . . . 10 ((π‘₯ = ⟨𝐴, 𝐡⟩ ∧ 𝑦 = 𝑀) β†’ ⟨(1st β€˜π‘₯), π‘šβŸ© = ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©)
129fveq2d 6896 . . . . . . . . . . . . 13 ((π‘₯ = ⟨𝐴, 𝐡⟩ ∧ 𝑦 = 𝑀) β†’ (2nd β€˜π‘₯) = (2nd β€˜βŸ¨π΄, 𝐡⟩))
1312oveq2d 7425 . . . . . . . . . . . 12 ((π‘₯ = ⟨𝐴, 𝐡⟩ ∧ 𝑦 = 𝑀) β†’ (π‘š + (2nd β€˜π‘₯)) = (π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)))
1413oveq1d 7424 . . . . . . . . . . 11 ((π‘₯ = ⟨𝐴, 𝐡⟩ ∧ 𝑦 = 𝑀) β†’ ((π‘š + (2nd β€˜π‘₯)) / 2) = ((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2))
1514, 12opeq12d 4882 . . . . . . . . . 10 ((π‘₯ = ⟨𝐴, 𝐡⟩ ∧ 𝑦 = 𝑀) β†’ ⟨((π‘š + (2nd β€˜π‘₯)) / 2), (2nd β€˜π‘₯)⟩ = ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩)
168, 11, 15ifbieq12d 4557 . . . . . . . . 9 ((π‘₯ = ⟨𝐴, 𝐡⟩ ∧ 𝑦 = 𝑀) β†’ if(π‘š < 𝑦, ⟨(1st β€˜π‘₯), π‘šβŸ©, ⟨((π‘š + (2nd β€˜π‘₯)) / 2), (2nd β€˜π‘₯)⟩) = if(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩))
1716csbeq2dv 3901 . . . . . . . 8 ((π‘₯ = ⟨𝐴, 𝐡⟩ ∧ 𝑦 = 𝑀) β†’ ⦋(((1st β€˜π‘₯) + (2nd β€˜π‘₯)) / 2) / π‘šβ¦Œif(π‘š < 𝑦, ⟨(1st β€˜π‘₯), π‘šβŸ©, ⟨((π‘š + (2nd β€˜π‘₯)) / 2), (2nd β€˜π‘₯)⟩) = ⦋(((1st β€˜π‘₯) + (2nd β€˜π‘₯)) / 2) / π‘šβ¦Œif(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩))
1810, 12oveq12d 7427 . . . . . . . . . 10 ((π‘₯ = ⟨𝐴, 𝐡⟩ ∧ 𝑦 = 𝑀) β†’ ((1st β€˜π‘₯) + (2nd β€˜π‘₯)) = ((1st β€˜βŸ¨π΄, 𝐡⟩) + (2nd β€˜βŸ¨π΄, 𝐡⟩)))
1918oveq1d 7424 . . . . . . . . 9 ((π‘₯ = ⟨𝐴, 𝐡⟩ ∧ 𝑦 = 𝑀) β†’ (((1st β€˜π‘₯) + (2nd β€˜π‘₯)) / 2) = (((1st β€˜βŸ¨π΄, 𝐡⟩) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2))
2019csbeq1d 3898 . . . . . . . 8 ((π‘₯ = ⟨𝐴, 𝐡⟩ ∧ 𝑦 = 𝑀) β†’ ⦋(((1st β€˜π‘₯) + (2nd β€˜π‘₯)) / 2) / π‘šβ¦Œif(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩) = ⦋(((1st β€˜βŸ¨π΄, 𝐡⟩) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2) / π‘šβ¦Œif(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩))
2117, 20eqtrd 2773 . . . . . . 7 ((π‘₯ = ⟨𝐴, 𝐡⟩ ∧ 𝑦 = 𝑀) β†’ ⦋(((1st β€˜π‘₯) + (2nd β€˜π‘₯)) / 2) / π‘šβ¦Œif(π‘š < 𝑦, ⟨(1st β€˜π‘₯), π‘šβŸ©, ⟨((π‘š + (2nd β€˜π‘₯)) / 2), (2nd β€˜π‘₯)⟩) = ⦋(((1st β€˜βŸ¨π΄, 𝐡⟩) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2) / π‘šβ¦Œif(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩))
22 eqid 2733 . . . . . . 7 (π‘₯ ∈ (ℝ Γ— ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st β€˜π‘₯) + (2nd β€˜π‘₯)) / 2) / π‘šβ¦Œif(π‘š < 𝑦, ⟨(1st β€˜π‘₯), π‘šβŸ©, ⟨((π‘š + (2nd β€˜π‘₯)) / 2), (2nd β€˜π‘₯)⟩)) = (π‘₯ ∈ (ℝ Γ— ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st β€˜π‘₯) + (2nd β€˜π‘₯)) / 2) / π‘šβ¦Œif(π‘š < 𝑦, ⟨(1st β€˜π‘₯), π‘šβŸ©, ⟨((π‘š + (2nd β€˜π‘₯)) / 2), (2nd β€˜π‘₯)⟩))
23 opex 5465 . . . . . . . . 9 ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ© ∈ V
24 opex 5465 . . . . . . . . 9 ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩ ∈ V
2523, 24ifex 4579 . . . . . . . 8 if(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩) ∈ V
2625csbex 5312 . . . . . . 7 ⦋(((1st β€˜βŸ¨π΄, 𝐡⟩) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2) / π‘šβ¦Œif(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩) ∈ V
2721, 22, 26ovmpoa 7563 . . . . . 6 ((⟨𝐴, 𝐡⟩ ∈ (ℝ Γ— ℝ) ∧ 𝑀 ∈ ℝ) β†’ (⟨𝐴, 𝐡⟩(π‘₯ ∈ (ℝ Γ— ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st β€˜π‘₯) + (2nd β€˜π‘₯)) / 2) / π‘šβ¦Œif(π‘š < 𝑦, ⟨(1st β€˜π‘₯), π‘šβŸ©, ⟨((π‘š + (2nd β€˜π‘₯)) / 2), (2nd β€˜π‘₯)⟩))𝑀) = ⦋(((1st β€˜βŸ¨π΄, 𝐡⟩) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2) / π‘šβ¦Œif(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩))
285, 6, 27syl2anc 585 . . . . 5 (πœ‘ β†’ (⟨𝐴, 𝐡⟩(π‘₯ ∈ (ℝ Γ— ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st β€˜π‘₯) + (2nd β€˜π‘₯)) / 2) / π‘šβ¦Œif(π‘š < 𝑦, ⟨(1st β€˜π‘₯), π‘šβŸ©, ⟨((π‘š + (2nd β€˜π‘₯)) / 2), (2nd β€˜π‘₯)⟩))𝑀) = ⦋(((1st β€˜βŸ¨π΄, 𝐡⟩) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2) / π‘šβ¦Œif(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩))
292, 28eqtrd 2773 . . . 4 (πœ‘ β†’ (⟨𝐴, π΅βŸ©π·π‘€) = ⦋(((1st β€˜βŸ¨π΄, 𝐡⟩) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2) / π‘šβ¦Œif(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩))
30 op1stg 7987 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (1st β€˜βŸ¨π΄, 𝐡⟩) = 𝐴)
313, 4, 30syl2anc 585 . . . . . . . 8 (πœ‘ β†’ (1st β€˜βŸ¨π΄, 𝐡⟩) = 𝐴)
32 op2ndg 7988 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (2nd β€˜βŸ¨π΄, 𝐡⟩) = 𝐡)
333, 4, 32syl2anc 585 . . . . . . . 8 (πœ‘ β†’ (2nd β€˜βŸ¨π΄, 𝐡⟩) = 𝐡)
3431, 33oveq12d 7427 . . . . . . 7 (πœ‘ β†’ ((1st β€˜βŸ¨π΄, 𝐡⟩) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) = (𝐴 + 𝐡))
3534oveq1d 7424 . . . . . 6 (πœ‘ β†’ (((1st β€˜βŸ¨π΄, 𝐡⟩) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2) = ((𝐴 + 𝐡) / 2))
3635csbeq1d 3898 . . . . 5 (πœ‘ β†’ ⦋(((1st β€˜βŸ¨π΄, 𝐡⟩) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2) / π‘šβ¦Œif(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩) = ⦋((𝐴 + 𝐡) / 2) / π‘šβ¦Œif(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩))
37 ovex 7442 . . . . . . 7 ((𝐴 + 𝐡) / 2) ∈ V
38 breq1 5152 . . . . . . . 8 (π‘š = ((𝐴 + 𝐡) / 2) β†’ (π‘š < 𝑀 ↔ ((𝐴 + 𝐡) / 2) < 𝑀))
39 opeq2 4875 . . . . . . . 8 (π‘š = ((𝐴 + 𝐡) / 2) β†’ ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ© = ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), ((𝐴 + 𝐡) / 2)⟩)
40 oveq1 7416 . . . . . . . . . 10 (π‘š = ((𝐴 + 𝐡) / 2) β†’ (π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) = (((𝐴 + 𝐡) / 2) + (2nd β€˜βŸ¨π΄, 𝐡⟩)))
4140oveq1d 7424 . . . . . . . . 9 (π‘š = ((𝐴 + 𝐡) / 2) β†’ ((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2) = ((((𝐴 + 𝐡) / 2) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2))
4241opeq1d 4880 . . . . . . . 8 (π‘š = ((𝐴 + 𝐡) / 2) β†’ ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩ = ⟨((((𝐴 + 𝐡) / 2) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩)
4338, 39, 42ifbieq12d 4557 . . . . . . 7 (π‘š = ((𝐴 + 𝐡) / 2) β†’ if(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩) = if(((𝐴 + 𝐡) / 2) < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), ((𝐴 + 𝐡) / 2)⟩, ⟨((((𝐴 + 𝐡) / 2) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩))
4437, 43csbie 3930 . . . . . 6 ⦋((𝐴 + 𝐡) / 2) / π‘šβ¦Œif(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩) = if(((𝐴 + 𝐡) / 2) < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), ((𝐴 + 𝐡) / 2)⟩, ⟨((((𝐴 + 𝐡) / 2) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩)
4531opeq1d 4880 . . . . . . 7 (πœ‘ β†’ ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), ((𝐴 + 𝐡) / 2)⟩ = ⟨𝐴, ((𝐴 + 𝐡) / 2)⟩)
4633oveq2d 7425 . . . . . . . . 9 (πœ‘ β†’ (((𝐴 + 𝐡) / 2) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) = (((𝐴 + 𝐡) / 2) + 𝐡))
4746oveq1d 7424 . . . . . . . 8 (πœ‘ β†’ ((((𝐴 + 𝐡) / 2) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2) = ((((𝐴 + 𝐡) / 2) + 𝐡) / 2))
4847, 33opeq12d 4882 . . . . . . 7 (πœ‘ β†’ ⟨((((𝐴 + 𝐡) / 2) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩ = ⟨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩)
4945, 48ifeq12d 4550 . . . . . 6 (πœ‘ β†’ if(((𝐴 + 𝐡) / 2) < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), ((𝐴 + 𝐡) / 2)⟩, ⟨((((𝐴 + 𝐡) / 2) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩) = if(((𝐴 + 𝐡) / 2) < 𝑀, ⟨𝐴, ((𝐴 + 𝐡) / 2)⟩, ⟨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩))
5044, 49eqtrid 2785 . . . . 5 (πœ‘ β†’ ⦋((𝐴 + 𝐡) / 2) / π‘šβ¦Œif(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩) = if(((𝐴 + 𝐡) / 2) < 𝑀, ⟨𝐴, ((𝐴 + 𝐡) / 2)⟩, ⟨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩))
5136, 50eqtrd 2773 . . . 4 (πœ‘ β†’ ⦋(((1st β€˜βŸ¨π΄, 𝐡⟩) + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2) / π‘šβ¦Œif(π‘š < 𝑀, ⟨(1st β€˜βŸ¨π΄, 𝐡⟩), π‘šβŸ©, ⟨((π‘š + (2nd β€˜βŸ¨π΄, 𝐡⟩)) / 2), (2nd β€˜βŸ¨π΄, 𝐡⟩)⟩) = if(((𝐴 + 𝐡) / 2) < 𝑀, ⟨𝐴, ((𝐴 + 𝐡) / 2)⟩, ⟨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩))
5229, 51eqtrd 2773 . . 3 (πœ‘ β†’ (⟨𝐴, π΅βŸ©π·π‘€) = if(((𝐴 + 𝐡) / 2) < 𝑀, ⟨𝐴, ((𝐴 + 𝐡) / 2)⟩, ⟨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩))
533, 4readdcld 11243 . . . . . 6 (πœ‘ β†’ (𝐴 + 𝐡) ∈ ℝ)
5453rehalfcld 12459 . . . . 5 (πœ‘ β†’ ((𝐴 + 𝐡) / 2) ∈ ℝ)
553, 54opelxpd 5716 . . . 4 (πœ‘ β†’ ⟨𝐴, ((𝐴 + 𝐡) / 2)⟩ ∈ (ℝ Γ— ℝ))
5654, 4readdcld 11243 . . . . . 6 (πœ‘ β†’ (((𝐴 + 𝐡) / 2) + 𝐡) ∈ ℝ)
5756rehalfcld 12459 . . . . 5 (πœ‘ β†’ ((((𝐴 + 𝐡) / 2) + 𝐡) / 2) ∈ ℝ)
5857, 4opelxpd 5716 . . . 4 (πœ‘ β†’ ⟨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩ ∈ (ℝ Γ— ℝ))
5955, 58ifcld 4575 . . 3 (πœ‘ β†’ if(((𝐴 + 𝐡) / 2) < 𝑀, ⟨𝐴, ((𝐴 + 𝐡) / 2)⟩, ⟨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩) ∈ (ℝ Γ— ℝ))
6052, 59eqeltrd 2834 . 2 (πœ‘ β†’ (⟨𝐴, π΅βŸ©π·π‘€) ∈ (ℝ Γ— ℝ))
61 ruclem1.6 . . 3 𝑋 = (1st β€˜(⟨𝐴, π΅βŸ©π·π‘€))
6252fveq2d 6896 . . . 4 (πœ‘ β†’ (1st β€˜(⟨𝐴, π΅βŸ©π·π‘€)) = (1st β€˜if(((𝐴 + 𝐡) / 2) < 𝑀, ⟨𝐴, ((𝐴 + 𝐡) / 2)⟩, ⟨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩)))
63 fvif 6908 . . . . 5 (1st β€˜if(((𝐴 + 𝐡) / 2) < 𝑀, ⟨𝐴, ((𝐴 + 𝐡) / 2)⟩, ⟨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩)) = if(((𝐴 + 𝐡) / 2) < 𝑀, (1st β€˜βŸ¨π΄, ((𝐴 + 𝐡) / 2)⟩), (1st β€˜βŸ¨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩))
64 op1stg 7987 . . . . . . 7 ((𝐴 ∈ ℝ ∧ ((𝐴 + 𝐡) / 2) ∈ V) β†’ (1st β€˜βŸ¨π΄, ((𝐴 + 𝐡) / 2)⟩) = 𝐴)
653, 37, 64sylancl 587 . . . . . 6 (πœ‘ β†’ (1st β€˜βŸ¨π΄, ((𝐴 + 𝐡) / 2)⟩) = 𝐴)
66 ovex 7442 . . . . . . 7 ((((𝐴 + 𝐡) / 2) + 𝐡) / 2) ∈ V
67 op1stg 7987 . . . . . . 7 ((((((𝐴 + 𝐡) / 2) + 𝐡) / 2) ∈ V ∧ 𝐡 ∈ ℝ) β†’ (1st β€˜βŸ¨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩) = ((((𝐴 + 𝐡) / 2) + 𝐡) / 2))
6866, 4, 67sylancr 588 . . . . . 6 (πœ‘ β†’ (1st β€˜βŸ¨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩) = ((((𝐴 + 𝐡) / 2) + 𝐡) / 2))
6965, 68ifeq12d 4550 . . . . 5 (πœ‘ β†’ if(((𝐴 + 𝐡) / 2) < 𝑀, (1st β€˜βŸ¨π΄, ((𝐴 + 𝐡) / 2)⟩), (1st β€˜βŸ¨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩)) = if(((𝐴 + 𝐡) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐡) / 2) + 𝐡) / 2)))
7063, 69eqtrid 2785 . . . 4 (πœ‘ β†’ (1st β€˜if(((𝐴 + 𝐡) / 2) < 𝑀, ⟨𝐴, ((𝐴 + 𝐡) / 2)⟩, ⟨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩)) = if(((𝐴 + 𝐡) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐡) / 2) + 𝐡) / 2)))
7162, 70eqtrd 2773 . . 3 (πœ‘ β†’ (1st β€˜(⟨𝐴, π΅βŸ©π·π‘€)) = if(((𝐴 + 𝐡) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐡) / 2) + 𝐡) / 2)))
7261, 71eqtrid 2785 . 2 (πœ‘ β†’ 𝑋 = if(((𝐴 + 𝐡) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐡) / 2) + 𝐡) / 2)))
73 ruclem1.7 . . 3 π‘Œ = (2nd β€˜(⟨𝐴, π΅βŸ©π·π‘€))
7452fveq2d 6896 . . . 4 (πœ‘ β†’ (2nd β€˜(⟨𝐴, π΅βŸ©π·π‘€)) = (2nd β€˜if(((𝐴 + 𝐡) / 2) < 𝑀, ⟨𝐴, ((𝐴 + 𝐡) / 2)⟩, ⟨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩)))
75 fvif 6908 . . . . 5 (2nd β€˜if(((𝐴 + 𝐡) / 2) < 𝑀, ⟨𝐴, ((𝐴 + 𝐡) / 2)⟩, ⟨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩)) = if(((𝐴 + 𝐡) / 2) < 𝑀, (2nd β€˜βŸ¨π΄, ((𝐴 + 𝐡) / 2)⟩), (2nd β€˜βŸ¨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩))
76 op2ndg 7988 . . . . . . 7 ((𝐴 ∈ ℝ ∧ ((𝐴 + 𝐡) / 2) ∈ V) β†’ (2nd β€˜βŸ¨π΄, ((𝐴 + 𝐡) / 2)⟩) = ((𝐴 + 𝐡) / 2))
773, 37, 76sylancl 587 . . . . . 6 (πœ‘ β†’ (2nd β€˜βŸ¨π΄, ((𝐴 + 𝐡) / 2)⟩) = ((𝐴 + 𝐡) / 2))
78 op2ndg 7988 . . . . . . 7 ((((((𝐴 + 𝐡) / 2) + 𝐡) / 2) ∈ V ∧ 𝐡 ∈ ℝ) β†’ (2nd β€˜βŸ¨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩) = 𝐡)
7966, 4, 78sylancr 588 . . . . . 6 (πœ‘ β†’ (2nd β€˜βŸ¨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩) = 𝐡)
8077, 79ifeq12d 4550 . . . . 5 (πœ‘ β†’ if(((𝐴 + 𝐡) / 2) < 𝑀, (2nd β€˜βŸ¨π΄, ((𝐴 + 𝐡) / 2)⟩), (2nd β€˜βŸ¨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩)) = if(((𝐴 + 𝐡) / 2) < 𝑀, ((𝐴 + 𝐡) / 2), 𝐡))
8175, 80eqtrid 2785 . . . 4 (πœ‘ β†’ (2nd β€˜if(((𝐴 + 𝐡) / 2) < 𝑀, ⟨𝐴, ((𝐴 + 𝐡) / 2)⟩, ⟨((((𝐴 + 𝐡) / 2) + 𝐡) / 2), 𝐡⟩)) = if(((𝐴 + 𝐡) / 2) < 𝑀, ((𝐴 + 𝐡) / 2), 𝐡))
8274, 81eqtrd 2773 . . 3 (πœ‘ β†’ (2nd β€˜(⟨𝐴, π΅βŸ©π·π‘€)) = if(((𝐴 + 𝐡) / 2) < 𝑀, ((𝐴 + 𝐡) / 2), 𝐡))
8373, 82eqtrid 2785 . 2 (πœ‘ β†’ π‘Œ = if(((𝐴 + 𝐡) / 2) < 𝑀, ((𝐴 + 𝐡) / 2), 𝐡))
8460, 72, 833jca 1129 1 (πœ‘ β†’ ((⟨𝐴, π΅βŸ©π·π‘€) ∈ (ℝ Γ— ℝ) ∧ 𝑋 = if(((𝐴 + 𝐡) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐡) / 2) + 𝐡) / 2)) ∧ π‘Œ = if(((𝐴 + 𝐡) / 2) < 𝑀, ((𝐴 + 𝐡) / 2), 𝐡)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  Vcvv 3475  β¦‹csb 3894  ifcif 4529  βŸ¨cop 4635   class class class wbr 5149   Γ— cxp 5675  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409   ∈ cmpo 7411  1st c1st 7973  2nd c2nd 7974  β„cr 11109   + caddc 11113   < clt 11248   / cdiv 11871  β„•cn 12212  2c2 12267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-1st 7975  df-2nd 7976  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-2 12275
This theorem is referenced by:  ruclem2  16175  ruclem3  16176  ruclem6  16178
  Copyright terms: Public domain W3C validator