Theorem 1re 11054

Description: The number 1 is real. This used to be one of our postulates for complex numbers, but Eric Schmidt discovered that it could be derived from a weaker postulate, ax-1cn 11008, by exploiting properties of the imaginary unit i. (Contributed by Eric Schmidt, 11-Apr-2007.) (Revised by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
1re	⊢ 1 ∈ ℝ

Proof of Theorem 1re

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-1ne0 11019	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11008	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11051	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3003	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 248	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11046	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11051	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3004	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 248	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3163	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3163	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3163	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3163	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 981	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2941	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 357	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2941	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 357	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 627	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 277	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 7324	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 7335	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 216	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2968	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 3003	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 3004	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3580	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1120	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 744	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 3003	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 3004	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3580	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1120	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 743	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 856	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3201	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3192	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2762	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 413	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2961	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 3003	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3569	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
50	49	expcom 414	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
51	47, 50	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
52	51	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
53	52	adantld 491	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54		neeq1 3003	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3569	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
56	55	expcom 414	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
57	56	adantrd 492	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
58	57	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
59	53, 58	pm2.61ine 3025	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3192	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 11022	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 11035	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 712	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2824	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 244	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3148	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3140	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 844   = wceq 1540   ∈ wcel 2105   ≠ wne 2940  ∃wrex 3070  (class class class)co 7316  ℂcc 10948  ℝcr 10949  0cc0 10950  1c1 10951  ici 10952   + caddc 10953   · cmul 10955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-1cn 11008  ax-icn 11009  ax-addcl 11010  ax-mulcl 11012  ax-mulrcl 11013  ax-i2m1 11018  ax-1ne0 11019  ax-rrecex 11022  ax-cnre 11023

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3442  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-br 5087  df-iota 6417  df-fv 6473  df-ov 7319

This theorem is referenced by:  1red  11055  1xr  11113  dedekind  11217  peano2re  11227  mul02lem2  11231  addid1  11234  renegcl  11363  peano2rem  11367  0reALT  11397  0lt1  11576  0le1  11577  relin01  11578  1le1  11682  eqneg  11774  ltp1  11894  ltm1  11896  recgt0  11900  mulgt1  11913  ltmulgt11  11914  lemulge11  11916  reclt1  11949  recgt1  11950  recgt1i  11951  recp1lt1  11952  recreclt  11953  recgt0ii  11960  ledivp1i  11979  ltdivp1i  11980  inelr  12042  cju  12048  nnssre  12056  nnge1  12080  nngt1ne1  12081  nnle1eq1  12082  nngt0  12083  nnnlt1  12084  nnne0  12086  nnrecre  12094  nnrecgt0  12095  nnsub  12096  2re  12126  3re  12132  4re  12136  5re  12139  6re  12142  7re  12145  8re  12148  9re  12151  0le2  12154  2pos  12155  3pos  12157  4pos  12159  5pos  12161  6pos  12162  7pos  12163  8pos  12164  9pos  12165  neg1rr  12167  neg1lt0  12169  1lt2  12223  1lt3  12225  1lt4  12228  1lt5  12232  1lt6  12237  1lt7  12243  1lt8  12250  1lt9  12258  1ne2  12260  1le2  12261  1le3  12264  halflt1  12270  addltmul  12288  nnunb  12308  elnnnn0c  12357  nn0ge2m1nn  12381  elnnz1  12425  znnnlt1  12426  zltp1le  12449  zleltp1  12450  nn0lt2  12462  recnz  12474  gtndiv  12476  3halfnz  12478  10re  12535  1lt10  12655  eluzp1m1  12687  eluzp1p1  12689  eluz2b2  12740  zbtwnre  12765  rebtwnz  12766  1rp  12813  divlt1lt  12878  divle1le  12879  nnledivrp  12921  qbtwnxr  13013  xmulid1  13092  xmulm1  13094  x2times  13112  xrub  13125  elicc01  13277  1elunit  13281  divelunit  13305  lincmb01cmp  13306  unitssre  13310  0nelfz1  13354  fzpreddisj  13384  fznatpl1  13389  fztpval  13397  fraclt1  13601  fracle1  13602  flbi2  13616  fldiv4p1lem1div2  13634  fldiv4lem1div2  13636  fldiv  13659  modid  13695  1mod  13702  m1modnnsub1  13716  modm1p1mod0  13721  seqf1olem1  13841  reexpcl  13878  reexpclz  13881  expge0  13898  expge1  13899  expgt1  13900  bernneq  14023  bernneq2  14024  expnbnd  14026  expnlbnd  14027  expnlbnd2  14028  expmulnbnd  14029  discr1  14033  facwordi  14082  faclbnd3  14085  faclbnd4lem1  14086  faclbnd4lem4  14089  faclbnd6  14092  facavg  14094  hashv01gt1  14138  hashnn0n0nn  14184  hashunsnggt  14187  hash1snb  14212  hashgt12el  14215  hashgt12el2  14216  hashfun  14230  hashge2el2dif  14272  lsw0  14346  f1oun2prg  14706  cjexp  14937  re1  14941  im1  14942  rei  14943  imi  14944  sqrlem1  15030  sqrlem2  15031  sqrlem3  15032  sqrlem4  15033  sqrlem7  15036  resqrex  15038  sqrt1  15059  sqrt2gt1lt2  15062  sqrtm1  15063  abs1  15085  absrdbnd  15129  caubnd2  15145  mulcn2  15381  reccn2  15382  rlimno1  15441  o1fsum  15601  expcnv  15652  geolim  15658  geolim2  15659  georeclim  15660  geomulcvg  15664  geoisumr  15666  geoisum1c  15668  fprodge0  15779  fprodge1  15781  rerisefaccl  15803  refallfaccl  15804  ere  15874  ege2le3  15875  efgt1  15901  resin4p  15923  recos4p  15924  tanhbnd  15946  sinbnd  15965  cosbnd  15966  sinbnd2  15967  cosbnd2  15968  ef01bndlem  15969  sin01bnd  15970  cos01bnd  15971  cos1bnd  15972  cos2bnd  15973  sinltx  15974  sin01gt0  15975  cos01gt0  15976  sin02gt0  15977  sincos1sgn  15978  ene1  15995  rpnnen2lem2  16000  rpnnen2lem3  16001  rpnnen2lem4  16002  rpnnen2lem9  16007  rpnnen2lem12  16010  ruclem6  16020  ruclem11  16025  ruclem12  16026  3dvds  16116  flodddiv4  16198  sadcadd  16241  isprm3  16462  sqnprm  16481  coprm  16490  phibndlem  16545  pythagtriplem3  16593  pcmpt  16667  fldivp1  16672  pockthi  16682  infpn2  16688  resslemOLD  17026  basendxnmulrndx  17079  basendxnmulrndxOLD  17080  starvndxnbasendx  17088  scandxnbasendx  17100  vscandxnbasendx  17105  ipndxnbasendx  17116  basendxnocndx  17167  slotsbhcdif  17199  slotsbhcdifOLD  17200  oppcbasOLD  17503  rescbasOLD  17616  rescabsOLD  17622  odubasOLD  18084  symgvalstructOLD  19078  lt6abl  19568  srgbinomlem4  19851  abvneg  20174  abvtrivd  20180  rmodislmodOLD  20272  0ringnnzr  20620  cnfldfunALTOLD  20691  xrsmcmn  20701  xrsnsgrp  20714  gzrngunitlem  20743  gzrngunit  20744  rge0srg  20749  psgnodpmr  20875  remulg  20892  resubdrg  20893  thlbasOLD  20982  tuslemOLD  23499  setsmsbasOLD  23709  dscmet  23808  dscopn  23809  nrginvrcnlem  23935  idnghm  23987  tgioo  24039  blcvx  24041  iicmp  24129  iiconn  24130  iirev  24172  iihalf1  24174  iihalf2  24176  iihalf2cn  24177  elii1  24178  elii2  24179  iimulcl  24180  icopnfcnv  24185  icopnfhmeo  24186  iccpnfhmeo  24188  xrhmeo  24189  xrhmph  24190  evth  24202  xlebnum  24208  htpycc  24223  reparphti  24240  pcoval1  24256  pco1  24258  pcoval2  24259  pcocn  24260  pcohtpylem  24262  pcopt  24265  pcopt2  24266  pcoass  24267  pcorevlem  24269  nmhmcn  24363  ncvs1  24401  ovolunlem1a  24740  vitalilem2  24853  vitalilem4  24855  vitalilem5  24856  vitali  24857  i1f1  24934  itg11  24935  itg2const  24985  dveflem  25223  dvlipcn  25238  dvcvx  25264  ply1remlem  25407  fta1blem  25413  vieta1lem2  25551  aalioulem3  25574  aalioulem5  25576  aaliou3lem2  25583  ulmbdd  25637  iblulm  25646  radcnvlem1  25652  dvradcnv  25660  abelthlem2  25671  abelthlem3  25672  abelthlem5  25674  abelthlem7  25677  abelth  25680  abelth2  25681  reeff1olem  25685  reeff1o  25686  sinhalfpilem  25700  tangtx  25742  sincos4thpi  25750  pige3ALT  25756  coskpi  25759  cos0pilt1  25768  recosf1o  25771  tanregt0  25775  efif1olem3  25780  efif1olem4  25781  loge  25822  logdivlti  25855  logcnlem4  25880  logf1o2  25885  logtayl  25895  logccv  25898  recxpcl  25910  cxplea  25931  cxpcn3lem  25980  cxpaddlelem  25984  loglesqrt  25991  ang180lem2  26040  angpined  26060  acosrecl  26133  atancj  26140  atanlogaddlem  26143  atantan  26153  atans2  26161  ressatans  26164  leibpi  26172  log2le1  26180  birthdaylem3  26183  cxp2lim  26206  cxploglim  26207  cxploglim2  26208  divsqrtsumlem  26209  cvxcl  26214  scvxcvx  26215  jensenlem2  26217  amgmlem  26219  emcllem2  26226  emcllem4  26228  emcllem6  26230  emcllem7  26231  emre  26235  emgt0  26236  harmonicbnd3  26237  harmonicubnd  26239  harmonicbnd4  26240  zetacvg  26244  ftalem1  26302  ftalem2  26303  ftalem5  26306  issqf  26365  cht1  26394  chp1  26396  ppiltx  26406  mumullem2  26409  ppiublem1  26430  ppiub  26432  chtublem  26439  chtub  26440  logfacbnd3  26451  logexprlim  26453  perfectlem2  26458  dchrinv  26489  dchr1re  26491  efexple  26509  bposlem1  26512  bposlem2  26513  bposlem5  26516  bposlem8  26519  lgsdir2lem1  26553  lgsdir2lem5  26557  lgsdir  26560  lgsne0  26563  lgsabs1  26564  lgsdinn0  26573  gausslemma2dlem0i  26592  lgseisen  26607  m1lgs  26616  2lgslem3  26632  addsq2nreurex  26672  2sqreultblem  26676  2sqreunnltblem  26679  chebbnd1lem3  26699  chebbnd1  26700  chtppilimlem1  26701  chtppilimlem2  26702  chtppilim  26703  chpchtlim  26707  vmadivsumb  26711  rplogsumlem2  26713  rpvmasumlem  26715  dchrmusumlema  26721  dchrmusum2  26722  dchrvmasumlem2  26726  dchrvmasumiflem1  26729  dchrisum0flblem1  26736  dchrisum0flblem2  26737  dchrisum0fno1  26739  rpvmasum2  26740  dchrisum0re  26741  dchrisum0lema  26742  dchrisum0lem1b  26743  dchrisum0lem1  26744  dchrisum0lem2a  26745  dchrisum0lem2  26746  logdivsum  26761  mulog2sumlem2  26763  2vmadivsumlem  26768  log2sumbnd  26772  selbergb  26777  selberg2b  26780  chpdifbndlem1  26781  selberg3lem1  26785  selberg3lem2  26786  selberg4lem1  26788  pntrmax  26792  pntrsumo1  26793  selbergsb  26803  pntrlog2bndlem3  26807  pntrlog2bndlem5  26809  pntpbnd1a  26813  pntpbnd2  26815  pntibndlem1  26817  pntibndlem3  26820  pntlemd  26822  pntlemc  26823  pntlemb  26825  pntlemr  26830  pntlemf  26833  pntlemk  26834  pntlemo  26835  pntlem3  26837  pntleml  26839  abvcxp  26843  ostth2lem1  26846  ostth1  26861  ostth2lem2  26862  ostth2lem3  26863  ostth2lem4  26864  ostth2  26865  ostth3  26866  ostth  26867  slotsinbpsd  26935  slotslnbpsd  26936  trgcgrg  27009  brbtwn2  27406  colinearalglem4  27410  ax5seglem2  27430  ax5seglem3  27432  axpaschlem  27441  axpasch  27442  axlowdimlem6  27448  axlowdimlem10  27452  axlowdimlem16  27458  axlowdim1  27460  axlowdim2  27461  axlowdim  27462  axcontlem2  27466  elntg2  27486  lfgrnloop  27628  lfuhgr1v0e  27754  usgrexmpldifpr  27758  usgrexmplef  27759  1loopgrvd2  28003  vdegp1bi  28037  lfgrwlkprop  28187  pthdlem1  28266  pthdlem2  28268  clwlkclwwlkf  28504  upgr4cycl4dv4e  28681  konigsberglem2  28749  konigsberglem3  28750  konigsberglem5  28752  frgrreg  28890  ex-dif  28919  ex-in  28921  ex-pss  28924  ex-res  28937  ex-fl  28943  nv1  29169  smcnlem  29191  ipidsq  29204  nmlno0lem  29287  norm-ii-i  29631  bcs2  29676  norm1  29743  nmopub2tALT  30403  nmfnleub2  30420  nmlnop0iALT  30489  unopbd  30509  nmopadjlem  30583  nmopcoadji  30595  pjnmopi  30642  pjbdlni  30643  hstle1  30720  hstle  30724  hstles  30725  stge1i  30732  stlesi  30735  staddi  30740  stadd3i  30742  strlem1  30744  strlem5  30749  jplem1  30762  cdj1i  30927  addltmulALT  30940  xlt2addrd  31212  pr01ssre  31269  dp2lt10  31289  dp2ltsuc  31291  dp2ltc  31292  dplti  31310  dpmul4  31319  cshw1s2  31363  xrsmulgzz  31418  resvbasOLD  31667  rearchi  31680  xrge0slmod  31682  prmidl0  31761  submateqlem1  31893  xrge0iifcnv  32019  xrge0iifcv  32020  xrge0iifiso  32021  xrge0iifhom  32023  zrhre  32105  indf  32119  indfval  32120  esumcst  32167  cntnevol  32332  omssubadd  32403  iwrdsplit  32490  dstfrvclim1  32580  coinfliprv  32585  ballotlem2  32591  ballotlem4  32601  ballotlemi1  32605  ballotlemic  32609  sgnclre  32642  sgnnbi  32648  sgnpbi  32649  sgnmulsgp  32653  plymulx0  32662  plymulx  32663  signswch  32676  signstf  32681  signsvfn  32697  itgexpif  32722  hgt750lemd  32764  logdivsqrle  32766  hgt750lem  32767  hgt750lem2  32768  hgt750leme  32774  tgoldbachgnn  32775  subfacp1lem1  33276  subfacp1lem5  33281  resconn  33343  iisconn  33349  iillysconn  33350  problem2  33759  problem3  33760  sinccvglem  33765  fz0n  33827  dnibndlem12  34739  knoppcnlem4  34746  knoppndvlem13  34774  cnndvlem1  34787  irrdiff  35574  relowlpssretop  35612  sin2h  35844  cos2h  35845  tan2h  35846  poimirlem7  35861  poimirlem16  35870  poimirlem17  35871  poimirlem19  35873  poimirlem20  35874  poimirlem22  35876  poimirlem23  35877  poimirlem29  35883  poimirlem31  35885  itg2addnclem3  35907  asindmre  35937  dvasin  35938  dvacos  35939  dvreasin  35940  dvreacos  35941  fdc  35980  geomcau  35994  cntotbnd  36031  heiborlem8  36053  bfplem2  36058  bfp  36059  aks4d1p1p7  40308  2xp3dxp2ge1d  40391  factwoffsmonot  40392  1t1e1ALT  40513  re1m1e0m0  40601  sn-00idlem1  40602  sn-00idlem2  40603  remul02  40609  sn-0ne2  40610  reixi  40625  rei4  40626  remulid2  40636  ipiiie0  40640  sn-0tie0  40642  mulgt0b2d  40651  sn-0lt1  40653  sn-ltp1  40654  reneg1lt0  40655  sn-inelr  40656  rabren3dioph  40858  pellexlem5  40876  pellexlem6  40877  pell1qrgaplem  40916  pell14qrgap  40918  pellqrex  40922  pellfundre  40924  pellfundlb  40927  pellfund14gap  40930  jm2.17a  41004  acongeq  41027  jm2.23  41040  jm3.1lem2  41062  sqrtcval  41488  sqrtcval2  41489  resqrtval  41490  imsqrtval  41491  relexp01min  41560  mnringbasedOLD  42069  cvgdvgrat  42170  lhe4.4ex1a  42186  binomcxplemnotnn0  42213  isosctrlem1ALT  42793  supxrgelem  43130  xrlexaddrp  43145  infxr  43160  infleinflem2  43164  sumnnodd  43426  limsup10exlem  43568  limsup10ex  43569  dvnprodlem3  43744  stoweidlem1  43797  stoweidlem18  43814  stoweidlem19  43815  stoweidlem26  43822  stoweidlem34  43830  stoweidlem40  43836  stoweidlem41  43837  stoweidlem59  43855  stoweid  43859  stirlinglem10  43879  stirlinglem11  43880  dirkercncflem1  43899  fourierdlem16  43919  fourierdlem21  43924  fourierdlem22  43925  fourierdlem42  43945  fourierdlem68  43970  fourierdlem83  43985  fourierdlem103  44005  sqwvfourb  44025  fouriersw  44027  etransclem23  44053  salgencntex  44137  ovn0lem  44359  smfmullem3  44587  smfmullem4  44588  zm1nn  45064  m1mod0mod1  45091  fmtnosqrt  45261  perfectALTVlem2  45444  2exp340mod341  45455  8exp8mod9  45458  nfermltl8rev  45464  nnsum3primesprm  45512  nnsum4primesodd  45518  nnsum4primesoddALTV  45519  nnsum4primeseven  45522  nnsum4primesevenALTV  45523  tgblthelfgott  45537  tgoldbach  45539  rege1logbrege0  46174  rege1logbzge0  46175  blennnelnn  46192  dignnld  46219  nn0sumshdiglemA  46235  nn0sumshdiglem1  46237  rrx2xpref1o  46334  rrxlines  46349  eenglngeehlnmlem1  46353  eenglngeehlnmlem2  46354  line2ylem  46367  line2x  46370  icccldii  46482  io1ii  46484  sepfsepc  46491