Theorem 25or6to4 43072

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 11182	. . 3 ⊢ 1 ∈ ℂ
3	1, 2	eqeltrdi 2868	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		ax-1ne0 11193	. . . 4 ⊢ 1 ≠ 0
5	4	a1i 11	. . 3 ⊢ (𝜑 → 1 ≠ 0)
6	1, 5	eqnetrd 3022	. 2 ⊢ (𝜑 → 𝐴 ≠ 0)
7		25or6to4.b	. . 3 ⊢ (𝜑 → 𝐵 = -(;53 / 2))
8		df-dec 12737	. . . . . 6 ⊢ ;53 = (((9 + 1) · 5) + 3)
9		9cn 12365	. . . . . . . . 9 ⊢ 9 ∈ ℂ
10	9, 2	addcli 11239	. . . . . . . 8 ⊢ (9 + 1) ∈ ℂ
11		5cn 12353	. . . . . . . 8 ⊢ 5 ∈ ℂ
12	10, 11	mulcli 11240	. . . . . . 7 ⊢ ((9 + 1) · 5) ∈ ℂ
13		3cn 12346	. . . . . . 7 ⊢ 3 ∈ ℂ
14	12, 13	addcli 11239	. . . . . 6 ⊢ (((9 + 1) · 5) + 3) ∈ ℂ
15	8, 14	eqeltri 2856	. . . . 5 ⊢ ;53 ∈ ℂ
16		2cn 12340	. . . . 5 ⊢ 2 ∈ ℂ
17		2ne0 12371	. . . . 5 ⊢ 2 ≠ 0
18	15, 16, 17	divcli 11981	. . . 4 ⊢ (;53 / 2) ∈ ℂ
19	18	negcli 11550	. . 3 ⊢ -(;53 / 2) ∈ ℂ
20	7, 19	eqeltrdi 2868	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
21		25or6to4.c	. . 3 ⊢ (𝜑 → 𝐶 = (;75 / 2))
22		df-dec 12737	. . . . 5 ⊢ ;75 = (((9 + 1) · 7) + 5)
23	9, 2	addcli 11239	. . . . . . 7 ⊢ (9 + 1) ∈ ℂ
24		7cn 12359	. . . . . . 7 ⊢ 7 ∈ ℂ
25	23, 24	mulcli 11240	. . . . . 6 ⊢ ((9 + 1) · 7) ∈ ℂ
26	25, 11	addcli 11239	. . . . 5 ⊢ (((9 + 1) · 7) + 5) ∈ ℂ
27	22, 26	eqeltri 2856	. . . 4 ⊢ ;75 ∈ ℂ
28	27, 16, 17	divcli 11981	. . 3 ⊢ (;75 / 2) ∈ ℂ
29	21, 28	eqeltrdi 2868	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
30		25or6to4.x	. 2 ⊢ (𝜑 → 𝑋 ∈ ℂ)
31		df-dec 12737	. . . 4 ⊢ ;25 = (((9 + 1) · 2) + 5)
32	9, 2	addcli 11239	. . . . . 6 ⊢ (9 + 1) ∈ ℂ
33	32, 16	mulcli 11240	. . . . 5 ⊢ ((9 + 1) · 2) ∈ ℂ
34	33, 11	addcli 11239	. . . 4 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
35	31, 34	eqeltri 2856	. . 3 ⊢ ;25 ∈ ℂ
36	35	a1i 11	. 2 ⊢ (𝜑 → ;25 ∈ ℂ)
37		6cn 12356	. . . 4 ⊢ 6 ∈ ℂ
38		4cn 12350	. . . 4 ⊢ 4 ∈ ℂ
39		4ne0 12376	. . . 4 ⊢ 4 ≠ 0
40	37, 38, 39	divcli 11981	. . 3 ⊢ (6 / 4) ∈ ℂ
41	40	a1i 11	. 2 ⊢ (𝜑 → (6 / 4) ∈ ℂ)
42		df-dec 12737	. . . . . . . . . . 11 ⊢ ;25 = (((9 + 1) · 2) + 5)
43	9, 2	addcli 11239	. . . . . . . . . . . . 13 ⊢ (9 + 1) ∈ ℂ
44	43, 16	mulcli 11240	. . . . . . . . . . . 12 ⊢ ((9 + 1) · 2) ∈ ℂ
45	44, 11	addcli 11239	. . . . . . . . . . 11 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
46	42, 45	eqeltri 2856	. . . . . . . . . 10 ⊢ ;25 ∈ ℂ
47	46, 16, 17	divcan4i 11986	. . . . . . . . 9 ⊢ ((;25 · 2) / 2) = ;25
48		2nn0 12545	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ0
49		5nn0 12548	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ0
50		eqid 2760	. . . . . . . . . . 11 ⊢ ;25 = ;25
51		0nn0 12543	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ0
52		1nn0 12544	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
53		2t2e4 12428	. . . . . . . . . . . . 13 ⊢ (2 · 2) = 4
54	53	oveq1i 7423	. . . . . . . . . . . 12 ⊢ ((2 · 2) + 1) = (4 + 1)
55		4p1e5 12410	. . . . . . . . . . . 12 ⊢ (4 + 1) = 5
56	54, 55	eqtri 2783	. . . . . . . . . . 11 ⊢ ((2 · 2) + 1) = 5
57		5t2e10 12841	. . . . . . . . . . 11 ⊢ (5 · 2) = ;10
58	48, 48, 49, 50, 51, 52, 56, 57	decmul1c 12806	. . . . . . . . . 10 ⊢ (;25 · 2) = ;50
59	58	oveq1i 7423	. . . . . . . . 9 ⊢ ((;25 · 2) / 2) = (;50 / 2)
60	47, 59	eqtr3i 2785	. . . . . . . 8 ⊢ ;25 = (;50 / 2)
61		6t2e12 12845	. . . . . . . . . 10 ⊢ (6 · 2) = ;12
62		4t3e12 12839	. . . . . . . . . . 11 ⊢ (4 · 3) = ;12
63	38, 13, 62	mulcomli 11242	. . . . . . . . . 10 ⊢ (3 · 4) = ;12
64	61, 63	eqtr4i 2786	. . . . . . . . 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 12477	. . . . . . . . . . . 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 11944	. . . . . . . . . 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 7425	. . . . . . 7 ⊢ (;25 + (6 / 4)) = ((;50 / 2) + (3 / 2))
74		dfdec10 12739	. . . . . . . . . 10 ⊢ ;53 = ((;10 · 5) + 3)
75	49	dec0u 12762	. . . . . . . . . . 11 ⊢ (;10 · 5) = ;50
76	75	oveq1i 7423	. . . . . . . . . 10 ⊢ ((;10 · 5) + 3) = (;50 + 3)
77	74, 76	eqtri 2783	. . . . . . . . 9 ⊢ ;53 = (;50 + 3)
78	77	oveq1i 7423	. . . . . . . 8 ⊢ (;53 / 2) = ((;50 + 3) / 2)
79		df-dec 12737	. . . . . . . . . 10 ⊢ ;50 = (((9 + 1) · 5) + 0)
80	9, 2	addcli 11239	. . . . . . . . . . . 12 ⊢ (9 + 1) ∈ ℂ
81	80, 11	mulcli 11240	. . . . . . . . . . 11 ⊢ ((9 + 1) · 5) ∈ ℂ
82		0cn 11222	. . . . . . . . . . 11 ⊢ 0 ∈ ℂ
83	81, 82	addcli 11239	. . . . . . . . . 10 ⊢ (((9 + 1) · 5) + 0) ∈ ℂ
84	79, 83	eqeltri 2856	. . . . . . . . 9 ⊢ ;50 ∈ ℂ
85	84, 13, 16, 17	divdiri 11996	. . . . . . . 8 ⊢ ((;50 + 3) / 2) = ((;50 / 2) + (3 / 2))
86	78, 85	eqtri 2783	. . . . . . 7 ⊢ (;53 / 2) = ((;50 / 2) + (3 / 2))
87	73, 86	eqtr4i 2786	. . . . . 6 ⊢ (;25 + (6 / 4)) = (;53 / 2)
88		df-dec 12737	. . . . . . . 8 ⊢ ;53 = (((9 + 1) · 5) + 3)
89	9, 2	addcli 11239	. . . . . . . . . 10 ⊢ (9 + 1) ∈ ℂ
90	89, 11	mulcli 11240	. . . . . . . . 9 ⊢ ((9 + 1) · 5) ∈ ℂ
91	90, 13	addcli 11239	. . . . . . . 8 ⊢ (((9 + 1) · 5) + 3) ∈ ℂ
92	88, 91	eqeltri 2856	. . . . . . 7 ⊢ ;53 ∈ ℂ
93	92, 16, 17	divcli 11981	. . . . . 6 ⊢ (;53 / 2) ∈ ℂ
94	87, 93	eqeltri 2856	. . . . 5 ⊢ (;25 + (6 / 4)) ∈ ℂ
95	94	negnegi 11552	. . . 4 ⊢ --(;25 + (6 / 4)) = (;25 + (6 / 4))
96		df-dec 12737	. . . . . . . . . . . 12 ⊢ ;25 = (((9 + 1) · 2) + 5)
97	9, 2	addcli 11239	. . . . . . . . . . . . . 14 ⊢ (9 + 1) ∈ ℂ
98	97, 16	mulcli 11240	. . . . . . . . . . . . 13 ⊢ ((9 + 1) · 2) ∈ ℂ
99	98, 11	addcli 11239	. . . . . . . . . . . 12 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
100	96, 99	eqeltri 2856	. . . . . . . . . . 11 ⊢ ;25 ∈ ℂ
101	100, 16, 17	divcan4i 11986	. . . . . . . . . 10 ⊢ ((;25 · 2) / 2) = ;25
102		eqid 2760	. . . . . . . . . . . 12 ⊢ ;25 = ;25
103	53	oveq1i 7423	. . . . . . . . . . . . 13 ⊢ ((2 · 2) + 1) = (4 + 1)
104	103, 55	eqtri 2783	. . . . . . . . . . . 12 ⊢ ((2 · 2) + 1) = 5
105	48, 48, 49, 102, 51, 52, 104, 57	decmul1c 12806	. . . . . . . . . . 11 ⊢ (;25 · 2) = ;50
106	105	oveq1i 7423	. . . . . . . . . 10 ⊢ ((;25 · 2) / 2) = (;50 / 2)
107	101, 106	eqtr3i 2785	. . . . . . . . 9 ⊢ ;25 = (;50 / 2)
108	38, 13, 62	mulcomli 11242	. . . . . . . . . . 11 ⊢ (3 · 4) = ;12
109	61, 108	eqtr4i 2786	. . . . . . . . . 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 11944	. . . . . . . . . . 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 7425	. . . . . . . 8 ⊢ (;25 + (6 / 4)) = ((;50 / 2) + (3 / 2))
118		dfdec10 12739	. . . . . . . . . . 11 ⊢ ;53 = ((;10 · 5) + 3)
119	49	dec0u 12762	. . . . . . . . . . . 12 ⊢ (;10 · 5) = ;50
120	119	oveq1i 7423	. . . . . . . . . . 11 ⊢ ((;10 · 5) + 3) = (;50 + 3)
121	118, 120	eqtri 2783	. . . . . . . . . 10 ⊢ ;53 = (;50 + 3)
122	121	oveq1i 7423	. . . . . . . . 9 ⊢ (;53 / 2) = ((;50 + 3) / 2)
123		df-dec 12737	. . . . . . . . . . 11 ⊢ ;50 = (((9 + 1) · 5) + 0)
124	9, 2	addcli 11239	. . . . . . . . . . . . 13 ⊢ (9 + 1) ∈ ℂ
125	124, 11	mulcli 11240	. . . . . . . . . . . 12 ⊢ ((9 + 1) · 5) ∈ ℂ
126	125, 82	addcli 11239	. . . . . . . . . . 11 ⊢ (((9 + 1) · 5) + 0) ∈ ℂ
127	123, 126	eqeltri 2856	. . . . . . . . . 10 ⊢ ;50 ∈ ℂ
128	127, 13, 16, 17	divdiri 11996	. . . . . . . . 9 ⊢ ((;50 + 3) / 2) = ((;50 / 2) + (3 / 2))
129	122, 128	eqtri 2783	. . . . . . . 8 ⊢ (;53 / 2) = ((;50 / 2) + (3 / 2))
130	117, 129	eqtr4i 2786	. . . . . . 7 ⊢ (;25 + (6 / 4)) = (;53 / 2)
131	130	negeqi 11474	. . . . . 6 ⊢ -(;25 + (6 / 4)) = -(;53 / 2)
132		df-dec 12737	. . . . . . . . . 10 ⊢ ;53 = (((9 + 1) · 5) + 3)
133	9, 2	addcli 11239	. . . . . . . . . . . 12 ⊢ (9 + 1) ∈ ℂ
134	133, 11	mulcli 11240	. . . . . . . . . . 11 ⊢ ((9 + 1) · 5) ∈ ℂ
135	134, 13	addcli 11239	. . . . . . . . . 10 ⊢ (((9 + 1) · 5) + 3) ∈ ℂ
136	132, 135	eqeltri 2856	. . . . . . . . 9 ⊢ ;53 ∈ ℂ
137	136, 16, 17	divcli 11981	. . . . . . . 8 ⊢ (;53 / 2) ∈ ℂ
138	137	negcli 11550	. . . . . . 7 ⊢ -(;53 / 2) ∈ ℂ
139	138	div1i 11967	. . . . . 6 ⊢ (-(;53 / 2) / 1) = -(;53 / 2)
140	131, 139	eqtr4i 2786	. . . . 5 ⊢ -(;25 + (6 / 4)) = (-(;53 / 2) / 1)
141	140	negeqi 11474	. . . 4 ⊢ --(;25 + (6 / 4)) = -(-(;53 / 2) / 1)
142	95, 141	eqtr3i 2785	. . 3 ⊢ (;25 + (6 / 4)) = -(-(;53 / 2) / 1)
143	7, 1	oveq12d 7431	. . . 4 ⊢ (𝜑 → (𝐵 / 𝐴) = (-(;53 / 2) / 1))
144	143	negeqd 11475	. . 3 ⊢ (𝜑 → -(𝐵 / 𝐴) = -(-(;53 / 2) / 1))
145	142, 144	eqtr4id 2814	. 2 ⊢ (𝜑 → (;25 + (6 / 4)) = -(𝐵 / 𝐴))
146		df-dec 12737	. . . . . . 7 ⊢ ;75 = (((9 + 1) · 7) + 5)
147	9, 2	addcli 11239	. . . . . . . . 9 ⊢ (9 + 1) ∈ ℂ
148	147, 24	mulcli 11240	. . . . . . . 8 ⊢ ((9 + 1) · 7) ∈ ℂ
149	148, 11	addcli 11239	. . . . . . 7 ⊢ (((9 + 1) · 7) + 5) ∈ ℂ
150	146, 149	eqeltri 2856	. . . . . 6 ⊢ ;75 ∈ ℂ
151	150, 16, 17	divcli 11981	. . . . 5 ⊢ (;75 / 2) ∈ ℂ
152	151	div1i 11967	. . . 4 ⊢ ((;75 / 2) / 1) = (;75 / 2)
153		df-dec 12737	. . . . . . 7 ⊢ ;25 = (((9 + 1) · 2) + 5)
154	9, 2	addcli 11239	. . . . . . . . 9 ⊢ (9 + 1) ∈ ℂ
155	154, 16	mulcli 11240	. . . . . . . 8 ⊢ ((9 + 1) · 2) ∈ ℂ
156	155, 11	addcli 11239	. . . . . . 7 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
157	153, 156	eqeltri 2856	. . . . . 6 ⊢ ;25 ∈ ℂ
158	157, 13, 16, 17	divassi 11995	. . . . 5 ⊢ ((;25 · 3) / 2) = (;25 · (3 / 2))
159		3nn0 12546	. . . . . . 7 ⊢ 3 ∈ ℕ0
160		eqid 2760	. . . . . . 7 ⊢ ;25 = ;25
161		2t3e6 12431	. . . . . . . . 9 ⊢ (2 · 3) = 6
162	161	oveq1i 7423	. . . . . . . 8 ⊢ ((2 · 3) + 1) = (6 + 1)
163		6p1e7 12412	. . . . . . . 8 ⊢ (6 + 1) = 7
164	162, 163	eqtri 2783	. . . . . . 7 ⊢ ((2 · 3) + 1) = 7
165		5t3e15 12842	. . . . . . 7 ⊢ (5 · 3) = ;15
166	159, 48, 49, 160, 49, 52, 164, 165	decmul1c 12806	. . . . . 6 ⊢ (;25 · 3) = ;75
167	166	oveq1i 7423	. . . . 5 ⊢ ((;25 · 3) / 2) = (;75 / 2)
168	158, 167	eqtr3i 2785	. . . 4 ⊢ (;25 · (3 / 2)) = (;75 / 2)
169	38, 13, 62	mulcomli 11242	. . . . . . . 8 ⊢ (3 · 4) = ;12
170	61, 169	eqtr4i 2786	. . . . . . 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 11944	. . . . . . . 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 7424	. . . . 5 ⊢ (;25 · (6 / 4)) = (;25 · (3 / 2))
179	178	eqcomi 2769	. . . 4 ⊢ (;25 · (3 / 2)) = (;25 · (6 / 4))
180	152, 168, 179	3eqtr2ri 2790	. . 3 ⊢ (;25 · (6 / 4)) = ((;75 / 2) / 1)
181	21, 1	oveq12d 7431	. . 3 ⊢ (𝜑 → (𝐶 / 𝐴) = ((;75 / 2) / 1))
182	180, 181	eqtr4id 2814	. 2 ⊢ (𝜑 → (;25 · (6 / 4)) = (𝐶 / 𝐴))
183	3, 6, 20, 29, 30, 36, 41, 145, 182	quadfac 43071	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 2955  (class class class)co 7413  ℂcc 11122  0cc0 11124  1c1 11125   + caddc 11127   · cmul 11129  -cneg 11466   / cdiv 11895  2c2 12319  3c3 12320  4c4 12321  5c5 12322  6c6 12323  7c7 12324  9c9 12326  ;cdc 12736  ↑cexp 14125

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 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  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 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-div 11896  df-nn 12258  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12529  df-z 12616  df-dec 12737  df-uz 12888  df-seq 14066  df-exp 14126

This theorem is used by: (None)