Theorem 25or6to4 42858

Description: Question 67 of 68 from a lecture Prof. Loof Lirpa held last Saturday in Lincoln Park. When asked why the smaller root wasn't reduced to 3/2, Lirpa responded "It really doesn't matter anyhow." (Contributed by Luke Murphy, 10-Jul-2026.)

Hypotheses

Ref	Expression
25or6to4.a	⊢ (𝜑 → 𝐴 = 1)
25or6to4.b	⊢ (𝜑 → 𝐵 = -(;53 / 2))
25or6to4.c	⊢ (𝜑 → 𝐶 = (;75 / 2))
25or6to4.x	⊢ (𝜑 → 𝑋 ∈ ℂ)

Assertion

Ref	Expression
25or6to4	⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ;25 ∨ 𝑋 = (6 / 4))))

Proof of Theorem 25or6to4

Step	Hyp	Ref	Expression
1		25or6to4.a	. . 3 ⊢ (𝜑 → 𝐴 = 1)
2		ax-1cn 11154	. . 3 ⊢ 1 ∈ ℂ
3	1, 2	eqeltrdi 2877	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		ax-1ne0 11165	. . . 4 ⊢ 1 ≠ 0
5	4	a1i 11	. . 3 ⊢ (𝜑 → 1 ≠ 0)
6	1, 5	eqnetrd 3031	. 2 ⊢ (𝜑 → 𝐴 ≠ 0)
7		25or6to4.b	. . 3 ⊢ (𝜑 → 𝐵 = -(;53 / 2))
8		df-dec 12708	. . . . . 6 ⊢ ;53 = (((9 + 1) · 5) + 3)
9		9cn 12337	. . . . . . . . 9 ⊢ 9 ∈ ℂ
10	9, 2	addcli 11211	. . . . . . . 8 ⊢ (9 + 1) ∈ ℂ
11		5cn 12325	. . . . . . . 8 ⊢ 5 ∈ ℂ
12	10, 11	mulcli 11212	. . . . . . 7 ⊢ ((9 + 1) · 5) ∈ ℂ
13		3cn 12318	. . . . . . 7 ⊢ 3 ∈ ℂ
14	12, 13	addcli 11211	. . . . . 6 ⊢ (((9 + 1) · 5) + 3) ∈ ℂ
15	8, 14	eqeltri 2865	. . . . 5 ⊢ ;53 ∈ ℂ
16		2cn 12312	. . . . 5 ⊢ 2 ∈ ℂ
17		2ne0 12343	. . . . 5 ⊢ 2 ≠ 0
18	15, 16, 17	divcli 11953	. . . 4 ⊢ (;53 / 2) ∈ ℂ
19	18	negcli 11522	. . 3 ⊢ -(;53 / 2) ∈ ℂ
20	7, 19	eqeltrdi 2877	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
21		25or6to4.c	. . 3 ⊢ (𝜑 → 𝐶 = (;75 / 2))
22		df-dec 12708	. . . . 5 ⊢ ;75 = (((9 + 1) · 7) + 5)
23	9, 2	addcli 11211	. . . . . . 7 ⊢ (9 + 1) ∈ ℂ
24		7cn 12331	. . . . . . 7 ⊢ 7 ∈ ℂ
25	23, 24	mulcli 11212	. . . . . 6 ⊢ ((9 + 1) · 7) ∈ ℂ
26	25, 11	addcli 11211	. . . . 5 ⊢ (((9 + 1) · 7) + 5) ∈ ℂ
27	22, 26	eqeltri 2865	. . . 4 ⊢ ;75 ∈ ℂ
28	27, 16, 17	divcli 11953	. . 3 ⊢ (;75 / 2) ∈ ℂ
29	21, 28	eqeltrdi 2877	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
30		25or6to4.x	. 2 ⊢ (𝜑 → 𝑋 ∈ ℂ)
31		df-dec 12708	. . . 4 ⊢ ;25 = (((9 + 1) · 2) + 5)
32	9, 2	addcli 11211	. . . . . 6 ⊢ (9 + 1) ∈ ℂ
33	32, 16	mulcli 11212	. . . . 5 ⊢ ((9 + 1) · 2) ∈ ℂ
34	33, 11	addcli 11211	. . . 4 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
35	31, 34	eqeltri 2865	. . 3 ⊢ ;25 ∈ ℂ
36	35	a1i 11	. 2 ⊢ (𝜑 → ;25 ∈ ℂ)
37		6cn 12328	. . . 4 ⊢ 6 ∈ ℂ
38		4cn 12322	. . . 4 ⊢ 4 ∈ ℂ
39		4ne0 12348	. . . 4 ⊢ 4 ≠ 0
40	37, 38, 39	divcli 11953	. . 3 ⊢ (6 / 4) ∈ ℂ
41	40	a1i 11	. 2 ⊢ (𝜑 → (6 / 4) ∈ ℂ)
42		df-dec 12708	. . . . . . . . . . 11 ⊢ ;25 = (((9 + 1) · 2) + 5)
43	9, 2	addcli 11211	. . . . . . . . . . . . 13 ⊢ (9 + 1) ∈ ℂ
44	43, 16	mulcli 11212	. . . . . . . . . . . 12 ⊢ ((9 + 1) · 2) ∈ ℂ
45	44, 11	addcli 11211	. . . . . . . . . . 11 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
46	42, 45	eqeltri 2865	. . . . . . . . . 10 ⊢ ;25 ∈ ℂ
47	46, 16, 17	divcan4i 11958	. . . . . . . . 9 ⊢ ((;25 · 2) / 2) = ;25
48		2nn0 12517	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ0
49		5nn0 12520	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ0
50		eqid 2769	. . . . . . . . . . 11 ⊢ ;25 = ;25
51		0nn0 12515	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ0
52		1nn0 12516	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
53		2t2e4 12400	. . . . . . . . . . . . 13 ⊢ (2 · 2) = 4
54	53	oveq1i 7418	. . . . . . . . . . . 12 ⊢ ((2 · 2) + 1) = (4 + 1)
55		4p1e5 12382	. . . . . . . . . . . 12 ⊢ (4 + 1) = 5
56	54, 55	eqtri 2792	. . . . . . . . . . 11 ⊢ ((2 · 2) + 1) = 5
57		5t2e10 12812	. . . . . . . . . . 11 ⊢ (5 · 2) = ;10
58	48, 48, 49, 50, 51, 52, 56, 57	decmul1c 12777	. . . . . . . . . 10 ⊢ (;25 · 2) = ;50
59	58	oveq1i 7418	. . . . . . . . 9 ⊢ ((;25 · 2) / 2) = (;50 / 2)
60	47, 59	eqtr3i 2794	. . . . . . . 8 ⊢ ;25 = (;50 / 2)
61		6t2e12 12816	. . . . . . . . . 10 ⊢ (6 · 2) = ;12
62		4t3e12 12810	. . . . . . . . . . 11 ⊢ (4 · 3) = ;12
63	38, 13, 62	mulcomli 11214	. . . . . . . . . 10 ⊢ (3 · 4) = ;12
64	61, 63	eqtr4i 2795	. . . . . . . . 9 ⊢ (6 · 2) = (3 · 4)
65	37, 13	pm3.2i 475	. . . . . . . . . . 11 ⊢ (6 ∈ ℂ ∧ 3 ∈ ℂ)
66	38, 39	pm3.2i 475	. . . . . . . . . . . 12 ⊢ (4 ∈ ℂ ∧ 4 ≠ 0)
67		2cnne0 12449	. . . . . . . . . . . 12 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
68	66, 67	pm3.2i 475	. . . . . . . . . . 11 ⊢ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))
69	65, 68	pm3.2i 475	. . . . . . . . . 10 ⊢ ((6 ∈ ℂ ∧ 3 ∈ ℂ) ∧ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)))
70		divmuleq 11916	. . . . . . . . . 10 ⊢ (((6 ∈ ℂ ∧ 3 ∈ ℂ) ∧ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))) → ((6 / 4) = (3 / 2) ↔ (6 · 2) = (3 · 4)))
71	69, 70	ax-mp 5	. . . . . . . . 9 ⊢ ((6 / 4) = (3 / 2) ↔ (6 · 2) = (3 · 4))
72	64, 71	mpbir 234	. . . . . . . 8 ⊢ (6 / 4) = (3 / 2)
73	60, 72	oveq12i 7420	. . . . . . 7 ⊢ (;25 + (6 / 4)) = ((;50 / 2) + (3 / 2))
74		dfdec10 12710	. . . . . . . . . 10 ⊢ ;53 = ((;10 · 5) + 3)
75	49	dec0u 12733	. . . . . . . . . . 11 ⊢ (;10 · 5) = ;50
76	75	oveq1i 7418	. . . . . . . . . 10 ⊢ ((;10 · 5) + 3) = (;50 + 3)
77	74, 76	eqtri 2792	. . . . . . . . 9 ⊢ ;53 = (;50 + 3)
78	77	oveq1i 7418	. . . . . . . 8 ⊢ (;53 / 2) = ((;50 + 3) / 2)
79		df-dec 12708	. . . . . . . . . 10 ⊢ ;50 = (((9 + 1) · 5) + 0)
80	9, 2	addcli 11211	. . . . . . . . . . . 12 ⊢ (9 + 1) ∈ ℂ
81	80, 11	mulcli 11212	. . . . . . . . . . 11 ⊢ ((9 + 1) · 5) ∈ ℂ
82		0cn 11194	. . . . . . . . . . 11 ⊢ 0 ∈ ℂ
83	81, 82	addcli 11211	. . . . . . . . . 10 ⊢ (((9 + 1) · 5) + 0) ∈ ℂ
84	79, 83	eqeltri 2865	. . . . . . . . 9 ⊢ ;50 ∈ ℂ
85	84, 13, 16, 17	divdiri 11968	. . . . . . . 8 ⊢ ((;50 + 3) / 2) = ((;50 / 2) + (3 / 2))
86	78, 85	eqtri 2792	. . . . . . 7 ⊢ (;53 / 2) = ((;50 / 2) + (3 / 2))
87	73, 86	eqtr4i 2795	. . . . . 6 ⊢ (;25 + (6 / 4)) = (;53 / 2)
88		df-dec 12708	. . . . . . . 8 ⊢ ;53 = (((9 + 1) · 5) + 3)
89	9, 2	addcli 11211	. . . . . . . . . 10 ⊢ (9 + 1) ∈ ℂ
90	89, 11	mulcli 11212	. . . . . . . . 9 ⊢ ((9 + 1) · 5) ∈ ℂ
91	90, 13	addcli 11211	. . . . . . . 8 ⊢ (((9 + 1) · 5) + 3) ∈ ℂ
92	88, 91	eqeltri 2865	. . . . . . 7 ⊢ ;53 ∈ ℂ
93	92, 16, 17	divcli 11953	. . . . . 6 ⊢ (;53 / 2) ∈ ℂ
94	87, 93	eqeltri 2865	. . . . 5 ⊢ (;25 + (6 / 4)) ∈ ℂ
95	94	negnegi 11524	. . . 4 ⊢ --(;25 + (6 / 4)) = (;25 + (6 / 4))
96		df-dec 12708	. . . . . . . . . . . 12 ⊢ ;25 = (((9 + 1) · 2) + 5)
97	9, 2	addcli 11211	. . . . . . . . . . . . . 14 ⊢ (9 + 1) ∈ ℂ
98	97, 16	mulcli 11212	. . . . . . . . . . . . 13 ⊢ ((9 + 1) · 2) ∈ ℂ
99	98, 11	addcli 11211	. . . . . . . . . . . 12 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
100	96, 99	eqeltri 2865	. . . . . . . . . . 11 ⊢ ;25 ∈ ℂ
101	100, 16, 17	divcan4i 11958	. . . . . . . . . 10 ⊢ ((;25 · 2) / 2) = ;25
102		eqid 2769	. . . . . . . . . . . 12 ⊢ ;25 = ;25
103	53	oveq1i 7418	. . . . . . . . . . . . 13 ⊢ ((2 · 2) + 1) = (4 + 1)
104	103, 55	eqtri 2792	. . . . . . . . . . . 12 ⊢ ((2 · 2) + 1) = 5
105	48, 48, 49, 102, 51, 52, 104, 57	decmul1c 12777	. . . . . . . . . . 11 ⊢ (;25 · 2) = ;50
106	105	oveq1i 7418	. . . . . . . . . 10 ⊢ ((;25 · 2) / 2) = (;50 / 2)
107	101, 106	eqtr3i 2794	. . . . . . . . 9 ⊢ ;25 = (;50 / 2)
108	38, 13, 62	mulcomli 11214	. . . . . . . . . . 11 ⊢ (3 · 4) = ;12
109	61, 108	eqtr4i 2795	. . . . . . . . . 10 ⊢ (6 · 2) = (3 · 4)
110	37, 13	pm3.2i 475	. . . . . . . . . . . 12 ⊢ (6 ∈ ℂ ∧ 3 ∈ ℂ)
111	38, 39	pm3.2i 475	. . . . . . . . . . . . 13 ⊢ (4 ∈ ℂ ∧ 4 ≠ 0)
112	111, 67	pm3.2i 475	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))
113	110, 112	pm3.2i 475	. . . . . . . . . . 11 ⊢ ((6 ∈ ℂ ∧ 3 ∈ ℂ) ∧ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)))
114		divmuleq 11916	. . . . . . . . . . 11 ⊢ (((6 ∈ ℂ ∧ 3 ∈ ℂ) ∧ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))) → ((6 / 4) = (3 / 2) ↔ (6 · 2) = (3 · 4)))
115	113, 114	ax-mp 5	. . . . . . . . . 10 ⊢ ((6 / 4) = (3 / 2) ↔ (6 · 2) = (3 · 4))
116	109, 115	mpbir 234	. . . . . . . . 9 ⊢ (6 / 4) = (3 / 2)
117	107, 116	oveq12i 7420	. . . . . . . 8 ⊢ (;25 + (6 / 4)) = ((;50 / 2) + (3 / 2))
118		dfdec10 12710	. . . . . . . . . . 11 ⊢ ;53 = ((;10 · 5) + 3)
119	49	dec0u 12733	. . . . . . . . . . . 12 ⊢ (;10 · 5) = ;50
120	119	oveq1i 7418	. . . . . . . . . . 11 ⊢ ((;10 · 5) + 3) = (;50 + 3)
121	118, 120	eqtri 2792	. . . . . . . . . 10 ⊢ ;53 = (;50 + 3)
122	121	oveq1i 7418	. . . . . . . . 9 ⊢ (;53 / 2) = ((;50 + 3) / 2)
123		df-dec 12708	. . . . . . . . . . 11 ⊢ ;50 = (((9 + 1) · 5) + 0)
124	9, 2	addcli 11211	. . . . . . . . . . . . 13 ⊢ (9 + 1) ∈ ℂ
125	124, 11	mulcli 11212	. . . . . . . . . . . 12 ⊢ ((9 + 1) · 5) ∈ ℂ
126	125, 82	addcli 11211	. . . . . . . . . . 11 ⊢ (((9 + 1) · 5) + 0) ∈ ℂ
127	123, 126	eqeltri 2865	. . . . . . . . . 10 ⊢ ;50 ∈ ℂ
128	127, 13, 16, 17	divdiri 11968	. . . . . . . . 9 ⊢ ((;50 + 3) / 2) = ((;50 / 2) + (3 / 2))
129	122, 128	eqtri 2792	. . . . . . . 8 ⊢ (;53 / 2) = ((;50 / 2) + (3 / 2))
130	117, 129	eqtr4i 2795	. . . . . . 7 ⊢ (;25 + (6 / 4)) = (;53 / 2)
131	130	negeqi 11446	. . . . . 6 ⊢ -(;25 + (6 / 4)) = -(;53 / 2)
132		df-dec 12708	. . . . . . . . . 10 ⊢ ;53 = (((9 + 1) · 5) + 3)
133	9, 2	addcli 11211	. . . . . . . . . . . 12 ⊢ (9 + 1) ∈ ℂ
134	133, 11	mulcli 11212	. . . . . . . . . . 11 ⊢ ((9 + 1) · 5) ∈ ℂ
135	134, 13	addcli 11211	. . . . . . . . . 10 ⊢ (((9 + 1) · 5) + 3) ∈ ℂ
136	132, 135	eqeltri 2865	. . . . . . . . 9 ⊢ ;53 ∈ ℂ
137	136, 16, 17	divcli 11953	. . . . . . . 8 ⊢ (;53 / 2) ∈ ℂ
138	137	negcli 11522	. . . . . . 7 ⊢ -(;53 / 2) ∈ ℂ
139	138	div1i 11939	. . . . . 6 ⊢ (-(;53 / 2) / 1) = -(;53 / 2)
140	131, 139	eqtr4i 2795	. . . . 5 ⊢ -(;25 + (6 / 4)) = (-(;53 / 2) / 1)
141	140	negeqi 11446	. . . 4 ⊢ --(;25 + (6 / 4)) = -(-(;53 / 2) / 1)
142	95, 141	eqtr3i 2794	. . 3 ⊢ (;25 + (6 / 4)) = -(-(;53 / 2) / 1)
143	7, 1	oveq12d 7426	. . . 4 ⊢ (𝜑 → (𝐵 / 𝐴) = (-(;53 / 2) / 1))
144	143	negeqd 11447	. . 3 ⊢ (𝜑 → -(𝐵 / 𝐴) = -(-(;53 / 2) / 1))
145	142, 144	eqtr4id 2823	. 2 ⊢ (𝜑 → (;25 + (6 / 4)) = -(𝐵 / 𝐴))
146		df-dec 12708	. . . . . . 7 ⊢ ;75 = (((9 + 1) · 7) + 5)
147	9, 2	addcli 11211	. . . . . . . . 9 ⊢ (9 + 1) ∈ ℂ
148	147, 24	mulcli 11212	. . . . . . . 8 ⊢ ((9 + 1) · 7) ∈ ℂ
149	148, 11	addcli 11211	. . . . . . 7 ⊢ (((9 + 1) · 7) + 5) ∈ ℂ
150	146, 149	eqeltri 2865	. . . . . 6 ⊢ ;75 ∈ ℂ
151	150, 16, 17	divcli 11953	. . . . 5 ⊢ (;75 / 2) ∈ ℂ
152	151	div1i 11939	. . . 4 ⊢ ((;75 / 2) / 1) = (;75 / 2)
153		df-dec 12708	. . . . . . 7 ⊢ ;25 = (((9 + 1) · 2) + 5)
154	9, 2	addcli 11211	. . . . . . . . 9 ⊢ (9 + 1) ∈ ℂ
155	154, 16	mulcli 11212	. . . . . . . 8 ⊢ ((9 + 1) · 2) ∈ ℂ
156	155, 11	addcli 11211	. . . . . . 7 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
157	153, 156	eqeltri 2865	. . . . . 6 ⊢ ;25 ∈ ℂ
158	157, 13, 16, 17	divassi 11967	. . . . 5 ⊢ ((;25 · 3) / 2) = (;25 · (3 / 2))
159		3nn0 12518	. . . . . . 7 ⊢ 3 ∈ ℕ0
160		eqid 2769	. . . . . . 7 ⊢ ;25 = ;25
161		2t3e6 12403	. . . . . . . . 9 ⊢ (2 · 3) = 6
162	161	oveq1i 7418	. . . . . . . 8 ⊢ ((2 · 3) + 1) = (6 + 1)
163		6p1e7 12384	. . . . . . . 8 ⊢ (6 + 1) = 7
164	162, 163	eqtri 2792	. . . . . . 7 ⊢ ((2 · 3) + 1) = 7
165		5t3e15 12813	. . . . . . 7 ⊢ (5 · 3) = ;15
166	159, 48, 49, 160, 49, 52, 164, 165	decmul1c 12777	. . . . . 6 ⊢ (;25 · 3) = ;75
167	166	oveq1i 7418	. . . . 5 ⊢ ((;25 · 3) / 2) = (;75 / 2)
168	158, 167	eqtr3i 2794	. . . 4 ⊢ (;25 · (3 / 2)) = (;75 / 2)
169	38, 13, 62	mulcomli 11214	. . . . . . . 8 ⊢ (3 · 4) = ;12
170	61, 169	eqtr4i 2795	. . . . . . 7 ⊢ (6 · 2) = (3 · 4)
171	37, 13	pm3.2i 475	. . . . . . . . 9 ⊢ (6 ∈ ℂ ∧ 3 ∈ ℂ)
172	38, 39	pm3.2i 475	. . . . . . . . . 10 ⊢ (4 ∈ ℂ ∧ 4 ≠ 0)
173	172, 67	pm3.2i 475	. . . . . . . . 9 ⊢ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))
174	171, 173	pm3.2i 475	. . . . . . . 8 ⊢ ((6 ∈ ℂ ∧ 3 ∈ ℂ) ∧ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)))
175		divmuleq 11916	. . . . . . . 8 ⊢ (((6 ∈ ℂ ∧ 3 ∈ ℂ) ∧ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))) → ((6 / 4) = (3 / 2) ↔ (6 · 2) = (3 · 4)))
176	174, 175	ax-mp 5	. . . . . . 7 ⊢ ((6 / 4) = (3 / 2) ↔ (6 · 2) = (3 · 4))
177	170, 176	mpbir 234	. . . . . 6 ⊢ (6 / 4) = (3 / 2)
178	177	oveq2i 7419	. . . . 5 ⊢ (;25 · (6 / 4)) = (;25 · (3 / 2))
179	178	eqcomi 2778	. . . 4 ⊢ (;25 · (3 / 2)) = (;25 · (6 / 4))
180	152, 168, 179	3eqtr2ri 2799	. . 3 ⊢ (;25 · (6 / 4)) = ((;75 / 2) / 1)
181	21, 1	oveq12d 7426	. . 3 ⊢ (𝜑 → (𝐶 / 𝐴) = ((;75 / 2) / 1))
182	180, 181	eqtr4id 2823	. 2 ⊢ (𝜑 → (;25 · (6 / 4)) = (𝐶 / 𝐴))
183	3, 6, 20, 29, 30, 36, 41, 145, 182	quadfac 42857	1 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ;25 ∨ 𝑋 = (6 / 4))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  (class class class)co 7408  ℂcc 11094  0cc0 11096  1c1 11097   + caddc 11099   · cmul 11101  -cneg 11438   / cdiv 11867  2c2 12291  3c3 12292  4c4 12293  5c5 12294  6c6 12295  7c7 12296  9c9 12298  ;cdc 12707  ↑cexp 14093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-cnex 11152  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172  ax-pre-mulgt0 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6300  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-sub 11439  df-neg 11440  df-div 11868  df-nn 12230  df-2 12299  df-3 12300  df-4 12301  df-5 12302  df-6 12303  df-7 12304  df-8 12305  df-9 12306  df-n0 12501  df-z 12588  df-dec 12708  df-uz 12859  df-seq 14034  df-exp 14094

This theorem is referenced by: (None)