Metamath Proof Explorer

Theorem itsclc0yqsollem2

Description: Lemma 2 for itsclc0yqsol . (Contributed by AV, 6-Feb-2023)

Ref Expression
Hypotheses itscnhlc0yqe.q ⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
itscnhlc0yqe.t ⊢ 𝑇 = - ( 2 · ( 𝐵 · 𝐶 ) )
itscnhlc0yqe.u ⊢ 𝑈 = ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) )
itsclc0yqsollem1.d ⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
Assertion itsclc0yqsollem2 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( √ ‘ ( ( 𝑇 ↑ 2 ) − ( 4 · ( 𝑄 · 𝑈 ) ) ) ) = ( ( 2 · ( abs ‘ 𝐴 ) ) · ( √ ‘ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 itscnhlc0yqe.q ⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
2 itscnhlc0yqe.t ⊢ 𝑇 = - ( 2 · ( 𝐵 · 𝐶 ) )
3 itscnhlc0yqe.u ⊢ 𝑈 = ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) )
4 itsclc0yqsollem1.d ⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
5 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
6 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
7 recn ⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
8 5 6 7 3anim123i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
9 recn ⊢ ( 𝑅 ∈ ℝ → 𝑅 ∈ ℂ )
10 8 9 anim12i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ) → ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) )
11 10 3adant3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) )
12 1 2 3 4 itsclc0yqsollem1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝑇 ↑ 2 ) − ( 4 · ( 𝑄 · 𝑈 ) ) ) = ( ( 4 · ( 𝐴 ↑ 2 ) ) · 𝐷 ) )
13 11 12 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( ( 𝑇 ↑ 2 ) − ( 4 · ( 𝑄 · 𝑈 ) ) ) = ( ( 4 · ( 𝐴 ↑ 2 ) ) · 𝐷 ) )
14 13 fveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( √ ‘ ( ( 𝑇 ↑ 2 ) − ( 4 · ( 𝑄 · 𝑈 ) ) ) ) = ( √ ‘ ( ( 4 · ( 𝐴 ↑ 2 ) ) · 𝐷 ) ) )
15 4re ⊢ 4 ∈ ℝ
16 15 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → 4 ∈ ℝ )
17 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
18 17 resqcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
19 18 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
20 16 19 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( 4 · ( 𝐴 ↑ 2 ) ) ∈ ℝ )
21 0re ⊢ 0 ∈ ℝ
22 4pos ⊢ 0 < 4
23 21 15 22 ltleii ⊢ 0 ≤ 4
24 23 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → 0 ≤ 4 )
25 17 sqge0d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 0 ≤ ( 𝐴 ↑ 2 ) )
26 25 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → 0 ≤ ( 𝐴 ↑ 2 ) )
27 16 19 24 26 mulge0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → 0 ≤ ( 4 · ( 𝐴 ↑ 2 ) ) )
28 simp2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → 𝑅 ∈ ℝ )
29 28 resqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
30 1 resum2sqcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑄 ∈ ℝ )
31 30 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝑄 ∈ ℝ )
32 31 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → 𝑄 ∈ ℝ )
33 29 32 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( ( 𝑅 ↑ 2 ) · 𝑄 ) ∈ ℝ )
34 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
35 34 resqcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ↑ 2 ) ∈ ℝ )
36 35 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( 𝐶 ↑ 2 ) ∈ ℝ )
37 33 36 resubcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) ) ∈ ℝ )
38 4 37 eqeltrid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → 𝐷 ∈ ℝ )
39 simp3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → 0 ≤ 𝐷 )
40 20 27 38 39 sqrtmuld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( √ ‘ ( ( 4 · ( 𝐴 ↑ 2 ) ) · 𝐷 ) ) = ( ( √ ‘ ( 4 · ( 𝐴 ↑ 2 ) ) ) · ( √ ‘ 𝐷 ) ) )
41 15 23 pm3.2i ⊢ ( 4 ∈ ℝ ∧ 0 ≤ 4 )
42 41 a1i ⊢ ( 𝐴 ∈ ℝ → ( 4 ∈ ℝ ∧ 0 ≤ 4 ) )
43 resqcl ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ↑ 2 ) ∈ ℝ )
44 sqge0 ⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 ↑ 2 ) )
45 sqrtmul ⊢ ( ( ( 4 ∈ ℝ ∧ 0 ≤ 4 ) ∧ ( ( 𝐴 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 ↑ 2 ) ) ) → ( √ ‘ ( 4 · ( 𝐴 ↑ 2 ) ) ) = ( ( √ ‘ 4 ) · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) )
46 42 43 44 45 syl12anc ⊢ ( 𝐴 ∈ ℝ → ( √ ‘ ( 4 · ( 𝐴 ↑ 2 ) ) ) = ( ( √ ‘ 4 ) · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) )
47 46 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( √ ‘ ( 4 · ( 𝐴 ↑ 2 ) ) ) = ( ( √ ‘ 4 ) · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) )
48 47 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( √ ‘ ( 4 · ( 𝐴 ↑ 2 ) ) ) = ( ( √ ‘ 4 ) · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) )
49 sqrt4 ⊢ ( √ ‘ 4 ) = 2
50 49 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( √ ‘ 4 ) = 2 )
51 absre ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 ↑ 2 ) ) )
52 51 eqcomd ⊢ ( 𝐴 ∈ ℝ → ( √ ‘ ( 𝐴 ↑ 2 ) ) = ( abs ‘ 𝐴 ) )
53 52 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( √ ‘ ( 𝐴 ↑ 2 ) ) = ( abs ‘ 𝐴 ) )
54 53 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( √ ‘ ( 𝐴 ↑ 2 ) ) = ( abs ‘ 𝐴 ) )
55 50 54 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 4 ) · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) = ( 2 · ( abs ‘ 𝐴 ) ) )
56 48 55 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( √ ‘ ( 4 · ( 𝐴 ↑ 2 ) ) ) = ( 2 · ( abs ‘ 𝐴 ) ) )
57 56 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ ( 4 · ( 𝐴 ↑ 2 ) ) ) · ( √ ‘ 𝐷 ) ) = ( ( 2 · ( abs ‘ 𝐴 ) ) · ( √ ‘ 𝐷 ) ) )
58 14 40 57 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( √ ‘ ( ( 𝑇 ↑ 2 ) − ( 4 · ( 𝑄 · 𝑈 ) ) ) ) = ( ( 2 · ( abs ‘ 𝐴 ) ) · ( √ ‘ 𝐷 ) ) )