Theorem 25or6to4 43006

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 11169	. . 3 ⊢ 1 ∈ ℂ
3	1, 2	eqeltrdi 2873	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		ax-1ne0 11180	. . . 4 ⊢ 1 ≠ 0
5	4	a1i 11	. . 3 ⊢ (𝜑 → 1 ≠ 0)
6	1, 5	eqnetrd 3027	. 2 ⊢ (𝜑 → 𝐴 ≠ 0)
7		25or6to4.b	. . 3 ⊢ (𝜑 → 𝐵 = -(;53 / 2))
8		df-dec 12724	. . . . . 6 ⊢ ;53 = (((9 + 1) · 5) + 3)
9		9cn 12352	. . . . . . . . 9 ⊢ 9 ∈ ℂ
10	9, 2	addcli 11226	. . . . . . . 8 ⊢ (9 + 1) ∈ ℂ
11		5cn 12340	. . . . . . . 8 ⊢ 5 ∈ ℂ
12	10, 11	mulcli 11227	. . . . . . 7 ⊢ ((9 + 1) · 5) ∈ ℂ
13		3cn 12333	. . . . . . 7 ⊢ 3 ∈ ℂ
14	12, 13	addcli 11226	. . . . . 6 ⊢ (((9 + 1) · 5) + 3) ∈ ℂ
15	8, 14	eqeltri 2861	. . . . 5 ⊢ ;53 ∈ ℂ
16		2cn 12327	. . . . 5 ⊢ 2 ∈ ℂ
17		2ne0 12358	. . . . 5 ⊢ 2 ≠ 0
18	15, 16, 17	divcli 11968	. . . 4 ⊢ (;53 / 2) ∈ ℂ
19	18	negcli 11537	. . 3 ⊢ -(;53 / 2) ∈ ℂ
20	7, 19	eqeltrdi 2873	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
21		25or6to4.c	. . 3 ⊢ (𝜑 → 𝐶 = (;75 / 2))
22		df-dec 12724	. . . . 5 ⊢ ;75 = (((9 + 1) · 7) + 5)
23	9, 2	addcli 11226	. . . . . . 7 ⊢ (9 + 1) ∈ ℂ
24		7cn 12346	. . . . . . 7 ⊢ 7 ∈ ℂ
25	23, 24	mulcli 11227	. . . . . 6 ⊢ ((9 + 1) · 7) ∈ ℂ
26	25, 11	addcli 11226	. . . . 5 ⊢ (((9 + 1) · 7) + 5) ∈ ℂ
27	22, 26	eqeltri 2861	. . . 4 ⊢ ;75 ∈ ℂ
28	27, 16, 17	divcli 11968	. . 3 ⊢ (;75 / 2) ∈ ℂ
29	21, 28	eqeltrdi 2873	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
30		25or6to4.x	. 2 ⊢ (𝜑 → 𝑋 ∈ ℂ)
31		df-dec 12724	. . . 4 ⊢ ;25 = (((9 + 1) · 2) + 5)
32	9, 2	addcli 11226	. . . . . 6 ⊢ (9 + 1) ∈ ℂ
33	32, 16	mulcli 11227	. . . . 5 ⊢ ((9 + 1) · 2) ∈ ℂ
34	33, 11	addcli 11226	. . . 4 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
35	31, 34	eqeltri 2861	. . 3 ⊢ ;25 ∈ ℂ
36	35	a1i 11	. 2 ⊢ (𝜑 → ;25 ∈ ℂ)
37		6cn 12343	. . . 4 ⊢ 6 ∈ ℂ
38		4cn 12337	. . . 4 ⊢ 4 ∈ ℂ
39		4ne0 12363	. . . 4 ⊢ 4 ≠ 0
40	37, 38, 39	divcli 11968	. . 3 ⊢ (6 / 4) ∈ ℂ
41	40	a1i 11	. 2 ⊢ (𝜑 → (6 / 4) ∈ ℂ)
42		df-dec 12724	. . . . . . . . . . 11 ⊢ ;25 = (((9 + 1) · 2) + 5)
43	9, 2	addcli 11226	. . . . . . . . . . . . 13 ⊢ (9 + 1) ∈ ℂ
44	43, 16	mulcli 11227	. . . . . . . . . . . 12 ⊢ ((9 + 1) · 2) ∈ ℂ
45	44, 11	addcli 11226	. . . . . . . . . . 11 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
46	42, 45	eqeltri 2861	. . . . . . . . . 10 ⊢ ;25 ∈ ℂ
47	46, 16, 17	divcan4i 11973	. . . . . . . . 9 ⊢ ((;25 · 2) / 2) = ;25
48		2nn0 12532	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ0
49		5nn0 12535	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ0
50		eqid 2765	. . . . . . . . . . 11 ⊢ ;25 = ;25
51		0nn0 12530	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ0
52		1nn0 12531	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
53		2t2e4 12415	. . . . . . . . . . . . 13 ⊢ (2 · 2) = 4
54	53	oveq1i 7426	. . . . . . . . . . . 12 ⊢ ((2 · 2) + 1) = (4 + 1)
55		4p1e5 12397	. . . . . . . . . . . 12 ⊢ (4 + 1) = 5
56	54, 55	eqtri 2788	. . . . . . . . . . 11 ⊢ ((2 · 2) + 1) = 5
57		5t2e10 12828	. . . . . . . . . . 11 ⊢ (5 · 2) = ;10
58	48, 48, 49, 50, 51, 52, 56, 57	decmul1c 12793	. . . . . . . . . 10 ⊢ (;25 · 2) = ;50
59	58	oveq1i 7426	. . . . . . . . 9 ⊢ ((;25 · 2) / 2) = (;50 / 2)
60	47, 59	eqtr3i 2790	. . . . . . . 8 ⊢ ;25 = (;50 / 2)
61		6t2e12 12832	. . . . . . . . . 10 ⊢ (6 · 2) = ;12
62		4t3e12 12826	. . . . . . . . . . 11 ⊢ (4 · 3) = ;12
63	38, 13, 62	mulcomli 11229	. . . . . . . . . 10 ⊢ (3 · 4) = ;12
64	61, 63	eqtr4i 2791	. . . . . . . . 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 12464	. . . . . . . . . . . 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 11931	. . . . . . . . . 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 7428	. . . . . . 7 ⊢ (;25 + (6 / 4)) = ((;50 / 2) + (3 / 2))
74		dfdec10 12726	. . . . . . . . . 10 ⊢ ;53 = ((;10 · 5) + 3)
75	49	dec0u 12749	. . . . . . . . . . 11 ⊢ (;10 · 5) = ;50
76	75	oveq1i 7426	. . . . . . . . . 10 ⊢ ((;10 · 5) + 3) = (;50 + 3)
77	74, 76	eqtri 2788	. . . . . . . . 9 ⊢ ;53 = (;50 + 3)
78	77	oveq1i 7426	. . . . . . . 8 ⊢ (;53 / 2) = ((;50 + 3) / 2)
79		df-dec 12724	. . . . . . . . . 10 ⊢ ;50 = (((9 + 1) · 5) + 0)
80	9, 2	addcli 11226	. . . . . . . . . . . 12 ⊢ (9 + 1) ∈ ℂ
81	80, 11	mulcli 11227	. . . . . . . . . . 11 ⊢ ((9 + 1) · 5) ∈ ℂ
82		0cn 11209	. . . . . . . . . . 11 ⊢ 0 ∈ ℂ
83	81, 82	addcli 11226	. . . . . . . . . 10 ⊢ (((9 + 1) · 5) + 0) ∈ ℂ
84	79, 83	eqeltri 2861	. . . . . . . . 9 ⊢ ;50 ∈ ℂ
85	84, 13, 16, 17	divdiri 11983	. . . . . . . 8 ⊢ ((;50 + 3) / 2) = ((;50 / 2) + (3 / 2))
86	78, 85	eqtri 2788	. . . . . . 7 ⊢ (;53 / 2) = ((;50 / 2) + (3 / 2))
87	73, 86	eqtr4i 2791	. . . . . 6 ⊢ (;25 + (6 / 4)) = (;53 / 2)
88		df-dec 12724	. . . . . . . 8 ⊢ ;53 = (((9 + 1) · 5) + 3)
89	9, 2	addcli 11226	. . . . . . . . . 10 ⊢ (9 + 1) ∈ ℂ
90	89, 11	mulcli 11227	. . . . . . . . 9 ⊢ ((9 + 1) · 5) ∈ ℂ
91	90, 13	addcli 11226	. . . . . . . 8 ⊢ (((9 + 1) · 5) + 3) ∈ ℂ
92	88, 91	eqeltri 2861	. . . . . . 7 ⊢ ;53 ∈ ℂ
93	92, 16, 17	divcli 11968	. . . . . 6 ⊢ (;53 / 2) ∈ ℂ
94	87, 93	eqeltri 2861	. . . . 5 ⊢ (;25 + (6 / 4)) ∈ ℂ
95	94	negnegi 11539	. . . 4 ⊢ --(;25 + (6 / 4)) = (;25 + (6 / 4))
96		df-dec 12724	. . . . . . . . . . . 12 ⊢ ;25 = (((9 + 1) · 2) + 5)
97	9, 2	addcli 11226	. . . . . . . . . . . . . 14 ⊢ (9 + 1) ∈ ℂ
98	97, 16	mulcli 11227	. . . . . . . . . . . . 13 ⊢ ((9 + 1) · 2) ∈ ℂ
99	98, 11	addcli 11226	. . . . . . . . . . . 12 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
100	96, 99	eqeltri 2861	. . . . . . . . . . 11 ⊢ ;25 ∈ ℂ
101	100, 16, 17	divcan4i 11973	. . . . . . . . . 10 ⊢ ((;25 · 2) / 2) = ;25
102		eqid 2765	. . . . . . . . . . . 12 ⊢ ;25 = ;25
103	53	oveq1i 7426	. . . . . . . . . . . . 13 ⊢ ((2 · 2) + 1) = (4 + 1)
104	103, 55	eqtri 2788	. . . . . . . . . . . 12 ⊢ ((2 · 2) + 1) = 5
105	48, 48, 49, 102, 51, 52, 104, 57	decmul1c 12793	. . . . . . . . . . 11 ⊢ (;25 · 2) = ;50
106	105	oveq1i 7426	. . . . . . . . . 10 ⊢ ((;25 · 2) / 2) = (;50 / 2)
107	101, 106	eqtr3i 2790	. . . . . . . . 9 ⊢ ;25 = (;50 / 2)
108	38, 13, 62	mulcomli 11229	. . . . . . . . . . 11 ⊢ (3 · 4) = ;12
109	61, 108	eqtr4i 2791	. . . . . . . . . 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 11931	. . . . . . . . . . 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 7428	. . . . . . . 8 ⊢ (;25 + (6 / 4)) = ((;50 / 2) + (3 / 2))
118		dfdec10 12726	. . . . . . . . . . 11 ⊢ ;53 = ((;10 · 5) + 3)
119	49	dec0u 12749	. . . . . . . . . . . 12 ⊢ (;10 · 5) = ;50
120	119	oveq1i 7426	. . . . . . . . . . 11 ⊢ ((;10 · 5) + 3) = (;50 + 3)
121	118, 120	eqtri 2788	. . . . . . . . . 10 ⊢ ;53 = (;50 + 3)
122	121	oveq1i 7426	. . . . . . . . 9 ⊢ (;53 / 2) = ((;50 + 3) / 2)
123		df-dec 12724	. . . . . . . . . . 11 ⊢ ;50 = (((9 + 1) · 5) + 0)
124	9, 2	addcli 11226	. . . . . . . . . . . . 13 ⊢ (9 + 1) ∈ ℂ
125	124, 11	mulcli 11227	. . . . . . . . . . . 12 ⊢ ((9 + 1) · 5) ∈ ℂ
126	125, 82	addcli 11226	. . . . . . . . . . 11 ⊢ (((9 + 1) · 5) + 0) ∈ ℂ
127	123, 126	eqeltri 2861	. . . . . . . . . 10 ⊢ ;50 ∈ ℂ
128	127, 13, 16, 17	divdiri 11983	. . . . . . . . 9 ⊢ ((;50 + 3) / 2) = ((;50 / 2) + (3 / 2))
129	122, 128	eqtri 2788	. . . . . . . 8 ⊢ (;53 / 2) = ((;50 / 2) + (3 / 2))
130	117, 129	eqtr4i 2791	. . . . . . 7 ⊢ (;25 + (6 / 4)) = (;53 / 2)
131	130	negeqi 11461	. . . . . 6 ⊢ -(;25 + (6 / 4)) = -(;53 / 2)
132		df-dec 12724	. . . . . . . . . 10 ⊢ ;53 = (((9 + 1) · 5) + 3)
133	9, 2	addcli 11226	. . . . . . . . . . . 12 ⊢ (9 + 1) ∈ ℂ
134	133, 11	mulcli 11227	. . . . . . . . . . 11 ⊢ ((9 + 1) · 5) ∈ ℂ
135	134, 13	addcli 11226	. . . . . . . . . 10 ⊢ (((9 + 1) · 5) + 3) ∈ ℂ
136	132, 135	eqeltri 2861	. . . . . . . . 9 ⊢ ;53 ∈ ℂ
137	136, 16, 17	divcli 11968	. . . . . . . 8 ⊢ (;53 / 2) ∈ ℂ
138	137	negcli 11537	. . . . . . 7 ⊢ -(;53 / 2) ∈ ℂ
139	138	div1i 11954	. . . . . 6 ⊢ (-(;53 / 2) / 1) = -(;53 / 2)
140	131, 139	eqtr4i 2791	. . . . 5 ⊢ -(;25 + (6 / 4)) = (-(;53 / 2) / 1)
141	140	negeqi 11461	. . . 4 ⊢ --(;25 + (6 / 4)) = -(-(;53 / 2) / 1)
142	95, 141	eqtr3i 2790	. . 3 ⊢ (;25 + (6 / 4)) = -(-(;53 / 2) / 1)
143	7, 1	oveq12d 7434	. . . 4 ⊢ (𝜑 → (𝐵 / 𝐴) = (-(;53 / 2) / 1))
144	143	negeqd 11462	. . 3 ⊢ (𝜑 → -(𝐵 / 𝐴) = -(-(;53 / 2) / 1))
145	142, 144	eqtr4id 2819	. 2 ⊢ (𝜑 → (;25 + (6 / 4)) = -(𝐵 / 𝐴))
146		df-dec 12724	. . . . . . 7 ⊢ ;75 = (((9 + 1) · 7) + 5)
147	9, 2	addcli 11226	. . . . . . . . 9 ⊢ (9 + 1) ∈ ℂ
148	147, 24	mulcli 11227	. . . . . . . 8 ⊢ ((9 + 1) · 7) ∈ ℂ
149	148, 11	addcli 11226	. . . . . . 7 ⊢ (((9 + 1) · 7) + 5) ∈ ℂ
150	146, 149	eqeltri 2861	. . . . . 6 ⊢ ;75 ∈ ℂ
151	150, 16, 17	divcli 11968	. . . . 5 ⊢ (;75 / 2) ∈ ℂ
152	151	div1i 11954	. . . 4 ⊢ ((;75 / 2) / 1) = (;75 / 2)
153		df-dec 12724	. . . . . . 7 ⊢ ;25 = (((9 + 1) · 2) + 5)
154	9, 2	addcli 11226	. . . . . . . . 9 ⊢ (9 + 1) ∈ ℂ
155	154, 16	mulcli 11227	. . . . . . . 8 ⊢ ((9 + 1) · 2) ∈ ℂ
156	155, 11	addcli 11226	. . . . . . 7 ⊢ (((9 + 1) · 2) + 5) ∈ ℂ
157	153, 156	eqeltri 2861	. . . . . 6 ⊢ ;25 ∈ ℂ
158	157, 13, 16, 17	divassi 11982	. . . . 5 ⊢ ((;25 · 3) / 2) = (;25 · (3 / 2))
159		3nn0 12533	. . . . . . 7 ⊢ 3 ∈ ℕ0
160		eqid 2765	. . . . . . 7 ⊢ ;25 = ;25
161		2t3e6 12418	. . . . . . . . 9 ⊢ (2 · 3) = 6
162	161	oveq1i 7426	. . . . . . . 8 ⊢ ((2 · 3) + 1) = (6 + 1)
163		6p1e7 12399	. . . . . . . 8 ⊢ (6 + 1) = 7
164	162, 163	eqtri 2788	. . . . . . 7 ⊢ ((2 · 3) + 1) = 7
165		5t3e15 12829	. . . . . . 7 ⊢ (5 · 3) = ;15
166	159, 48, 49, 160, 49, 52, 164, 165	decmul1c 12793	. . . . . 6 ⊢ (;25 · 3) = ;75
167	166	oveq1i 7426	. . . . 5 ⊢ ((;25 · 3) / 2) = (;75 / 2)
168	158, 167	eqtr3i 2790	. . . 4 ⊢ (;25 · (3 / 2)) = (;75 / 2)
169	38, 13, 62	mulcomli 11229	. . . . . . . 8 ⊢ (3 · 4) = ;12
170	61, 169	eqtr4i 2791	. . . . . . 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 11931	. . . . . . . 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 7427	. . . . 5 ⊢ (;25 · (6 / 4)) = (;25 · (3 / 2))
179	178	eqcomi 2774	. . . 4 ⊢ (;25 · (3 / 2)) = (;25 · (6 / 4))
180	152, 168, 179	3eqtr2ri 2795	. . 3 ⊢ (;25 · (6 / 4)) = ((;75 / 2) / 1)
181	21, 1	oveq12d 7434	. . 3 ⊢ (𝜑 → (𝐶 / 𝐴) = ((;75 / 2) / 1))
182	180, 181	eqtr4id 2819	. 2 ⊢ (𝜑 → (;25 · (6 / 4)) = (𝐶 / 𝐴))
183	3, 6, 20, 29, 30, 36, 41, 145, 182	quadfac 43005	1 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ;25 ∨ 𝑋 = (6 / 4))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  (class class class)co 7416  ℂcc 11109  0cc0 11111  1c1 11112   + caddc 11114   · cmul 11116  -cneg 11453   / cdiv 11882  2c2 12306  3c3 12307  4c4 12308  5c5 12309  6c6 12310  7c7 12311  9c9 12313  ;cdc 12723  ↑cexp 14111

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-cnex 11167  ax-resscn 11168  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-mulcom 11175  ax-addass 11176  ax-mulass 11177  ax-distr 11178  ax-i2m1 11179  ax-1ne0 11180  ax-1rid 11181  ax-rnegex 11182  ax-rrecex 11183  ax-cnre 11184  ax-pre-lttri 11185  ax-pre-lttrn 11186  ax-pre-ltadd 11187  ax-pre-mulgt0 11188

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11454  df-neg 11455  df-div 11883  df-nn 12245  df-2 12314  df-3 12315  df-4 12316  df-5 12317  df-6 12318  df-7 12319  df-8 12320  df-9 12321  df-n0 12516  df-z 12603  df-dec 12724  df-uz 12875  df-seq 14052  df-exp 14112

This theorem is used by: (None)