Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem projlem3 5195

Description: Part of Lemma 3.6 of [Beran] p. 100, bottom inequality. Used by projlem6 5198.

**Hypotheses**
Ref	Expression
projlem3.1	⊢ R ∈ ℝ
projlem3.2	⊢ D ∈ ℕ
projlem3.3	⊢ G ∈ ℕ

**Assertion**
Ref	Expression
projlem3	⊢ (((2 · ((R + (1 / D))↑2)) + (2 · ((R + (1 / G))↑2))) − (4 · (R↑2))) ≤ (((4 · R) + 2) · ((1 / D) + (1 / G)))

**Proof of Theorem projlem3**
Step	Hyp	Ref	Expression
1		2cn 4471	. . . . . 6 ⊢ 2 ∈ ℂ
2		projlem3.1	. . . . . . . . 9 ⊢ R ∈ ℝ
3		ax1re 4064	. . . . . . . . . 10 ⊢ 1 ∈ ℝ
4		projlem3.2	. . . . . . . . . . 11 ⊢ D ∈ ℕ
5	4	nnre 4429	. . . . . . . . . 10 ⊢ D ∈ ℝ
6	4	nnne0 4446	. . . . . . . . . 10 ⊢ D ≠ 0
7	3, 5, 6	redivcl 4274	. . . . . . . . 9 ⊢ (1 / D) ∈ ℝ
8	2, 7	readdcl 4118	. . . . . . . 8 ⊢ (R + (1 / D)) ∈ ℝ
9	8	sqrecl 4699	. . . . . . 7 ⊢ ((R + (1 / D))↑2) ∈ ℝ
10	9	recn 4098	. . . . . 6 ⊢ ((R + (1 / D))↑2) ∈ ℂ
11		projlem3.3	. . . . . . . . . . 11 ⊢ G ∈ ℕ
12	11	nnre 4429	. . . . . . . . . 10 ⊢ G ∈ ℝ
13	11	nnne0 4446	. . . . . . . . . 10 ⊢ G ≠ 0
14	3, 12, 13	redivcl 4274	. . . . . . . . 9 ⊢ (1 / G) ∈ ℝ
15	2, 14	readdcl 4118	. . . . . . . 8 ⊢ (R + (1 / G)) ∈ ℝ
16	15	sqrecl 4699	. . . . . . 7 ⊢ ((R + (1 / G))↑2) ∈ ℝ
17	16	recn 4098	. . . . . 6 ⊢ ((R + (1 / G))↑2) ∈ ℂ
18	1, 10, 17	adddi 4110	. . . . 5 ⊢ (2 · (((R + (1 / D))↑2) + ((R + (1 / G))↑2))) = ((2 · ((R + (1 / D))↑2)) + (2 · ((R + (1 / G))↑2)))
19	2	recn 4098	. . . . . . . . . 10 ⊢ R ∈ ℂ
20	7	recn 4098	. . . . . . . . . 10 ⊢ (1 / D) ∈ ℂ
21	19, 20	binom 4712	. . . . . . . . 9 ⊢ ((R + (1 / D))↑2) = (((R↑2) + (2 · (R · (1 / D)))) + ((1 / D)↑2))
22	19	sqcl 4686	. . . . . . . . . 10 ⊢ (R↑2) ∈ ℂ
23	19, 20	mulcl 4105	. . . . . . . . . . 11 ⊢ (R · (1 / D)) ∈ ℂ
24	1, 23	mulcl 4105	. . . . . . . . . 10 ⊢ (2 · (R · (1 / D))) ∈ ℂ
25	20	sqcl 4686	. . . . . . . . . 10 ⊢ ((1 / D)↑2) ∈ ℂ
26	22, 24, 25	addass 4108	. . . . . . . . 9 ⊢ (((R↑2) + (2 · (R · (1 / D)))) + ((1 / D)↑2)) = ((R↑2) + ((2 · (R · (1 / D))) + ((1 / D)↑2)))
27	21, 26	eqtr 1119	. . . . . . . 8 ⊢ ((R + (1 / D))↑2) = ((R↑2) + ((2 · (R · (1 / D))) + ((1 / D)↑2)))
28	14	recn 4098	. . . . . . . . . 10 ⊢ (1 / G) ∈ ℂ
29	19, 28	binom 4712	. . . . . . . . 9 ⊢ ((R + (1 / G))↑2) = (((R↑2) + (2 · (R · (1 / G)))) + ((1 / G)↑2))
30	19, 28	mulcl 4105	. . . . . . . . . . 11 ⊢ (R · (1 / G)) ∈ ℂ
31	1, 30	mulcl 4105	. . . . . . . . . 10 ⊢ (2 · (R · (1 / G))) ∈ ℂ
32	28	sqcl 4686	. . . . . . . . . 10 ⊢ ((1 / G)↑2) ∈ ℂ
33	22, 31, 32	addass 4108	. . . . . . . . 9 ⊢ (((R↑2) + (2 · (R · (1 / G)))) + ((1 / G)↑2)) = ((R↑2) + ((2 · (R · (1 / G))) + ((1 / G)↑2)))
34	29, 33	eqtr 1119	. . . . . . . 8 ⊢ ((R + (1 / G))↑2) = ((R↑2) + ((2 · (R · (1 / G))) + ((1 / G)↑2)))
35	27, 34	opreq12i 3011	. . . . . . 7 ⊢ (((R + (1 / D))↑2) + ((R + (1 / G))↑2)) = (((R↑2) + ((2 · (R · (1 / D))) + ((1 / D)↑2))) + ((R↑2) + ((2 · (R · (1 / G))) + ((1 / G)↑2))))
36	24, 25	addcl 4104	. . . . . . . 8 ⊢ ((2 · (R · (1 / D))) + ((1 / D)↑2)) ∈ ℂ
37	31, 32	addcl 4104	. . . . . . . 8 ⊢ ((2 · (R · (1 / G))) + ((1 / G)↑2)) ∈ ℂ
38	22, 36, 22, 37	add4 4130	. . . . . . 7 ⊢ (((R↑2) + ((2 · (R · (1 / D))) + ((1 / D)↑2))) + ((R↑2) + ((2 · (R · (1 / G))) + ((1 / G)↑2)))) = (((R↑2) + (R↑2)) + (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2))))
39	35, 38	eqtr 1119	. . . . . 6 ⊢ (((R + (1 / D))↑2) + ((R + (1 / G))↑2)) = (((R↑2) + (R↑2)) + (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2))))
40	39	opreq2i 3010	. . . . 5 ⊢ (2 · (((R + (1 / D))↑2) + ((R + (1 / G))↑2))) = (2 · (((R↑2) + (R↑2)) + (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2)))))
41	18, 40	eqtr3 1121	. . . 4 ⊢ ((2 · ((R + (1 / D))↑2)) + (2 · ((R + (1 / G))↑2))) = (2 · (((R↑2) + (R↑2)) + (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2)))))
42	1, 1, 22	mulass 4109	. . . . 5 ⊢ ((2 · 2) · (R↑2)) = (2 · (2 · (R↑2)))
43		2t2e4 4503	. . . . . 6 ⊢ (2 · 2) = 4
44	43	opreq1i 3009	. . . . 5 ⊢ ((2 · 2) · (R↑2)) = (4 · (R↑2))
45	22	2times 4489	. . . . . 6 ⊢ (2 · (R↑2)) = ((R↑2) + (R↑2))
46	45	opreq2i 3010	. . . . 5 ⊢ (2 · (2 · (R↑2))) = (2 · ((R↑2) + (R↑2)))
47	42, 44, 46	3eqtr3 1124	. . . 4 ⊢ (4 · (R↑2)) = (2 · ((R↑2) + (R↑2)))
48	41, 47	opreq12i 3011	. . 3 ⊢ (((2 · ((R + (1 / D))↑2)) + (2 · ((R + (1 / G))↑2))) − (4 · (R↑2))) = ((2 · (((R↑2) + (R↑2)) + (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2))))) − (2 · ((R↑2) + (R↑2))))
49	22, 22	addcl 4104	. . . . . 6 ⊢ ((R↑2) + (R↑2)) ∈ ℂ
50	36, 37	addcl 4104	. . . . . 6 ⊢ (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2))) ∈ ℂ
51	49, 50	addcl 4104	. . . . 5 ⊢ (((R↑2) + (R↑2)) + (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2)))) ∈ ℂ
52	1, 51, 49	subdi 4182	. . . 4 ⊢ (2 · ((((R↑2) + (R↑2)) + (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2)))) − ((R↑2) + (R↑2)))) = ((2 · (((R↑2) + (R↑2)) + (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2))))) − (2 · ((R↑2) + (R↑2))))
53	49, 50, 49	addsubass 4152	. . . . . 6 ⊢ ((((R↑2) + (R↑2)) + (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2)))) − ((R↑2) + (R↑2))) = (((R↑2) + (R↑2)) + ((((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2))) − ((R↑2) + (R↑2))))
54	49, 50	subaddeq 4146	. . . . . 6 ⊢ (((R↑2) + (R↑2)) + ((((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2))) − ((R↑2) + (R↑2)))) = (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2)))
55	24, 25, 31, 32	add4 4130	. . . . . . 7 ⊢ (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2))) = (((2 · (R · (1 / D))) + (2 · (R · (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2)))
56	19, 20, 28	adddi 4110	. . . . . . . . . 10 ⊢ (R · ((1 / D) + (1 / G))) = ((R · (1 / D)) + (R · (1 / G)))
57	56	opreq2i 3010	. . . . . . . . 9 ⊢ (2 · (R · ((1 / D) + (1 / G)))) = (2 · ((R · (1 / D)) + (R · (1 / G))))
58	1, 23, 30	adddi 4110	. . . . . . . . 9 ⊢ (2 · ((R · (1 / D)) + (R · (1 / G)))) = ((2 · (R · (1 / D))) + (2 · (R · (1 / G))))
59	57, 58	eqtr 1119	. . . . . . . 8 ⊢ (2 · (R · ((1 / D) + (1 / G)))) = ((2 · (R · (1 / D))) + (2 · (R · (1 / G))))
60	59	opreq1i 3009	. . . . . . 7 ⊢ ((2 · (R · ((1 / D) + (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2))) = (((2 · (R · (1 / D))) + (2 · (R · (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2)))
61	55, 60	eqtr4 1122	. . . . . 6 ⊢ (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2))) = ((2 · (R · ((1 / D) + (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2)))
62	53, 54, 61	3eqtr 1123	. . . . 5 ⊢ ((((R↑2) + (R↑2)) + (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2)))) − ((R↑2) + (R↑2))) = ((2 · (R · ((1 / D) + (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2)))
63	62	opreq2i 3010	. . . 4 ⊢ (2 · ((((R↑2) + (R↑2)) + (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2)))) − ((R↑2) + (R↑2)))) = (2 · ((2 · (R · ((1 / D) + (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2))))
64	52, 63	eqtr3 1121	. . 3 ⊢ ((2 · (((R↑2) + (R↑2)) + (((2 · (R · (1 / D))) + ((1 / D)↑2)) + ((2 · (R · (1 / G))) + ((1 / G)↑2))))) − (2 · ((R↑2) + (R↑2)))) = (2 · ((2 · (R · ((1 / D) + (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2))))
65	48, 64	eqtr 1119	. 2 ⊢ (((2 · ((R + (1 / D))↑2)) + (2 · ((R + (1 / G))↑2))) − (4 · (R↑2))) = (2 · ((2 · (R · ((1 / D) + (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2))))
66	4	nncn 4430	. . . . . . . 8 ⊢ D ∈ ℂ
67	66, 6	sqreci 4690	. . . . . . 7 ⊢ ((1 / D)↑2) = (1 / (D↑2))
68	4	nnlesq 4718	. . . . . . . 8 ⊢ D ≤ (D↑2)
69	4	nngt0 4445	. . . . . . . . 9 ⊢ 0 < D
70	5	sqegt0 4703	. . . . . . . . . 10 ⊢ (D ≠ 0 → 0 < (D↑2))
71	6, 70	ax-mp 6	. . . . . . . . 9 ⊢ 0 < (D↑2)
72	5	sqrecl 4699	. . . . . . . . . 10 ⊢ (D↑2) ∈ ℝ
73	5, 72	lerec 4411	. . . . . . . . 9 ⊢ ((0 < D ∧ 0 < (D↑2)) → (D ≤ (D↑2) ↔ (1 / (D↑2)) ≤ (1 / D)))
74	69, 71, 73	mp2an 520	. . . . . . . 8 ⊢ (D ≤ (D↑2) ↔ (1 / (D↑2)) ≤ (1 / D))
75	68, 74	mpbi 164	. . . . . . 7 ⊢ (1 / (D↑2)) ≤ (1 / D)
76	67, 75	eqbrtr 2076	. . . . . 6 ⊢ ((1 / D)↑2) ≤ (1 / D)
77	11	nncn 4430	. . . . . . . 8 ⊢ G ∈ ℂ
78	77, 13	sqreci 4690	. . . . . . 7 ⊢ ((1 / G)↑2) = (1 / (G↑2))
79	11	nnlesq 4718	. . . . . . . 8 ⊢ G ≤ (G↑2)
80	11	nngt0 4445	. . . . . . . . 9 ⊢ 0 < G
81	12	sqegt0 4703	. . . . . . . . . 10 ⊢ (G ≠ 0 → 0 < (G↑2))
82	13, 81	ax-mp 6	. . . . . . . . 9 ⊢ 0 < (G↑2)
83	12	sqrecl 4699	. . . . . . . . . 10 ⊢ (G↑2) ∈ ℝ
84	12, 83	lerec 4411	. . . . . . . . 9 ⊢ ((0 < G ∧ 0 < (G↑2)) → (G ≤ (G↑2) ↔ (1 / (G↑2)) ≤ (1 / G)))
85	80, 82, 84	mp2an 520	. . . . . . . 8 ⊢ (G ≤ (G↑2) ↔ (1 / (G↑2)) ≤ (1 / G))
86	79, 85	mpbi 164	. . . . . . 7 ⊢ (1 / (G↑2)) ≤ (1 / G)
87	78, 86	eqbrtr 2076	. . . . . 6 ⊢ ((1 / G)↑2) ≤ (1 / G)
88	7	sqrecl 4699	. . . . . . 7 ⊢ ((1 / D)↑2) ∈ ℝ
89	14	sqrecl 4699	. . . . . . 7 ⊢ ((1 / G)↑2) ∈ ℝ
90	88, 89, 7, 14	le2add 4322	. . . . . 6 ⊢ ((((1 / D)↑2) ≤ (1 / D) ∧ ((1 / G)↑2) ≤ (1 / G)) → (((1 / D)↑2) + ((1 / G)↑2)) ≤ ((1 / D) + (1 / G)))
91	76, 87, 90	mp2an 520	. . . . 5 ⊢ (((1 / D)↑2) + ((1 / G)↑2)) ≤ ((1 / D) + (1 / G))
92	88, 89	readdcl 4118	. . . . . 6 ⊢ (((1 / D)↑2) + ((1 / G)↑2)) ∈ ℝ
93	7, 14	readdcl 4118	. . . . . 6 ⊢ ((1 / D) + (1 / G)) ∈ ℝ
94		2re 4470	. . . . . . 7 ⊢ 2 ∈ ℝ
95	2, 93	remulcl 4119	. . . . . . 7 ⊢ (R · ((1 / D) + (1 / G))) ∈ ℝ
96	94, 95	remulcl 4119	. . . . . 6 ⊢ (2 · (R · ((1 / D) + (1 / G)))) ∈ ℝ
97	92, 93, 96	leadd2 4315	. . . . 5 ⊢ ((((1 / D)↑2) + ((1 / G)↑2)) ≤ ((1 / D) + (1 / G)) ↔ ((2 · (R · ((1 / D) + (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2))) ≤ ((2 · (R · ((1 / D) + (1 / G)))) + ((1 / D) + (1 / G))))
98	91, 97	mpbi 164	. . . 4 ⊢ ((2 · (R · ((1 / D) + (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2))) ≤ ((2 · (R · ((1 / D) + (1 / G)))) + ((1 / D) + (1 / G)))
99		2pos 4479	. . . . 5 ⊢ 0 < 2
100	96, 92	readdcl 4118	. . . . . 6 ⊢ ((2 · (R · ((1 / D) + (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2))) ∈ ℝ
101	96, 93	readdcl 4118	. . . . . 6 ⊢ ((2 · (R · ((1 / D) + (1 / G)))) + ((1 / D) + (1 / G))) ∈ ℝ
102	100, 101, 94	lemul2 4396	. . . . 5 ⊢ (0 < 2 → (((2 · (R · ((1 / D) + (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2))) ≤ ((2 · (R · ((1 / D) + (1 / G)))) + ((1 / D) + (1 / G))) ↔ (2 · ((2 · (R · ((1 / D) + (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2)))) ≤ (2 · ((2 · (R · ((1 / D) + (1 / G)))) + ((1 / D) + (1 / G))))))
103	99, 102	ax-mp 6	. . . 4 ⊢ (((2 · (R · ((1 / D) + (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2))) ≤ ((2 · (R · ((1 / D) + (1 / G)))) + ((1 / D) + (1 / G))) ↔ (2 · ((2 · (R · ((1 / D) + (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2)))) ≤ (2 · ((2 · (R · ((1 / D) + (1 / G)))) + ((1 / D) + (1 / G)))))
104	98, 103	mpbi 164	. . 3 ⊢ (2 · ((2 · (R · ((1 / D) + (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2)))) ≤ (2 · ((2 · (R · ((1 / D) + (1 / G)))) + ((1 / D) + (1 / G))))
105	93	recn 4098	. . . . . . . 8 ⊢ ((1 / D) + (1 / G)) ∈ ℂ
106	19, 105	mulcl 4105	. . . . . . 7 ⊢ (R · ((1 / D) + (1 / G))) ∈ ℂ
107	1, 1, 106	mulass 4109	. . . . . 6 ⊢ ((2 · 2) · (R · ((1 / D) + (1 / G)))) = (2 · (2 · (R · ((1 / D) + (1 / G)))))
108	43	opreq1i 3009	. . . . . . 7 ⊢ ((2 · 2) · (R · ((1 / D) + (1 / G)))) = (4 · (R · ((1 / D) + (1 / G))))
109		4re 4473	. . . . . . . . 9 ⊢ 4 ∈ ℝ
110	109	recn 4098	. . . . . . . 8 ⊢ 4 ∈ ℂ
111	110, 19, 105	mulass 4109	. . . . . . 7 ⊢ ((4 · R) · ((1 / D) + (1 / G))) = (4 · (R · ((1 / D) + (1 / G))))
112	108, 111	eqtr4 1122	. . . . . 6 ⊢ ((2 · 2) · (R · ((1 / D) + (1 / G)))) = ((4 · R) · ((1 / D) + (1 / G)))
113	107, 112	eqtr3 1121	. . . . 5 ⊢ (2 · (2 · (R · ((1 / D) + (1 / G))))) = ((4 · R) · ((1 / D) + (1 / G)))
114	113	opreq1i 3009	. . . 4 ⊢ ((2 · (2 · (R · ((1 / D) + (1 / G))))) + (2 · ((1 / D) + (1 / G)))) = (((4 · R) · ((1 / D) + (1 / G))) + (2 · ((1 / D) + (1 / G))))
115	1, 106	mulcl 4105	. . . . 5 ⊢ (2 · (R · ((1 / D) + (1 / G)))) ∈ ℂ
116	1, 115, 105	adddi 4110	. . . 4 ⊢ (2 · ((2 · (R · ((1 / D) + (1 / G)))) + ((1 / D) + (1 / G)))) = ((2 · (2 · (R · ((1 / D) + (1 / G))))) + (2 · ((1 / D) + (1 / G))))
117	109, 2	remulcl 4119	. . . . . 6 ⊢ (4 · R) ∈ ℝ
118	117	recn 4098	. . . . 5 ⊢ (4 · R) ∈ ℂ
119	118, 1, 105	adddir 4111	. . . 4 ⊢ (((4 · R) + 2) · ((1 / D) + (1 / G))) = (((4 · R) · ((1 / D) + (1 / G))) + (2 · ((1 / D) + (1 / G))))
120	114, 116, 119	3eqtr4 1126	. . 3 ⊢ (2 · ((2 · (R · ((1 / D) + (1 / G)))) + ((1 / D) + (1 / G)))) = (((4 · R) + 2) · ((1 / D) + (1 / G)))
121	104, 120	breqtr 2080	. 2 ⊢ (2 · ((2 · (R · ((1 / D) + (1 / G)))) + (((1 / D)↑2) + ((1 / G)↑2)))) ≤ (((4 · R) + 2) · ((1 / D) + (1 / G)))
122	65, 121	eqbrtr 2076	1 ⊢ (((2 · ((R + (1 / D))↑2)) + (2 · ((R + (1 / G))↑2))) − (4 · (R↑2))) ≤ (((4 · R) + 2) · ((1 / D) + (1 / G)))

Colors of variables: wff set class

Syntax hints: ↔ wb 127 ∈ wcel 1092 ≠ wne 1190 class class class wbr 2054 (class class class)co 3001 ℝcr 4027 0cc0 4028 1c1 4029 + caddc 4031 · cmulc 4032 < clt 4033 − cmin 4089 / cdiv 4091 ≤ cle 4092 ℕcn 4093 2c2 4454 4c4 4456 ↑cexp 4675

This theorem is referenced by: projlem6 5198

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fo 2436 df-f1o 2437 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1st 3087 df-2nd 3088 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-mp 3883 df-ltp 3884 df-plpr 3958 df-mpr 3959 df-enr 3960 df-nr 3961 df-plr 3962 df-mr 3963 df-ltr 3964 df-0r 3965 df-1r 3966 df-m1r 3967 df-c 4034 df-0 4035 df-1 4036 df-r 4038 df-plus 4039 df-mul 4040 df-lt 4041 df-sub 4133 df-neg 4135 df-div 4216 df-le 4277 df-n 4423 df-2 4462 df-3 4463 df-4 4464 df-n0 4535 df-z 4564 df-seq 4661 df-exp 4676

metamath.org