Step |
Hyp |
Ref |
Expression |
1 |
|
remulcl |
⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( 𝑆 · 𝑈 ) ∈ ℝ ) |
2 |
1
|
3adant2 |
⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( 𝑆 · 𝑈 ) ∈ ℝ ) |
3 |
2
|
adantr |
⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ) → ( 𝑆 · 𝑈 ) ∈ ℝ ) |
4 |
|
simpl2 |
⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ) → 𝑇 ∈ ℝ ) |
5 |
|
resqrtcl |
⊢ ( ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) → ( √ ‘ 𝑉 ) ∈ ℝ ) |
6 |
5
|
adantl |
⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ) → ( √ ‘ 𝑉 ) ∈ ℝ ) |
7 |
4 6
|
remulcld |
⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ) → ( 𝑇 · ( √ ‘ 𝑉 ) ) ∈ ℝ ) |
8 |
3 7
|
readdcld |
⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ) → ( ( 𝑆 · 𝑈 ) + ( 𝑇 · ( √ ‘ 𝑉 ) ) ) ∈ ℝ ) |
9 |
8
|
3adant3 |
⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ∧ ( 𝑊 ∈ ℝ ∧ 𝑊 ≠ 0 ) ) → ( ( 𝑆 · 𝑈 ) + ( 𝑇 · ( √ ‘ 𝑉 ) ) ) ∈ ℝ ) |
10 |
|
simp3l |
⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ∧ ( 𝑊 ∈ ℝ ∧ 𝑊 ≠ 0 ) ) → 𝑊 ∈ ℝ ) |
11 |
|
simp3r |
⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ∧ ( 𝑊 ∈ ℝ ∧ 𝑊 ≠ 0 ) ) → 𝑊 ≠ 0 ) |
12 |
9 10 11
|
redivcld |
⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ∧ ( 𝑊 ∈ ℝ ∧ 𝑊 ≠ 0 ) ) → ( ( ( 𝑆 · 𝑈 ) + ( 𝑇 · ( √ ‘ 𝑉 ) ) ) / 𝑊 ) ∈ ℝ ) |