Theorem 1re 10039

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 9994, 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 10005	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 9994	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 10036	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 2856	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 239	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 10032	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 10036	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 2857	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 239	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3016	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3016	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3016	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3016	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 511	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2795	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 347	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2795	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 347	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 733	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 267	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 6658	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 6669	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 207	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2821	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 2856	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 2857	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3324	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1267	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 783	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 2856	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 2857	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3324	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1267	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 782	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 395	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3038	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3036	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2643	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 450	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2815	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 2856	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3309	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
50	49	expcom 451	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
51	47, 50	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
52	51	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
53	52	adantld 483	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54		neeq1 2856	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3309	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
56	55	expcom 451	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
57	56	adantrd 484	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
58	57	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
59	53, 58	pm2.61ine 2877	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3036	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 10008	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 10021	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 751	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2689	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 235	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3031	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3028	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 383   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∃wrex 2913  (class class class)co 6650  ℂcc 9934  ℝcr 9935  0cc0 9936  1c1 9937  ici 9938   + caddc 9939   · cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  0re  10040  1red  10055  dedekind  10200  peano2re  10209  mul02lem2  10213  addid1  10216  renegcl  10344  peano2rem  10348  0reALT  10378  0lt1  10550  0le1  10551  relin01  10552  1le1  10655  eqneg  10745  ltp1  10861  ltm1  10863  recgt0  10867  mulgt1  10882  ltmulgt11  10883  lemulge11  10885  reclt1  10918  recgt1  10919  recgt1i  10920  recp1lt1  10921  recreclt  10922  recgt0ii  10929  ledivp1i  10949  ltdivp1i  10950  inelr  11010  cju  11016  nnssre  11024  nnge1  11046  nngt1ne1  11047  nnle1eq1  11048  nngt0  11049  nnnlt1  11050  nnrecre  11057  nnrecgt0  11058  nnsub  11059  2re  11090  3re  11094  4re  11097  5re  11099  6re  11101  7re  11103  8re  11105  9re  11107  10reOLD  11109  0le2  11111  2pos  11112  3pos  11114  4pos  11116  5pos  11118  6pos  11119  7pos  11120  8pos  11121  9pos  11122  10posOLD  11123  neg1rr  11125  neg1lt0  11127  1lt2  11194  1lt3  11196  1lt4  11199  1lt5  11203  1lt6  11208  1lt7  11214  1lt8  11221  1lt9  11229  1lt10OLD  11238  1ne2  11240  1le2  11241  1le3  11244  halflt1  11250  addltmul  11268  nnunb  11288  elnnnn0c  11338  nn0ge2m1nn  11360  elnnz1  11403  znnnlt1  11404  zltp1le  11427  zleltp1  11428  nn0lt2  11440  recnz  11452  gtndiv  11454  3halfnz  11456  1lt10  11681  eluzp1m1  11711  eluzp1p1  11713  eluz2b2  11761  zbtwnre  11786  rebtwnz  11787  1rp  11836  divlt1lt  11899  divle1le  11900  nnledivrp  11940  qbtwnxr  12031  xmulid1  12109  xmulid2  12110  xmulm1  12111  x2times  12129  xrub  12142  0elunit  12290  1elunit  12291  divelunit  12314  lincmb01cmp  12315  iccf1o  12316  xov1plusxeqvd  12318  unitssre  12319  0nelfz1  12360  fzpreddisj  12390  fznatpl1  12395  fztpval  12402  fraclt1  12603  fracle1  12604  flbi2  12618  ico01fl0  12620  fldiv4p1lem1div2  12636  fldiv4lem1div2  12638  fldiv  12659  modid  12695  1mod  12702  m1modnnsub1  12716  modm1p1mod0  12721  seqf1olem1  12840  reexpcl  12877  reexpclz  12880  expge0  12896  expge1  12897  expgt1  12898  bernneq  12990  bernneq2  12991  expnbnd  12993  expnlbnd  12994  expnlbnd2  12995  expmulnbnd  12996  discr1  13000  facwordi  13076  faclbnd3  13079  faclbnd4lem1  13080  faclbnd4lem4  13083  faclbnd6  13086  facavg  13088  hashv01gt1  13133  hashge1  13178  hashnn0n0nn  13180  hash1snb  13207  hashgt12el  13210  hashgt12el2  13211  hashfun  13224  hashge2el2dif  13262  brfi1indALT  13282  brfi1indALTOLD  13288  lsw0  13352  f1oun2prg  13662  sgn1  13832  cjexp  13890  re1  13894  im1  13895  rei  13896  imi  13897  sqrlem1  13983  sqrlem2  13984  sqrlem3  13985  sqrlem4  13986  sqrlem7  13989  resqrex  13991  sqrt1  14012  sqrt2gt1lt2  14015  sqrtm1  14016  abs1  14037  absrdbnd  14081  caubnd2  14097  mulcn2  14326  reccn2  14327  rlimno1  14384  o1fsum  14545  expcnv  14596  geolim  14601  geolim2  14602  georeclim  14603  geomulcvg  14607  geoisumr  14609  geoisum1c  14611  geoihalfsum  14614  fprodreclf  14689  fprodge0  14724  fprodge1  14726  rerisefaccl  14748  refallfaccl  14749  ere  14819  ege2le3  14820  efgt1  14846  resin4p  14868  recos4p  14869  tanhbnd  14891  sinbnd  14910  cosbnd  14911  sinbnd2  14912  cosbnd2  14913  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  cos1bnd  14917  cos2bnd  14918  sinltx  14919  sin01gt0  14920  cos01gt0  14921  sin02gt0  14922  sincos1sgn  14923  ene1  14938  rpnnen2lem2  14944  rpnnen2lem3  14945  rpnnen2lem4  14946  rpnnen2lem9  14951  rpnnen2lem12  14954  ruclem6  14964  ruclem11  14969  ruclem12  14970  3dvds  15052  3dvdsOLD  15053  halfleoddlt  15086  n2dvds1  15104  flodddiv4  15137  sadcadd  15180  isprm3  15396  sqnprm  15414  coprm  15423  phibndlem  15475  pythagtriplem3  15523  pcmpt  15596  fldivp1  15601  pockthi  15611  infpn2  15617  resslem  15933  basendxnmulrndx  15999  slotsbhcdif  16080  oppcbas  16378  rescbas  16489  rescabs  16493  odubas  17133  lt6abl  18296  srgbinomlem4  18543  abvneg  18834  abvtrivd  18840  rmodislmod  18931  isnzr2hash  19264  0ringnnzr  19269  cnfldfun  19758  xrsmcmn  19769  xrsnsgrp  19782  gzrngunitlem  19811  gzrngunit  19812  rge0srg  19817  psgnodpmr  19936  remulg  19953  resubdrg  19954  thlbas  20040  matbas  20219  leordtval2  21016  tuslem  22071  setsmsbas  22280  dscmet  22377  dscopn  22378  nrginvrcnlem  22495  nmoid  22546  idnghm  22547  tgioo  22599  blcvx  22601  metnrmlem1a  22661  metnrmlem1  22662  iicmp  22689  iiconn  22690  iirev  22728  iihalf1  22730  iihalf2  22732  iihalf2cn  22733  elii1  22734  elii2  22735  iimulcl  22736  icopnfcnv  22741  icopnfhmeo  22742  iccpnfcnv  22743  iccpnfhmeo  22744  xrhmeo  22745  xrhmph  22746  evth  22758  xlebnum  22764  lebnumii  22765  htpycc  22779  reparphti  22797  pcoval1  22813  pco1  22815  pcoval2  22816  pcocn  22817  pcohtpylem  22819  pcopt  22822  pcopt2  22823  pcoass  22824  pcorevlem  22826  nmhmcn  22920  ncvs1  22957  ovolunlem1a  23264  vitalilem2  23378  vitalilem4  23380  vitalilem5  23381  vitali  23382  i1f1  23457  itg11  23458  itg2const  23507  itg2monolem1  23517  itg2monolem3  23519  dveflem  23742  dvlipcn  23757  dvcvx  23783  ply1remlem  23922  fta1blem  23928  vieta1lem2  24066  aalioulem3  24089  aalioulem5  24091  aaliou3lem2  24098  ulmbdd  24152  iblulm  24161  radcnvlem1  24167  dvradcnv  24175  abelthlem2  24186  abelthlem3  24187  abelthlem5  24189  abelthlem7  24192  abelth  24195  abelth2  24196  reeff1olem  24200  reeff1o  24201  sinhalfpilem  24215  tangtx  24257  sincos4thpi  24265  pige3  24269  coskpi  24272  recosf1o  24281  tanregt0  24285  efif1olem3  24290  efif1olem4  24291  loge  24333  logdivlti  24366  logcnlem4  24391  logf1o2  24396  dvlog2lem  24398  logtayl  24406  logccv  24409  recxpcl  24421  cxplea  24442  cxpcn3lem  24488  cxpaddlelem  24492  loglesqrt  24499  logblog  24530  ang180lem2  24540  angpined  24557  chordthmlem4  24562  acosrecl  24630  atancj  24637  atanlogaddlem  24640  atantan  24650  atans2  24658  ressatans  24661  leibpi  24669  log2le1  24677  birthdaylem3  24680  cxp2lim  24703  cxploglim  24704  cxploglim2  24705  divsqrtsumlem  24706  cvxcl  24711  scvxcvx  24712  jensenlem2  24714  amgmlem  24716  emcllem2  24723  emcllem4  24725  emcllem6  24727  emcllem7  24728  emre  24732  emgt0  24733  harmonicbnd3  24734  harmonicubnd  24736  harmonicbnd4  24737  zetacvg  24741  lgamgulmlem2  24756  ftalem1  24799  ftalem2  24800  ftalem5  24803  issqf  24862  cht1  24891  chp1  24893  ppiltx  24903  mumullem2  24906  ppiublem1  24927  ppiub  24929  chtublem  24936  chtub  24937  logfacbnd3  24948  logexprlim  24950  perfectlem2  24955  dchrinv  24986  dchr1re  24988  efexple  25006  bposlem1  25009  bposlem2  25010  bposlem5  25013  bposlem8  25016  lgsdir2lem1  25050  lgsdir2lem5  25054  lgsdir  25057  lgsne0  25060  lgsabs1  25061  lgsdinn0  25070  gausslemma2dlem0i  25089  lgseisen  25104  m1lgs  25113  2lgslem3  25129  chebbnd1lem3  25160  chebbnd1  25161  chtppilimlem1  25162  chtppilimlem2  25163  chtppilim  25164  chpchtlim  25168  vmadivsumb  25172  rplogsumlem2  25174  rpvmasumlem  25176  dchrmusumlema  25182  dchrmusum2  25183  dchrvmasumlem2  25187  dchrvmasumiflem1  25190  dchrisum0flblem1  25197  dchrisum0flblem2  25198  dchrisum0fno1  25200  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lema  25203  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  logdivsum  25222  mulog2sumlem2  25224  2vmadivsumlem  25229  log2sumbnd  25233  selbergb  25238  selberg2b  25241  chpdifbndlem1  25242  selberg3lem1  25246  selberg3lem2  25247  selberg4lem1  25249  pntrmax  25253  pntrsumo1  25254  selbergsb  25264  pntrlog2bndlem3  25268  pntrlog2bndlem5  25270  pntpbnd1a  25274  pntpbnd2  25276  pntibndlem1  25278  pntibndlem2  25280  pntibndlem3  25281  pntibnd  25282  pntlemd  25283  pntlemc  25284  pntlemb  25286  pntlemr  25291  pntlemf  25294  pntlemk  25295  pntlemo  25296  pntlem3  25298  pntleml  25300  pnt  25303  abvcxp  25304  ostth2lem1  25307  padicabvf  25320  padicabvcxp  25321  ostth1  25322  ostth2lem2  25323  ostth2lem3  25324  ostth2lem4  25325  ostth2  25326  ostth3  25327  ostth  25328  trgcgrg  25410  ttgcontlem1  25765  brbtwn2  25785  colinearalglem4  25789  ax5seglem1  25808  ax5seglem2  25809  ax5seglem3  25811  ax5seglem5  25813  ax5seglem6  25814  ax5seglem9  25817  ax5seg  25818  axbtwnid  25819  axpaschlem  25820  axpasch  25821  axlowdimlem6  25827  axlowdimlem10  25831  axlowdimlem16  25837  axlowdim1  25839  axlowdim2  25840  axlowdim  25841  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  lfgrnloop  26020  lfuhgr1v0e  26146  usgrexmpldifpr  26150  usgrexmplef  26151  1loopgrvd2  26399  vdegp1bi  26433  lfgrwlkprop  26584  pthdlem1  26662  pthdlem2  26664  upgr4cycl4dv4e  27045  konigsberglem2  27115  konigsberglem3  27116  konigsberglem5  27118  frgrreg  27252  ex-dif  27280  ex-in  27282  ex-pss  27285  ex-res  27298  ex-fl  27304  nv1  27530  smcnlem  27552  ipidsq  27565  nmlno0lem  27648  norm-ii-i  27994  bcs2  28039  norm1  28106  nmopub2tALT  28768  nmfnleub2  28785  nmlnop0iALT  28854  nmopun  28873  unopbd  28874  nmopadjlem  28948  nmopcoadji  28960  pjnmopi  29007  pjbdlni  29008  stge0  29083  stle1  29084  hstle1  29085  hstle  29089  hstles  29090  stge1i  29097  stlesi  29100  staddi  29105  stadd3i  29107  strlem1  29109  strlem3a  29111  strlem5  29114  jplem1  29127  cdj1i  29292  addltmulALT  29305  xlt2addrd  29523  pr01ssre  29570  dp2lt10  29591  dp2ltsuc  29593  dp2ltc  29594  dplti  29613  dpmul4  29622  xdivrec  29635  xrsmulgzz  29678  xrnarchi  29738  resvbas  29832  rearchi  29842  xrge0slmod  29844  submateqlem1  29873  elunitrn  29943  elunitge0  29945  unitssxrge0  29946  unitdivcld  29947  xrge0iifcnv  29979  xrge0iifcv  29980  xrge0iifiso  29981  xrge0iifhom  29983  zrhre  30063  indf  30077  indfval  30078  esumcst  30125  hasheuni  30147  cntnevol  30291  ddemeas  30299  omssubadd  30362  iwrdsplit  30449  prob01  30475  dstfrvclim1  30539  coinfliprv  30544  ballotlem2  30550  ballotlem4  30560  ballotlemi1  30564  ballotlemic  30568  sgnclre  30601  sgnnbi  30607  sgnpbi  30608  sgnmulsgp  30612  plymulx0  30624  plymulx  30625  signswch  30638  signstf  30643  signsvfn  30659  itgexpif  30684  hgt750lemd  30726  logdivsqrle  30728  hgt750lem  30729  hgt750lem2  30730  hgt750leme  30736  tgoldbachgnn  30737  subfacp1lem1  31161  subfacp1lem5  31166  resconn  31228  iisconn  31234  iillysconn  31235  snmlff  31311  problem2  31559  problem2OLD  31560  problem3  31561  sinccvglem  31566  fz0n  31616  dnizeq0  32465  dnibndlem12  32479  knoppcnlem4  32486  knoppndvlem13  32515  cnndvlem1  32528  relowlpssretop  33212  sin2h  33399  cos2h  33400  tan2h  33401  poimirlem7  33416  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  poimirlem23  33432  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  broucube  33443  itg2addnclem3  33463  asindmre  33495  dvasin  33496  dvacos  33497  dvreasin  33498  dvreacos  33499  areacirclem1  33500  fdc  33541  geomcau  33555  cntotbnd  33595  heiborlem8  33617  bfplem2  33622  bfp  33623  rabren3dioph  37379  pellexlem5  37397  pellexlem6  37398  pell1qrgaplem  37437  pell14qrgap  37439  pellqrex  37443  pellfundre  37445  pellfundlb  37448  pellfund14gap  37451  rmspecsqrtnqOLD  37471  jm2.17a  37527  acongeq  37550  jm2.23  37563  jm3.1lem2  37585  relexp01min  38005  imo72b2  38475  cvgdvgrat  38512  lhe4.4ex1a  38528  binomcxplemnotnn0  38555  isosctrlem1ALT  39170  supxrgelem  39553  xrlexaddrp  39568  infxr  39583  infleinflem2  39587  1xr  39686  sumnnodd  39862  limsup10exlem  40004  limsup10ex  40005  liminf10ex  40006  dvnprodlem3  40163  stoweidlem1  40218  stoweidlem18  40235  stoweidlem19  40236  stoweidlem26  40243  stoweidlem34  40251  stoweidlem40  40257  stoweidlem41  40258  stoweidlem59  40276  stoweid  40280  stirlinglem10  40300  stirlinglem11  40301  dirkercncflem1  40320  fourierdlem16  40340  fourierdlem21  40345  fourierdlem22  40346  fourierdlem42  40366  fourierdlem68  40391  fourierdlem83  40406  fourierdlem103  40426  sqwvfourb  40446  fouriersw  40448  etransclem23  40474  salexct2  40557  salgencntex  40561  ovn0lem  40779  smfmullem3  41000  smfmullem4  41001  zm1nn  41316  m1mod0mod1  41339  fmtnosqrt  41451  perfectALTVlem2  41631  nnsum3primesprm  41678  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  tgblthelfgott  41703  tgoldbach  41705  tgblthelfgottOLD  41709  tgoldbachOLD  41712  expnegico01  42308  regt1loggt0  42330  rege1logbrege0  42352  rege1logbzge0  42353  blennnelnn  42370  dignnld  42397  nn0sumshdiglemA  42413  nn0sumshdiglem1  42415