Theorem quart1cl

Description: Closure lemmas for quart . (Contributed by Mario Carneiro, 7-May-2015)

	Ref	Expression
Hypotheses	quart1.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	quart1.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	quart1.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	quart1.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
	quart1.p	⊢ ( 𝜑 → 𝑃 = ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) )
	quart1.q	⊢ ( 𝜑 → 𝑄 = ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) )
	quart1.r	⊢ ( 𝜑 → 𝑅 = ( ( 𝐷 − ( ( 𝐶 · 𝐴 ) / 4 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) )
Assertion	quart1cl	⊢ ( 𝜑 → ( 𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		quart1.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		quart1.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		quart1.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		quart1.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
5		quart1.p	⊢ ( 𝜑 → 𝑃 = ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) )
6		quart1.q	⊢ ( 𝜑 → 𝑄 = ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) )
7		quart1.r	⊢ ( 𝜑 → 𝑅 = ( ( 𝐷 − ( ( 𝐶 · 𝐴 ) / 4 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) )
8		3cn	⊢ 3 ∈ ℂ
9		8cn	⊢ 8 ∈ ℂ
10		8nn	⊢ 8 ∈ ℕ
11	10	nnne0i	⊢ 8 ≠ 0
12	8 9 11	divcli	⊢ ( 3 / 8 ) ∈ ℂ
13	1	sqcld	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
14		mulcl	⊢ ( ( ( 3 / 8 ) ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ∈ ℂ )
15	12 13 14	sylancr	⊢ ( 𝜑 → ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ∈ ℂ )
16	2 15	subcld	⊢ ( 𝜑 → ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
17	5 16	eqeltrd	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
18	1 2	mulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℂ )
19	18	halfcld	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) / 2 ) ∈ ℂ )
20	3 19	subcld	⊢ ( 𝜑 → ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) ∈ ℂ )
21		3nn0	⊢ 3 ∈ ℕ0
22		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝐴 ↑ 3 ) ∈ ℂ )
23	1 21 22	sylancl	⊢ ( 𝜑 → ( 𝐴 ↑ 3 ) ∈ ℂ )
24	9	a1i	⊢ ( 𝜑 → 8 ∈ ℂ )
25	11	a1i	⊢ ( 𝜑 → 8 ≠ 0 )
26	23 24 25	divcld	⊢ ( 𝜑 → ( ( 𝐴 ↑ 3 ) / 8 ) ∈ ℂ )
27	20 26	addcld	⊢ ( 𝜑 → ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) ∈ ℂ )
28	6 27	eqeltrd	⊢ ( 𝜑 → 𝑄 ∈ ℂ )
29	3 1	mulcld	⊢ ( 𝜑 → ( 𝐶 · 𝐴 ) ∈ ℂ )
30		4cn	⊢ 4 ∈ ℂ
31	30	a1i	⊢ ( 𝜑 → 4 ∈ ℂ )
32		4ne0	⊢ 4 ≠ 0
33	32	a1i	⊢ ( 𝜑 → 4 ≠ 0 )
34	29 31 33	divcld	⊢ ( 𝜑 → ( ( 𝐶 · 𝐴 ) / 4 ) ∈ ℂ )
35	4 34	subcld	⊢ ( 𝜑 → ( 𝐷 − ( ( 𝐶 · 𝐴 ) / 4 ) ) ∈ ℂ )
36	13 2	mulcld	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · 𝐵 ) ∈ ℂ )
37		1nn0	⊢ 1 ∈ ℕ0
38		6nn	⊢ 6 ∈ ℕ
39	37 38	decnncl	⊢ ; 1 6 ∈ ℕ
40	39	nncni	⊢ ; 1 6 ∈ ℂ
41	40	a1i	⊢ ( 𝜑 → ; 1 6 ∈ ℂ )
42	39	nnne0i	⊢ ; 1 6 ≠ 0
43	42	a1i	⊢ ( 𝜑 → ; 1 6 ≠ 0 )
44	36 41 43	divcld	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ∈ ℂ )
45		25nn0	⊢ ; 2 5 ∈ ℕ0
46	45 38	decnncl	⊢ ; ; 2 5 6 ∈ ℕ
47	46	nncni	⊢ ; ; 2 5 6 ∈ ℂ
48	46	nnne0i	⊢ ; ; 2 5 6 ≠ 0
49	8 47 48	divcli	⊢ ( 3 / ; ; 2 5 6 ) ∈ ℂ
50		4nn0	⊢ 4 ∈ ℕ0
51		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 4 ∈ ℕ0 ) → ( 𝐴 ↑ 4 ) ∈ ℂ )
52	1 50 51	sylancl	⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) ∈ ℂ )
53		mulcl	⊢ ( ( ( 3 / ; ; 2 5 6 ) ∈ ℂ ∧ ( 𝐴 ↑ 4 ) ∈ ℂ ) → ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ∈ ℂ )
54	49 52 53	sylancr	⊢ ( 𝜑 → ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ∈ ℂ )
55	44 54	subcld	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ∈ ℂ )
56	35 55	addcld	⊢ ( 𝜑 → ( ( 𝐷 − ( ( 𝐶 · 𝐴 ) / 4 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) ∈ ℂ )
57	7 56	eqeltrd	⊢ ( 𝜑 → 𝑅 ∈ ℂ )
58	17 28 57	3jca	⊢ ( 𝜑 → ( 𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) )