Proof of Theorem quart1cl
Step | Hyp | Ref
| Expression |
1 | | quart1.p |
. . 3
⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2)))) |
2 | | quart1.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℂ) |
3 | | 3cn 11911 |
. . . . . 6
⊢ 3 ∈
ℂ |
4 | | 8cn 11927 |
. . . . . 6
⊢ 8 ∈
ℂ |
5 | | 8nn 11925 |
. . . . . . 7
⊢ 8 ∈
ℕ |
6 | 5 | nnne0i 11870 |
. . . . . 6
⊢ 8 ≠
0 |
7 | 3, 4, 6 | divcli 11574 |
. . . . 5
⊢ (3 / 8)
∈ ℂ |
8 | | quart1.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
9 | 8 | sqcld 13714 |
. . . . 5
⊢ (𝜑 → (𝐴↑2) ∈ ℂ) |
10 | | mulcl 10813 |
. . . . 5
⊢ (((3 / 8)
∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((3 / 8)
· (𝐴↑2)) ∈
ℂ) |
11 | 7, 9, 10 | sylancr 590 |
. . . 4
⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) ∈
ℂ) |
12 | 2, 11 | subcld 11189 |
. . 3
⊢ (𝜑 → (𝐵 − ((3 / 8) · (𝐴↑2))) ∈
ℂ) |
13 | 1, 12 | eqeltrd 2838 |
. 2
⊢ (𝜑 → 𝑃 ∈ ℂ) |
14 | | quart1.q |
. . 3
⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))) |
15 | | quart1.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℂ) |
16 | 8, 2 | mulcld 10853 |
. . . . . 6
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) |
17 | 16 | halfcld 12075 |
. . . . 5
⊢ (𝜑 → ((𝐴 · 𝐵) / 2) ∈ ℂ) |
18 | 15, 17 | subcld 11189 |
. . . 4
⊢ (𝜑 → (𝐶 − ((𝐴 · 𝐵) / 2)) ∈ ℂ) |
19 | | 3nn0 12108 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
20 | | expcl 13653 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 3 ∈
ℕ0) → (𝐴↑3) ∈ ℂ) |
21 | 8, 19, 20 | sylancl 589 |
. . . . 5
⊢ (𝜑 → (𝐴↑3) ∈ ℂ) |
22 | 4 | a1i 11 |
. . . . 5
⊢ (𝜑 → 8 ∈
ℂ) |
23 | 6 | a1i 11 |
. . . . 5
⊢ (𝜑 → 8 ≠ 0) |
24 | 21, 22, 23 | divcld 11608 |
. . . 4
⊢ (𝜑 → ((𝐴↑3) / 8) ∈
ℂ) |
25 | 18, 24 | addcld 10852 |
. . 3
⊢ (𝜑 → ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) ∈
ℂ) |
26 | 14, 25 | eqeltrd 2838 |
. 2
⊢ (𝜑 → 𝑄 ∈ ℂ) |
27 | | quart1.r |
. . 3
⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4))))) |
28 | | quart1.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ ℂ) |
29 | 15, 8 | mulcld 10853 |
. . . . . 6
⊢ (𝜑 → (𝐶 · 𝐴) ∈ ℂ) |
30 | | 4cn 11915 |
. . . . . . 7
⊢ 4 ∈
ℂ |
31 | 30 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 4 ∈
ℂ) |
32 | | 4ne0 11938 |
. . . . . . 7
⊢ 4 ≠
0 |
33 | 32 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 4 ≠ 0) |
34 | 29, 31, 33 | divcld 11608 |
. . . . 5
⊢ (𝜑 → ((𝐶 · 𝐴) / 4) ∈ ℂ) |
35 | 28, 34 | subcld 11189 |
. . . 4
⊢ (𝜑 → (𝐷 − ((𝐶 · 𝐴) / 4)) ∈ ℂ) |
36 | 9, 2 | mulcld 10853 |
. . . . . 6
⊢ (𝜑 → ((𝐴↑2) · 𝐵) ∈ ℂ) |
37 | | 1nn0 12106 |
. . . . . . . . 9
⊢ 1 ∈
ℕ0 |
38 | | 6nn 11919 |
. . . . . . . . 9
⊢ 6 ∈
ℕ |
39 | 37, 38 | decnncl 12313 |
. . . . . . . 8
⊢ ;16 ∈ ℕ |
40 | 39 | nncni 11840 |
. . . . . . 7
⊢ ;16 ∈ ℂ |
41 | 40 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ;16 ∈ ℂ) |
42 | 39 | nnne0i 11870 |
. . . . . . 7
⊢ ;16 ≠ 0 |
43 | 42 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ;16 ≠ 0) |
44 | 36, 41, 43 | divcld 11608 |
. . . . 5
⊢ (𝜑 → (((𝐴↑2) · 𝐵) / ;16) ∈ ℂ) |
45 | | 2nn0 12107 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
46 | | 5nn0 12110 |
. . . . . . . . . 10
⊢ 5 ∈
ℕ0 |
47 | 45, 46 | deccl 12308 |
. . . . . . . . 9
⊢ ;25 ∈
ℕ0 |
48 | 47, 38 | decnncl 12313 |
. . . . . . . 8
⊢ ;;256 ∈ ℕ |
49 | 48 | nncni 11840 |
. . . . . . 7
⊢ ;;256 ∈ ℂ |
50 | 48 | nnne0i 11870 |
. . . . . . 7
⊢ ;;256 ≠ 0 |
51 | 3, 49, 50 | divcli 11574 |
. . . . . 6
⊢ (3 /
;;256) ∈ ℂ |
52 | | 4nn0 12109 |
. . . . . . 7
⊢ 4 ∈
ℕ0 |
53 | | expcl 13653 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 4 ∈
ℕ0) → (𝐴↑4) ∈ ℂ) |
54 | 8, 52, 53 | sylancl 589 |
. . . . . 6
⊢ (𝜑 → (𝐴↑4) ∈ ℂ) |
55 | | mulcl 10813 |
. . . . . 6
⊢ (((3 /
;;256) ∈ ℂ ∧ (𝐴↑4) ∈ ℂ) → ((3 / ;;256) · (𝐴↑4)) ∈ ℂ) |
56 | 51, 54, 55 | sylancr 590 |
. . . . 5
⊢ (𝜑 → ((3 / ;;256)
· (𝐴↑4)) ∈
ℂ) |
57 | 44, 56 | subcld 11189 |
. . . 4
⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4)))
∈ ℂ) |
58 | 35, 57 | addcld 10852 |
. . 3
⊢ (𝜑 → ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4))))
∈ ℂ) |
59 | 27, 58 | eqeltrd 2838 |
. 2
⊢ (𝜑 → 𝑅 ∈ ℂ) |
60 | 13, 26, 59 | 3jca 1130 |
1
⊢ (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ)) |