Theorem 1re 11203

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 11153, 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 11164	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11153	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11200	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3020	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 252	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11193	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11200	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3021	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 252	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3180	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3180	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 68	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3180	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3180	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 21	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 23	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7418	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7429	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 418	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2979	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 33	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2972	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 876	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 3020	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 3021	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3594	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1139	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 759	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 3020	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 3021	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3594	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
34	33	3expia 1139	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35	34	ad2ant2l 758	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
36	30, 35	jaod 872	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
37	25, 36	syl5 35	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
38	37	rexlimdvva 3222	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3207	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2785	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 417	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2979	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 3020	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3581	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
46	45	expcom 418	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
47	43, 46	syl6 36	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
48	47	com23 87	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
49	48	adantld 495	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
50		neeq1 3020	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3581	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
52	51	expcom 418	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
53	52	adantrd 496	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
54	53	a1dd 51	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
55	49, 54	pm2.61ine 3041	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3207	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11167	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11180	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 727	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2851	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 248	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3166	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 16	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3158	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 860   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∃wrex 3089  (class class class)co 7410  ℂcc 11093  ℝcr 11094  0cc0 11095  1c1 11096  ici 11097   + caddc 11098   · cmul 11100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-mulcl 11157  ax-mulrcl 11158  ax-i2m1 11163  ax-1ne0 11164  ax-rrecex 11167  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is referenced by:  1red  11204  pr01ssre  11207  1xr  11263  dedekind  11368  peano2re  11378  mul02lem2  11382  addrid  11385  renegcl  11516  peano2rem  11520  0reALT  11550  0lt1  11731  0le1  11732  relin01  11733  1le1  11837  eqneg  11930  ltp1  12050  ltm1  12052  recgt0  12056  ltmulgt11  12069  lemulge11  12072  reclt1  12105  recgt1  12106  recgt1i  12107  recp1lt1  12108  recreclt  12109  recgt0ii  12116  ledivp1i  12135  ltdivp1i  12136  neg1rr  12199  neg1lt0  12201  cju  12209  indf  12219  indfval  12220  nnssre  12232  nnge1  12259  nngt1ne1  12260  nnle1eq1  12261  nngt0  12262  nnnlt1  12263  nnne0  12265  nnrecre  12273  nnrecgt0  12274  nnsub  12275  1t1e1ALT  12286  2re  12310  3re  12316  4re  12320  5re  12323  6re  12326  7re  12329  8re  12332  9re  12335  0le2OLD  12339  2posOLD  12341  1lt2  12408  1lt3  12411  1lt4  12414  1lt5  12418  1lt6  12423  1lt7  12429  1lt8  12436  1lt9  12444  1ne2  12446  1le2  12447  1le3  12450  halflt1  12456  addltmul  12475  nnunb  12495  elnnnn0c  12544  nn0ge2m1nn  12569  elnnz1  12615  znnnlt1  12616  zltp1le  12639  zleltp1  12640  nn0lt2  12654  recnz  12666  gtndiv  12668  3halfnz  12670  10re  12729  1lt10  12851  1lt10OLD  12852  eluzp1m1  12883  eluzp1p1  12885  eluz2b2  12940  zbtwnre  12965  rebtwnz  12966  1rp  13015  divlt1lt  13082  divle1le  13083  nnledivrp  13125  qbtwnxr  13221  xmulrid  13300  xmulm1  13302  x2times  13320  xrub  13333  elicc01  13488  1elunit  13492  divelunit  13516  lincmb01cmp  13517  unitssre  13521  0nelfz1  13566  fzpreddisj  13597  fznatpl1  13602  fztpval  13610  fraclt1  13831  fracle1  13832  flbi2  13846  fldiv4p1lem1div2  13864  fldiv4lem1div2  13866  fldiv  13889  modid  13925  1mod  13932  m1modnnsub1  13949  modm1p1mod0  13954  seqf1olem1  14073  reexpcl  14110  reexpclz  14114  expge0  14130  expge1  14131  expgt1  14132  bernneq  14261  bernneq2  14262  expnbnd  14264  expnlbnd  14265  expnlbnd2  14266  expmulnbnd  14267  discr1  14271  facwordi  14321  faclbnd3  14324  faclbnd4lem1  14325  faclbnd4lem4  14328  faclbnd6  14331  facavg  14333  hashv01gt1  14377  hashnn0n0nn  14423  hashunsnggt  14426  hash1snb  14452  hashgt12el  14455  hashgt12el2  14456  hashfun  14470  hashge2el2dif  14513  tpf1ofv2  14531  lsw0  14598  f1oun2prg  14950  sgnclre  15135  sgnnbi  15137  sgnpbi  15138  cjexp  15197  re1  15201  im1  15202  rei  15203  imi  15204  01sqrexlem1  15289  01sqrexlem2  15290  01sqrexlem3  15291  01sqrexlem4  15292  01sqrexlem7  15295  resqrex  15297  sqrt1  15318  sqrt2gt1lt2  15321  sqrtm1  15322  abs1  15344  absrdbnd  15389  caubnd2  15405  mulcn2  15643  reccn2  15644  rlimno1  15701  o1fsum  15861  expcnv  15914  geolim  15920  geolim2  15921  georeclim  15922  geomulcvg  15926  geoisumr  15928  geoisum1c  15930  fprodge0  16043  fprodge1  16045  rerisefaccl  16067  refallfaccl  16068  ere  16138  ege2le3  16139  efgt1  16167  resin4p  16189  recos4p  16190  tanhbnd  16212  sinbnd  16231  cosbnd  16232  sinbnd2  16233  cosbnd2  16234  ef01bndlem  16235  sin01bnd  16236  cos01bnd  16237  cos1bnd  16238  cos2bnd  16239  sinltx  16240  sin01gt0  16241  cos01gt0  16242  sin02gt0  16243  sincos1sgn  16244  ene1  16261  rpnnen2lem2  16266  rpnnen2lem3  16267  rpnnen2lem4  16268  rpnnen2lem9  16273  rpnnen2lem12  16276  ruclem6  16286  ruclem11  16291  ruclem12  16292  3dvds  16384  flodddiv4  16468  sadcadd  16511  isprm3  16736  sqnprm  16756  coprm  16765  phibndlem  16824  pythagtriplem3  16873  pcmpt  16947  fldivp1  16952  pockthi  16962  infpn2  16968  basendxnmulrndx  17344  starvndxnbasendx  17352  scandxnbasendx  17364  vscandxnbasendx  17369  ipndxnbasendx  17380  basendxnocndx  17431  slotsbhcdif  17463  lt6abl  19960  srgbinomlem4  20306  0ringnnzr  20623  abvneg  20929  abvtrivd  20935  prmidl0  21478  xrsmcmn  21545  xrsnsgrp  21558  gzrngunitlem  21582  gzrngunit  21583  rge0srg  21588  psgnodpmr  21740  remulg  21757  resubdrg  21758  psdmvr  22332  dscmet  24729  dscopn  24730  nrginvrcnlem  24848  idnghm  24900  tgioo  24953  blcvx  24955  iicmp  25045  iiconn  25046  iirev  25088  iihalf1  25090  iihalf2  25092  elii1  25094  elii2  25095  iimulcl  25096  icopnfcnv  25101  icopnfhmeo  25102  iccpnfhmeo  25104  xrhmeo  25105  xrhmph  25106  evth  25118  xlebnum  25124  htpycc  25139  reparphti  25156  pcoval1  25172  pco1  25174  pcoval2  25175  pcocn  25176  pcohtpylem  25178  pcopt  25181  pcopt2  25182  pcoass  25183  pcorevlem  25185  nmhmcn  25279  ncvs1  25316  ovolunlem1a  25655  vitalilem2  25768  vitalilem4  25770  vitalilem5  25771  vitali  25772  i1f1  25849  itg11  25850  itg2const  25899  dveflem  26138  dvlipcn  26153  dvcvx  26179  ply1remlem  26322  fta1blem  26328  plyn0mulidp  26442  plymulidp  26443  vieta1lem2  26472  aalioulem3  26497  aalioulem5  26499  aaliou3lem2  26506  ulmbdd  26561  iblulm  26570  radcnvlem1  26576  dvradcnv  26584  abelthlem2  26595  abelthlem3  26596  abelthlem5  26598  abelthlem7  26601  abelth  26604  abelth2  26605  reeff1olem  26609  reeff1o  26610  sinhalfpilem  26628  tangtx  26670  sincos4thpi  26678  pige3ALT  26685  coskpi  26688  cos0pilt1  26697  recosf1o  26700  tanregt0  26704  efif1olem3  26709  efif1olem4  26710  loge  26751  logdivlti  26785  logcnlem4  26810  logf1o2  26815  logtayl  26825  logccv  26828  recxpcl  26840  cxplea  26861  cxpcn3lem  26912  cxpaddlelem  26916  loglesqrt  26926  ang180lem2  26975  angpined  26995  acosrecl  27068  atancj  27075  atanlogaddlem  27078  atantan  27088  atans2  27096  ressatans  27099  leibpi  27107  log2le1  27115  birthdaylem3  27118  cxp2lim  27141  cxploglim  27142  cxploglim2  27143  divsqrtsumlem  27144  cvxcl  27149  scvxcvx  27150  jensenlem2  27152  amgmlem  27154  emcllem2  27161  emcllem4  27163  emcllem6  27165  emcllem7  27166  emre  27170  emgt0  27171  harmonicbnd3  27172  harmonicubnd  27174  harmonicbnd4  27175  zetacvg  27179  ftalem1  27237  ftalem2  27238  ftalem5  27241  issqf  27300  cht1  27329  chp1  27331  ppiltx  27341  mumullem2  27344  ppiublem1  27366  ppiub  27368  chtublem  27375  chtub  27376  logfacbnd3  27387  logexprlim  27389  perfectlem2  27394  dchrinv  27425  dchr1re  27427  efexple  27445  bposlem1  27448  bposlem2  27449  bposlem5  27452  bposlem8  27455  lgsdir2lem1  27489  lgsdir2lem5  27493  lgsdir  27496  lgsne0  27499  lgsabs1  27500  lgsdinn0  27509  gausslemma2dlem0i  27528  lgseisen  27543  m1lgs  27552  2lgslem3  27568  addsq2nreurex  27608  2sqreultblem  27612  2sqreunnltblem  27615  chebbnd1lem3  27635  chebbnd1  27636  chtppilimlem1  27637  chtppilimlem2  27638  chtppilim  27639  chpchtlim  27643  vmadivsumb  27647  rplogsumlem2  27649  rpvmasumlem  27651  dchrmusumlema  27657  dchrmusum2  27658  dchrvmasumlem2  27662  dchrvmasumiflem1  27665  dchrisum0flblem1  27672  dchrisum0flblem2  27673  dchrisum0fno1  27675  rpvmasum2  27676  dchrisum0re  27677  dchrisum0lema  27678  dchrisum0lem1b  27679  dchrisum0lem1  27680  dchrisum0lem2a  27681  dchrisum0lem2  27682  logdivsum  27697  mulog2sumlem2  27699  2vmadivsumlem  27704  log2sumbnd  27708  selbergb  27713  selberg2b  27716  chpdifbndlem1  27717  selberg3lem1  27721  selberg3lem2  27722  selberg4lem1  27724  pntrmax  27728  pntrsumo1  27729  selbergsb  27739  pntrlog2bndlem3  27743  pntrlog2bndlem5  27745  pntpbnd1a  27749  pntpbnd2  27751  pntibndlem1  27753  pntibndlem3  27756  pntlemd  27758  pntlemc  27759  pntlemb  27761  pntlemr  27766  pntlemf  27769  pntlemk  27770  pntlemo  27771  pntlem3  27773  pntleml  27775  abvcxp  27779  ostth2lem1  27782  ostth1  27797  ostth2lem2  27798  ostth2lem3  27799  ostth2lem4  27800  ostth2  27801  ostth3  27802  ostth  27803  slotsinbpsd  28710  slotslnbpsd  28711  trgcgrg  28784  brbtwn2  29255  colinearalglem4  29259  ax5seglem2  29279  ax5seglem3  29281  axpaschlem  29290  axpasch  29291  axlowdimlem6  29297  axlowdimlem10  29301  axlowdimlem16  29307  axlowdim1  29309  axlowdim2  29310  axlowdim  29311  axcontlem2  29315  elntg2  29335  lfgrnloop  29475  lfuhgr1v0e  29604  usgrexmpldifpr  29608  usgrexmplef  29609  1loopgrvd2  29853  vdegp1bi  29887  lfgrwlkprop  30035  pthdlem1  30115  pthdlem2  30117  clwlkclwwlkf  30359  upgr4cycl4dv4e  30536  konigsberglem2  30604  konigsberglem3  30605  konigsberglem5  30607  frgrreg  30745  ex-dif  30774  ex-in  30776  ex-pss  30779  ex-res  30792  ex-fl  30798  nv1  31027  smcnlem  31049  ipidsq  31062  nmlno0lem  31145  norm-ii-i  31489  bcs2  31534  norm1  31601  nmopub2tALT  32261  nmfnleub2  32278  nmlnop0iALT  32347  unopbd  32367  nmopadjlem  32441  nmopcoadji  32453  pjnmopi  32500  pjbdlni  32501  hstle1  32578  hstle  32582  hstles  32583  stge1i  32590  stlesi  32593  staddi  32598  stadd3i  32600  strlem1  32602  strlem5  32607  jplem1  32620  cdj1i  32785  addltmulALT  32798  xlt2addrd  33104  sgnmulsgp  33176  dp2lt10  33203  dp2ltsuc  33205  dp2ltc  33206  dplti  33224  dpmul4  33233  cshw1s2  33280  xrsmulgzz  33329  rearchi  33666  xrge0slmod  33668  evl1deg3  33868  constrconj  34135  2sqr3minply  34170  submateqlem1  34197  xrge0iifcnv  34323  xrge0iifcv  34324  xrge0iifiso  34325  xrge0iifhom  34327  zrhre  34409  esumcst  34453  cntnevol  34618  omssubadd  34690  iwrdsplit  34777  dstfrvclim1  34868  coinfliprv  34873  ballotlem2  34879  ballotlem4  34889  ballotlemi1  34893  ballotlemic  34897  signswch  34948  signstf  34953  signsvfn  34969  itgexpif  34993  hgt750lemd  35035  logdivsqrle  35037  hgt750lem  35038  hgt750lem2  35039  hgt750leme  35045  tgoldbachgnn  35046  subfacp1lem1  35671  subfacp1lem5  35676  resconn  35738  iisconn  35744  iillysconn  35745  problem2  36158  problem3  36159  sinccvglem  36164  fz0n  36223  dnibndlem12  37078  knoppcnlem4  37085  knoppndvlem13  37113  cnndvlem1  37126  irrdiff  37970  relowlpssretop  38010  sin2h  38261  cos2h  38262  tan2h  38263  poimirlem7  38278  poimirlem16  38287  poimirlem17  38288  poimirlem19  38290  poimirlem20  38291  poimirlem22  38293  poimirlem23  38294  poimirlem29  38300  poimirlem31  38302  itg2addnclem3  38324  asindmre  38354  dvasin  38355  dvacos  38356  dvreasin  38357  dvreacos  38358  fdc  38396  geomcau  38410  cntotbnd  38447  heiborlem8  38469  bfplem2  38474  bfp  38475  aks4d1p1p7  42841  ine1  43075  re1m1e0m0  43158  sn-00idlem1  43159  sn-00idlem2  43160  remul02  43166  sn-0ne2  43167  reixi  43184  rei4  43185  remullid  43195  ipiiie0  43199  sn-0tie0  43225  sn-nnne0  43234  mulgt0b1d  43246  sn-0lt1  43249  sn-ltp1  43250  reneg1lt0  43254  sn-inelr  43261  rabren3dioph  43542  pellexlem5  43560  pellexlem6  43561  pell1qrgaplem  43600  pell14qrgap  43602  pellqrex  43606  pellfundre  43608  pellfundlb  43611  pellfund14gap  43614  jm2.17a  43687  acongeq  43710  jm2.23  43723  jm3.1lem2  43745  sqrtcval  44367  sqrtcval2  44368  resqrtval  44369  imsqrtval  44370  relexp01min  44439  cvgdvgrat  45023  lhe4.4ex1a  45039  binomcxplemnotnn0  45066  isosctrlem1ALT  45642  supxrgelem  46053  xrlexaddrp  46068  infxr  46082  infleinflem2  46086  sumnnodd  46346  limsup10exlem  46486  limsup10ex  46487  dvnprodlem3  46662  stoweidlem1  46715  stoweidlem18  46732  stoweidlem19  46733  stoweidlem26  46740  stoweidlem34  46748  stoweidlem40  46754  stoweidlem41  46755  stoweidlem59  46773  stoweid  46777  stirlinglem10  46797  stirlinglem11  46798  dirkercncflem1  46817  fourierdlem16  46837  fourierdlem21  46842  fourierdlem22  46843  fourierdlem42  46863  fourierdlem68  46888  fourierdlem83  46903  fourierdlem103  46923  sqwvfourb  46943  fouriersw  46945  etransclem23  46971  salgencntex  47057  ovn0lem  47279  smfmullem3  47507  smfmullem4  47508  nthrucw  47607  cjnpoly  47626  zm1nn  48039  ceilhalf1  48075  m1mod0mod1  48097  muldvdsfacgt  48123  fmtnosqrt  48291  nprmdvdsfacm1lem4  48375  perfectALTVlem2  48487  2exp340mod341  48498  8exp8mod9  48501  nfermltl8rev  48507  nnsum3primesprm  48555  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  nnsum4primeseven  48565  nnsum4primesevenALTV  48566  tgblthelfgott  48580  tgoldbach  48582  usgrexmpl1lem  48786  usgrexmpl2lem  48791  usgrexmpl2nb1  48797  usgrexmpl2nb3  48799  usgrexmpl2nb4  48800  usgrexmpl2nb5  48801  usgrexmpl2trifr  48802  gpg3kgrtriexlem3  48850  pgnbgreunbgrlem2lem1  48879  pgnbgreunbgrlem2lem2  48880  rege1logbrege0  49338  rege1logbzge0  49339  blennnelnn  49356  dignnld  49383  nn0sumshdiglemA  49399  nn0sumshdiglem1  49401  rrx2xpref1o  49498  rrxlines  49513  eenglngeehlnmlem1  49517  eenglngeehlnmlem2  49518  line2ylem  49531  line2x  49534  icccldii  49697  io1ii  49699  sepfsepc  49706