ip1ilem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ip1ilem		Structured version Visualization version GIF version

Theorem ip1ilem 30702

Description: Lemma for ip1i 30703. (Contributed by NM, 21-Apr-2007.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
ip1i.1	⊢ 𝑋 = (BaseSet‘𝑈)
ip1i.2	⊢ 𝐺 = ( +_𝑣 ‘𝑈)
ip1i.4	⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
ip1i.7	⊢ 𝑃 = (·_𝑖OLD‘𝑈)
ip1i.9	⊢ 𝑈 ∈ CPreHil_OLD
ip1i.a	⊢ 𝐴 ∈ 𝑋
ip1i.b	⊢ 𝐵 ∈ 𝑋
ip1i.c	⊢ 𝐶 ∈ 𝑋
ip1i.6	⊢ 𝑁 = (norm_CV‘𝑈)
ip0i.j	⊢ 𝐽 ∈ ℂ

**Assertion**
Ref	Expression
ip1ilem	⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶))

**Proof of Theorem ip1ilem**
Step	Hyp	Ref	Expression
1		ip1i.9	. . . . . . 7 ⊢ 𝑈 ∈ CPreHil_OLD
2	1	phnvi 30692	. . . . . 6 ⊢ 𝑈 ∈ NrmCVec
3		ip1i.a	. . . . . 6 ⊢ 𝐴 ∈ 𝑋
4		ip1i.c	. . . . . 6 ⊢ 𝐶 ∈ 𝑋
5		ip1i.1	. . . . . . 7 ⊢ 𝑋 = (BaseSet‘𝑈)
6		ip1i.2	. . . . . . 7 ⊢ 𝐺 = ( +_𝑣 ‘𝑈)
7		ip1i.4	. . . . . . 7 ⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
8		ip1i.6	. . . . . . 7 ⊢ 𝑁 = (norm_CV‘𝑈)
9		ip1i.7	. . . . . . 7 ⊢ 𝑃 = (·_𝑖OLD‘𝑈)
10	5, 6, 7, 8, 9	4ipval2 30584	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (4 · (𝐴𝑃𝐶)) = ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))))
11	2, 3, 4, 10	mp3an 1457	. . . . 5 ⊢ (4 · (𝐴𝑃𝐶)) = ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
12	11	oveq2i 7429	. . . 4 ⊢ (2 · (4 · (𝐴𝑃𝐶))) = (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))))
13		2cn 12318	. . . . 5 ⊢ 2 ∈ ℂ
14		4cn 12328	. . . . 5 ⊢ 4 ∈ ℂ
15	5, 9	dipcl 30588	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑃𝐶) ∈ ℂ)
16	2, 3, 4, 15	mp3an 1457	. . . . 5 ⊢ (𝐴𝑃𝐶) ∈ ℂ
17	13, 14, 16	mul12i 11440	. . . 4 ⊢ (2 · (4 · (𝐴𝑃𝐶))) = (4 · (2 · (𝐴𝑃𝐶)))
18	5, 6	nvgcl 30496	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝐺𝐶) ∈ 𝑋)
19	2, 3, 4, 18	mp3an 1457	. . . . . . . . . . 11 ⊢ (𝐴𝐺𝐶) ∈ 𝑋
20	5, 8, 2, 19	nvcli 30538	. . . . . . . . . 10 ⊢ (𝑁‘(𝐴𝐺𝐶)) ∈ ℝ
21	20	resqcli 14183	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺𝐶))↑2) ∈ ℝ
22	21	recni 11259	. . . . . . . 8 ⊢ ((𝑁‘(𝐴𝐺𝐶))↑2) ∈ ℂ
23		ax-1cn 11197	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
24	23	negcli 11559	. . . . . . . . . . . . 13 ⊢ -1 ∈ ℂ
25	5, 7	nvscl 30502	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐶 ∈ 𝑋) → (-1𝑆𝐶) ∈ 𝑋)
26	2, 24, 4, 25	mp3an 1457	. . . . . . . . . . . 12 ⊢ (-1𝑆𝐶) ∈ 𝑋
27	5, 6	nvgcl 30496	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐶)) ∈ 𝑋)
28	2, 3, 26, 27	mp3an 1457	. . . . . . . . . . 11 ⊢ (𝐴𝐺(-1𝑆𝐶)) ∈ 𝑋
29	5, 8, 2, 28	nvcli 30538	. . . . . . . . . 10 ⊢ (𝑁‘(𝐴𝐺(-1𝑆𝐶))) ∈ ℝ
30	29	resqcli 14183	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2) ∈ ℝ
31	30	recni 11259	. . . . . . . 8 ⊢ ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2) ∈ ℂ
32	22, 31	subcli 11567	. . . . . . 7 ⊢ (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) ∈ ℂ
33		ax-icn 11198	. . . . . . . 8 ⊢ i ∈ ℂ
34	5, 7	nvscl 30502	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ i ∈ ℂ ∧ 𝐶 ∈ 𝑋) → (i𝑆𝐶) ∈ 𝑋)
35	2, 33, 4, 34	mp3an 1457	. . . . . . . . . . . . 13 ⊢ (i𝑆𝐶) ∈ 𝑋
36	5, 6	nvgcl 30496	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(i𝑆𝐶)) ∈ 𝑋)
37	2, 3, 35, 36	mp3an 1457	. . . . . . . . . . . 12 ⊢ (𝐴𝐺(i𝑆𝐶)) ∈ 𝑋
38	5, 8, 2, 37	nvcli 30538	. . . . . . . . . . 11 ⊢ (𝑁‘(𝐴𝐺(i𝑆𝐶))) ∈ ℝ
39	38	resqcli 14183	. . . . . . . . . 10 ⊢ ((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) ∈ ℝ
40	39	recni 11259	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) ∈ ℂ
41	33	negcli 11559	. . . . . . . . . . . . . 14 ⊢ -i ∈ ℂ
42	5, 7	nvscl 30502	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ -i ∈ ℂ ∧ 𝐶 ∈ 𝑋) → (-i𝑆𝐶) ∈ 𝑋)
43	2, 41, 4, 42	mp3an 1457	. . . . . . . . . . . . 13 ⊢ (-i𝑆𝐶) ∈ 𝑋
44	5, 6	nvgcl 30496	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-i𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(-i𝑆𝐶)) ∈ 𝑋)
45	2, 3, 43, 44	mp3an 1457	. . . . . . . . . . . 12 ⊢ (𝐴𝐺(-i𝑆𝐶)) ∈ 𝑋
46	5, 8, 2, 45	nvcli 30538	. . . . . . . . . . 11 ⊢ (𝑁‘(𝐴𝐺(-i𝑆𝐶))) ∈ ℝ
47	46	resqcli 14183	. . . . . . . . . 10 ⊢ ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2) ∈ ℝ
48	47	recni 11259	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2) ∈ ℂ
49	40, 48	subcli 11567	. . . . . . . 8 ⊢ (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)) ∈ ℂ
50	33, 49	mulcli 11252	. . . . . . 7 ⊢ (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))) ∈ ℂ
51	13, 32, 50	adddii 11257	. . . . . 6 ⊢ (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))) = ((2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2))) + (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))))
52		ip1i.b	. . . . . . . . 9 ⊢ 𝐵 ∈ 𝑋
53	5, 6, 7, 9, 1, 3, 52, 4, 8, 23	ip0i 30701	. . . . . . . 8 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)))
54	5, 7	nvsid 30503	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐶 ∈ 𝑋) → (1𝑆𝐶) = 𝐶)
55	2, 4, 54	mp2an 690	. . . . . . . . . . . . 13 ⊢ (1𝑆𝐶) = 𝐶
56	55	oveq2i 7429	. . . . . . . . . . . 12 ⊢ ((𝐴𝐺𝐵)𝐺(1𝑆𝐶)) = ((𝐴𝐺𝐵)𝐺𝐶)
57	56	fveq2i 6898	. . . . . . . . . . 11 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶))) = (𝑁‘((𝐴𝐺𝐵)𝐺𝐶))
58	57	oveq1i 7428	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) = ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2)
59	58	oveq1i 7428	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) = (((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2))
60	55	oveq2i 7429	. . . . . . . . . . . 12 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)) = ((𝐴𝐺(-1𝑆𝐵))𝐺𝐶)
61	60	fveq2i 6898	. . . . . . . . . . 11 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶))) = (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))
62	61	oveq1i 7428	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) = ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2)
63	62	oveq1i 7428	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) = (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))
64	59, 63	oveq12i 7430	. . . . . . . 8 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)))
65	55	oveq2i 7429	. . . . . . . . . . . 12 ⊢ (𝐴𝐺(1𝑆𝐶)) = (𝐴𝐺𝐶)
66	65	fveq2i 6898	. . . . . . . . . . 11 ⊢ (𝑁‘(𝐴𝐺(1𝑆𝐶))) = (𝑁‘(𝐴𝐺𝐶))
67	66	oveq1i 7428	. . . . . . . . . 10 ⊢ ((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) = ((𝑁‘(𝐴𝐺𝐶))↑2)
68	67	oveq1i 7428	. . . . . . . . 9 ⊢ (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) = (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2))
69	68	oveq2i 7429	. . . . . . . 8 ⊢ (2 · (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)))
70	53, 64, 69	3eqtr3i 2761	. . . . . . 7 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)))
71	5, 6, 7, 9, 1, 3, 52, 4, 8, 33	ip0i 30701	. . . . . . . . 9 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))
72	71	oveq2i 7429	. . . . . . . 8 ⊢ (i · ((((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))) = (i · (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
73	5, 6	nvgcl 30496	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
74	2, 3, 52, 73	mp3an 1457	. . . . . . . . . . . . . 14 ⊢ (𝐴𝐺𝐵) ∈ 𝑋
75	5, 6	nvgcl 30496	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(i𝑆𝐶)) ∈ 𝑋)
76	2, 74, 35, 75	mp3an 1457	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺𝐵)𝐺(i𝑆𝐶)) ∈ 𝑋
77	5, 8, 2, 76	nvcli 30538	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶))) ∈ ℝ
78	77	resqcli 14183	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) ∈ ℝ
79	78	recni 11259	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) ∈ ℂ
80	5, 6	nvgcl 30496	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (-i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)) ∈ 𝑋)
81	2, 74, 43, 80	mp3an 1457	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)) ∈ 𝑋
82	5, 8, 2, 81	nvcli 30538	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶))) ∈ ℝ
83	82	resqcli 14183	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2) ∈ ℝ
84	83	recni 11259	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2) ∈ ℂ
85	79, 84	subcli 11567	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) ∈ ℂ
86	5, 7	nvscl 30502	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (-1𝑆𝐵) ∈ 𝑋)
87	2, 24, 52, 86	mp3an 1457	. . . . . . . . . . . . . . 15 ⊢ (-1𝑆𝐵) ∈ 𝑋
88	5, 6	nvgcl 30496	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
89	2, 3, 87, 88	mp3an 1457	. . . . . . . . . . . . . 14 ⊢ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋
90	5, 6	nvgcl 30496	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)) ∈ 𝑋)
91	2, 89, 35, 90	mp3an 1457	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)) ∈ 𝑋
92	5, 8, 2, 91	nvcli 30538	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶))) ∈ ℝ
93	92	resqcli 14183	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) ∈ ℝ
94	93	recni 11259	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) ∈ ℂ
95	5, 6	nvgcl 30496	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ (-i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)) ∈ 𝑋)
96	2, 89, 43, 95	mp3an 1457	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)) ∈ 𝑋
97	5, 8, 2, 96	nvcli 30538	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶))) ∈ ℝ
98	97	resqcli 14183	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2) ∈ ℝ
99	98	recni 11259	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2) ∈ ℂ
100	94, 99	subcli 11567	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)) ∈ ℂ
101	33, 85, 100	adddii 11257	. . . . . . . 8 ⊢ (i · ((((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))) = ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))))
102	33, 13, 49	mul12i 11440	. . . . . . . 8 ⊢ (i · (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))) = (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
103	72, 101, 102	3eqtr3i 2761	. . . . . . 7 ⊢ ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))) = (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
104	70, 103	oveq12i 7430	. . . . . 6 ⊢ (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) + ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))))) = ((2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2))) + (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))))
105	51, 104	eqtr4i 2756	. . . . 5 ⊢ (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))) = (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) + ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))))
106	5, 6	nvgcl 30496	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺𝐶) ∈ 𝑋)
107	2, 74, 4, 106	mp3an 1457	. . . . . . . . . 10 ⊢ ((𝐴𝐺𝐵)𝐺𝐶) ∈ 𝑋
108	5, 8, 2, 107	nvcli 30538	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺𝐶)) ∈ ℝ
109	108	resqcli 14183	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) ∈ ℝ
110	109	recni 11259	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) ∈ ℂ
111	5, 6	nvgcl 30496	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (-1𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)) ∈ 𝑋)
112	2, 74, 26, 111	mp3an 1457	. . . . . . . . . 10 ⊢ ((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)) ∈ 𝑋
113	5, 8, 2, 112	nvcli 30538	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶))) ∈ ℝ
114	113	resqcli 14183	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2) ∈ ℝ
115	114	recni 11259	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2) ∈ ℂ
116	110, 115	subcli 11567	. . . . . 6 ⊢ (((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) ∈ ℂ
117	5, 6	nvgcl 30496	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺𝐶) ∈ 𝑋)
118	2, 89, 4, 117	mp3an 1457	. . . . . . . . . 10 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺𝐶) ∈ 𝑋
119	5, 8, 2, 118	nvcli 30538	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶)) ∈ ℝ
120	119	resqcli 14183	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) ∈ ℝ
121	120	recni 11259	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) ∈ ℂ
122	5, 6	nvgcl 30496	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ (-1𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)) ∈ 𝑋)
123	2, 89, 26, 122	mp3an 1457	. . . . . . . . . 10 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)) ∈ 𝑋
124	5, 8, 2, 123	nvcli 30538	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶))) ∈ ℝ
125	124	resqcli 14183	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2) ∈ ℝ
126	125	recni 11259	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2) ∈ ℂ
127	121, 126	subcli 11567	. . . . . 6 ⊢ (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) ∈ ℂ
128	33, 85	mulcli 11252	. . . . . 6 ⊢ (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) ∈ ℂ
129	33, 100	mulcli 11252	. . . . . 6 ⊢ (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))) ∈ ℂ
130	116, 127, 128, 129	add4i 11469	. . . . 5 ⊢ (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) + ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))))) = (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)))) + ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))))
131	5, 9	dipcl 30588	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺𝐵)𝑃𝐶) ∈ ℂ)
132	2, 74, 4, 131	mp3an 1457	. . . . . . 7 ⊢ ((𝐴𝐺𝐵)𝑃𝐶) ∈ ℂ
133	5, 9	dipcl 30588	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶) ∈ ℂ)
134	2, 89, 4, 133	mp3an 1457	. . . . . . 7 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶) ∈ ℂ
135	14, 132, 134	adddii 11257	. . . . . 6 ⊢ (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) = ((4 · ((𝐴𝐺𝐵)𝑃𝐶)) + (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)))
136	5, 6, 7, 8, 9	4ipval2 30584	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (4 · ((𝐴𝐺𝐵)𝑃𝐶)) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)))))
137	2, 74, 4, 136	mp3an 1457	. . . . . . 7 ⊢ (4 · ((𝐴𝐺𝐵)𝑃𝐶)) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))))
138	5, 6, 7, 8, 9	4ipval2 30584	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))))
139	2, 89, 4, 138	mp3an 1457	. . . . . . 7 ⊢ (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))))
140	137, 139	oveq12i 7430	. . . . . 6 ⊢ ((4 · ((𝐴𝐺𝐵)𝑃𝐶)) + (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) = (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)))) + ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))))
141	135, 140	eqtr2i 2754	. . . . 5 ⊢ (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)))) + ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))))) = (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)))
142	105, 130, 141	3eqtri 2757	. . . 4 ⊢ (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))) = (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)))
143	12, 17, 142	3eqtr3ri 2762	. . 3 ⊢ (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) = (4 · (2 · (𝐴𝑃𝐶)))
144	143	oveq1i 7428	. 2 ⊢ ((4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) / 4) = ((4 · (2 · (𝐴𝑃𝐶))) / 4)
145	132, 134	addcli 11251	. . 3 ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) ∈ ℂ
146		4ne0 12351	. . 3 ⊢ 4 ≠ 0
147	145, 14, 146	divcan3i 11991	. 2 ⊢ ((4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) / 4) = (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))
148	13, 16	mulcli 11252	. . 3 ⊢ (2 · (𝐴𝑃𝐶)) ∈ ℂ
149	148, 14, 146	divcan3i 11991	. 2 ⊢ ((4 · (2 · (𝐴𝑃𝐶))) / 4) = (2 · (𝐴𝑃𝐶))
150	144, 147, 149	3eqtr3i 2761	1 ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶))

Colors of variables: wff setvar class

Syntax hints: = wceq 1533 ∈ wcel 2098 ‘cfv 6548 (class class class)co 7418 ℂcc 11137 1c1 11140 ici 11141 + caddc 11142 · cmul 11144 − cmin 11475 -cneg 11476 / cdiv 11902 2c2 12298 4c4 12300 ↑cexp 14060 NrmCVeccnv 30460 +_𝑣 cpv 30461 BaseSetcba 30462 ·_𝑠OLD cns 30463 norm_CVcnmcv 30466 ·_𝑖OLDcdip 30576 CPreHil_OLDccphlo 30688

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 ax-un 7740 ax-inf2 9665 ax-cnex 11195 ax-resscn 11196 ax-1cn 11197 ax-icn 11198 ax-addcl 11199 ax-addrcl 11200 ax-mulcl 11201 ax-mulrcl 11202 ax-mulcom 11203 ax-addass 11204 ax-mulass 11205 ax-distr 11206 ax-i2m1 11207 ax-1ne0 11208 ax-1rid 11209 ax-rnegex 11210 ax-rrecex 11211 ax-cnre 11212 ax-pre-lttri 11213 ax-pre-lttrn 11214 ax-pre-ltadd 11215 ax-pre-mulgt0 11216 ax-pre-sup 11217

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3964 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-int 4951 df-iun 4999 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-se 5634 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-pred 6306 df-ord 6373 df-on 6374 df-lim 6375 df-suc 6376 df-iota 6500 df-fun 6550 df-fn 6551 df-f 6552 df-f1 6553 df-fo 6554 df-f1o 6555 df-fv 6556 df-isom 6557 df-riota 7374 df-ov 7421 df-oprab 7422 df-mpo 7423 df-om 7871 df-1st 7993 df-2nd 7994 df-frecs 8286 df-wrecs 8317 df-recs 8391 df-rdg 8430 df-1o 8486 df-er 8724 df-en 8964 df-dom 8965 df-sdom 8966 df-fin 8967 df-sup 9466 df-oi 9534 df-card 9963 df-pnf 11281 df-mnf 11282 df-xr 11283 df-ltxr 11284 df-le 11285 df-sub 11477 df-neg 11478 df-div 11903 df-nn 12244 df-2 12306 df-3 12307 df-4 12308 df-n0 12504 df-z 12590 df-uz 12854 df-rp 13008 df-fz 13518 df-fzo 13661 df-seq 14001 df-exp 14061 df-hash 14324 df-cj 15080 df-re 15081 df-im 15082 df-sqrt 15216 df-abs 15217 df-clim 15466 df-sum 15667 df-grpo 30369 df-ablo 30421 df-vc 30435 df-nv 30468 df-va 30471 df-ba 30472 df-sm 30473 df-0v 30474 df-nmcv 30476 df-dip 30577 df-ph 30689

This theorem is referenced by: ip1i 30703

W3C validator

	
		OSZAR »