ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bdtrilem GIF version

Theorem bdtrilem 11282
Description: Lemma for bdtri 11283. (Contributed by Steven Nguyen and Jim Kingdon, 17-May-2023.)
Assertion
Ref Expression
bdtrilem (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((abs‘(𝐴𝐶)) + (abs‘(𝐵𝐶))) ≤ (𝐶 + (abs‘((𝐴 + 𝐵) − 𝐶))))

Proof of Theorem bdtrilem
StepHypRef Expression
1 simp1l 1023 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 𝐴 ∈ ℝ)
2 simp3 1001 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 𝐶 ∈ ℝ+)
32rpred 9728 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 𝐶 ∈ ℝ)
41, 3resubcld 8369 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴𝐶) ∈ ℝ)
54resqcld 10714 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴𝐶)↑2) ∈ ℝ)
6 2re 9020 . . . . . . . . . . . 12 2 ∈ ℝ
76a1i 9 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 2 ∈ ℝ)
81recnd 8017 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 𝐴 ∈ ℂ)
92rpcnd 9730 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 𝐶 ∈ ℂ)
108, 9subcld 8299 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴𝐶) ∈ ℂ)
1110abscld 11225 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘(𝐴𝐶)) ∈ ℝ)
12 simp2l 1025 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 𝐵 ∈ ℝ)
1312recnd 8017 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 𝐵 ∈ ℂ)
1413, 9subcld 8299 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐵𝐶) ∈ ℂ)
1514abscld 11225 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘(𝐵𝐶)) ∈ ℝ)
1611, 15remulcld 8019 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))) ∈ ℝ)
177, 16remulcld 8019 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶)))) ∈ ℝ)
185, 17readdcld 8018 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴𝐶)↑2) + (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))))) ∈ ℝ)
191, 12remulcld 8019 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 · 𝐵) ∈ ℝ)
207, 19remulcld 8019 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (2 · (𝐴 · 𝐵)) ∈ ℝ)
218, 13addcld 8008 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 + 𝐵) ∈ ℂ)
2221, 9subcld 8299 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴 + 𝐵) − 𝐶) ∈ ℂ)
2322abscld 11225 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘((𝐴 + 𝐵) − 𝐶)) ∈ ℝ)
243, 23remulcld 8019 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))) ∈ ℝ)
257, 24remulcld 8019 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶)))) ∈ ℝ)
2620, 25readdcld 8018 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((2 · (𝐴 · 𝐵)) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))) ∈ ℝ)
275, 26readdcld 8018 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴𝐶)↑2) + ((2 · (𝐴 · 𝐵)) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶)))))) ∈ ℝ)
2812, 3resubcld 8369 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐵𝐶) ∈ ℝ)
2928resqcld 10714 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐵𝐶)↑2) ∈ ℝ)
3019, 24readdcld 8018 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴 · 𝐵) + (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶)))) ∈ ℝ)
31 0le2 9040 . . . . . . . . . . . . 13 0 ≤ 2
3231a1i 9 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 0 ≤ 2)
338, 9, 13, 9mulsubd 8405 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴𝐶) · (𝐵𝐶)) = (((𝐴 · 𝐵) + (𝐶 · 𝐶)) − ((𝐴 · 𝐶) + (𝐵 · 𝐶))))
3419recnd 8017 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 · 𝐵) ∈ ℂ)
359, 9mulcld 8009 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐶 · 𝐶) ∈ ℂ)
368, 9mulcld 8009 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 · 𝐶) ∈ ℂ)
3713, 9mulcld 8009 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐵 · 𝐶) ∈ ℂ)
3836, 37addcld 8008 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴 · 𝐶) + (𝐵 · 𝐶)) ∈ ℂ)
3934, 35, 38addsubassd 8319 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴 · 𝐵) + (𝐶 · 𝐶)) − ((𝐴 · 𝐶) + (𝐵 · 𝐶))) = ((𝐴 · 𝐵) + ((𝐶 · 𝐶) − ((𝐴 · 𝐶) + (𝐵 · 𝐶)))))
4033, 39eqtrd 2222 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴𝐶) · (𝐵𝐶)) = ((𝐴 · 𝐵) + ((𝐶 · 𝐶) − ((𝐴 · 𝐶) + (𝐵 · 𝐶)))))
4140fveq2d 5538 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘((𝐴𝐶) · (𝐵𝐶))) = (abs‘((𝐴 · 𝐵) + ((𝐶 · 𝐶) − ((𝐴 · 𝐶) + (𝐵 · 𝐶))))))
4235, 38subcld 8299 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐶 · 𝐶) − ((𝐴 · 𝐶) + (𝐵 · 𝐶))) ∈ ℂ)
4334, 42abstrid 11240 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘((𝐴 · 𝐵) + ((𝐶 · 𝐶) − ((𝐴 · 𝐶) + (𝐵 · 𝐶))))) ≤ ((abs‘(𝐴 · 𝐵)) + (abs‘((𝐶 · 𝐶) − ((𝐴 · 𝐶) + (𝐵 · 𝐶))))))
4441, 43eqbrtrd 4040 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘((𝐴𝐶) · (𝐵𝐶))) ≤ ((abs‘(𝐴 · 𝐵)) + (abs‘((𝐶 · 𝐶) − ((𝐴 · 𝐶) + (𝐵 · 𝐶))))))
45 simp1r 1024 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 0 ≤ 𝐴)
46 simp2r 1026 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 0 ≤ 𝐵)
471, 12, 45, 46mulge0d 8609 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 0 ≤ (𝐴 · 𝐵))
4819, 47absidd 11211 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘(𝐴 · 𝐵)) = (𝐴 · 𝐵))
499, 21subcld 8299 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐶 − (𝐴 + 𝐵)) ∈ ℂ)
5049, 9absmuld 11238 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘((𝐶 − (𝐴 + 𝐵)) · 𝐶)) = ((abs‘(𝐶 − (𝐴 + 𝐵))) · (abs‘𝐶)))
519, 21, 9subdird 8403 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐶 − (𝐴 + 𝐵)) · 𝐶) = ((𝐶 · 𝐶) − ((𝐴 + 𝐵) · 𝐶)))
528, 13, 9adddird 8014 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
5352oveq2d 5913 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐶 · 𝐶) − ((𝐴 + 𝐵) · 𝐶)) = ((𝐶 · 𝐶) − ((𝐴 · 𝐶) + (𝐵 · 𝐶))))
5451, 53eqtrd 2222 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐶 − (𝐴 + 𝐵)) · 𝐶) = ((𝐶 · 𝐶) − ((𝐴 · 𝐶) + (𝐵 · 𝐶))))
5554fveq2d 5538 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘((𝐶 − (𝐴 + 𝐵)) · 𝐶)) = (abs‘((𝐶 · 𝐶) − ((𝐴 · 𝐶) + (𝐵 · 𝐶)))))
569, 21abssubd 11237 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘(𝐶 − (𝐴 + 𝐵))) = (abs‘((𝐴 + 𝐵) − 𝐶)))
572rpge0d 9732 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 0 ≤ 𝐶)
583, 57absidd 11211 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘𝐶) = 𝐶)
5956, 58oveq12d 5915 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((abs‘(𝐶 − (𝐴 + 𝐵))) · (abs‘𝐶)) = ((abs‘((𝐴 + 𝐵) − 𝐶)) · 𝐶))
6050, 55, 593eqtr3d 2230 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘((𝐶 · 𝐶) − ((𝐴 · 𝐶) + (𝐵 · 𝐶)))) = ((abs‘((𝐴 + 𝐵) − 𝐶)) · 𝐶))
6148, 60oveq12d 5915 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((abs‘(𝐴 · 𝐵)) + (abs‘((𝐶 · 𝐶) − ((𝐴 · 𝐶) + (𝐵 · 𝐶))))) = ((𝐴 · 𝐵) + ((abs‘((𝐴 + 𝐵) − 𝐶)) · 𝐶)))
6244, 61breqtrd 4044 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘((𝐴𝐶) · (𝐵𝐶))) ≤ ((𝐴 · 𝐵) + ((abs‘((𝐴 + 𝐵) − 𝐶)) · 𝐶)))
6310, 14absmuld 11238 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘((𝐴𝐶) · (𝐵𝐶))) = ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))))
6423recnd 8017 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘((𝐴 + 𝐵) − 𝐶)) ∈ ℂ)
6564, 9mulcomd 8010 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((abs‘((𝐴 + 𝐵) − 𝐶)) · 𝐶) = (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))
6665oveq2d 5913 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴 · 𝐵) + ((abs‘((𝐴 + 𝐵) − 𝐶)) · 𝐶)) = ((𝐴 · 𝐵) + (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶)))))
6762, 63, 663brtr3d 4049 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))) ≤ ((𝐴 · 𝐵) + (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶)))))
6816, 30, 7, 32, 67lemul2ad 8928 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶)))) ≤ (2 · ((𝐴 · 𝐵) + (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))))
697recnd 8017 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 2 ∈ ℂ)
709, 64mulcld 8009 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))) ∈ ℂ)
7169, 34, 70adddid 8013 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (2 · ((𝐴 · 𝐵) + (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))) = ((2 · (𝐴 · 𝐵)) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))))
7268, 71breqtrd 4044 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶)))) ≤ ((2 · (𝐴 · 𝐵)) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))))
7317, 26, 5, 72leadd2dd 8548 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴𝐶)↑2) + (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))))) ≤ (((𝐴𝐶)↑2) + ((2 · (𝐴 · 𝐵)) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶)))))))
7418, 27, 29, 73leadd1dd 8547 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((𝐴𝐶)↑2) + (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))))) + ((𝐵𝐶)↑2)) ≤ ((((𝐴𝐶)↑2) + ((2 · (𝐴 · 𝐵)) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶)))))) + ((𝐵𝐶)↑2)))
755recnd 8017 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴𝐶)↑2) ∈ ℂ)
7626recnd 8017 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((2 · (𝐴 · 𝐵)) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))) ∈ ℂ)
7729recnd 8017 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐵𝐶)↑2) ∈ ℂ)
7875, 76, 77add32d 8156 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((𝐴𝐶)↑2) + ((2 · (𝐴 · 𝐵)) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶)))))) + ((𝐵𝐶)↑2)) = ((((𝐴𝐶)↑2) + ((𝐵𝐶)↑2)) + ((2 · (𝐴 · 𝐵)) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶)))))))
7974, 78breqtrd 4044 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((𝐴𝐶)↑2) + (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))))) + ((𝐵𝐶)↑2)) ≤ ((((𝐴𝐶)↑2) + ((𝐵𝐶)↑2)) + ((2 · (𝐴 · 𝐵)) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶)))))))
8075, 77addcld 8008 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴𝐶)↑2) + ((𝐵𝐶)↑2)) ∈ ℂ)
8169, 34mulcld 8009 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (2 · (𝐴 · 𝐵)) ∈ ℂ)
8269, 70mulcld 8009 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶)))) ∈ ℂ)
8380, 81, 82addassd 8011 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((((𝐴𝐶)↑2) + ((𝐵𝐶)↑2)) + (2 · (𝐴 · 𝐵))) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))) = ((((𝐴𝐶)↑2) + ((𝐵𝐶)↑2)) + ((2 · (𝐴 · 𝐵)) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶)))))))
8479, 83breqtrrd 4046 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((𝐴𝐶)↑2) + (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))))) + ((𝐵𝐶)↑2)) ≤ (((((𝐴𝐶)↑2) + ((𝐵𝐶)↑2)) + (2 · (𝐴 · 𝐵))) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))))
858sqcld 10686 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴↑2) ∈ ℂ)
8669, 36mulcld 8009 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (2 · (𝐴 · 𝐶)) ∈ ℂ)
8785, 86subcld 8299 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴↑2) − (2 · (𝐴 · 𝐶))) ∈ ℂ)
889sqcld 10686 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐶↑2) ∈ ℂ)
8987, 88addcld 8008 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) ∈ ℂ)
9089, 81addcld 8008 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (2 · (𝐴 · 𝐵))) ∈ ℂ)
9113sqcld 10686 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐵↑2) ∈ ℂ)
9269, 37mulcld 8009 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (2 · (𝐵 · 𝐶)) ∈ ℂ)
9391, 92subcld 8299 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐵↑2) − (2 · (𝐵 · 𝐶))) ∈ ℂ)
9490, 93addcld 8008 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (2 · (𝐴 · 𝐵))) + ((𝐵↑2) − (2 · (𝐵 · 𝐶)))) ∈ ℂ)
9593, 88addcld 8008 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐵↑2) − (2 · (𝐵 · 𝐶))) + (𝐶↑2)) ∈ ℂ)
9689, 95, 81add32d 8156 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (((𝐵↑2) − (2 · (𝐵 · 𝐶))) + (𝐶↑2))) + (2 · (𝐴 · 𝐵))) = (((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (2 · (𝐴 · 𝐵))) + (((𝐵↑2) − (2 · (𝐵 · 𝐶))) + (𝐶↑2))))
9790, 93, 88addassd 8011 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (2 · (𝐴 · 𝐵))) + ((𝐵↑2) − (2 · (𝐵 · 𝐶)))) + (𝐶↑2)) = (((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (2 · (𝐴 · 𝐵))) + (((𝐵↑2) − (2 · (𝐵 · 𝐶))) + (𝐶↑2))))
9896, 97eqtr4d 2225 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (((𝐵↑2) − (2 · (𝐵 · 𝐶))) + (𝐶↑2))) + (2 · (𝐴 · 𝐵))) = ((((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (2 · (𝐴 · 𝐵))) + ((𝐵↑2) − (2 · (𝐵 · 𝐶)))) + (𝐶↑2)))
9994, 88, 98comraddd 8145 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (((𝐵↑2) − (2 · (𝐵 · 𝐶))) + (𝐶↑2))) + (2 · (𝐴 · 𝐵))) = ((𝐶↑2) + (((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (2 · (𝐴 · 𝐵))) + ((𝐵↑2) − (2 · (𝐵 · 𝐶))))))
10081, 93addcld 8008 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((2 · (𝐴 · 𝐵)) + ((𝐵↑2) − (2 · (𝐵 · 𝐶)))) ∈ ℂ)
10187, 100addcld 8008 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + ((2 · (𝐴 · 𝐵)) + ((𝐵↑2) − (2 · (𝐵 · 𝐶))))) ∈ ℂ)
10289, 81, 93addassd 8011 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (2 · (𝐴 · 𝐵))) + ((𝐵↑2) − (2 · (𝐵 · 𝐶)))) = ((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + ((2 · (𝐴 · 𝐵)) + ((𝐵↑2) − (2 · (𝐵 · 𝐶))))))
10387, 88addcomd 8139 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) = ((𝐶↑2) + ((𝐴↑2) − (2 · (𝐴 · 𝐶)))))
104103oveq1d 5912 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + ((2 · (𝐴 · 𝐵)) + ((𝐵↑2) − (2 · (𝐵 · 𝐶))))) = (((𝐶↑2) + ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) + ((2 · (𝐴 · 𝐵)) + ((𝐵↑2) − (2 · (𝐵 · 𝐶))))))
105102, 104eqtrd 2222 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (2 · (𝐴 · 𝐵))) + ((𝐵↑2) − (2 · (𝐵 · 𝐶)))) = (((𝐶↑2) + ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) + ((2 · (𝐴 · 𝐵)) + ((𝐵↑2) − (2 · (𝐵 · 𝐶))))))
10688, 87, 100addassd 8011 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐶↑2) + ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) + ((2 · (𝐴 · 𝐵)) + ((𝐵↑2) − (2 · (𝐵 · 𝐶))))) = ((𝐶↑2) + (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + ((2 · (𝐴 · 𝐵)) + ((𝐵↑2) − (2 · (𝐵 · 𝐶)))))))
107105, 106eqtrd 2222 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (2 · (𝐴 · 𝐵))) + ((𝐵↑2) − (2 · (𝐵 · 𝐶)))) = ((𝐶↑2) + (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + ((2 · (𝐴 · 𝐵)) + ((𝐵↑2) − (2 · (𝐵 · 𝐶)))))))
10888, 101, 107comraddd 8145 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (2 · (𝐴 · 𝐵))) + ((𝐵↑2) − (2 · (𝐵 · 𝐶)))) = ((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + ((2 · (𝐴 · 𝐵)) + ((𝐵↑2) − (2 · (𝐵 · 𝐶))))) + (𝐶↑2)))
10985, 86, 93subadd23d 8321 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + ((𝐵↑2) − (2 · (𝐵 · 𝐶)))) = ((𝐴↑2) + (((𝐵↑2) − (2 · (𝐵 · 𝐶))) − (2 · (𝐴 · 𝐶)))))
11091, 92, 86subsub4d 8330 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐵↑2) − (2 · (𝐵 · 𝐶))) − (2 · (𝐴 · 𝐶))) = ((𝐵↑2) − ((2 · (𝐵 · 𝐶)) + (2 · (𝐴 · 𝐶)))))
11192, 86addcomd 8139 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((2 · (𝐵 · 𝐶)) + (2 · (𝐴 · 𝐶))) = ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶))))
112111oveq2d 5913 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐵↑2) − ((2 · (𝐵 · 𝐶)) + (2 · (𝐴 · 𝐶)))) = ((𝐵↑2) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))))
113110, 112eqtrd 2222 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐵↑2) − (2 · (𝐵 · 𝐶))) − (2 · (𝐴 · 𝐶))) = ((𝐵↑2) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))))
114113oveq2d 5913 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴↑2) + (((𝐵↑2) − (2 · (𝐵 · 𝐶))) − (2 · (𝐴 · 𝐶)))) = ((𝐴↑2) + ((𝐵↑2) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶))))))
115109, 114eqtrd 2222 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + ((𝐵↑2) − (2 · (𝐵 · 𝐶)))) = ((𝐴↑2) + ((𝐵↑2) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶))))))
116115oveq2d 5913 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((2 · (𝐴 · 𝐵)) + (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + ((𝐵↑2) − (2 · (𝐵 · 𝐶))))) = ((2 · (𝐴 · 𝐵)) + ((𝐴↑2) + ((𝐵↑2) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))))))
11787, 81, 93add12d 8155 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + ((2 · (𝐴 · 𝐵)) + ((𝐵↑2) − (2 · (𝐵 · 𝐶))))) = ((2 · (𝐴 · 𝐵)) + (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + ((𝐵↑2) − (2 · (𝐵 · 𝐶))))))
11886, 92addcld 8008 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶))) ∈ ℂ)
11991, 118subcld 8299 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐵↑2) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))) ∈ ℂ)
12085, 119addcld 8008 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴↑2) + ((𝐵↑2) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶))))) ∈ ℂ)
12185, 81addcld 8008 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴↑2) + (2 · (𝐴 · 𝐵))) ∈ ℂ)
122121, 91, 118addsubassd 8319 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + ((𝐵↑2) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶))))))
12385, 81, 119add32d 8156 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + ((𝐵↑2) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶))))) = (((𝐴↑2) + ((𝐵↑2) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶))))) + (2 · (𝐴 · 𝐵))))
124122, 123eqtrd 2222 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))) = (((𝐴↑2) + ((𝐵↑2) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶))))) + (2 · (𝐴 · 𝐵))))
125120, 81, 124comraddd 8145 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))) = ((2 · (𝐴 · 𝐵)) + ((𝐴↑2) + ((𝐵↑2) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))))))
126116, 117, 1253eqtr4d 2232 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + ((2 · (𝐴 · 𝐵)) + ((𝐵↑2) − (2 · (𝐵 · 𝐶))))) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))))
127126oveq1d 5912 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + ((2 · (𝐴 · 𝐵)) + ((𝐵↑2) − (2 · (𝐵 · 𝐶))))) + (𝐶↑2)) = (((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))) + (𝐶↑2)))
128108, 127eqtrd 2222 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (2 · (𝐴 · 𝐵))) + ((𝐵↑2) − (2 · (𝐵 · 𝐶)))) = (((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))) + (𝐶↑2)))
129128oveq2d 5913 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐶↑2) + (((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (2 · (𝐴 · 𝐵))) + ((𝐵↑2) − (2 · (𝐵 · 𝐶))))) = ((𝐶↑2) + (((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))) + (𝐶↑2))))
13099, 129eqtrd 2222 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (((𝐵↑2) − (2 · (𝐵 · 𝐶))) + (𝐶↑2))) + (2 · (𝐴 · 𝐵))) = ((𝐶↑2) + (((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))) + (𝐶↑2))))
131 binom2sub 10668 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴𝐶)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)))
1328, 9, 131syl2anc 411 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴𝐶)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)))
133 binom2sub 10668 . . . . . . . . . . 11 ((𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐵𝐶)↑2) = (((𝐵↑2) − (2 · (𝐵 · 𝐶))) + (𝐶↑2)))
13413, 9, 133syl2anc 411 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐵𝐶)↑2) = (((𝐵↑2) − (2 · (𝐵 · 𝐶))) + (𝐶↑2)))
135132, 134oveq12d 5915 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴𝐶)↑2) + ((𝐵𝐶)↑2)) = ((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (((𝐵↑2) − (2 · (𝐵 · 𝐶))) + (𝐶↑2))))
136135oveq1d 5912 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((𝐴𝐶)↑2) + ((𝐵𝐶)↑2)) + (2 · (𝐴 · 𝐵))) = (((((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)) + (((𝐵↑2) − (2 · (𝐵 · 𝐶))) + (𝐶↑2))) + (2 · (𝐴 · 𝐵))))
137 binom2sub 10668 . . . . . . . . . . 11 (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐶)↑2) = ((((𝐴 + 𝐵)↑2) − (2 · ((𝐴 + 𝐵) · 𝐶))) + (𝐶↑2)))
13821, 9, 137syl2anc 411 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴 + 𝐵) − 𝐶)↑2) = ((((𝐴 + 𝐵)↑2) − (2 · ((𝐴 + 𝐵) · 𝐶))) + (𝐶↑2)))
139 binom2 10666 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)))
1408, 13, 139syl2anc 411 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)))
14152oveq2d 5913 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (2 · ((𝐴 + 𝐵) · 𝐶)) = (2 · ((𝐴 · 𝐶) + (𝐵 · 𝐶))))
14269, 36, 37adddid 8013 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (2 · ((𝐴 · 𝐶) + (𝐵 · 𝐶))) = ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶))))
143141, 142eqtrd 2222 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (2 · ((𝐴 + 𝐵) · 𝐶)) = ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶))))
144140, 143oveq12d 5915 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴 + 𝐵)↑2) − (2 · ((𝐴 + 𝐵) · 𝐶))) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))))
145144oveq1d 5912 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((𝐴 + 𝐵)↑2) − (2 · ((𝐴 + 𝐵) · 𝐶))) + (𝐶↑2)) = (((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))) + (𝐶↑2)))
146138, 145eqtrd 2222 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴 + 𝐵) − 𝐶)↑2) = (((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))) + (𝐶↑2)))
147146oveq2d 5913 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐶↑2) + (((𝐴 + 𝐵) − 𝐶)↑2)) = ((𝐶↑2) + (((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) − ((2 · (𝐴 · 𝐶)) + (2 · (𝐵 · 𝐶)))) + (𝐶↑2))))
148130, 136, 1473eqtr4d 2232 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((𝐴𝐶)↑2) + ((𝐵𝐶)↑2)) + (2 · (𝐴 · 𝐵))) = ((𝐶↑2) + (((𝐴 + 𝐵) − 𝐶)↑2)))
149148oveq1d 5912 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((((𝐴𝐶)↑2) + ((𝐵𝐶)↑2)) + (2 · (𝐴 · 𝐵))) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))) = (((𝐶↑2) + (((𝐴 + 𝐵) − 𝐶)↑2)) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))))
15084, 149breqtrd 4044 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((𝐴𝐶)↑2) + (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))))) + ((𝐵𝐶)↑2)) ≤ (((𝐶↑2) + (((𝐴 + 𝐵) − 𝐶)↑2)) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))))
15122sqcld 10686 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐴 + 𝐵) − 𝐶)↑2) ∈ ℂ)
15288, 151, 82add32d 8156 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐶↑2) + (((𝐴 + 𝐵) − 𝐶)↑2)) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))) = (((𝐶↑2) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))) + (((𝐴 + 𝐵) − 𝐶)↑2)))
153150, 152breqtrd 4044 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((𝐴𝐶)↑2) + (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))))) + ((𝐵𝐶)↑2)) ≤ (((𝐶↑2) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))) + (((𝐴 + 𝐵) − 𝐶)↑2)))
154 absresq 11122 . . . . . . 7 ((𝐴𝐶) ∈ ℝ → ((abs‘(𝐴𝐶))↑2) = ((𝐴𝐶)↑2))
1554, 154syl 14 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((abs‘(𝐴𝐶))↑2) = ((𝐴𝐶)↑2))
156155oveq1d 5912 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((abs‘(𝐴𝐶))↑2) + (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))))) = (((𝐴𝐶)↑2) + (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))))))
157 absresq 11122 . . . . . 6 ((𝐵𝐶) ∈ ℝ → ((abs‘(𝐵𝐶))↑2) = ((𝐵𝐶)↑2))
15828, 157syl 14 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((abs‘(𝐵𝐶))↑2) = ((𝐵𝐶)↑2))
159156, 158oveq12d 5915 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((abs‘(𝐴𝐶))↑2) + (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))))) + ((abs‘(𝐵𝐶))↑2)) = ((((𝐴𝐶)↑2) + (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))))) + ((𝐵𝐶)↑2)))
1601, 12readdcld 8018 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 + 𝐵) ∈ ℝ)
161160, 3resubcld 8369 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐴 + 𝐵) − 𝐶) ∈ ℝ)
162 absresq 11122 . . . . . 6 (((𝐴 + 𝐵) − 𝐶) ∈ ℝ → ((abs‘((𝐴 + 𝐵) − 𝐶))↑2) = (((𝐴 + 𝐵) − 𝐶)↑2))
163161, 162syl 14 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((abs‘((𝐴 + 𝐵) − 𝐶))↑2) = (((𝐴 + 𝐵) − 𝐶)↑2))
164163oveq2d 5913 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((𝐶↑2) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))) + ((abs‘((𝐴 + 𝐵) − 𝐶))↑2)) = (((𝐶↑2) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))) + (((𝐴 + 𝐵) − 𝐶)↑2)))
165153, 159, 1643brtr4d 4050 . . 3 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((((abs‘(𝐴𝐶))↑2) + (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))))) + ((abs‘(𝐵𝐶))↑2)) ≤ (((𝐶↑2) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))) + ((abs‘((𝐴 + 𝐵) − 𝐶))↑2)))
16611recnd 8017 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘(𝐴𝐶)) ∈ ℂ)
16715recnd 8017 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (abs‘(𝐵𝐶)) ∈ ℂ)
168 binom2 10666 . . . 4 (((abs‘(𝐴𝐶)) ∈ ℂ ∧ (abs‘(𝐵𝐶)) ∈ ℂ) → (((abs‘(𝐴𝐶)) + (abs‘(𝐵𝐶)))↑2) = ((((abs‘(𝐴𝐶))↑2) + (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))))) + ((abs‘(𝐵𝐶))↑2)))
169166, 167, 168syl2anc 411 . . 3 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((abs‘(𝐴𝐶)) + (abs‘(𝐵𝐶)))↑2) = ((((abs‘(𝐴𝐶))↑2) + (2 · ((abs‘(𝐴𝐶)) · (abs‘(𝐵𝐶))))) + ((abs‘(𝐵𝐶))↑2)))
170 binom2 10666 . . . 4 ((𝐶 ∈ ℂ ∧ (abs‘((𝐴 + 𝐵) − 𝐶)) ∈ ℂ) → ((𝐶 + (abs‘((𝐴 + 𝐵) − 𝐶)))↑2) = (((𝐶↑2) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))) + ((abs‘((𝐴 + 𝐵) − 𝐶))↑2)))
1719, 64, 170syl2anc 411 . . 3 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((𝐶 + (abs‘((𝐴 + 𝐵) − 𝐶)))↑2) = (((𝐶↑2) + (2 · (𝐶 · (abs‘((𝐴 + 𝐵) − 𝐶))))) + ((abs‘((𝐴 + 𝐵) − 𝐶))↑2)))
172165, 169, 1713brtr4d 4050 . 2 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((abs‘(𝐴𝐶)) + (abs‘(𝐵𝐶)))↑2) ≤ ((𝐶 + (abs‘((𝐴 + 𝐵) − 𝐶)))↑2))
17311, 15readdcld 8018 . . 3 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((abs‘(𝐴𝐶)) + (abs‘(𝐵𝐶))) ∈ ℝ)
1743, 23readdcld 8018 . . 3 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐶 + (abs‘((𝐴 + 𝐵) − 𝐶))) ∈ ℝ)
17510absge0d 11228 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 0 ≤ (abs‘(𝐴𝐶)))
17614absge0d 11228 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 0 ≤ (abs‘(𝐵𝐶)))
17711, 15, 175, 176addge0d 8510 . . 3 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 0 ≤ ((abs‘(𝐴𝐶)) + (abs‘(𝐵𝐶))))
17822absge0d 11228 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 0 ≤ (abs‘((𝐴 + 𝐵) − 𝐶)))
1793, 23, 57, 178addge0d 8510 . . 3 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → 0 ≤ (𝐶 + (abs‘((𝐴 + 𝐵) − 𝐶))))
180173, 174, 177, 179le2sqd 10720 . 2 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (((abs‘(𝐴𝐶)) + (abs‘(𝐵𝐶))) ≤ (𝐶 + (abs‘((𝐴 + 𝐵) − 𝐶))) ↔ (((abs‘(𝐴𝐶)) + (abs‘(𝐵𝐶)))↑2) ≤ ((𝐶 + (abs‘((𝐴 + 𝐵) − 𝐶)))↑2)))
181172, 180mpbird 167 1 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → ((abs‘(𝐴𝐶)) + (abs‘(𝐵𝐶))) ≤ (𝐶 + (abs‘((𝐴 + 𝐵) − 𝐶))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 980   = wceq 1364  wcel 2160   class class class wbr 4018  cfv 5235  (class class class)co 5897  cc 7840  cr 7841  0cc0 7842   + caddc 7845   · cmul 7847  cle 8024  cmin 8159  2c2 9001  +crp 9685  cexp 10553  abscabs 11041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-setind 4554  ax-iinf 4605  ax-cnex 7933  ax-resscn 7934  ax-1cn 7935  ax-1re 7936  ax-icn 7937  ax-addcl 7938  ax-addrcl 7939  ax-mulcl 7940  ax-mulrcl 7941  ax-addcom 7942  ax-mulcom 7943  ax-addass 7944  ax-mulass 7945  ax-distr 7946  ax-i2m1 7947  ax-0lt1 7948  ax-1rid 7949  ax-0id 7950  ax-rnegex 7951  ax-precex 7952  ax-cnre 7953  ax-pre-ltirr 7954  ax-pre-ltwlin 7955  ax-pre-lttrn 7956  ax-pre-apti 7957  ax-pre-ltadd 7958  ax-pre-mulgt0 7959  ax-pre-mulext 7960  ax-arch 7961  ax-caucvg 7962
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-if 3550  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4311  df-po 4314  df-iso 4315  df-iord 4384  df-on 4386  df-ilim 4387  df-suc 4389  df-iom 4608  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-f1 5240  df-fo 5241  df-f1o 5242  df-fv 5243  df-riota 5852  df-ov 5900  df-oprab 5901  df-mpo 5902  df-1st 6166  df-2nd 6167  df-recs 6331  df-frec 6417  df-pnf 8025  df-mnf 8026  df-xr 8027  df-ltxr 8028  df-le 8029  df-sub 8161  df-neg 8162  df-reap 8563  df-ap 8570  df-div 8661  df-inn 8951  df-2 9009  df-3 9010  df-4 9011  df-n0 9208  df-z 9285  df-uz 9560  df-rp 9686  df-seqfrec 10479  df-exp 10554  df-cj 10886  df-re 10887  df-im 10888  df-rsqrt 11042  df-abs 11043
This theorem is referenced by:  bdtri  11283
  Copyright terms: Public domain W3C validator