Metamath Proof Explorer

Theorem itsclc0yqsollem2

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

Ref Expression
Hypotheses itscnhlc0yqe.q ⊢ Q = A 2 + B 2
itscnhlc0yqe.t ⊢ T = − 2 ⁢ B ⁢ C
itscnhlc0yqe.u ⊢ U = C 2 − A 2 ⁢ R 2
itsclc0yqsollem1.d ⊢ D = R 2 ⁢ Q − C 2
Assertion itsclc0yqsollem2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ R ∈ ℝ ∧ 0 ≤ D → T 2 − 4 ⁢ Q ⁢ U = 2 ⁢ A ⁢ D

Proof

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