Theorem 1re 10641

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 10595, 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 10606	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 10595	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 10638	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3078	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 251	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 10633	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 10638	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3079	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 251	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3273	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3273	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3273	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3273	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 980	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 3017	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 360	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 3017	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 360	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 628	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 280	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 7164	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 7175	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 219	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 3043	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 3078	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 3079	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3635	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1117	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 745	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 3078	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 3079	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3635	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1117	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 744	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 855	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3294	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3292	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2843	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 415	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 3037	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 3078	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3623	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
50	49	expcom 416	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
51	47, 50	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
52	51	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
53	52	adantld 493	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54		neeq1 3078	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3623	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
56	55	expcom 416	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
57	56	adantrd 494	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
58	57	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
59	53, 58	pm2.61ine 3100	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3292	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 10609	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 10622	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 713	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2900	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 247	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3284	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3281	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∨ wo 843   = wceq 1537   ∈ wcel 2114   ≠ wne 3016  ∃wrex 3139  (class class class)co 7156  ℂcc 10535  ℝcr 10536  0cc0 10537  1c1 10538  ici 10539   + caddc 10540   · cmul 10542

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-mulcl 10599  ax-mulrcl 10600  ax-i2m1 10605  ax-1ne0 10606  ax-rrecex 10609  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  1red  10642  1xr  10700  dedekind  10803  peano2re  10813  mul02lem2  10817  addid1  10820  renegcl  10949  peano2rem  10953  0reALT  10983  0lt1  11162  0le1  11163  relin01  11164  1le1  11268  eqneg  11360  ltp1  11480  ltm1  11482  recgt0  11486  mulgt1  11499  ltmulgt11  11500  lemulge11  11502  reclt1  11535  recgt1  11536  recgt1i  11537  recp1lt1  11538  recreclt  11539  recgt0ii  11546  ledivp1i  11565  ltdivp1i  11566  inelr  11628  cju  11634  nnssre  11642  nnge1  11666  nngt1ne1  11667  nnle1eq1  11668  nngt0  11669  nnnlt1  11670  nnne0  11672  nnrecre  11680  nnrecgt0  11681  nnsub  11682  2re  11712  3re  11718  4re  11722  5re  11725  6re  11728  7re  11731  8re  11734  9re  11737  0le2  11740  2pos  11741  3pos  11743  4pos  11745  5pos  11747  6pos  11748  7pos  11749  8pos  11750  9pos  11751  neg1rr  11753  neg1lt0  11755  1lt2  11809  1lt3  11811  1lt4  11814  1lt5  11818  1lt6  11823  1lt7  11829  1lt8  11836  1lt9  11844  1ne2  11846  1le2  11847  1le3  11850  halflt1  11856  addltmul  11874  nnunb  11894  elnnnn0c  11943  nn0ge2m1nn  11965  elnnz1  12009  znnnlt1  12010  zltp1le  12033  zleltp1  12034  nn0lt2  12046  recnz  12058  gtndiv  12060  3halfnz  12062  10re  12118  1lt10  12238  eluzp1m1  12269  eluzp1p1  12271  eluz2b2  12322  zbtwnre  12347  rebtwnz  12348  1rp  12394  divlt1lt  12459  divle1le  12460  nnledivrp  12502  qbtwnxr  12594  xmulid1  12673  xmulm1  12675  x2times  12693  xrub  12706  elicc01  12855  1elunit  12857  divelunit  12881  lincmb01cmp  12882  unitssre  12886  0nelfz1  12927  fzpreddisj  12957  fznatpl1  12962  fztpval  12970  fraclt1  13173  fracle1  13174  flbi2  13188  fldiv4p1lem1div2  13206  fldiv4lem1div2  13208  fldiv  13229  modid  13265  1mod  13272  m1modnnsub1  13286  modm1p1mod0  13291  seqf1olem1  13410  reexpcl  13447  reexpclz  13450  expge0  13466  expge1  13467  expgt1  13468  bernneq  13591  bernneq2  13592  expnbnd  13594  expnlbnd  13595  expnlbnd2  13596  expmulnbnd  13597  discr1  13601  facwordi  13650  faclbnd3  13653  faclbnd4lem1  13654  faclbnd4lem4  13657  faclbnd6  13660  facavg  13662  hashv01gt1  13706  hashnn0n0nn  13753  hashunsnggt  13756  hash1snb  13781  hashgt12el  13784  hashgt12el2  13785  hashfun  13799  hashge2el2dif  13839  brfi1indALT  13859  lsw0  13917  f1oun2prg  14279  cjexp  14509  re1  14513  im1  14514  rei  14515  imi  14516  sqrlem1  14602  sqrlem2  14603  sqrlem3  14604  sqrlem4  14605  sqrlem7  14608  resqrex  14610  sqrt1  14631  sqrt2gt1lt2  14634  sqrtm1  14635  abs1  14657  absrdbnd  14701  caubnd2  14717  mulcn2  14952  reccn2  14953  rlimno1  15010  o1fsum  15168  expcnv  15219  geolim  15226  geolim2  15227  georeclim  15228  geomulcvg  15232  geoisumr  15234  geoisum1c  15236  fprodge0  15347  fprodge1  15349  rerisefaccl  15371  refallfaccl  15372  ere  15442  ege2le3  15443  efgt1  15469  resin4p  15491  recos4p  15492  tanhbnd  15514  sinbnd  15533  cosbnd  15534  sinbnd2  15535  cosbnd2  15536  ef01bndlem  15537  sin01bnd  15538  cos01bnd  15539  cos1bnd  15540  cos2bnd  15541  sinltx  15542  sin01gt0  15543  cos01gt0  15544  sin02gt0  15545  sincos1sgn  15546  ene1  15563  rpnnen2lem2  15568  rpnnen2lem3  15569  rpnnen2lem4  15570  rpnnen2lem9  15575  rpnnen2lem12  15578  ruclem6  15588  ruclem11  15593  ruclem12  15594  3dvds  15680  n2dvds1OLD  15718  flodddiv4  15764  sadcadd  15807  isprm3  16027  sqnprm  16046  coprm  16055  phibndlem  16107  pythagtriplem3  16155  pcmpt  16228  fldivp1  16233  pockthi  16243  infpn2  16249  resslem  16557  basendxnmulrndx  16618  slotsbhcdif  16693  oppcbas  16988  rescbas  17099  rescabs  17103  odubas  17743  symgvalstruct  18525  lt6abl  19015  srgbinomlem4  19293  abvneg  19605  abvtrivd  19611  rmodislmod  19702  0ringnnzr  20042  cnfldfun  20557  xrsmcmn  20568  xrsnsgrp  20581  gzrngunitlem  20610  gzrngunit  20611  rge0srg  20616  psgnodpmr  20734  remulg  20751  resubdrg  20752  thlbas  20840  tuslem  22876  setsmsbas  23085  dscmet  23182  dscopn  23183  nrginvrcnlem  23300  idnghm  23352  tgioo  23404  blcvx  23406  iicmp  23494  iiconn  23495  iirev  23533  iihalf1  23535  iihalf2  23537  iihalf2cn  23538  elii1  23539  elii2  23540  iimulcl  23541  icopnfcnv  23546  icopnfhmeo  23547  iccpnfhmeo  23549  xrhmeo  23550  xrhmph  23551  evth  23563  xlebnum  23569  htpycc  23584  reparphti  23601  pcoval1  23617  pco1  23619  pcoval2  23620  pcocn  23621  pcohtpylem  23623  pcopt  23626  pcopt2  23627  pcoass  23628  pcorevlem  23630  nmhmcn  23724  ncvs1  23761  ovolunlem1a  24097  vitalilem2  24210  vitalilem4  24212  vitalilem5  24213  vitali  24214  i1f1  24291  itg11  24292  itg2const  24341  dveflem  24576  dvlipcn  24591  dvcvx  24617  ply1remlem  24756  fta1blem  24762  vieta1lem2  24900  aalioulem3  24923  aalioulem5  24925  aaliou3lem2  24932  ulmbdd  24986  iblulm  24995  radcnvlem1  25001  dvradcnv  25009  abelthlem2  25020  abelthlem3  25021  abelthlem5  25023  abelthlem7  25026  abelth  25029  abelth2  25030  reeff1olem  25034  reeff1o  25035  sinhalfpilem  25049  tangtx  25091  sincos4thpi  25099  pige3ALT  25105  coskpi  25108  recosf1o  25119  tanregt0  25123  efif1olem3  25128  efif1olem4  25129  loge  25170  logdivlti  25203  logcnlem4  25228  logf1o2  25233  logtayl  25243  logccv  25246  recxpcl  25258  cxplea  25279  cxpcn3lem  25328  cxpaddlelem  25332  loglesqrt  25339  ang180lem2  25388  angpined  25408  acosrecl  25481  atancj  25488  atanlogaddlem  25491  atantan  25501  atans2  25509  ressatans  25512  leibpi  25520  log2le1  25528  birthdaylem3  25531  cxp2lim  25554  cxploglim  25555  cxploglim2  25556  divsqrtsumlem  25557  cvxcl  25562  scvxcvx  25563  jensenlem2  25565  amgmlem  25567  emcllem2  25574  emcllem4  25576  emcllem6  25578  emcllem7  25579  emre  25583  emgt0  25584  harmonicbnd3  25585  harmonicubnd  25587  harmonicbnd4  25588  zetacvg  25592  ftalem1  25650  ftalem2  25651  ftalem5  25654  issqf  25713  cht1  25742  chp1  25744  ppiltx  25754  mumullem2  25757  ppiublem1  25778  ppiub  25780  chtublem  25787  chtub  25788  logfacbnd3  25799  logexprlim  25801  perfectlem2  25806  dchrinv  25837  dchr1re  25839  efexple  25857  bposlem1  25860  bposlem2  25861  bposlem5  25864  bposlem8  25867  lgsdir2lem1  25901  lgsdir2lem5  25905  lgsdir  25908  lgsne0  25911  lgsabs1  25912  lgsdinn0  25921  gausslemma2dlem0i  25940  lgseisen  25955  m1lgs  25964  2lgslem3  25980  addsq2nreurex  26020  2sqreultblem  26024  2sqreunnltblem  26027  chebbnd1lem3  26047  chebbnd1  26048  chtppilimlem1  26049  chtppilimlem2  26050  chtppilim  26051  chpchtlim  26055  vmadivsumb  26059  rplogsumlem2  26061  rpvmasumlem  26063  dchrmusumlema  26069  dchrmusum2  26070  dchrvmasumlem2  26074  dchrvmasumiflem1  26077  dchrisum0flblem1  26084  dchrisum0flblem2  26085  dchrisum0fno1  26087  rpvmasum2  26088  dchrisum0re  26089  dchrisum0lema  26090  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0lem2a  26093  dchrisum0lem2  26094  logdivsum  26109  mulog2sumlem2  26111  2vmadivsumlem  26116  log2sumbnd  26120  selbergb  26125  selberg2b  26128  chpdifbndlem1  26129  selberg3lem1  26133  selberg3lem2  26134  selberg4lem1  26136  pntrmax  26140  pntrsumo1  26141  selbergsb  26151  pntrlog2bndlem3  26155  pntrlog2bndlem5  26157  pntpbnd1a  26161  pntpbnd2  26163  pntibndlem1  26165  pntibndlem3  26168  pntlemd  26170  pntlemc  26171  pntlemb  26173  pntlemr  26178  pntlemf  26181  pntlemk  26182  pntlemo  26183  pntlem3  26185  pntleml  26187  abvcxp  26191  ostth2lem1  26194  ostth1  26209  ostth2lem2  26210  ostth2lem3  26211  ostth2lem4  26212  ostth2  26213  ostth3  26214  ostth  26215  trgcgrg  26301  brbtwn2  26691  colinearalglem4  26695  ax5seglem2  26715  ax5seglem3  26717  axpaschlem  26726  axpasch  26727  axlowdimlem6  26733  axlowdimlem10  26737  axlowdimlem16  26743  axlowdim1  26745  axlowdim2  26746  axlowdim  26747  axcontlem2  26751  elntg2  26771  lfgrnloop  26910  lfuhgr1v0e  27036  usgrexmpldifpr  27040  usgrexmplef  27041  1loopgrvd2  27285  vdegp1bi  27319  lfgrwlkprop  27469  pthdlem1  27547  pthdlem2  27549  clwlkclwwlkf  27786  upgr4cycl4dv4e  27964  konigsberglem2  28032  konigsberglem3  28033  konigsberglem5  28035  frgrreg  28173  ex-dif  28202  ex-in  28204  ex-pss  28207  ex-res  28220  ex-fl  28226  nv1  28452  smcnlem  28474  ipidsq  28487  nmlno0lem  28570  norm-ii-i  28914  bcs2  28959  norm1  29026  nmopub2tALT  29686  nmfnleub2  29703  nmlnop0iALT  29772  unopbd  29792  nmopadjlem  29866  nmopcoadji  29878  pjnmopi  29925  pjbdlni  29926  hstle1  30003  hstle  30007  hstles  30008  stge1i  30015  stlesi  30018  staddi  30023  stadd3i  30025  strlem1  30027  strlem5  30032  jplem1  30045  cdj1i  30210  addltmulALT  30223  xlt2addrd  30482  pr01ssre  30540  dp2lt10  30560  dp2ltsuc  30562  dp2ltc  30563  dplti  30581  dpmul4  30590  cshw1s2  30634  xrsmulgzz  30665  resvbas  30905  rearchi  30915  xrge0slmod  30917  submateqlem1  31072  xrge0iifcnv  31176  xrge0iifcv  31177  xrge0iifiso  31178  xrge0iifhom  31180  zrhre  31260  indf  31274  indfval  31275  esumcst  31322  cntnevol  31487  omssubadd  31558  iwrdsplit  31645  dstfrvclim1  31735  coinfliprv  31740  ballotlem2  31746  ballotlem4  31756  ballotlemi1  31760  ballotlemic  31764  sgnclre  31797  sgnnbi  31803  sgnpbi  31804  sgnmulsgp  31808  plymulx0  31817  plymulx  31818  signswch  31831  signstf  31836  signsvfn  31852  itgexpif  31877  hgt750lemd  31919  logdivsqrle  31921  hgt750lem  31922  hgt750lem2  31923  hgt750leme  31929  tgoldbachgnn  31930  subfacp1lem1  32426  subfacp1lem5  32431  resconn  32493  iisconn  32499  iillysconn  32500  problem2  32909  problem3  32910  sinccvglem  32915  fz0n  32962  dnibndlem12  33828  knoppcnlem4  33835  knoppndvlem13  33863  cnndvlem1  33876  relowlpssretop  34648  sin2h  34897  cos2h  34898  tan2h  34899  poimirlem7  34914  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem22  34929  poimirlem23  34930  poimirlem29  34936  poimirlem31  34938  itg2addnclem3  34960  asindmre  34992  dvasin  34993  dvacos  34994  dvreasin  34995  dvreacos  34996  fdc  35035  geomcau  35049  cntotbnd  35089  heiborlem8  35111  bfplem2  35116  bfp  35117  2xp3dxp2ge1d  39146  factwoffsmonot  39147  1t1e1ALT  39204  re1m1e0m0  39276  sn-00idlem1  39277  sn-00idlem2  39278  remul02  39284  sn-0ne2  39285  sn-0lt1  39295  sn-ltp1  39296  remulid2  39298  rabren3dioph  39461  pellexlem5  39479  pellexlem6  39480  pell1qrgaplem  39519  pell14qrgap  39521  pellqrex  39525  pellfundre  39527  pellfundlb  39530  pellfund14gap  39533  jm2.17a  39606  acongeq  39629  jm2.23  39642  jm3.1lem2  39664  relexp01min  40107  cvgdvgrat  40694  lhe4.4ex1a  40710  binomcxplemnotnn0  40737  isosctrlem1ALT  41317  supxrgelem  41654  xrlexaddrp  41669  infxr  41684  infleinflem2  41688  sumnnodd  41960  limsup10exlem  42102  limsup10ex  42103  dvnprodlem3  42282  stoweidlem1  42335  stoweidlem18  42352  stoweidlem19  42353  stoweidlem26  42360  stoweidlem34  42368  stoweidlem40  42374  stoweidlem41  42375  stoweidlem59  42393  stoweid  42397  stirlinglem10  42417  stirlinglem11  42418  dirkercncflem1  42437  fourierdlem16  42457  fourierdlem21  42462  fourierdlem22  42463  fourierdlem42  42483  fourierdlem68  42508  fourierdlem83  42523  fourierdlem103  42543  sqwvfourb  42563  fouriersw  42565  etransclem23  42591  salgencntex  42675  ovn0lem  42896  smfmullem3  43117  smfmullem4  43118  zm1nn  43551  m1mod0mod1  43578  fmtnosqrt  43750  perfectALTVlem2  43936  2exp340mod341  43947  8exp8mod9  43950  nfermltl8rev  43956  nnsum3primesprm  44004  nnsum4primesodd  44010  nnsum4primesoddALTV  44011  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  tgblthelfgott  44029  tgoldbach  44031  rege1logbrege0  44667  rege1logbzge0  44668  blennnelnn  44685  dignnld  44712  nn0sumshdiglemA  44728  nn0sumshdiglem1  44730  rrx2xpref1o  44754  rrxlines  44769  eenglngeehlnmlem1  44773  eenglngeehlnmlem2  44774  line2ylem  44787  line2x  44790