Theorem 25or6to4 43236

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 11251	. . 3 ⊢ 1 ∈ ℂ
3	1, 2	eqeltrdi 2869	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		ax-1ne0 11262	. . . 4 ⊢ 1 ≠ 0
5	4	a1i 11	. . 3 ⊢ (𝜑 → 1 ≠ 0)
6	1, 5	eqnetrd 3023	. 2 ⊢ (𝜑 → 𝐴 ≠ 0)
7		25or6to4.b	. . 3 ⊢ (𝜑 → 𝐵 = -(;53 / 2))
8		df-dec 12808	. . . . . 6 ⊢ ;53 = (((9 + 1) · 5) + 3)
9		9cn 12436	. . . . . . . . 9 ⊢ 9 ∈ ℂ
10	9, 2	addcli 11308	. . . . . . . 8 ⊢ (9 + 1) ∈ ℂ
11		5cn 12424	. . . . . . . 8 ⊢ 5 ∈ ℂ
12	10, 11	mulcli 11309	. . . . . . 7 ⊢ ((9 + 1) · 5) ∈ ℂ
13		3cn 12417	. . . . . . 7 ⊢ 3 ∈ ℂ
14	12, 13	addcli 11308	. . . . . 6 ⊢ (((9 + 1) · 5) + 3) ∈ ℂ
15	8, 14	eqeltri 2857	. . . . 5 ⊢ ;53 ∈ ℂ
16		2cn 12411	. . . . 5 ⊢ 2 ∈ ℂ
17		2ne0 12442	. . . . 5 ⊢ 2 ≠ 0
18	15, 16, 17	divcli 12052	. . . 4 ⊢ (;53 / 2) ∈ ℂ
19	18	negcli 11619	. . 3 ⊢ -(;53 / 2) ∈ ℂ
20	7, 19	eqeltrdi 2869	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
21		25or6to4.c	. . 3 ⊢ (𝜑 → 𝐶 = (;75 / 2))
22		df-dec 12808	. . . . 5 ⊢ ;75 = (((9 + 1) · 7) + 5)
23	9, 2	addcli 11308	. . . . . . 7 ⊢ (9 + 1) ∈ ℂ
24		7cn 12430	. . . . . . 7 ⊢ 7 ∈ ℂ
25	23, 24	mulcli 11309	. . . . . 6 ⊢ ((9 + 1) · 7) ∈ ℂ
26	25, 11	addcli 11308	. . . . 5 ⊢ (((9 + 1) · 7) + 5) ∈ ℂ
27	22, 26	eqeltri 2857	. . . 4 ⊢ ;75 ∈ ℂ
28	27, 16, 17	divcli 12052	. . 3 ⊢ (;75 / 2) ∈ ℂ
29	21, 28	eqeltrdi 2869	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
30		25or6to4.x	. 2 ⊢ (𝜑 → 𝑋 ∈ ℂ)
31		df-dec 12808	. . . 4 ⊢ ;25 = (((9 + 1) · 2) + 5)
32	9, 2	addcli 11308	. . . . . 6 ⊢ (9 + 1) ∈ ℂ
33	32, 16	mulcli 11309	. . . . 5 ⊢ ((9 + 1) · 2) ∈ ℂ
34	33, 11	addcli 11308	. . . 4 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
35	31, 34	eqeltri 2857	. . 3 ⊢ ;25 ∈ ℂ
36	35	a1i 11	. 2 ⊢ (𝜑 → ;25 ∈ ℂ)
37		6cn 12427	. . . 4 ⊢ 6 ∈ ℂ
38		4cn 12421	. . . 4 ⊢ 4 ∈ ℂ
39		4ne0 12447	. . . 4 ⊢ 4 ≠ 0
40	37, 38, 39	divcli 12052	. . 3 ⊢ (6 / 4) ∈ ℂ
41	40	a1i 11	. 2 ⊢ (𝜑 → (6 / 4) ∈ ℂ)
42		df-dec 12808	. . . . . . . . . . 11 ⊢ ;25 = (((9 + 1) · 2) + 5)
43	9, 2	addcli 11308	. . . . . . . . . . . . 13 ⊢ (9 + 1) ∈ ℂ
44	43, 16	mulcli 11309	. . . . . . . . . . . 12 ⊢ ((9 + 1) · 2) ∈ ℂ
45	44, 11	addcli 11308	. . . . . . . . . . 11 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
46	42, 45	eqeltri 2857	. . . . . . . . . 10 ⊢ ;25 ∈ ℂ
47	46, 16, 17	divcan4i 12057	. . . . . . . . 9 ⊢ ((;25 · 2) / 2) = ;25
48		2nn0 12616	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ0
49		5nn0 12619	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ0
50		eqid 2761	. . . . . . . . . . 11 ⊢ ;25 = ;25
51		0nn0 12614	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ0
52		1nn0 12615	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
53		2t2e4 12499	. . . . . . . . . . . . 13 ⊢ (2 · 2) = 4
54	53	oveq1i 7428	. . . . . . . . . . . 12 ⊢ ((2 · 2) + 1) = (4 + 1)
55		4p1e5 12481	. . . . . . . . . . . 12 ⊢ (4 + 1) = 5
56	54, 55	eqtri 2784	. . . . . . . . . . 11 ⊢ ((2 · 2) + 1) = 5
57		5t2e10 12912	. . . . . . . . . . 11 ⊢ (5 · 2) = ;10
58	48, 48, 49, 50, 51, 52, 56, 57	decmul1c 12877	. . . . . . . . . 10 ⊢ (;25 · 2) = ;50
59	58	oveq1i 7428	. . . . . . . . 9 ⊢ ((;25 · 2) / 2) = (;50 / 2)
60	47, 59	eqtr3i 2786	. . . . . . . 8 ⊢ ;25 = (;50 / 2)
61		6t2e12 12916	. . . . . . . . . 10 ⊢ (6 · 2) = ;12
62		4t3e12 12910	. . . . . . . . . . 11 ⊢ (4 · 3) = ;12
63	38, 13, 62	mulcomli 11311	. . . . . . . . . 10 ⊢ (3 · 4) = ;12
64	61, 63	eqtr4i 2787	. . . . . . . . 9 ⊢ (6 · 2) = (3 · 4)
65	37, 13	pm3.2i 476	. . . . . . . . . . 11 ⊢ (6 ∈ ℂ ∧ 3 ∈ ℂ)
66	38, 39	pm3.2i 476	. . . . . . . . . . . 12 ⊢ (4 ∈ ℂ ∧ 4 ≠ 0)
67		2cnne0 12548	. . . . . . . . . . . 12 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
68	66, 67	pm3.2i 476	. . . . . . . . . . 11 ⊢ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))
69	65, 68	pm3.2i 476	. . . . . . . . . 10 ⊢ ((6 ∈ ℂ ∧ 3 ∈ ℂ) ∧ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)))
70		divmuleq 12015	. . . . . . . . . 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 7430	. . . . . . 7 ⊢ (;25 + (6 / 4)) = ((;50 / 2) + (3 / 2))
74		dfdec10 12810	. . . . . . . . . 10 ⊢ ;53 = ((;10 · 5) + 3)
75	49	dec0u 12833	. . . . . . . . . . 11 ⊢ (;10 · 5) = ;50
76	75	oveq1i 7428	. . . . . . . . . 10 ⊢ ((;10 · 5) + 3) = (;50 + 3)
77	74, 76	eqtri 2784	. . . . . . . . 9 ⊢ ;53 = (;50 + 3)
78	77	oveq1i 7428	. . . . . . . 8 ⊢ (;53 / 2) = ((;50 + 3) / 2)
79		df-dec 12808	. . . . . . . . . 10 ⊢ ;50 = (((9 + 1) · 5) + 0)
80	9, 2	addcli 11308	. . . . . . . . . . . 12 ⊢ (9 + 1) ∈ ℂ
81	80, 11	mulcli 11309	. . . . . . . . . . 11 ⊢ ((9 + 1) · 5) ∈ ℂ
82		0cn 11291	. . . . . . . . . . 11 ⊢ 0 ∈ ℂ
83	81, 82	addcli 11308	. . . . . . . . . 10 ⊢ (((9 + 1) · 5) + 0) ∈ ℂ
84	79, 83	eqeltri 2857	. . . . . . . . 9 ⊢ ;50 ∈ ℂ
85	84, 13, 16, 17	divdiri 12067	. . . . . . . 8 ⊢ ((;50 + 3) / 2) = ((;50 / 2) + (3 / 2))
86	78, 85	eqtri 2784	. . . . . . 7 ⊢ (;53 / 2) = ((;50 / 2) + (3 / 2))
87	73, 86	eqtr4i 2787	. . . . . 6 ⊢ (;25 + (6 / 4)) = (;53 / 2)
88		df-dec 12808	. . . . . . . 8 ⊢ ;53 = (((9 + 1) · 5) + 3)
89	9, 2	addcli 11308	. . . . . . . . . 10 ⊢ (9 + 1) ∈ ℂ
90	89, 11	mulcli 11309	. . . . . . . . 9 ⊢ ((9 + 1) · 5) ∈ ℂ
91	90, 13	addcli 11308	. . . . . . . 8 ⊢ (((9 + 1) · 5) + 3) ∈ ℂ
92	88, 91	eqeltri 2857	. . . . . . 7 ⊢ ;53 ∈ ℂ
93	92, 16, 17	divcli 12052	. . . . . 6 ⊢ (;53 / 2) ∈ ℂ
94	87, 93	eqeltri 2857	. . . . 5 ⊢ (;25 + (6 / 4)) ∈ ℂ
95	94	negnegi 11621	. . . 4 ⊢ --(;25 + (6 / 4)) = (;25 + (6 / 4))
96		df-dec 12808	. . . . . . . . . . . 12 ⊢ ;25 = (((9 + 1) · 2) + 5)
97	9, 2	addcli 11308	. . . . . . . . . . . . . 14 ⊢ (9 + 1) ∈ ℂ
98	97, 16	mulcli 11309	. . . . . . . . . . . . 13 ⊢ ((9 + 1) · 2) ∈ ℂ
99	98, 11	addcli 11308	. . . . . . . . . . . 12 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
100	96, 99	eqeltri 2857	. . . . . . . . . . 11 ⊢ ;25 ∈ ℂ
101	100, 16, 17	divcan4i 12057	. . . . . . . . . 10 ⊢ ((;25 · 2) / 2) = ;25
102		eqid 2761	. . . . . . . . . . . 12 ⊢ ;25 = ;25
103	53	oveq1i 7428	. . . . . . . . . . . . 13 ⊢ ((2 · 2) + 1) = (4 + 1)
104	103, 55	eqtri 2784	. . . . . . . . . . . 12 ⊢ ((2 · 2) + 1) = 5
105	48, 48, 49, 102, 51, 52, 104, 57	decmul1c 12877	. . . . . . . . . . 11 ⊢ (;25 · 2) = ;50
106	105	oveq1i 7428	. . . . . . . . . 10 ⊢ ((;25 · 2) / 2) = (;50 / 2)
107	101, 106	eqtr3i 2786	. . . . . . . . 9 ⊢ ;25 = (;50 / 2)
108	38, 13, 62	mulcomli 11311	. . . . . . . . . . 11 ⊢ (3 · 4) = ;12
109	61, 108	eqtr4i 2787	. . . . . . . . . 10 ⊢ (6 · 2) = (3 · 4)
110	37, 13	pm3.2i 476	. . . . . . . . . . . 12 ⊢ (6 ∈ ℂ ∧ 3 ∈ ℂ)
111	38, 39	pm3.2i 476	. . . . . . . . . . . . 13 ⊢ (4 ∈ ℂ ∧ 4 ≠ 0)
112	111, 67	pm3.2i 476	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))
113	110, 112	pm3.2i 476	. . . . . . . . . . 11 ⊢ ((6 ∈ ℂ ∧ 3 ∈ ℂ) ∧ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)))
114		divmuleq 12015	. . . . . . . . . . 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 7430	. . . . . . . 8 ⊢ (;25 + (6 / 4)) = ((;50 / 2) + (3 / 2))
118		dfdec10 12810	. . . . . . . . . . 11 ⊢ ;53 = ((;10 · 5) + 3)
119	49	dec0u 12833	. . . . . . . . . . . 12 ⊢ (;10 · 5) = ;50
120	119	oveq1i 7428	. . . . . . . . . . 11 ⊢ ((;10 · 5) + 3) = (;50 + 3)
121	118, 120	eqtri 2784	. . . . . . . . . 10 ⊢ ;53 = (;50 + 3)
122	121	oveq1i 7428	. . . . . . . . 9 ⊢ (;53 / 2) = ((;50 + 3) / 2)
123		df-dec 12808	. . . . . . . . . . 11 ⊢ ;50 = (((9 + 1) · 5) + 0)
124	9, 2	addcli 11308	. . . . . . . . . . . . 13 ⊢ (9 + 1) ∈ ℂ
125	124, 11	mulcli 11309	. . . . . . . . . . . 12 ⊢ ((9 + 1) · 5) ∈ ℂ
126	125, 82	addcli 11308	. . . . . . . . . . 11 ⊢ (((9 + 1) · 5) + 0) ∈ ℂ
127	123, 126	eqeltri 2857	. . . . . . . . . 10 ⊢ ;50 ∈ ℂ
128	127, 13, 16, 17	divdiri 12067	. . . . . . . . 9 ⊢ ((;50 + 3) / 2) = ((;50 / 2) + (3 / 2))
129	122, 128	eqtri 2784	. . . . . . . 8 ⊢ (;53 / 2) = ((;50 / 2) + (3 / 2))
130	117, 129	eqtr4i 2787	. . . . . . 7 ⊢ (;25 + (6 / 4)) = (;53 / 2)
131	130	negeqi 11543	. . . . . 6 ⊢ -(;25 + (6 / 4)) = -(;53 / 2)
132		df-dec 12808	. . . . . . . . . 10 ⊢ ;53 = (((9 + 1) · 5) + 3)
133	9, 2	addcli 11308	. . . . . . . . . . . 12 ⊢ (9 + 1) ∈ ℂ
134	133, 11	mulcli 11309	. . . . . . . . . . 11 ⊢ ((9 + 1) · 5) ∈ ℂ
135	134, 13	addcli 11308	. . . . . . . . . 10 ⊢ (((9 + 1) · 5) + 3) ∈ ℂ
136	132, 135	eqeltri 2857	. . . . . . . . 9 ⊢ ;53 ∈ ℂ
137	136, 16, 17	divcli 12052	. . . . . . . 8 ⊢ (;53 / 2) ∈ ℂ
138	137	negcli 11619	. . . . . . 7 ⊢ -(;53 / 2) ∈ ℂ
139	138	div1i 12038	. . . . . 6 ⊢ (-(;53 / 2) / 1) = -(;53 / 2)
140	131, 139	eqtr4i 2787	. . . . 5 ⊢ -(;25 + (6 / 4)) = (-(;53 / 2) / 1)
141	140	negeqi 11543	. . . 4 ⊢ --(;25 + (6 / 4)) = -(-(;53 / 2) / 1)
142	95, 141	eqtr3i 2786	. . 3 ⊢ (;25 + (6 / 4)) = -(-(;53 / 2) / 1)
143	7, 1	oveq12d 7436	. . . 4 ⊢ (𝜑 → (𝐵 / 𝐴) = (-(;53 / 2) / 1))
144	143	negeqd 11544	. . 3 ⊢ (𝜑 → -(𝐵 / 𝐴) = -(-(;53 / 2) / 1))
145	142, 144	eqtr4id 2815	. 2 ⊢ (𝜑 → (;25 + (6 / 4)) = -(𝐵 / 𝐴))
146		df-dec 12808	. . . . . . 7 ⊢ ;75 = (((9 + 1) · 7) + 5)
147	9, 2	addcli 11308	. . . . . . . . 9 ⊢ (9 + 1) ∈ ℂ
148	147, 24	mulcli 11309	. . . . . . . 8 ⊢ ((9 + 1) · 7) ∈ ℂ
149	148, 11	addcli 11308	. . . . . . 7 ⊢ (((9 + 1) · 7) + 5) ∈ ℂ
150	146, 149	eqeltri 2857	. . . . . 6 ⊢ ;75 ∈ ℂ
151	150, 16, 17	divcli 12052	. . . . 5 ⊢ (;75 / 2) ∈ ℂ
152	151	div1i 12038	. . . 4 ⊢ ((;75 / 2) / 1) = (;75 / 2)
153		df-dec 12808	. . . . . . 7 ⊢ ;25 = (((9 + 1) · 2) + 5)
154	9, 2	addcli 11308	. . . . . . . . 9 ⊢ (9 + 1) ∈ ℂ
155	154, 16	mulcli 11309	. . . . . . . 8 ⊢ ((9 + 1) · 2) ∈ ℂ
156	155, 11	addcli 11308	. . . . . . 7 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
157	153, 156	eqeltri 2857	. . . . . 6 ⊢ ;25 ∈ ℂ
158	157, 13, 16, 17	divassi 12066	. . . . 5 ⊢ ((;25 · 3) / 2) = (;25 · (3 / 2))
159		3nn0 12617	. . . . . . 7 ⊢ 3 ∈ ℕ0
160		eqid 2761	. . . . . . 7 ⊢ ;25 = ;25
161		2t3e6 12502	. . . . . . . . 9 ⊢ (2 · 3) = 6
162	161	oveq1i 7428	. . . . . . . 8 ⊢ ((2 · 3) + 1) = (6 + 1)
163		6p1e7 12483	. . . . . . . 8 ⊢ (6 + 1) = 7
164	162, 163	eqtri 2784	. . . . . . 7 ⊢ ((2 · 3) + 1) = 7
165		5t3e15 12913	. . . . . . 7 ⊢ (5 · 3) = ;15
166	159, 48, 49, 160, 49, 52, 164, 165	decmul1c 12877	. . . . . 6 ⊢ (;25 · 3) = ;75
167	166	oveq1i 7428	. . . . 5 ⊢ ((;25 · 3) / 2) = (;75 / 2)
168	158, 167	eqtr3i 2786	. . . 4 ⊢ (;25 · (3 / 2)) = (;75 / 2)
169	38, 13, 62	mulcomli 11311	. . . . . . . 8 ⊢ (3 · 4) = ;12
170	61, 169	eqtr4i 2787	. . . . . . 7 ⊢ (6 · 2) = (3 · 4)
171	37, 13	pm3.2i 476	. . . . . . . . 9 ⊢ (6 ∈ ℂ ∧ 3 ∈ ℂ)
172	38, 39	pm3.2i 476	. . . . . . . . . 10 ⊢ (4 ∈ ℂ ∧ 4 ≠ 0)
173	172, 67	pm3.2i 476	. . . . . . . . 9 ⊢ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))
174	171, 173	pm3.2i 476	. . . . . . . 8 ⊢ ((6 ∈ ℂ ∧ 3 ∈ ℂ) ∧ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)))
175		divmuleq 12015	. . . . . . . 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 7429	. . . . 5 ⊢ (;25 · (6 / 4)) = (;25 · (3 / 2))
179	178	eqcomi 2770	. . . 4 ⊢ (;25 · (3 / 2)) = (;25 · (6 / 4))
180	152, 168, 179	3eqtr2ri 2791	. . 3 ⊢ (;25 · (6 / 4)) = ((;75 / 2) / 1)
181	21, 1	oveq12d 7436	. . 3 ⊢ (𝜑 → (𝐶 / 𝐴) = ((;75 / 2) / 1))
182	180, 181	eqtr4id 2815	. 2 ⊢ (𝜑 → (;25 · (6 / 4)) = (𝐶 / 𝐴))
183	3, 6, 20, 29, 30, 36, 41, 145, 182	quadfac 43235	1 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ;25 ∨ 𝑋 = (6 / 4))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  (class class class)co 7418  ℂcc 11191  0cc0 11193  1c1 11194   + caddc 11196   · cmul 11198  -cneg 11535   / cdiv 11966  2c2 12390  3c3 12391  4c4 12392  5c5 12393  6c6 12394  7c7 12395  9c9 12397  ;cdc 12807  ↑cexp 14197

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-div 11967  df-nn 12329  df-2 12398  df-3 12399  df-4 12400  df-5 12401  df-6 12402  df-7 12403  df-8 12404  df-9 12405  df-n0 12600  df-z 12687  df-dec 12808  df-uz 12959  df-seq 14138  df-exp 14198

This theorem is used by: (None)