Theorem 1re 9918

Description: 1 is a real number. 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 9873, 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 9884	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 9873	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 9915	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 2844	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 238	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 9911	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 9915	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 2845	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 238	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 2999	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 2999	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 65	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 2999	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 2999	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 510	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2782	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 346	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2782	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 346	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 729	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 266	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 6557	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 6568	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 206	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2809	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 2844	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 2845	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3295	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1259	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 779	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 2844	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 2845	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3295	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1259	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 778	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 394	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 33	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3020	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3018	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2631	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 449	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2803	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 2844	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3282	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
50	49	expcom 450	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
51	47, 50	syl6 34	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
52	51	com23 84	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
53	52	adantld 482	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54		neeq1 2844	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3282	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
56	55	expcom 450	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
57	56	adantrd 483	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
58	57	a1dd 48	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
59	53, 58	pm2.61ine 2865	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3018	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 9887	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 9900	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 747	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2676	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 234	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3013	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3010	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816  ici 9817   + caddc 9818   · cmul 9820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  0re  9919  1red  9934  dedekind  10079  peano2re  10088  mul02lem2  10092  addid1  10095  renegcl  10223  peano2rem  10227  0reALT  10257  0lt1  10429  0le1  10430  relin01  10431  1le1  10534  eqneg  10624  ltp1  10740  ltm1  10742  recgt0  10746  mulgt1  10761  ltmulgt11  10762  lemulge11  10764  reclt1  10797  recgt1  10798  recgt1i  10799  recp1lt1  10800  recreclt  10801  recgt0ii  10808  ledivp1i  10828  ltdivp1i  10829  inelr  10887  cju  10893  nnssre  10901  nnge1  10923  nngt1ne1  10924  nnle1eq1  10925  nngt0  10926  nnnlt1  10927  nnrecre  10934  nnrecgt0  10935  nnsub  10936  2re  10967  3re  10971  4re  10974  5re  10976  6re  10978  7re  10980  8re  10982  9re  10984  10reOLD  10986  0le2  10988  2pos  10989  3pos  10991  4pos  10993  5pos  10995  6pos  10996  7pos  10997  8pos  10998  9pos  10999  10posOLD  11000  neg1rr  11002  neg1lt0  11004  1lt2  11071  1lt3  11073  1lt4  11076  1lt5  11080  1lt6  11085  1lt7  11091  1lt8  11098  1lt9  11106  1lt10OLD  11115  1ne2  11117  1le2  11118  1le3  11121  halflt1  11127  addltmul  11145  nnunb  11165  elnnnn0c  11215  nn0ge2m1nn  11237  elnnz1  11280  znnnlt1  11281  zltp1le  11304  zleltp1  11305  nn0lt2  11317  recnz  11328  gtndiv  11330  3halfnz  11332  1lt10  11557  eluzp1m1  11587  eluzp1p1  11589  eluz2b2  11637  zbtwnre  11662  rebtwnz  11663  1rp  11712  divlt1lt  11775  divle1le  11776  nnledivrp  11816  qbtwnxr  11905  xmulid1  11981  xmulid2  11982  xmulm1  11983  x2times  12001  xrub  12014  0elunit  12161  1elunit  12162  divelunit  12185  lincmb01cmp  12186  iccf1o  12187  xov1plusxeqvd  12189  unitssre  12190  0nelfz1  12231  fzpreddisj  12260  fznatpl1  12265  fztpval  12272  fraclt1  12465  fracle1  12466  flbi2  12480  ico01fl0  12482  fldiv4p1lem1div2  12498  fldiv4lem1div2  12500  fldiv  12521  modid  12557  1mod  12564  m1modnnsub1  12578  modm1p1mod0  12583  seqf1olem1  12702  reexpcl  12739  reexpclz  12742  expge0  12758  expge1  12759  expgt1  12760  bernneq  12852  bernneq2  12853  expnbnd  12855  expnlbnd  12856  expnlbnd2  12857  expmulnbnd  12858  discr1  12862  facwordi  12938  faclbnd3  12941  faclbnd4lem1  12942  faclbnd4lem4  12945  faclbnd6  12948  facavg  12950  hashv01gt1  12995  hashge1  13039  hashnn0n0nn  13041  hash1snb  13068  hashgt12el  13070  hashgt12el2  13071  hashfun  13084  hashge2el2dif  13117  brfi1indALT  13137  brfi1indALTOLD  13143  lsw0  13205  f1oun2prg  13512  sgn1  13680  cjexp  13738  re1  13742  im1  13743  rei  13744  imi  13745  sqrlem1  13831  sqrlem2  13832  sqrlem3  13833  sqrlem4  13834  sqrlem7  13837  resqrex  13839  sqrt1  13860  sqrt2gt1lt2  13863  sqrtm1  13864  abs1  13885  absrdbnd  13929  caubnd2  13945  mulcn2  14174  reccn2  14175  rlimno1  14232  o1fsum  14386  expcnv  14435  geolim  14440  geolim2  14441  georeclim  14442  geomulcvg  14446  geoisumr  14448  geoisum1c  14450  geoihalfsum  14453  fprodreclf  14528  fprodge0  14563  fprodge1  14565  rerisefaccl  14587  refallfaccl  14588  ere  14658  ege2le3  14659  efgt1  14685  resin4p  14707  recos4p  14708  tanhbnd  14730  sinbnd  14749  cosbnd  14750  sinbnd2  14751  cosbnd2  14752  ef01bndlem  14753  sin01bnd  14754  cos01bnd  14755  cos1bnd  14756  cos2bnd  14757  sinltx  14758  sin01gt0  14759  cos01gt0  14760  sin02gt0  14761  sincos1sgn  14762  ene1  14777  rpnnen2lem2  14783  rpnnen2lem3  14784  rpnnen2lem4  14785  rpnnen2lem9  14790  rpnnen2lem12  14793  ruclem6  14803  ruclem11  14808  ruclem12  14809  3dvds  14890  3dvdsOLD  14891  halfleoddlt  14924  n2dvds1  14942  flodddiv4  14975  sadcadd  15018  isprm3  15234  sqnprm  15252  coprm  15261  phibndlem  15313  pythagtriplem3  15361  pcmpt  15434  fldivp1  15439  pockthi  15449  infpn2  15455  resslem  15760  slotsbhcdif  15903  oppcbas  16201  rescbas  16312  rescabs  16316  odubas  16956  lt6abl  18119  srgbinomlem4  18366  abvneg  18657  abvtrivd  18663  isnzr2hash  19085  0ringnnzr  19090  xrsmcmn  19588  xrsnsgrp  19601  gzrngunitlem  19630  gzrngunit  19631  rge0srg  19636  psgnodpmr  19755  remulg  19772  resubdrg  19773  thlbas  19859  matbas  20038  leordtval2  20826  tuslem  21881  setsmsbas  22090  dscmet  22187  dscopn  22188  nrginvrcnlem  22305  nmoid  22356  idnghm  22357  tgioo  22407  blcvx  22409  metnrmlem1a  22469  metnrmlem1  22470  iicmp  22497  iicon  22498  iirev  22536  iihalf1  22538  iihalf2  22540  iihalf2cn  22541  elii1  22542  elii2  22543  iimulcl  22544  icopnfcnv  22549  icopnfhmeo  22550  iccpnfcnv  22551  iccpnfhmeo  22552  xrhmeo  22553  xrhmph  22554  evth  22566  xlebnum  22572  lebnumii  22573  htpycc  22587  reparphti  22605  pcoval1  22621  pco1  22623  pcoval2  22624  pcocn  22625  pcohtpylem  22627  pcopt  22630  pcopt2  22631  pcoass  22632  pcorevlem  22634  nmhmcn  22728  ncvs1  22765  ovolunlem1a  23071  vitalilem2  23184  vitalilem4  23186  vitalilem5  23187  vitali  23188  i1f1  23263  itg11  23264  itg2const  23313  itg2monolem1  23323  itg2monolem3  23325  dveflem  23546  dvlipcn  23561  dvcvx  23587  ply1remlem  23726  fta1blem  23732  vieta1lem2  23870  aalioulem3  23893  aalioulem5  23895  aaliou3lem2  23902  ulmbdd  23956  iblulm  23965  radcnvlem1  23971  dvradcnv  23979  abelthlem2  23990  abelthlem3  23991  abelthlem5  23993  abelthlem7  23996  abelth  23999  abelth2  24000  reeff1olem  24004  reeff1o  24005  sinhalfpilem  24019  tangtx  24061  sincos4thpi  24069  pige3  24073  coskpi  24076  recosf1o  24085  tanregt0  24089  efif1olem3  24094  efif1olem4  24095  loge  24137  logdivlti  24170  logcnlem4  24191  logf1o2  24196  dvlog2lem  24198  logtayl  24206  logccv  24209  recxpcl  24221  cxplea  24242  cxpcn3lem  24288  cxpaddlelem  24292  loglesqrt  24299  logblog  24330  ang180lem2  24340  angpined  24357  chordthmlem4  24362  acosrecl  24430  atancj  24437  atanlogaddlem  24440  atantan  24450  atans2  24458  ressatans  24461  leibpi  24469  log2le1  24477  birthdaylem3  24480  cxp2lim  24503  cxploglim  24504  cxploglim2  24505  divsqrtsumlem  24506  cvxcl  24511  scvxcvx  24512  jensenlem2  24514  amgmlem  24516  emcllem2  24523  emcllem4  24525  emcllem6  24527  emcllem7  24528  emre  24532  emgt0  24533  harmonicbnd3  24534  harmonicubnd  24536  harmonicbnd4  24537  zetacvg  24541  lgamgulmlem2  24556  ftalem1  24599  ftalem2  24600  ftalem5  24603  issqf  24662  cht1  24691  chp1  24693  ppiltx  24703  mumullem2  24706  ppiublem1  24727  ppiub  24729  chtublem  24736  chtub  24737  logfacbnd3  24748  logexprlim  24750  perfectlem2  24755  dchrinv  24786  dchr1re  24788  efexple  24806  bposlem1  24809  bposlem2  24810  bposlem5  24813  bposlem8  24816  lgsdir2lem1  24850  lgsdir2lem5  24854  lgsdir  24857  lgsne0  24860  lgsabs1  24861  lgsdinn0  24870  gausslemma2dlem0i  24889  lgseisen  24904  m1lgs  24913  2lgslem3  24929  chebbnd1lem3  24960  chebbnd1  24961  chtppilimlem1  24962  chtppilimlem2  24963  chtppilim  24964  chpchtlim  24968  vmadivsumb  24972  rplogsumlem2  24974  rpvmasumlem  24976  dchrmusumlema  24982  dchrmusum2  24983  dchrvmasumlem2  24987  dchrvmasumiflem1  24990  dchrisum0flblem1  24997  dchrisum0flblem2  24998  dchrisum0fno1  25000  rpvmasum2  25001  dchrisum0re  25002  dchrisum0lema  25003  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem2  25007  logdivsum  25022  mulog2sumlem2  25024  2vmadivsumlem  25029  log2sumbnd  25033  selbergb  25038  selberg2b  25041  chpdifbndlem1  25042  selberg3lem1  25046  selberg3lem2  25047  selberg4lem1  25049  pntrmax  25053  pntrsumo1  25054  selbergsb  25064  pntrlog2bndlem3  25068  pntrlog2bndlem5  25070  pntpbnd1a  25074  pntpbnd2  25076  pntibndlem1  25078  pntibndlem2  25080  pntibndlem3  25081  pntibnd  25082  pntlemd  25083  pntlemc  25084  pntlemb  25086  pntlemr  25091  pntlemf  25094  pntlemk  25095  pntlemo  25096  pntlem3  25098  pntleml  25100  pnt  25103  abvcxp  25104  ostth2lem1  25107  padicabvf  25120  padicabvcxp  25121  ostth1  25122  ostth2lem2  25123  ostth2lem3  25124  ostth2lem4  25125  ostth2  25126  ostth3  25127  ostth  25128  trgcgrg  25210  ttgcontlem1  25565  brbtwn2  25585  colinearalglem4  25589  ax5seglem1  25608  ax5seglem2  25609  ax5seglem3  25611  ax5seglem5  25613  ax5seglem6  25614  ax5seglem9  25617  ax5seg  25618  axbtwnid  25619  axpaschlem  25620  axpasch  25621  axlowdimlem6  25627  axlowdimlem10  25631  axlowdimlem16  25637  axlowdim1  25639  axlowdim2  25640  axlowdim  25641  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  lfgrnloop  25791  usgraex1elv  25925  usgraexmpldifpr  25928  spthispth  26103  constr3lem4  26175  constr3pthlem1  26183  konigsberg  26514  frgrawopreglem2  26572  frgrareg  26644  ex-dif  26672  ex-in  26674  ex-pss  26677  ex-res  26690  ex-fl  26696  nv1  26914  smcnlem  26936  ipidsq  26949  nmlno0lem  27032  norm-ii-i  27378  bcs2  27423  norm1  27490  nmopub2tALT  28152  nmfnleub2  28169  nmlnop0iALT  28238  nmopun  28257  unopbd  28258  nmopadjlem  28332  nmopcoadji  28344  pjnmopi  28391  pjbdlni  28392  stge0  28467  stle1  28468  hstle1  28469  hstle  28473  hstles  28474  stge1i  28481  stlesi  28484  staddi  28489  stadd3i  28491  strlem1  28493  strlem3a  28495  strlem5  28498  jplem1  28511  cdj1i  28676  addltmulALT  28689  xlt2addrd  28913  xdivrec  28966  xrsmulgzz  29009  xrnarchi  29069  resvbas  29163  rearchi  29173  xrge0slmod  29175  submateqlem1  29201  elunitrn  29271  elunitge0  29273  unitssxrge0  29274  unitdivcld  29275  xrge0iifcnv  29307  xrge0iifcv  29308  xrge0iifiso  29309  xrge0iifhom  29311  zrhre  29391  indf  29405  indfval  29406  pr01ssre  29407  esumcst  29452  hasheuni  29474  cntnevol  29618  ddemeas  29626  omssubadd  29689  iwrdsplit  29776  prob01  29802  dstfrvclim1  29866  coinfliprv  29871  ballotlem2  29877  ballotlem4  29887  ballotlemi1  29891  ballotlemic  29895  sgnclre  29928  sgnnbi  29934  sgnpbi  29935  sgnmulsgp  29939  plymulx0  29950  plymulx  29951  signswch  29964  signstf  29969  signsvfn  29985  subfacp1lem1  30415  subfacp1lem5  30420  rescon  30482  iiscon  30488  iillyscon  30489  snmlff  30565  problem2  30813  problem2OLD  30814  problem3  30815  sinccvglem  30820  fz0n  30869  dnizeq0  31635  dnibndlem12  31649  knoppcnlem4  31656  knoppndvlem13  31685  cnndvlem1  31698  relowlpssretop  32388  sin2h  32569  cos2h  32570  tan2h  32571  poimirlem7  32586  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem22  32601  poimirlem23  32602  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  broucube  32613  itg2addnclem3  32633  asindmre  32665  dvasin  32666  dvacos  32667  dvreasin  32668  dvreacos  32669  areacirclem1  32670  fdc  32711  geomcau  32725  cntotbnd  32765  heiborlem8  32787  bfplem2  32792  bfp  32793  rabren3dioph  36397  pellexlem5  36415  pellexlem6  36416  pell1qrgaplem  36455  pell14qrgap  36457  pellqrex  36461  pellfundre  36463  pellfundlb  36466  pellfund14gap  36469  rmspecsqrtnqOLD  36489  jm2.17a  36545  acongeq  36568  jm2.23  36581  jm3.1lem2  36603  relexp01min  37024  imo72b2  37497  cvgdvgrat  37534  lhe4.4ex1a  37550  binomcxplemnotnn0  37577  isosctrlem1ALT  38192  supxrgelem  38494  xrlexaddrp  38509  infxr  38524  infleinflem2  38528  sumnnodd  38697  dvnprodlem3  38838  stoweidlem1  38894  stoweidlem18  38911  stoweidlem19  38912  stoweidlem26  38919  stoweidlem34  38927  stoweidlem40  38933  stoweidlem41  38934  stoweidlem59  38952  stoweid  38956  stirlinglem10  38976  stirlinglem11  38977  dirkercncflem1  38996  fourierdlem16  39016  fourierdlem21  39021  fourierdlem22  39022  fourierdlem42  39042  fourierdlem68  39067  fourierdlem83  39082  fourierdlem103  39102  sqwvfourb  39122  fouriersw  39124  etransclem23  39150  salexct2  39233  salgencntex  39237  ovn0lem  39455  smfmullem3  39678  smfmullem4  39679  m1mod0mod1  39949  fmtnosqrt  39989  perfectALTVlem2  40165  nnsum3primesprm  40206  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  tgblthelfgott  40229  tgoldbach  40232  tgblthelfgottOLD  40236  tgoldbachOLD  40239  zm1nn  40348  lfuhgr1v0e  40480  1loopgrvd2  40718  vdegp1bi-av  40753  lfgrwlkprop  40896  pthdlem1  40972  pthdlem2  40974  upgr4cycl4dv4e  41352  konigsberglem2  41423  konigsberglem3  41424  konigsberglem5  41426  frgrwopreglem2  41482  av-frgrareg  41548  basendxnmulrndx  41744  expnegico01  42102  regt1loggt0  42128  rege1logbrege0  42150  rege1logbzge0  42151  blennnelnn  42168  dignnld  42195  nn0sumshdiglemA  42211  nn0sumshdiglem1  42213