Theorem quartlem2

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

	Ref	Expression
Hypotheses	quart.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	quart.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	quart.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	quart.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
	quart.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	quart.e	⊢ ( 𝜑 → 𝐸 = - ( 𝐴 / 4 ) )
	quart.p	⊢ ( 𝜑 → 𝑃 = ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) )
	quart.q	⊢ ( 𝜑 → 𝑄 = ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) )
	quart.r	⊢ ( 𝜑 → 𝑅 = ( ( 𝐷 − ( ( 𝐶 · 𝐴 ) / 4 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) )
	quart.u	⊢ ( 𝜑 → 𝑈 = ( ( 𝑃 ↑ 2 ) + ( ; 1 2 · 𝑅 ) ) )
	quart.v	⊢ ( 𝜑 → 𝑉 = ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) − ( ; 2 7 · ( 𝑄 ↑ 2 ) ) ) + ( ; 7 2 · ( 𝑃 · 𝑅 ) ) ) )
	quart.w	⊢ ( 𝜑 → 𝑊 = ( √ ‘ ( ( 𝑉 ↑ 2 ) − ( 4 · ( 𝑈 ↑ 3 ) ) ) ) )
Assertion	quartlem2	⊢ ( 𝜑 → ( 𝑈 ∈ ℂ ∧ 𝑉 ∈ ℂ ∧ 𝑊 ∈ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		quart.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		quart.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		quart.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		quart.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
5		quart.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
6		quart.e	⊢ ( 𝜑 → 𝐸 = - ( 𝐴 / 4 ) )
7		quart.p	⊢ ( 𝜑 → 𝑃 = ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) )
8		quart.q	⊢ ( 𝜑 → 𝑄 = ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) )
9		quart.r	⊢ ( 𝜑 → 𝑅 = ( ( 𝐷 − ( ( 𝐶 · 𝐴 ) / 4 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) )
10		quart.u	⊢ ( 𝜑 → 𝑈 = ( ( 𝑃 ↑ 2 ) + ( ; 1 2 · 𝑅 ) ) )
11		quart.v	⊢ ( 𝜑 → 𝑉 = ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) − ( ; 2 7 · ( 𝑄 ↑ 2 ) ) ) + ( ; 7 2 · ( 𝑃 · 𝑅 ) ) ) )
12		quart.w	⊢ ( 𝜑 → 𝑊 = ( √ ‘ ( ( 𝑉 ↑ 2 ) − ( 4 · ( 𝑈 ↑ 3 ) ) ) ) )
13	1 2 3 4 7 8 9	quart1cl	⊢ ( 𝜑 → ( 𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) )
14	13	simp1d	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
15	14	sqcld	⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ∈ ℂ )
16		1nn0	⊢ 1 ∈ ℕ0
17		2nn	⊢ 2 ∈ ℕ
18	16 17	decnncl	⊢ ; 1 2 ∈ ℕ
19	18	nncni	⊢ ; 1 2 ∈ ℂ
20	13	simp3d	⊢ ( 𝜑 → 𝑅 ∈ ℂ )
21		mulcl	⊢ ( ( ; 1 2 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( ; 1 2 · 𝑅 ) ∈ ℂ )
22	19 20 21	sylancr	⊢ ( 𝜑 → ( ; 1 2 · 𝑅 ) ∈ ℂ )
23	15 22	addcld	⊢ ( 𝜑 → ( ( 𝑃 ↑ 2 ) + ( ; 1 2 · 𝑅 ) ) ∈ ℂ )
24	10 23	eqeltrd	⊢ ( 𝜑 → 𝑈 ∈ ℂ )
25		2cn	⊢ 2 ∈ ℂ
26		3nn0	⊢ 3 ∈ ℕ0
27		expcl	⊢ ( ( 𝑃 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑃 ↑ 3 ) ∈ ℂ )
28	14 26 27	sylancl	⊢ ( 𝜑 → ( 𝑃 ↑ 3 ) ∈ ℂ )
29		mulcl	⊢ ( ( 2 ∈ ℂ ∧ ( 𝑃 ↑ 3 ) ∈ ℂ ) → ( 2 · ( 𝑃 ↑ 3 ) ) ∈ ℂ )
30	25 28 29	sylancr	⊢ ( 𝜑 → ( 2 · ( 𝑃 ↑ 3 ) ) ∈ ℂ )
31	30	negcld	⊢ ( 𝜑 → - ( 2 · ( 𝑃 ↑ 3 ) ) ∈ ℂ )
32		2nn0	⊢ 2 ∈ ℕ0
33		7nn	⊢ 7 ∈ ℕ
34	32 33	decnncl	⊢ ; 2 7 ∈ ℕ
35	34	nncni	⊢ ; 2 7 ∈ ℂ
36	13	simp2d	⊢ ( 𝜑 → 𝑄 ∈ ℂ )
37	36	sqcld	⊢ ( 𝜑 → ( 𝑄 ↑ 2 ) ∈ ℂ )
38		mulcl	⊢ ( ( ; 2 7 ∈ ℂ ∧ ( 𝑄 ↑ 2 ) ∈ ℂ ) → ( ; 2 7 · ( 𝑄 ↑ 2 ) ) ∈ ℂ )
39	35 37 38	sylancr	⊢ ( 𝜑 → ( ; 2 7 · ( 𝑄 ↑ 2 ) ) ∈ ℂ )
40	31 39	subcld	⊢ ( 𝜑 → ( - ( 2 · ( 𝑃 ↑ 3 ) ) − ( ; 2 7 · ( 𝑄 ↑ 2 ) ) ) ∈ ℂ )
41		7nn0	⊢ 7 ∈ ℕ0
42	41 17	decnncl	⊢ ; 7 2 ∈ ℕ
43	42	nncni	⊢ ; 7 2 ∈ ℂ
44	14 20	mulcld	⊢ ( 𝜑 → ( 𝑃 · 𝑅 ) ∈ ℂ )
45		mulcl	⊢ ( ( ; 7 2 ∈ ℂ ∧ ( 𝑃 · 𝑅 ) ∈ ℂ ) → ( ; 7 2 · ( 𝑃 · 𝑅 ) ) ∈ ℂ )
46	43 44 45	sylancr	⊢ ( 𝜑 → ( ; 7 2 · ( 𝑃 · 𝑅 ) ) ∈ ℂ )
47	40 46	addcld	⊢ ( 𝜑 → ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) − ( ; 2 7 · ( 𝑄 ↑ 2 ) ) ) + ( ; 7 2 · ( 𝑃 · 𝑅 ) ) ) ∈ ℂ )
48	11 47	eqeltrd	⊢ ( 𝜑 → 𝑉 ∈ ℂ )
49	48	sqcld	⊢ ( 𝜑 → ( 𝑉 ↑ 2 ) ∈ ℂ )
50		4cn	⊢ 4 ∈ ℂ
51		expcl	⊢ ( ( 𝑈 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑈 ↑ 3 ) ∈ ℂ )
52	24 26 51	sylancl	⊢ ( 𝜑 → ( 𝑈 ↑ 3 ) ∈ ℂ )
53		mulcl	⊢ ( ( 4 ∈ ℂ ∧ ( 𝑈 ↑ 3 ) ∈ ℂ ) → ( 4 · ( 𝑈 ↑ 3 ) ) ∈ ℂ )
54	50 52 53	sylancr	⊢ ( 𝜑 → ( 4 · ( 𝑈 ↑ 3 ) ) ∈ ℂ )
55	49 54	subcld	⊢ ( 𝜑 → ( ( 𝑉 ↑ 2 ) − ( 4 · ( 𝑈 ↑ 3 ) ) ) ∈ ℂ )
56	55	sqrtcld	⊢ ( 𝜑 → ( √ ‘ ( ( 𝑉 ↑ 2 ) − ( 4 · ( 𝑈 ↑ 3 ) ) ) ) ∈ ℂ )
57	12 56	eqeltrd	⊢ ( 𝜑 → 𝑊 ∈ ℂ )
58	24 48 57	3jca	⊢ ( 𝜑 → ( 𝑈 ∈ ℂ ∧ 𝑉 ∈ ℂ ∧ 𝑊 ∈ ℂ ) )